chore: sections and misc. cleanup

Mathlib/Tactic/TFAE.lean

@@ -27,7 +27,7 @@ syntax (" → " <|> " ↔ " <|> " ← ") : impArrow
 
 /--
 `tfae_have` introduces hypotheses for proving goals of the form `TFAE [P₁, P₂, ...]`. Specifically,
-`tfae_have : i arrow j` introduces a hypothesis of the form `Pᵢ arrow Pⱼ` to the local context,
+`tfae_have : i arrow j` introduces a hypothesis of type `Pᵢ arrow Pⱼ` to the local context,
 where `arrow` can be `→`, `←`, or `↔`. Note that `i` and `j` are natural number indices (beginning
 at 1) used to specify the propositions `P₁, P₂, ...` that appear in the `TFAE` goal list. A proof
 is required afterward, typically via a tactic block.
@@ -81,6 +81,8 @@ example : TFAE [P, Q, R] := by
 -/
 syntax (name := tfaeFinish) "tfae_finish" : tactic
 
+/-! # Setup -/
+
 /-- Extract a list of `Prop` expressions from an expression of the form `TFAE [P₁, P₂, ...]` as
 long as `[P₁, P₂, ...]` is an explicit list. -/
 partial def getTFAEList (t : Expr) : MetaM (List Q(Prop)) := do
@@ -117,6 +119,8 @@ partial def getTFAEListQ (t : Expr) : MetaM Q(List Prop) := do
 /-- Check that an expression representing a list is explicit. -/
 add_decl_doc getTFAEListQ.guardExplicitList
 
+/-! # Proof construction -/
+
 /-- Prove an implication via solve_by_elim. -/
 def proveImpl (P P' : Q(Prop)) : TacticM Q($P → $P') := do
   let t ← mkFreshExprMVar q($P → $P')
@@ -139,22 +143,24 @@ partial def proveChain (P : Q(Prop)) (l : Q(List Prop)) :
     return q(Chain.cons $p $cl')
 
 /-- Attempt to prove `ilast' P' l → P` given an explicit list `l`. -/
-partial def proveILast'Imp (P P' : Q(Prop)) (l : Q(List Prop)) :
+partial def proveILast'Impl (P P' : Q(Prop)) (l : Q(List Prop)) :
     TacticM Q(ilast' $P' $l → $P) := do
   match l with
   | ~q([]) => proveImpl P' P
-  | ~q($P'' :: $l') => proveILast'Imp P P'' l'
+  | ~q($P'' :: $l') => proveILast'Impl P P'' l'
 
-/-- Attempt to prove a statement of the form `TFAE l`, with `l` an explicit list. -/
+/-- Attempt to prove a statement of the form `TFAE [P₁, P₂, ...]`. -/
 def proveTFAE (l : Q(List Prop)) : TacticM Q(TFAE $l) := do
   match l with
   | ~q([]) => return q(tfae_nil)
   | ~q([$P]) => return q(tfae_singleton $P)
   | ~q($P :: $P' :: $l) =>
     let c ← proveChain P q($P' :: $l)
-    let il ← proveILast'Imp P P' l
+    let il ← proveILast'Impl P P' l
     return q(tfae_of_cycle $c $il)
 
+/-! # `tfae_have` components -/
+
 /-- Construct a name for a hypothesis introduced by `tfae_have`. -/
 def mkTFAEHypName (i j : TSyntax `num) (arr : TSyntax `impArrow) : TermElabM Name := do
   let arr ← match arr with
@@ -197,6 +203,8 @@ def mkImplType (Pi : Q(Prop)) (arr : TSyntax `impArrow) (Pj : Q(Prop)) : TacticM
   | `(impArrow| ↔ ) => pure q($Pi ↔ $Pj)
   | _ => throwErrorAt arr "expected '←', '→', or '↔'"
 
+/-! # Tactic implementation -/
+
 elab_rules : tactic
 | `(tactic| tfae_have $[$h:ident : ]? $i:num $arr:impArrow $j:num) => do
   let goal ← getMainGoal