refactor: tighten proof style from Mathlib PR review feedback

CLAUDE.md

@@ -55,6 +55,14 @@ copyright headers on all `.lean` files.
 - **Terminal `simp`**: do NOT squeeze (maintenance burden from lemma renames)
 - **Non-terminal `simp`**: MUST be `simp only [...]`
 - **One tactic per line** (semicolons only for short single-idea sequences)
+- **Set equality**: `ext v; simp [...]` is canonical — don't build manual
+  `constructor`/`rcases`/`absurd` chains when `simp` with the right lemma set closes it
+- **Skip `ext`** when `simp` alone closes a set equality (e.g., `ball_zero`)
+- **`simp` before `tauto`**: `simp` + commutativity lemmas (`adj_comm`, `or_comm`)
+  often closes goals that look like they need `tauto`
+- **`.rfl`** not `Iff.rfl` — dot notation for constructor terms
+- **Named lemmas over `show ... from rfl`**: e.g., `one_add_one_eq_two.symm`
+  not `show (2 : ℕ∞) = 1 + 1 from rfl`
 
 ### Attributes
 
@@ -72,6 +80,9 @@ copyright headers on all `.lean` files.
 - **Hypotheses left of colon** — `(h : 1 < n) : 0 < n` not `: 1 < n → 0 < n`
 - **`abbrev`** (reducible) requires justification; `@[irreducible]` requires justification
 - **Classical by default** — don't thread `Decidable` instances unless the type requires them
+- **Definition argument order**: choose to minimize downstream `symm`/`comm` calls —
+  e.g., `{v | G.edist v c < r}` not `{v | G.edist c v < r}` when most API lemmas
+  state the varying argument first
 
 ### Documentation
 
@@ -182,3 +193,10 @@ copyright headers on all `.lean` files.
 - **Commit messages**: substantive, not ceremonial
 - Feature branches merge to main via fast-forward; delete after merge
 - **Mathlib PR process**: post to Zulip first, small PRs preferred, AI disclosure required
+- **PR description format**: one-line summary → blank line → AI disclosure (1-2 sentences)
+  → Zulip link → `---` → template buttons. No design-decision sections, no tables.
+- **Review responses**: one sentence per comment, inline on the diff where possible.
+  No tables, headers, diff summaries, or structured documents. Let the code speak.
+- **AI disclosure**: in PR body only, not in commit `Co-Authored-By` tags
+- **Reviewer disagreements**: defer to the later or more authoritative reviewer
+- **File-author naming preferences**: defer (e.g., `ball_mono` over `ball_subset_ball`)

FdFormal/FlowerConstruction.lean

@@ -118,7 +118,7 @@ theorem flowerEdge_card (u v g : ℕ) :
   induction g with
   | zero => simp [FlowerEdge]
   | succ g ih =>
