refactor: proof golf from Aristotle — eliminate intermediate bindings

FdFormal/FlowerConstruction.lean

@@ -140,8 +140,8 @@ def FlowerVert.hub0 (u v g : ℕ) : FlowerVert u v g := .inl 0
 def FlowerVert.hub1 (u v g : ℕ) : FlowerVert u v g := .inl 1
 
 theorem FlowerVert.hub0_ne_hub1 (u v g : ℕ) :
-    FlowerVert.hub0 u v g ≠ FlowerVert.hub1 u v g := by
-  unfold hub0 hub1; exact Sum.inl_injective.ne (by decide)
+    FlowerVert.hub0 u v g ≠ FlowerVert.hub1 u v g :=
+  Sum.inl_injective.ne (by decide)
 
 /-- Embed a vertex from generation `g` into generation `g+1`.
 Hubs stay hubs. Internal vertices keep their identity (the generation
@@ -179,11 +179,8 @@ theorem FlowerVert.embed_ne_new {u v g : ℕ} (x : FlowerVert u v g)
   cases x with
   | inl _ => simp [embed]
   | inr val =>
-    intro h
-    have h := Sum.inr_injective h
-    have hk := congr_arg (fun s => (Sigma.fst s).val) h
-    simp only [Fin.val_castSucc] at hk
-    omega
+    intro h; have hk := congr_arg (fun s => (Sigma.fst s).val) (Sum.inr_injective h)
+    simp only [Fin.val_castSucc] at hk; omega
 
 /-- Within a single gadget, source and target positions are always distinct
 when `1 < u`. -/
@@ -250,16 +247,10 @@ theorem edgeSrc_ne_edgeTgt (u v g : ℕ) (e : FlowerEdge u v g) :
     have hpar := ih parent
     have hloc := localSrc_ne_localTgt u v localE
     simp only [edgeEndpoints, edgeSrc, edgeTgt] at hpar ⊢
-    -- Case-split on localSrc/localTgt values
     rcases hs : localSrc u v localE with src | tgt | ⟨i⟩ | ⟨j⟩ <;>
       rcases ht : localTgt u v localE with src | tgt | ⟨i'⟩ | ⟨j'⟩ <;>
-      simp only [hs, ht] at hloc ⊢
-    -- 16 cases from (localSrc × localTgt). Four closure patterns:
-    -- 1. absurd rfl hloc: same position (src=src, tgt=tgt) contradicts hloc
-    -- 2. embed_injective.ne: both endpoints are embedded, use inductive hypothesis
-    -- 3. embed_ne_new: one endpoint is embedded, the other is a new vertex
-    -- 4. Sum.inr_injective + simp_all: both are new vertices, extract index equality
-    all_goals first
+      simp only [hs, ht] at hloc ⊢ <;>
+    first
       | exact absurd rfl hloc
       | exact FlowerVert.embed_injective.ne hpar
       | exact Ne.symm (FlowerVert.embed_injective.ne hpar)
@@ -399,12 +390,10 @@ theorem gadget_adj_chain (u v g : ℕ) (hu : 1 < u)
 /-- The (u,v)-flower as a `SimpleGraph` on `FlowerVert`.
 Construction requires `edgeSrc_ne_edgeTgt` for irreflexivity. -/
 noncomputable def flowerGraph' (u v g : ℕ) :
-    SimpleGraph (FlowerVert u v g) := by
-  refine SimpleGraph.mk (flowerAdj' u v g) ?_ ?_
-  · -- symmetry
-    intro a b ⟨e, h⟩; exact ⟨e, h.symm⟩
-  · -- irreflexivity
-    exact ⟨fun a ⟨e, h⟩ => by
+    SimpleGraph (FlowerVert u v g) :=
+  SimpleGraph.mk (flowerAdj' u v g)
+    (fun _ _ ⟨e, h⟩ => ⟨e, h.symm⟩)
+    ⟨fun a ⟨e, h⟩ => by
       rcases h with ⟨h1, h2⟩ | ⟨h1, h2⟩ <;>
         exact edgeSrc_ne_edgeTgt u v g e (h1 ▸ h2)⟩
 
@@ -434,9 +423,7 @@ theorem gadget_short_walk (u v g : ℕ) (hu : 1 < u)
   | zero => exact ⟨.nil, rfl⟩
   | succ k ih =>
     obtain ⟨w, hw⟩ := ih (by omega)
-    exact ⟨w.append (.cons (hadj ⟨k, by omega⟩) .nil), by
-      simp only [SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_cons,
-        SimpleGraph.Walk.length_nil, hw]⟩
+    exact ⟨w.append (.cons (hadj ⟨k, by omega⟩) .nil), by simp [hw]⟩
 
 /-- Adjacent vertices in gen `g` are connected by a walk of length `u`
 in gen `g+1` (through the replacement gadget's short path). -/
@@ -467,8 +454,7 @@ theorem lift_walk (u v g : ℕ) (hu : 1 < u) {a b : FlowerVert u v g}
     obtain ⟨w_tail, hw_tail⟩ := ih
     exact ⟨w_step.append w_tail, by
       rw [SimpleGraph.Walk.length_append, hw_step, hw_tail,
-        SimpleGraph.Walk.length_cons, Nat.mul_succ]
-      omega⟩
+        SimpleGraph.Walk.length_cons, Nat.mul_succ]; omega⟩
 
 /-- **Upper bound**: there exists a walk of length `u^g` between hubs.
 
@@ -480,8 +466,7 @@ theorem flowerGraph'_walk_hubs (u v g : ℕ) (hu : 1 < u) :
       w.length = u ^ g := by
   induction g with
   | zero =>
-    exact ⟨.cons (⟨(), Or.inl ⟨rfl, rfl⟩⟩ : (flowerGraph' u v 0).Adj _ _) .nil,
-      by simp [SimpleGraph.Walk.length]⟩
+    exact ⟨.cons (⟨(), Or.inl ⟨rfl, rfl⟩⟩ : (flowerGraph' u v 0).Adj _ _) .nil, by simp⟩
   | succ g ih =>
     obtain ⟨w, hw⟩ := ih
     obtain ⟨w', hw'⟩ := lift_walk u v g hu w
@@ -640,8 +625,7 @@ def FlowerVert.rank (u v : ℕ) : (g : ℕ) → FlowerVert u v g → ℕ
     if hk : k.val < g then
       u * rank u v g (.inr ⟨⟨k.val, hk⟩, parent, pos⟩)
     else
-      have hkg : k.val = g := by omega
-      let parent' : FlowerEdge u v g := hkg ▸ parent
+      let parent' : FlowerEdge u v g := (show k.val = g by omega) ▸ parent
       let srcR := rank u v g (edgeSrc u v g parent')
       let tgtR := rank u v g (edgeTgt u v g parent')
       if srcR = tgtR then u * srcR
@@ -794,22 +778,18 @@ theorem walk_length_ge_rank (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v)
   | nil => omega
   | cons hab tail ih =>
     have hadj := rank_adj_le u v g hu huv _ _ hab
-    simp only [SimpleGraph.Walk.length_cons]
-    omega
+    simp only [SimpleGraph.Walk.length_cons]; omega
 
 /-- **Lower bound**: hub distance ≥ u^g.
 
 Uses the rank function as a 1-Lipschitz potential: any walk from hub0
 (rank 0) to hub1 (rank u^g) has length ≥ u^g. -/
 theorem flowerGraph'_dist_ge (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :
     u ^ g ≤ (flowerGraph' u v g).dist (.hub0 u v g) (.hub1 u v g) := by
-  obtain ⟨w, hw⟩ := flowerGraph'_walk_hubs u v g hu
-  have hreach : (flowerGraph' u v g).Reachable (.hub0 u v g) (.hub1 u v g) :=
-    ⟨w⟩
-  obtain ⟨p, hp⟩ := hreach.exists_walk_length_eq_dist
+  obtain ⟨p, hp⟩ :=
+    (flowerGraph'_walk_hubs u v g hu).choose.reachable.exists_walk_length_eq_dist
   have := walk_length_ge_rank u v g hu huv p
-  rw [rank_hub0, rank_hub1] at this
-  omega
+  rw [rank_hub0, rank_hub1] at this; omega
 
 /-- **F2 bridge on FlowerVert**: hub distance = u^g. -/
 theorem flowerGraph'_dist_hubs (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :
@@ -848,7 +828,7 @@ theorem flowerVert_card (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :
 /-- Equivalence to `Fin (flowerVertCount u v g)`. -/
 noncomputable def flowerVertEquiv (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :
     FlowerVert u v g ≃ Fin (flowerVertCount u v g) :=
-  (Fintype.equivFinOfCardEq (flowerVert_card u v g hu huv))
+  Fintype.equivFinOfCardEq (flowerVert_card u v g hu huv)
 
 /-- The (u,v)-flower on `Fin`. -/
 noncomputable def flowerGraph (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :
@@ -876,23 +856,17 @@ theorem flowerGraph_dist_hubs (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :
     change G.Adj (e.symm (e a)) (e.symm (e b))
     simp only [Equiv.symm_apply_apply]; exact h
   apply le_antisymm
-  · -- ≤: walk in G maps to walk in G'
-    obtain ⟨w, hw⟩ := (flowerGraph'_connected u v g hu huv).exists_walk_length_eq_dist
+  · obtain ⟨w, hw⟩ := (flowerGraph'_connected u v g hu huv).exists_walk_length_eq_dist
       (.hub0 u v g) (.hub1 u v g)
     calc G'.dist (e (.hub0 u v g)) (e (.hub1 u v g))
         ≤ (w.map ⟨e, @hom_fwd⟩).length := SimpleGraph.dist_le _
-      _ = w.length := SimpleGraph.Walk.length_map _ _
-      _ = _ := hw
-  · -- ≥: walk in G' maps to walk in G (e.symm preserves adjacency)
-    have hreach : G'.Reachable (e (.hub0 u v g)) (e (.hub1 u v g)) := by
-      obtain ⟨w, _⟩ := flowerGraph'_walk_hubs u v g hu
-      exact (w.map ⟨e, @hom_fwd⟩).reachable
+      _ = _ := by rw [SimpleGraph.Walk.length_map, hw]
+  · have hreach : G'.Reachable (e (.hub0 u v g)) (e (.hub1 u v g)) :=
+      ((flowerGraph'_walk_hubs u v g hu).choose.map ⟨e, @hom_fwd⟩).reachable
     obtain ⟨w', hw'⟩ := hreach.exists_walk_length_eq_dist
     calc G.dist _ _ ≤ ((w'.map ⟨e.symm, @hom_back⟩).copy
           (e.symm_apply_apply _) (e.symm_apply_apply _)).length := SimpleGraph.dist_le _
-      _ = w'.length := by
-          rw [SimpleGraph.Walk.length_copy, SimpleGraph.Walk.length_map]
-      _ = G'.dist _ _ := hw'
+      _ = G'.dist _ _ := by rw [SimpleGraph.Walk.length_copy, SimpleGraph.Walk.length_map, hw']
 
 /-! ## Projection map (for lower bound proof)
 

FdFormal/FlowerCounts.lean

@@ -107,10 +107,7 @@ theorem flowerVertCount_eq (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :
     omega
   | succ g ih =>
     simp only [flowerVertCount_succ, flowerEdgeCount_eq_pow, pow_succ]
-    have h1 : 1 ≤ u + v := by omega
-    have h2 : 2 ≤ u + v := by omega
-    zify [h1, h2] at ih ⊢
-    nlinarith [ih]
+    zify [show 1 ≤ u + v by omega, show 2 ≤ u + v by omega] at ih ⊢; nlinarith
 
 /-- The vertex count is always positive (holds for all `u`, `v`). -/
 theorem flowerVertCount_pos (u v g : ℕ) :
@@ -132,14 +129,10 @@ theorem flowerVertCount_lower (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :
 
 /-- Upper bound: `(w - 1) * N_g ≤ 2 * (w - 1) * w^g`. -/
 theorem flowerVertCount_upper (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :
-    (u + v - 1) * flowerVertCount u v g ≤
-    2 * (u + v - 1) * (u + v) ^ g := by
+    (u + v - 1) * flowerVertCount u v g ≤ 2 * (u + v - 1) * (u + v) ^ g := by
   rw [flowerVertCount_eq u v g hu huv]
-  have h1 : 1 ≤ u + v := by omega
-  have h2 : 2 ≤ u + v := by omega
   have h_pow : 1 ≤ (u + v) ^ g := Nat.one_le_pow _ _ (by omega)
-  zify [h1, h2] at h_pow ⊢
-  nlinarith [h_pow]
+  zify [show 1 ≤ u + v by omega, show 2 ≤ u + v by omega] at h_pow ⊢; nlinarith
 
 /-! ### Monotonicity -/
 
@@ -163,11 +156,10 @@ theorem flowerVertCount_cast_eq (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) :
     (↑(u + v) - 1 : ℝ) * (↑(flowerVertCount u v g) : ℝ) =
     (↑(u + v) - 2 : ℝ) * (↑(u + v) : ℝ) ^ g + (↑(u + v) : ℝ) := by
   have h := flowerVertCount_eq u v g hu huv
-  have h_cast := congr_arg (Nat.cast (R := ℝ)) h
-  simp only [Nat.cast_mul, Nat.cast_pow, Nat.cast_add] at h_cast
-  rw [Nat.cast_sub (by omega : 2 ≤ u + v),
-      Nat.cast_sub (by omega : 1 ≤ u + v)] at h_cast
-  exact_mod_cast h_cast
+  have := congr_arg (Nat.cast (R := ℝ)) h
+  simp only [Nat.cast_mul, Nat.cast_pow, Nat.cast_add] at this
+  rw [Nat.cast_sub (by omega), Nat.cast_sub (by omega)] at this
+  exact_mod_cast this
 
 /-! ### Real-valued wrappers -/
 
@@ -177,6 +169,5 @@ noncomputable def flowerVertCountReal (u v : ℕ) (g : ℕ) : ℝ :=
 
 /-- The real-valued vertex count is positive. -/
 theorem flowerVertCountReal_pos (u v g : ℕ) :
-    0 < flowerVertCountReal u v g := by
-  simp only [flowerVertCountReal]
-  exact Nat.cast_pos.mpr (flowerVertCount_pos u v g)
+    0 < flowerVertCountReal u v g :=
+  Nat.cast_pos.mpr (flowerVertCount_pos u v g)

FdFormal/FlowerDiameter.lean

@@ -78,8 +78,8 @@ theorem flowerHubDist_pos (u v g : ℕ) (hu : 1 < u) :
 
 /-- Hub distance grows strictly between generations. -/
 theorem flowerHubDist_strict_mono (u v g : ℕ) (hu : 1 < u) :
-    flowerHubDist u v g < flowerHubDist u v (g + 1) := by
-  exact lt_mul_of_one_lt_left (flowerHubDist_pos u v g hu) hu
+    flowerHubDist u v g < flowerHubDist u v (g + 1) :=
+  lt_mul_of_one_lt_left (flowerHubDist_pos u v g hu) hu
 
 /-! ### Cast identity -/
 
@@ -96,6 +96,5 @@ noncomputable def flowerHubDistReal (u v g : ℕ) : ℝ :=
 
 /-- The real-valued hub distance is positive when `1 < u`. -/
 theorem flowerHubDistReal_pos (u v g : ℕ) (hu : 1 < u) :
-    0 < flowerHubDistReal u v g := by
-  simp only [flowerHubDistReal]
-  exact Nat.cast_pos.mpr (flowerHubDist_pos u v g hu)
+    0 < flowerHubDistReal u v g :=
+  Nat.cast_pos.mpr (flowerHubDist_pos u v g hu)

FdFormal/FlowerDimension.lean

@@ -105,7 +105,6 @@ theorem flowerDimension (u v : ℕ) (hu : 1 < u) (huv : u ≤ v) :
         log ↑(flowerHubDist u v g))
       atTop
       (nhds (log ↑(u + v) / log ↑u)) := by
-  -- Positivity
   have hlogu : 0 < log (↑u : ℝ) :=
     log_pos (by exact_mod_cast hu)
   have hlogw : 0 < log (↑(u + v) : ℝ) :=
@@ -129,53 +128,40 @@ theorem flowerDimension (u v : ℕ) (hu : 1 < u) (huv : u ≤ v) :
     filter_upwards [eventually_gt_atTop 0] with g hg
     rw [h_log_hub]
   -- Step 3: Decompose ratio = residual + constant
-  -- log(N_g)/(g*log u) = [log(N_g) - g*log w]/(g*log u) + log w/log u
   have h_decomp : ∀ g : ℕ, 0 < (↑g : ℝ) →
       log ↑(flowerVertCount u v g) / (↑g * log (↑u : ℝ)) =
       (log ↑(flowerVertCount u v g) - ↑g * log ↑(u + v)) /
         (↑g * log (↑u : ℝ)) +
       log ↑(u + v) / log (↑u : ℝ) := by
-    intro g hg
-    have hg_ne : (↑g : ℝ) ≠ 0 := ne_of_gt hg
-    have hlogu_ne : log (↑u : ℝ) ≠ 0 := ne_of_gt hlogu
-    field_simp
-    ring
+    intro g hg; field_simp; ring
   -- Step 4: Show residual → 0
-  -- 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₁ :=
     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 :=
     Tendsto.atTop_mul_const hlogu (tendsto_natCast_atTop_atTop (R := ℝ))
-  -- Lower bound: log(c₁) ≤ log(N_g) - g * log(w)
   have h_res_lower : ∀ᶠ g in atTop,
       log c₁ / (↑g * log (↑u : ℝ)) ≤
       (log ↑(flowerVertCount u v g) - ↑g * log ↑(u + v)) /
         (↑g * log (↑u : ℝ)) := by
     filter_upwards [eventually_gt_atTop 0] with g hg
     have hg_pos : (0 : ℝ) < ↑g := Nat.cast_pos.mpr hg
     rw [div_le_div_iff_of_pos_right (mul_pos hg_pos hlogu)]
-    have h_bound := flowerVertCount_ge_real u v g hu huv
-    have h_cw_pos : 0 < c₁ * (↑(u + v) : ℝ) ^ g :=
-      mul_pos hc₁_pos (pow_pos hw_pos g)
-    have h_log := log_le_log h_cw_pos h_bound
+    have h_log := log_le_log (mul_pos hc₁_pos (pow_pos hw_pos g))
+      (flowerVertCount_ge_real u v g hu huv)
     rw [log_mul (ne_of_gt hc₁_pos) (ne_of_gt (pow_pos hw_pos g)),
         log_pow] at h_log
     linarith
-  -- Upper bound: log(N_g) - g * log(w) ≤ log(2)
   have h_res_upper : ∀ᶠ g in atTop,
       (log ↑(flowerVertCount u v g) - ↑g * log ↑(u + v)) /
         (↑g * log (↑u : ℝ)) ≤
       log 2 / (↑g * log (↑u : ℝ)) := by
     filter_upwards [eventually_gt_atTop 0] with g hg
     have hg_pos : (0 : ℝ) < ↑g := Nat.cast_pos.mpr hg
     rw [div_le_div_iff_of_pos_right (mul_pos hg_pos hlogu)]
-    have h_bound := flowerVertCount_le_real u v g hu huv
-    have h_log := log_le_log (hN_pos g) h_bound
+    have h_log := log_le_log (hN_pos g) (flowerVertCount_le_real u v g hu huv)
     rw [log_mul (by norm_num : (2 : ℝ) ≠ 0)
           (ne_of_gt (pow_pos hw_pos g)),
         log_pow] at h_log

FdFormal/FlowerLog.lean

@@ -74,11 +74,11 @@ theorem log_flowerVertCount_residual_lower :
   have h_ge : (↑(u + v) - 2) / (↑(u + v) - 1) * (↑(u + v) : ℝ) ^ g ≤
       ↑(flowerVertCount u v g) := by
     rw [div_mul_eq_mul_div, div_le_iff₀ hw1]
-    have h_cast := Nat.cast_le (α := ℝ) |>.mpr (flowerVertCount_lower u v g hu huv)
-    simp only [Nat.cast_mul, Nat.cast_pow] at h_cast
+    have := Nat.cast_le (α := ℝ) |>.mpr (flowerVertCount_lower u v g hu huv)
+    simp only [Nat.cast_mul, Nat.cast_pow] at this
     rw [Nat.cast_sub (by omega : 2 ≤ u + v),
-        Nat.cast_sub (by omega : 1 ≤ u + v)] at h_cast
-    simp only [Nat.cast_ofNat, Nat.cast_one] at h_cast
+        Nat.cast_sub (by omega : 1 ≤ u + v)] at this
+    simp only [Nat.cast_ofNat, Nat.cast_one] at this
     linarith [mul_comm (↑(u + v) - 1 : ℝ) (↑(flowerVertCount u v g) : ℝ)]
   have h_log := log_le_log (mul_pos hc (pow_pos hw_pos g)) h_ge
   rw [log_mul (ne_of_gt hc) (ne_of_gt (pow_pos hw_pos g)), log_pow] at h_log

FdFormal/GraphBall.lean

@@ -129,10 +129,8 @@ theorem mem_ball_of_mem_ball_of_mem_ball {c v w : V} {r₁ r₂ : ℕ∞}
     (hv : v ∈ G.ball c r₁) (hw : w ∈ G.ball v r₂) :
     w ∈ G.ball c (r₁ + r₂) := by
   simp only [mem_ball] at *
-  have hw_ne : G.edist v w ≠ ⊤ := ne_top_of_lt hw
-  calc G.edist c w
-    ≤ G.edist c v + G.edist v w := G.edist_triangle
-    _ < r₁ + G.edist v w := (ENat.add_lt_add_iff_right hw_ne).mpr hv
+  calc G.edist c w ≤ G.edist c v + G.edist v w := G.edist_triangle
+    _ < r₁ + G.edist v w := (ENat.add_lt_add_iff_right (ne_top_of_lt hw)).mpr hv
     _ ≤ r₁ + r₂ := by gcongr
 
 end SimpleGraph

FdFormal/PathGraphDist.lean

@@ -112,13 +112,10 @@ theorem pathGraph_edist {n : ℕ} (i j : Fin (n + 1)) :
     · obtain ⟨w', hw'⟩ := pathGraph_walk_le (show j.val ≤ i.val by omega)
       exact ⟨w'.reverse, by rw [Walk.length_reverse, hw']⟩
   apply le_antisymm
-  · -- Upper: edist ≤ walk length = target
-    calc (pathGraph (n + 1)).edist i j
+  · calc (pathGraph (n + 1)).edist i j
         ≤ ↑w.length := edist_le w
       _ = _ := by exact_mod_cast hw
-  · -- Lower: target ≤ every walk length → target ≤ iInf
-    simp only [edist]
-    exact le_iInf fun w' ↦ by exact_mod_cast pathGraph_walk_length_ge w'
+  · exact le_iInf fun w' ↦ by exact_mod_cast pathGraph_walk_length_ge w'
 
 /-! ### Distance formula -/