chore: add missing hypothesis names to by_cases (#8533)

I've also got a change to make this required, but I'd like to land this first.

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -66,27 +66,27 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
             refine ⟨fun _ => ?_, fun _ => ?_⟩
             · congr
               ext w
-              by_cases w = v <;> rename_i x
+              by_cases h : w = v <;> rename_i x
               · substs h
                 simp_all
               · simp_all
             · congr
               ext w
-              by_cases w = v <;> rename_i x
+              by_cases h : w = v <;> rename_i x
               · substs h
                 simp_all
               · simp_all
           · simp only [cond_true, h, ht₁]
             refine ⟨fun _ => ?_, fun _ => ?_⟩
             · congr
               ext w
-              by_cases w = v <;> rename_i x
+              by_cases h : w = v <;> rename_i x
               · substs h
                 simp_all
               · simp_all
             · congr
               ext w
-              by_cases w = v <;> rename_i x
+              by_cases h : w = v <;> rename_i x
               · substs h
                 simp_all
               · simp_all
@@ -105,7 +105,7 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
             constructor <;> assumption
         · have := ht₃ w
           have := he₃ w
-          by_cases w = v
+          by_cases h : w = v
           · subst h; simp_all
           · simp_all? says simp_all only [Option.elim, ne_eq, normalized, Bool.and_eq_true,
               Bool.not_eq_true', not_false_eq_true, AList.lookup_insert_ne]

Mathlib/Algebra/CharP/MixedCharZero.lean

@@ -347,7 +347,7 @@ theorem split_by_characteristic (h_pos : ∀ p : ℕ, p ≠ 0 → CharP R p →
     (h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P := by
   cases CharP.exists R with
   | intro p p_charP =>
-    by_cases p = 0
+    by_cases h : p = 0
     · rw [h] at p_charP
       haveI h0 : CharZero R := CharP.charP_to_charZero R
       exact split_equalCharZero_mixedCharZero R h_equal h_mixed

Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

@@ -427,14 +427,14 @@ variable (F G) (R)
 def δ_hom : Cochain F G n →ₗ[R] Cochain F G m where
   toFun := δ n m
   map_add' α β := by
-    by_cases n + 1 = m
+    by_cases h : n + 1 = m
     · ext p q hpq
       dsimp
       simp only [δ_v n m h _ p q hpq _ _ rfl rfl, Cochain.add_v, add_comp, comp_add, smul_add]
       abel
     · simp only [δ_shape _ _ h, add_zero]
   map_smul' r a := by
-    by_cases n + 1 = m
+    by_cases h : n + 1 = m
     · ext p q hpq
       dsimp
       simp only [δ_v n m h _ p q hpq _ _ rfl rfl, Cochain.smul_v, Linear.comp_smul,
@@ -514,7 +514,7 @@ lemma δ_zero_cochain_v (z : Cochain F G 0) (p q : ℤ) (hpq : p + 1 = q) :
 
 @[simp]
 lemma δ_ofHom {p : ℤ} (φ : F ⟶ G) : δ 0 p (Cochain.ofHom φ) = 0 := by
-  by_cases p = 1
+  by_cases h : p = 1
   · subst h
     ext
     simp

Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean

@@ -162,7 +162,7 @@ lemma comp_liftCycles {A' A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j)
 lemma liftCycles_homologyπ_eq_zero_of_boundary {A : C} (k : A ⟶ K.X i) (j : ι)
     (hj : c.next i = j) {i' : ι} (x : A ⟶ K.X i') (hx : k = x ≫ K.d i' i) :
     K.liftCycles k j hj (by rw [hx, assoc, K.d_comp_d, comp_zero]) ≫ K.homologyπ i = 0 := by
-  by_cases c.Rel i' i
+  by_cases h : c.Rel i' i
   · obtain rfl := c.prev_eq' h
     exact (K.sc i).liftCycles_homologyπ_eq_zero_of_boundary _ x hx
   · have : liftCycles K k j hj (by rw [hx, assoc, K.d_comp_d, comp_zero]) = 0 := by
@@ -265,7 +265,7 @@ lemma descOpcycles_comp {A A' : C} (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j
 lemma homologyι_descOpcycles_eq_zero_of_boundary {A : C} (k : K.X i ⟶ A) (j : ι)
     (hj : c.prev i = j) {i' : ι} (x : K.X i' ⟶ A) (hx : k = K.d i i' ≫ x) :
     K.homologyι i ≫ K.descOpcycles k j hj (by rw [hx, K.d_comp_d_assoc, zero_comp]) = 0 := by
-  by_cases c.Rel i i'
+  by_cases h : c.Rel i i'
   · obtain rfl := c.next_eq' h
     exact (K.sc i).homologyι_descOpcycles_eq_zero_of_boundary _ x hx
   · have : K.descOpcycles k j hj (by rw [hx, K.d_comp_d_assoc, zero_comp]) = 0 := by

Mathlib/Algebra/Homology/Single.lean

@@ -97,7 +97,7 @@ theorem single_map_f_self (j : ι) {A B : V} (f : A ⟶ B) :
 lemma from_single_hom_ext {K : HomologicalComplex V c} {j : ι} {A : V}
     {f g : (single V c j).obj A ⟶ K} (hfg : f.f j = g.f j) : f = g := by
   ext i
-  by_cases i = j
+  by_cases h : i = j
   · subst h
     exact hfg
   · apply (isZero_single_obj_X c j A i h).eq_of_src
@@ -106,7 +106,7 @@ lemma from_single_hom_ext {K : HomologicalComplex V c} {j : ι} {A : V}
 lemma to_single_hom_ext {K : HomologicalComplex V c} {j : ι} {A : V}
     {f g : K ⟶ (single V c j).obj A} (hfg : f.f j = g.f j) : f = g := by
   ext i
-  by_cases i = j
+  by_cases h : i = j
   · subst h
     exact hfg
   · apply (isZero_single_obj_X c j A i h).eq_of_tgt

Mathlib/Algebra/Squarefree.lean

@@ -199,7 +199,7 @@ theorem Squarefree.isRadical {x : R} (hx : Squarefree x) : IsRadical x :=
     And.right <|
       (dvd_gcd_iff x x y).1
         (by
-          by_cases gcd x y = 0
+          by_cases h : gcd x y = 0
           · rw [h]
             apply dvd_zero
           replace hy := ((dvd_gcd_iff x x _).2 ⟨dvd_rfl, hy⟩).trans gcd_pow_right_dvd_pow_gcd

Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean

@@ -62,7 +62,7 @@ theorem σ_comp_P_eq_zero (X : SimplicialObject C) {n q : ℕ} (i : Fin (n + 1))
     exfalso
     linarith [Fin.is_lt i]
   · intro i (hi : n + 1 ≤ i + q + 1)
-    by_cases n + 1 ≤ (i : ℕ) + q
+    by_cases h : n + 1 ≤ (i : ℕ) + q
     · rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]
     · replace hi : n = i + q := by
         obtain ⟨j, hj⟩ := le_iff_exists_add.mp hi

Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean

@@ -88,7 +88,7 @@ theorem Γ₀_obj_termwise_mapMono_comp_PInfty (X : SimplicialObject C) {Δ Δ'
   induction' Δ' using SimplexCategory.rec with n'
   dsimp
   -- We start with the case `i` is an identity
-  by_cases n = n'
+  by_cases h : n = n'
   · subst h
     simp only [SimplexCategory.eq_id_of_mono i, Γ₀.Obj.Termwise.mapMono_id, op_id, X.map_id]
     dsimp

Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean

@@ -38,7 +38,7 @@ by a splitting of a simplicial object. -/
 noncomputable def πSummand [HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ} (A : IndexSet Δ) :
     X.obj Δ ⟶ s.N A.1.unop.len := by
   refine' (s.iso Δ).inv ≫ Sigma.desc fun B => _
-  by_cases B = A
+  by_cases h : B = A
   · exact eqToHom (by subst h; rfl)
   · exact 0
 #align simplicial_object.splitting.π_summand SimplicialObject.Splitting.πSummand
@@ -254,7 +254,7 @@ noncomputable def nondegComplexFunctor : Split C ⥤ ChainComplex C ℕ where
         intro A
         dsimp [alternatingFaceMapComplex]
         erw [ιSummand_naturality_symm_assoc Φ A]
-        by_cases A.EqId
+        by_cases h : A.EqId
         · dsimp at h
           subst h
           simp only [Splitting.ι_πSummand_eq_id, comp_id, Splitting.ι_πSummand_eq_id_assoc]

Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

@@ -214,7 +214,7 @@ protected noncomputable def extraDegeneracy (Δ : SimplexCategory) :
     apply SimplexCategory.Hom.ext
     ext j : 2
     dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.standardSimplex]
-    by_cases j = 0
+    by_cases h : j = 0
     · subst h
       simp only [Fin.succ_succAbove_zero, shiftFun_0]
     · obtain ⟨_, rfl⟩ := Fin.eq_succ_of_ne_zero <| h
@@ -225,7 +225,7 @@ protected noncomputable def extraDegeneracy (Δ : SimplexCategory) :
     apply SimplexCategory.Hom.ext
     ext j : 2
     dsimp [SimplicialObject.σ, SimplexCategory.σ, SSet.standardSimplex]
-    by_cases j = 0
+    by_cases h : j = 0
     · subst h
       simp only [shiftFun_0]
       exact shiftFun_0 φ.toOrderHom
@@ -326,7 +326,7 @@ noncomputable def extraDegeneracy : SimplicialObject.Augmented.ExtraDegeneracy f
     dsimp [cechNerve, SimplicialObject.δ, SimplexCategory.δ]
     ext j
     · simp only [assoc, WidePullback.lift_π]
-      by_cases j = 0
+      by_cases h : j = 0
       · subst h
         erw [Fin.succ_succAbove_zero, ExtraDegeneracy.s_comp_π_0, ExtraDegeneracy.s_comp_π_0]
         dsimp
@@ -344,7 +344,7 @@ noncomputable def extraDegeneracy : SimplicialObject.Augmented.ExtraDegeneracy f
     dsimp [cechNerve, SimplicialObject.σ, SimplexCategory.σ]
     ext j
     · simp only [assoc, WidePullback.lift_π]
-      by_cases j = 0
+      by_cases h : j = 0
       · subst h
         erw [ExtraDegeneracy.s_comp_π_0, ExtraDegeneracy.s_comp_π_0]
         dsimp

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -512,7 +512,7 @@ instance {n : ℕ} {i : Fin (n + 1)} : Epi (σ i) := by
   rw [epi_iff_surjective]
   intro b
   simp only [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk]
-  by_cases b ≤ i
+  by_cases h : b ≤ i
   · use b
     -- This was not needed before leanprover/lean4#2644
     dsimp
@@ -661,7 +661,7 @@ theorem eq_σ_comp_of_not_injective {n : ℕ} {Δ' : SimplexCategory} (θ : mk (
 
 theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ mk (n + 1))
     (i : Fin (n + 2)) (hi : ∀ x, θ.toOrderHom x ≠ i) : ∃ θ' : Δ ⟶ mk n, θ = θ' ≫ δ i := by
-  by_cases i < Fin.last (n + 1)
+  by_cases h : i < Fin.last (n + 1)
   · use θ ≫ σ (Fin.castPred i)
     ext1
     ext1

Mathlib/Analysis/Complex/OpenMapping.lean

@@ -126,7 +126,7 @@ theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds {z₀ : E} (hg : Anal
     · exact hgr (by simpa [norm_smul, mem_sphere_zero_iff_norm.mp hz] using ht)
     · exact analyticAt_const.add
         ((ContinuousLinearMap.smulRight (ContinuousLinearMap.id ℂ ℂ) z).analyticAt t)
-  by_cases ∀ z ∈ sphere (0 : E) 1, ∀ᶠ t in 𝓝 0, gray z t = gray z 0
+  by_cases h : ∀ z ∈ sphere (0 : E) 1, ∀ᶠ t in 𝓝 0, gray z t = gray z 0
   · left
     -- If g is eventually constant along every direction, then it is eventually constant
     refine eventually_of_mem (ball_mem_nhds z₀ hr) fun z hz => ?_
@@ -162,7 +162,7 @@ is analytic on a connected set `U`, then either it is constant on `U`, or it is
 sense that it maps any open set contained in `U` to an open set in `ℂ`). -/
 theorem AnalyticOn.is_constant_or_isOpen (hg : AnalyticOn ℂ g U) (hU : IsPreconnected U) :
     (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ (s) (_ : s ⊆ U), IsOpen s → IsOpen (g '' s) := by
-  by_cases ∃ z₀ ∈ U, ∀ᶠ z in 𝓝 z₀, g z = g z₀
+  by_cases h : ∃ z₀ ∈ U, ∀ᶠ z in 𝓝 z₀, g z = g z₀
   · obtain ⟨z₀, hz₀, h⟩ := h
     exact Or.inl ⟨g z₀, hg.eqOn_of_preconnected_of_eventuallyEq analyticOn_const hU hz₀ h⟩
   · push_neg at h

Mathlib/Analysis/Complex/Schwarz.lean

@@ -116,7 +116,7 @@ theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div [CompleteSpace E] [St
     Set.EqOn f (fun z => f c + (z - c) • dslope f c z₀) (ball c R₁) := by
   set g := dslope f c
   rintro z hz
-  by_cases z = c; · simp [h]
+  by_cases h : z = c; · simp [h]
   have h_R₁ : 0 < R₁ := nonempty_ball.mp ⟨_, h_z₀⟩
   have g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁ := fun z hz =>
     norm_dslope_le_div_of_mapsTo_ball hd h_maps hz

Mathlib/Analysis/InnerProductSpace/Calculus.lean

@@ -262,7 +262,7 @@ theorem not_differentiableAt_abs_zero : ¬ DifferentiableAt ℝ (abs : ℝ → 
   rw [Filter.HasBasis.frequently_iff Metric.nhds_basis_ball]
   intro δ hδ
   obtain ⟨x, hx⟩ : ∃ x ∈ Metric.ball 0 δ, x ≠ 0 ∧ f x ≤ 0 := by
-    by_cases f (δ / 2) ≤ 0
+    by_cases h : f (δ / 2) ≤ 0
     · use (δ / 2)
       simp [h, abs_of_nonneg hδ.le, hδ, hδ.ne']
     · use -(δ / 2)

Mathlib/Analysis/NormedSpace/Spectrum.lean

@@ -185,7 +185,7 @@ theorem spectralRadius_le_pow_nnnorm_pow_one_div (a : A) (n : ℕ) :
 theorem spectralRadius_le_liminf_pow_nnnorm_pow_one_div (a : A) :
     spectralRadius 𝕜 a ≤ atTop.liminf fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ) := by
   refine' ENNReal.le_of_forall_lt_one_mul_le fun ε hε => _
-  by_cases ε = 0
+  by_cases h : ε = 0
   · simp only [h, zero_mul, zero_le']
   have hε' : ε⁻¹ ≠ ∞ := fun h' =>
     h (by simpa only [inv_inv, inv_top] using congr_arg (fun x : ℝ≥0∞ => x⁻¹) h')
@@ -273,7 +273,7 @@ theorem hasFPowerSeriesOnBall_inverse_one_sub_smul [CompleteSpace A] (a : A) :
       · refine'
           le_trans (le_trans (mul_le_mul_right' (nnnorm_pow_le' a n.succ_pos) (r ^ n.succ)) _)
             (le_max_left _ _)
-        · by_cases ‖a‖₊ = 0
+        · by_cases h : ‖a‖₊ = 0
           · simp only [h, zero_mul, zero_le', pow_succ]
           · rw [← coe_inv h, coe_lt_coe, NNReal.lt_inv_iff_mul_lt h] at hr
             simpa only [← mul_pow, mul_comm] using pow_le_one' hr.le n.succ

Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

@@ -322,7 +322,7 @@ theorem Gamma_eq_GammaAux (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : Gamma s = Ga
       refine' lt_add_of_lt_of_nonneg i0 _
       rw [← Nat.cast_zero, Nat.cast_le]; exact Nat.zero_le k
   convert (u <| n - ⌊1 - s.re⌋₊).symm; rw [Nat.add_sub_of_le]
-  by_cases 0 ≤ 1 - s.re
+  by_cases h : 0 ≤ 1 - s.re
   · apply Nat.le_of_lt_succ
     exact_mod_cast lt_of_le_of_lt (Nat.floor_le h) (by linarith : 1 - s.re < n + 1)
   · rw [Nat.floor_of_nonpos]; linarith; linarith

Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean

@@ -58,7 +58,7 @@ theorem zero_cpow_eq_iff {x : ℂ} {a : ℂ} : (0 : ℂ) ^ x = a ↔ x ≠ 0 ∧
   constructor
   · intro hyp
     simp only [cpow_def, eq_self_iff_true, if_true] at hyp
-    by_cases x = 0
+    by_cases h : x = 0
     · subst h
       simp only [if_true, eq_self_iff_true] at hyp
       right

Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

@@ -487,7 +487,7 @@ namespace ENNReal
 theorem eventually_pow_one_div_le {x : ℝ≥0∞} (hx : x ≠ ∞) {y : ℝ≥0∞} (hy : 1 < y) :
     ∀ᶠ n : ℕ in atTop, x ^ (1 / n : ℝ) ≤ y := by
   lift x to ℝ≥0 using hx
-  by_cases y = ∞
+  by_cases h : y = ∞
   · exact eventually_of_forall fun n => h.symm ▸ le_top
   · lift y to ℝ≥0 using h
     have := NNReal.eventually_pow_one_div_le x (mod_cast hy : 1 < y)

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -107,7 +107,7 @@ theorem zero_rpow_eq_iff {x : ℝ} {a : ℝ} : 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 
   constructor
   · intro hyp
     simp only [rpow_def, Complex.ofReal_zero] at hyp
-    by_cases x = 0
+    by_cases h : x = 0
     · subst h
       simp only [Complex.one_re, Complex.ofReal_zero, Complex.cpow_zero] at hyp
       exact Or.inr ⟨rfl, hyp.symm⟩

Mathlib/CategoryTheory/Extensive.lean

@@ -310,7 +310,7 @@ noncomputable def finitaryExtensiveTopCatAux (Z : TopCat.{u})
       (fun h => s.inl <| eX.symm ⟨x, h⟩) fun h => s.inr <| eY.symm ⟨x, (this x).resolve_left h⟩, _⟩
     rw [continuous_iff_continuousAt]
     intro x
-    by_cases f x = Sum.inl PUnit.unit
+    by_cases h : f x = Sum.inl PUnit.unit
     · revert h x
       apply (IsOpen.continuousOn_iff _).mp
       · rw [continuousOn_iff_continuous_restrict]

Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean

@@ -175,7 +175,7 @@ instance fintypeHom (j j' : WidePullbackShape J) : Fintype (j ⟶ j')
     · cases' j with j
       · exact {Hom.id none}
       · exact {Hom.term j}
-    · by_cases some j' = j
+    · by_cases h : some j' = j
       · rw [h]
         exact {Hom.id j}
       · exact ∅
@@ -199,7 +199,7 @@ instance fintypeHom (j j' : WidePushoutShape J) : Fintype (j ⟶ j') where
     · cases' j' with j'
       · exact {Hom.id none}
       · exact {Hom.init j'}
-    · by_cases some j = j'
+    · by_cases h : some j = j'
       · rw [h]
         exact {Hom.id j'}
       · exact ∅

Mathlib/CategoryTheory/Preadditive/Mat.lean

@@ -243,11 +243,11 @@ instance hasFiniteBiproducts : HasFiniteBiproducts (Mat_ C) where
               simp at hj
             simp only [eqToHom_refl, dite_eq_ite, ite_true, Category.id_comp, ne_eq,
               Sigma.mk.inj_iff, not_and, id_def]
-            by_cases i' = i
+            by_cases h : i' = i
             · subst h
               rw [dif_pos rfl]
               simp only [heq_eq_eq, true_and]
-              by_cases j' = j
+              by_cases h : j' = j
               · subst h
                 simp
               · rw [dif_neg h, dif_neg (Ne.symm h)]

Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

@@ -182,7 +182,7 @@ variable (α)
 /-- The adjacency matrix of `G` is an adjacency matrix. -/
 @[simp]
 theorem isAdjMatrix_adjMatrix [Zero α] [One α] : (G.adjMatrix α).IsAdjMatrix :=
-  { zero_or_one := fun i j => by by_cases G.Adj i j <;> simp [h] }
+  { zero_or_one := fun i j => by by_cases h : G.Adj i j <;> simp [h] }
 #align simple_graph.is_adj_matrix_adj_matrix SimpleGraph.isAdjMatrix_adjMatrix
 
 /-- The graph induced by the adjacency matrix of `G` is `G` itself. -/

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -383,7 +383,7 @@ instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (SimpleGrap
       exact x.irrefl h.1
     inf_compl_le_bot := fun G v w h => False.elim <| h.2.2 h.1
     top_le_sup_compl := fun G v w hvw => by
-      by_cases G.Adj v w
+      by_cases h : G.Adj v w
       · exact Or.inl h
       · exact Or.inr ⟨hvw, h⟩
     sSup := sSup

Mathlib/Computability/TMToPartrec.lean

@@ -1686,7 +1686,7 @@ theorem tr_ret_respects (k v s) : ∃ b₂,
       · simp
       rw [trList, List.headI, trNat, Nat.cast_succ, Num.add_one, Num.succ, List.tail]
       cases (n : Num).succ' <;> exact ⟨rfl, rfl⟩
-    by_cases v.headI = 0 <;> simp only [h, ite_true, ite_false] at this ⊢
+    by_cases h : v.headI = 0 <;> simp only [h, ite_true, ite_false] at this ⊢
     · obtain ⟨c, h₁, h₂⟩ := IH v.tail (trList v).head?
       refine' ⟨c, h₁, TransGen.head rfl _⟩
       simp only [Option.mem_def, TM2.stepAux, trContStack, contStack, elim_main, this, cond_true,

Mathlib/Data/DFinsupp/WellFounded.lean

@@ -146,7 +146,7 @@ theorem Lex.acc_single [DecidableEq ι] {i : ι} (hi : Acc (rᶜ ⊓ (· ≠ ·)
     refine Lex.acc_of_single hbot x fun j hj ↦ ?_
     obtain rfl | hij := eq_or_ne i j
     · exact ha _ hs
-    by_cases r j i
+    by_cases h : r j i
     · rw [hr j h, single_eq_of_ne hij, single_zero]
       exact Lex.acc_zero hbot
     · exact ih _ ⟨h, hij.symm⟩ _

Mathlib/Data/List/Intervals.lean

@@ -140,7 +140,7 @@ theorem pred_singleton {m : ℕ} (h : 0 < m) : Ico (m - 1) m = [m - 1] := by
 #align list.Ico.pred_singleton List.Ico.pred_singleton
 
 theorem chain'_succ (n m : ℕ) : Chain' (fun a b => b = succ a) (Ico n m) := by
-  by_cases n < m
+  by_cases h : n < m
   · rw [eq_cons h]
     exact chain_succ_range' _ _ 1
   · rw [eq_nil_of_le (le_of_not_gt h)]