chore(*): fix a few docstring syntax errors

This PR goes through the first few errors in the docstring Verso linter that haven't been silenced by leanprover-community#37588 and fixes the issues that got flagged. It is not a systematic cleanup, just things spotted while I was debugging the linter.

Author: Vierkantor

Mathlib/Data/List/Indexes.lean

@@ -8,7 +8,7 @@ module
 public import Mathlib.Data.List.Defs
 
 /-!
-# Lemmas about List.*Idx functions.
+# Lemmas about `List.*Idx` functions.
 
 Some specification lemmas for `List.mapIdx`, `List.mapIdxM`, `List.foldlIdx` and `List.foldrIdx`.
 

Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/SimplexAlgorithm.lean

@@ -107,7 +107,7 @@ def chooseExitingVar (enterIdx : Nat) : SimplexAlgorithmM matType Nat := do
 
 /--
 Chooses entering and exiting variables using
-(Bland's rule)[(https://en.wikipedia.org/wiki/Bland%27s_rule)] that guarantees that the Simplex
+[Bland's rule](https://en.wikipedia.org/wiki/Bland%27s_rule) that guarantees that the Simplex
 Algorithm terminates.
 -/
 def choosePivots : SimplexAlgorithmM matType (Nat × Nat) := do

Mathlib/Tactic/Relation/Rfl.lean

@@ -12,7 +12,7 @@ public meta import Lean.Meta.Tactic.Rfl
 # `Lean.MVarId.liftReflToEq`
 
 Convert a goal of the form `x ~ y` into the form `x = y`, where `~` is a reflexive
-relation, that is, a relation which has a reflexive lemma tagged with the attribute `[refl]`.
+relation, that is, a relation which has a reflexive lemma tagged with the attribute `@[refl]`.
 If this can't be done, returns the original `MVarId`.
 -/
 
@@ -24,7 +24,7 @@ open Lean Meta Elab Tactic Rfl
 
 /--
 This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
-relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
+relation, that is, a relation which has a reflexive lemma tagged with the attribute `@[refl]`.
 -/
 def rflTac : TacticM Unit :=
   withMainContext do liftMetaFinishingTactic (·.applyRfl)

Mathlib/Tactic/Translate/Core.lean

@@ -146,7 +146,7 @@ register_option linter.translateReorder : Bool := {
   descr := "Linter used by translate attributes that checks if the given reorder is \
     equal to the automatically generated one" }
 
-/-- Linter used by translate attributes that checks if the relevant_arg is
+/-- Linter used by translate attributes that checks if the `relevant_arg` is
 automatically generated. -/
 register_option linter.translateRelevantArg : Bool := {
   defValue := true

Mathlib/Tactic/Widget/Conv.lean

@@ -166,7 +166,7 @@ public def Path.ofSubExprPos (expr : Expr) (pos : SubExpr.Pos) : MetaM Path :=
 
 open Lean.Parser.Tactic.Conv in
 /--
-Given a `path : Path` and `xs : TSepArray ``enterArg ","`, generate the `conv` syntax
+Given a `path : Path` and ```xs : TSepArray ``enterArg ","```, generate the `conv` syntax
 corresponding to `enter [xs,*]` followed by traversing `path`. If `loc` is `some fvar`,
 start with `conv at fvar =>`, otherwise if `loc` is `none` start with `conv =>`.
 -/

Mathlib/Util/Tactic.lean

@@ -11,7 +11,7 @@ public meta import Lean.MetavarContext
 /-!
 # Miscellaneous helper functions for tactics.
 
-[TODO] Ideally we would find good homes for everything in this file, eventually removing it.
+TODO: Ideally we would find good homes for everything in this file, eventually removing it.
 -/
 
 public meta section