-    simp only [FlowerEdge, Fintype.card_prod, Fintype.card_sum, Fintype.card_fin, ih, pow_succ,
+    simp [FlowerEdge, Fintype.card_prod, Fintype.card_sum, Fintype.card_fin, ih, pow_succ,
       mul_comm]
 
 /-- Vertex type for the (u,v)-flower at generation `g`.
@@ -158,8 +158,7 @@ theorem FlowerVert.embed_injective {u v g : ℕ} :
   | inl a =>
     cases y with
     | inl _ =>
-      have := Sum.inl_injective hxy
-      exact congrArg Sum.inl this
+      exact congrArg Sum.inl (Sum.inl_injective hxy)
     | inr _ => simp [embed] at hxy
   | inr a =>
     cases y with
@@ -412,10 +411,7 @@ noncomputable def flowerGraph' (u v g : ℕ) :
 /-- The adjacency relation of `flowerGraph'` is `flowerAdj'`. -/
 theorem flowerGraph'_adj_iff (u v g : ℕ)
     (a b : FlowerVert u v g) :
-    (flowerGraph' u v g).Adj a b ↔ flowerAdj' u v g a b := by
-  constructor
-  · exact id
-  · exact id
+    (flowerGraph' u v g).Adj a b ↔ flowerAdj' u v g a b := .rfl
 
 /-! ## Layer 4: Walk construction and distance -/
 
@@ -757,13 +753,13 @@ theorem rank_edge_bounds (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v)
       | (have h := htgt_eq ‹_›; rw [h, mul_add, mul_one]
          constructor
          · exact Nat.add_le_add_left (Nat.div_le_of_le_mul (by
-             nlinarith [Nat.mul_le_mul_left u (show n + 1 ≤ v from by omega),
+             nlinarith [Nat.mul_le_mul_left u (show n + 1 ≤ v by omega),
                mul_comm (n + 1) u])) _
          · suffices u - 1 ≤ (n + 1) * u / v by omega
            calc u - 1 = (u - 1) * v / v :=
-                 (Nat.mul_div_cancel (u - 1) (show 0 < v from by omega)).symm
+                 (Nat.mul_div_cancel (u - 1) (show 0 < v by omega)).symm
              _ ≤ (n + 1) * u / v := Nat.div_le_div_right (by
-                 zify [show 1 ≤ u from by omega, show 1 ≤ v from by omega] at *
+                 zify [show 1 ≤ u by omega, show 1 ≤ v by omega] at *
                  nlinarith))
 
 /-- Rank is non-decreasing along edges: rank(edgeSrc) ≤ rank(edgeTgt). -/
@@ -941,8 +937,7 @@ theorem FlowerVert.project_embed (u v g : ℕ) (x : FlowerVert u v g) :
   | inl _ => rfl
   | inr val =>
     obtain ⟨k, e, pos⟩ := val
-    simp only [FlowerVert.embed, FlowerVert.project, Fin.val_castSucc, dif_pos k.isLt,
-      Fin.eta]
+    simp [FlowerVert.embed, FlowerVert.project, Fin.val_castSucc, Fin.eta]
 
 /-- Hub 0 projects to hub 0. -/
 theorem FlowerVert.project_hub0 (u v g : ℕ) :

FdFormal/FlowerCounts.lean

@@ -103,7 +103,7 @@ theorem flowerVertCount_eq (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :
     (u + v - 2) * (u + v) ^ g + (u + v) := by
   induction g with
   | zero =>
-    simp
+    simp only [flowerVertCount, pow_zero, mul_one]
     omega
   | succ g ih =>
     simp only [flowerVertCount_succ, flowerEdgeCount_eq_pow, pow_succ]
@@ -128,7 +128,7 @@ theorem flowerVertCount_lower (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :
     (u + v - 2) * (u + v) ^ g ≤
     (u + v - 1) * flowerVertCount u v g := by
   rw [flowerVertCount_eq u v g hu huv]
-  exact le_add_of_nonneg_right (Nat.zero_le _)
+  omega
 
 /-- Upper bound: `(w - 1) * N_g ≤ 2 * (w - 1) * w^g`. -/
 theorem flowerVertCount_upper (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :

FdFormal/FlowerDimension.lean

@@ -74,10 +74,8 @@ theorem flowerVertCount_ge_real (u v g : ℕ) (hu : 1 < u)
     (huv : u ≤ v) :
     (↑(u + v) - 2) / (↑(u + v) - 1) * (↑(u + v) : ℝ) ^ g ≤
     ↑(flowerVertCount u v g) := by
-  have hw1 : (0 : ℝ) < ↑(u + v) - 1 := by
-    have : (1 : ℝ) < ↑(u + v) := by
-      exact_mod_cast (show 1 < u + v from by omega)
-    linarith
+  have hw1 : (0 : ℝ) < ↑(u + v) - 1 :=
+    sub_pos.mpr (by exact_mod_cast (show 1 < u + v by omega))
   rw [div_mul_eq_mul_div, div_le_iff₀ hw1]
   have h := flowerVertCount_lower_real u v g hu huv
   linarith [mul_comm (↑(u + v) - 1 : ℝ) (↑(flowerVertCount u v g) : ℝ)]
@@ -86,13 +84,11 @@ theorem flowerVertCount_ge_real (u v g : ℕ) (hu : 1 < u)
 theorem flowerVertCount_le_real (u v g : ℕ) (hu : 1 < u)
     (huv : u ≤ v) :
     (↑(flowerVertCount u v g) : ℝ) ≤ 2 * (↑(u + v) : ℝ) ^ g := by
-  have hw1 : (0 : ℝ) < ↑(u + v) - 1 := by
-    have : (1 : ℝ) < ↑(u + v) := by
-      exact_mod_cast (show 1 < u + v from by omega)
-    linarith
+  have hw1 : (0 : ℝ) < ↑(u + v) - 1 :=
+    sub_pos.mpr (by exact_mod_cast (show 1 < u + v by omega))
   have h := flowerVertCount_upper_real u v g hu huv
   rw [show (2 : ℝ) * (↑(u + v) - 1) * (↑(u + v) : ℝ) ^ g =
-      (↑(u + v) - 1) * (2 * (↑(u + v) : ℝ) ^ g) from by ring] at h
+      (↑(u + v) - 1) * (2 * (↑(u + v) : ℝ) ^ g) by ring] at h
   exact (mul_le_mul_iff_right₀ hw1).mp h
 
 /-! ### The headline theorem -/
@@ -113,7 +109,7 @@ theorem flowerDimension (u v : ℕ) (hu : 1 < u) (huv : u ≤ v) :
   have hlogu : 0 < log (↑u : ℝ) :=
     log_pos (by exact_mod_cast hu)
   have hlogw : 0 < log (↑(u + v) : ℝ) :=
-    log_pos (by exact_mod_cast (show 1 < u + v from by omega))
+    log_pos (by exact_mod_cast (show 1 < u + v by omega))
   have hw_pos : (0 : ℝ) < ↑(u + v) :=
     Nat.cast_pos.mpr (by omega)
   have hN_pos : ∀ g, (0 : ℝ) < ↑(flowerVertCount u v g) :=
@@ -122,8 +118,8 @@ theorem flowerDimension (u v : ℕ) (hu : 1 < u) (huv : u ≤ v) :
   have h_log_hub : ∀ g : ℕ,
       log (↑(flowerHubDist u v g) : ℝ) = ↑g * log (↑u : ℝ) := by
     intro g
-    rw [show (↑(flowerHubDist u v g) : ℝ) = (↑u : ℝ) ^ g from by
-      simp [flowerHubDist_eq_pow, Nat.cast_pow]]
+    rw [show (↑(flowerHubDist u v g) : ℝ) = (↑u : ℝ) ^ g by
+      simp only [flowerHubDist_eq_pow, Nat.cast_pow]]
     exact log_pow (↑u) g
   -- Step 2: Suffices with g * log(u) in denominator
   suffices h : Tendsto
@@ -148,14 +144,9 @@ theorem flowerDimension (u v : ℕ) (hu : 1 < u) (huv : u ≤ v) :
   -- The residual is bounded between log(c₁)/(g*log u) and log(2)/(g*log u)
   -- where c₁ = (w-2)/(w-1) > 0
   set c₁ := (↑(u + v) - 2 : ℝ) / (↑(u + v) - 1) with hc₁_def
-  have hc₁_pos : 0 < c₁ := by
-    apply div_pos
-    · have : (2 : ℝ) < ↑(u + v) := by
-        exact_mod_cast (show 2 < u + v from by omega)
-      linarith
-    · have : (1 : ℝ) < ↑(u + v) := by
-        exact_mod_cast (show 1 < u + v from by omega)
-      linarith
+  have hc₁_pos : 0 < c₁ :=
+    div_pos (sub_pos.mpr (by exact_mod_cast (show 2 < u + v by omega)))
+      (sub_pos.mpr (by exact_mod_cast (show 1 < u + v by omega)))
   -- g * log(u) → ∞
   have h_denom : Tendsto (fun g : ℕ ↦ (↑g : ℝ) * log (↑u : ℝ))
       atTop atTop :=

FdFormal/FlowerLog.lean

@@ -66,13 +66,10 @@ theorem log_flowerVertCount_residual_lower :
     log ((↑(u + v) - 2 : ℝ) / (↑(u + v) - 1)) ≤
     log ↑(flowerVertCount u v g) - ↑g * log (↑(u + v) : ℝ) := by
   have hw_pos : (0 : ℝ) < ↑(u + v) := Nat.cast_pos.mpr (by omega)
-  have hw1 : (0 : ℝ) < ↑(u + v) - 1 := by
-    have : (1 : ℝ) < ↑(u + v) := by exact_mod_cast (show 1 < u + v by omega)
-    linarith
-  have hc : (0 : ℝ) < (↑(u + v) - 2) / (↑(u + v) - 1) := by
-    apply div_pos _ hw1
-    have : (2 : ℝ) < ↑(u + v) := by exact_mod_cast (show 2 < u + v by omega)
-    linarith
+  have hw1 : (0 : ℝ) < ↑(u + v) - 1 :=
+    sub_pos.mpr (by exact_mod_cast (show 1 < u + v by omega))
+  have hc : (0 : ℝ) < (↑(u + v) - 2) / (↑(u + v) - 1) :=
+    div_pos (sub_pos.mpr (by exact_mod_cast (show 2 < u + v by omega))) hw1
   -- From ℕ bound: (w-2)·w^g ≤ (w-1)·N_g → (w-2)/(w-1)·w^g ≤ N_g
   have h_ge : (↑(u + v) - 2) / (↑(u + v) - 1) * (↑(u + v) : ℝ) ^ g ≤
       ↑(flowerVertCount u v g) := by

FdFormal/GraphBall.lean

@@ -60,8 +60,7 @@ variable {G}
 
 @[simp]
 theorem mem_ball {c v : V} {r : ℕ∞} :
-    v ∈ G.ball c r ↔ G.edist c v < r :=
-  Iff.rfl
+    v ∈ G.ball c r ↔ G.edist c v < r := .rfl
 
 @[simp]
 theorem ball_zero {c : V} : G.ball c 0 = ∅ := by
@@ -70,29 +69,13 @@ theorem ball_zero {c : V} : G.ball c 0 = ∅ := by
 @[simp]
 theorem ball_one {c : V} : G.ball c 1 = {c} := by
   ext v
-  simp only [mem_ball, Set.mem_singleton_iff]
-  constructor
-  · intro h
-    have h0 : G.edist c v = 0 := by
-      have hne : G.edist c v ≠ ⊤ := ne_top_of_lt h
-      lift G.edist c v to ℕ using hne with d
-      have : d < 1 := by exact_mod_cast h
-      exact_mod_cast (show d = 0 from by omega)
-    exact (edist_eq_zero_iff.mp h0).symm
-  · rintro rfl; simp
+  simp [ball, ENat.lt_one_iff_eq_zero]
 
 @[simp]
 theorem ball_top {c : V} :
     G.ball c ⊤ = (G.connectedComponentMk c).supp := by
   ext v
-  simp only [mem_ball, ConnectedComponent.mem_supp_iff]
-  constructor
-  · intro h
-    exact (ConnectedComponent.eq.mpr
-      (reachable_of_edist_ne_top (ne_top_of_lt h))).symm
-  · intro h
-    exact lt_top_iff_ne_top.mpr
-      (edist_ne_top_iff_reachable.mpr (ConnectedComponent.eq.mp h.symm))
+  simp [lt_top_iff_ne_top, edist_ne_top_iff_reachable, reachable_comm]
 
 /-- Balls are monotone in the radius. -/
 theorem ball_mono {c : V} {r₁ r₂ : ℕ∞} (h : r₁ ≤ r₂) :
@@ -128,7 +111,7 @@ theorem ball_anti {G' : SimpleGraph V} {c : V} {r : ℕ∞} (h : G ≤ G') :
 theorem mem_ball_of_adj {c v : V} (h : G.Adj c v) :
     v ∈ G.ball c 2 := by
   simp only [mem_ball]
-  have h1 : (1 : ℕ∞) < 2 := by exact_mod_cast (show (1 : ℕ) < 2 from by omega)
+  have h1 : (1 : ℕ∞) < 2 := by exact_mod_cast (by omega : (1 : ℕ) < 2)
   exact lt_of_le_of_lt (edist_le_one_iff_adj_or_eq.mpr (Or.inl h)) h1
 
 theorem adj_of_mem_ball_two {c v : V} (h : v ∈ G.ball c 2) (hne : c ≠ v) :
@@ -138,7 +121,7 @@ theorem adj_of_mem_ball_two {c v : V} (h : v ∈ G.ball c 2) (hne : c ≠ v) :
     have hne_top : G.edist c v ≠ ⊤ := ne_top_of_lt h
     lift G.edist c v to ℕ using hne_top with d
     have : d < 2 := by exact_mod_cast h
-    exact_mod_cast (show d ≤ 1 from by omega)
+    exact_mod_cast (by omega : d ≤ 1)
   exact (edist_le_one_iff_adj_or_eq.mp hle).resolve_right hne
 
 /-- If `v ∈ ball c r₁` and `w ∈ ball v r₂`, then `w ∈ ball c (r₁ + r₂)`. -/

FdFormal/PathGraphDist.lean

@@ -74,16 +74,15 @@ private theorem pathGraph_walk_le {n : ℕ} {i j : Fin (n + 1)} (hij : i.val ≤
     ∃ w : (pathGraph (n + 1)).Walk i j, w.length = j.val - i.val := by
   induction j using Fin.inductionOn with
   | zero =>
-    have hi : i = 0 := by ext; exact Nat.le_zero.mp hij
+    have hi : i = 0 := by ext; omega
     exact hi ▸ ⟨.nil, by simp⟩
   | succ j ih =>
     by_cases h : i.val ≤ j.val
     · obtain ⟨w, hw⟩ := ih h
       have hadj : (pathGraph (n + 1)).Adj j.castSucc j.succ := by
         rw [pathGraph_adj]; left; simp [Fin.val_succ, Fin.val_castSucc]
       exact ⟨w.append (.cons hadj .nil), by simp [hw]; omega⟩
-    · have hval : j.succ.val = j.val + 1 := Fin.val_succ j
-      have hi : i = j.succ := Fin.ext (by omega)
+    · have hi : i = j.succ := Fin.ext (by omega)
       subst hi; exact ⟨.nil, by simp⟩
 
 /-- Any walk in `pathGraph` has length ≥ the index difference between endpoints.
@@ -127,7 +126,7 @@ theorem pathGraph_edist {n : ℕ} (i j : Fin (n + 1)) :
 theorem pathGraph_dist {n : ℕ} (i j : Fin (n + 1)) :
     (pathGraph (n + 1)).dist i j =
       if i.val ≤ j.val then j.val - i.val else i.val - j.val := by
-  simp only [SimpleGraph.dist, pathGraph_edist, ENat.toNat_coe]
+  simp [SimpleGraph.dist, pathGraph_edist, ENat.toNat_coe]
 
 /-- Distance from `0` to `Fin.last n` in `pathGraph (n + 1)` is `n`. -/
 theorem pathGraph_dist_zero_last (n : ℕ) :