chore: remove unused cases' names (#9451)

These unused names will soon acquire a linter warning. Easiest to clean them up pre-emptively. (Thanks to @nomeata for fixing these on `nightly-testing`.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Jan 5, 2024 · 26348e8 · 26348e8 · nomeata · Jan 5, 2024
1 parent cf7dace
commit 26348e8
Show file tree

Hide file tree

Showing 9 changed files with 11 additions and 11 deletions.
diff --git a/Mathlib/Data/FP/Basic.lean b/Mathlib/Data/FP/Basic.lean
@@ -147,10 +147,10 @@ def divNatLtTwoPow (n d : ℕ) : ℤ → Bool
 @[nolint docBlame]
 unsafe def ofPosRatDn (n : ℕ+) (d : ℕ+) : Float × Bool := by
   let e₁ : ℤ := n.1.size - d.1.size - prec
-  cases' h₁ : Int.shift2 d.1 n.1 (e₁ + prec) with d₁ n₁
+  cases' Int.shift2 d.1 n.1 (e₁ + prec) with d₁ n₁
   let e₂ := if n₁ < d₁ then e₁ - 1 else e₁
   let e₃ := max e₂ emin
-  cases' h₂ : Int.shift2 d.1 n.1 (e₃ + prec) with d₂ n₂
+  cases' Int.shift2 d.1 n.1 (e₃ + prec) with d₂ n₂
   let r := mkRat n₂ d₂
   let m := r.floor
   refine' (Float.finite Bool.false e₃ (Int.toNat m) _, r.den = 1)

diff --git a/Mathlib/Data/List/MinMax.lean b/Mathlib/Data/List/MinMax.lean
@@ -346,7 +346,7 @@ variable [LinearOrder α] {l : List α} {a m : α}
 
 theorem maximum_concat (a : α) (l : List α) : maximum (l ++ [a]) = max (maximum l) a := by
   simp only [maximum, argmax_concat, id]
-  cases h : argmax id l
+  cases argmax id l
   · exact (max_eq_right bot_le).symm
   · simp [WithBot.some_eq_coe, max_def_lt, WithBot.coe_lt_coe]
 #align list.maximum_concat List.maximum_concat

diff --git a/Mathlib/Data/PFunctor/Univariate/M.lean b/Mathlib/Data/PFunctor/Univariate/M.lean
@@ -129,7 +129,7 @@ def sCorec : X → ∀ n, CofixA F n
 theorem P_corec (i : X) (n : ℕ) : Agree (sCorec f i n) (sCorec f i (succ n)) := by
   induction' n with n n_ih generalizing i
   constructor
-  cases' h : f i with y g
+  cases' f i with y g
   constructor
   introv
   apply n_ih
@@ -578,7 +578,7 @@ theorem corec_def {X} (f : X → F X) (x₀ : X) : M.corec f x₀ = M.mk (F.map
   cases' n with n
   · dsimp only [sCorec, Approx.sMk]
   · dsimp only [sCorec, Approx.sMk]
-    cases h : f x₀
+    cases f x₀
     dsimp only [PFunctor.map]
     congr
 set_option linter.uppercaseLean3 false in

diff --git a/Mathlib/Data/QPF/Univariate/Basic.lean b/Mathlib/Data/QPF/Univariate/Basic.lean
@@ -541,7 +541,7 @@ def comp : QPF (Functor.Comp F₂ F₁) where
     conv =>
       rhs
       rw [← abs_repr x]
-    cases' h : repr x with a f
+    cases' repr x with a f
     dsimp
     congr with x
     cases' h' : repr (f x) with b g

diff --git a/Mathlib/Logic/Encodable/Basic.lean b/Mathlib/Logic/Encodable/Basic.lean
@@ -644,7 +644,7 @@ theorem sequence_mono_nat {r : β → β → Prop} {f : α → β} (hf : Directe
     r (f (hf.sequence f n)) (f (hf.sequence f (n + 1))) := by
   dsimp [Directed.sequence]
   generalize hf.sequence f n = p
-  cases' h : (decode n: Option α) with a
+  cases' (decode n : Option α) with a
   · exact (Classical.choose_spec (hf p p)).1
   · exact (Classical.choose_spec (hf p a)).1
 #align directed.sequence_mono_nat Directed.sequence_mono_nat

diff --git a/Mathlib/Order/Estimator.lean b/Mathlib/Order/Estimator.lean
@@ -179,7 +179,7 @@ instance (a b : Thunk ℕ) {εa εb : Type*} [Estimator a εa] [Estimator b εb]
     have s₁ := Estimator.improve_spec (a := a) e.1
     have s₂ := Estimator.improve_spec (a := b) e.2
     revert s₁ s₂
-    cases h₁ : improve a e.fst <;> cases h₂ : improve b e.snd <;> intro s₁ s₂ <;> simp_all only
+    cases improve a e.fst <;> cases improve b e.snd <;> intro s₁ s₂ <;> simp_all only
     · apply Nat.add_lt_add_left s₂
     · apply Nat.add_lt_add_right s₁
     · apply Nat.add_lt_add_right s₁

diff --git a/Mathlib/Order/InitialSeg.lean b/Mathlib/Order/InitialSeg.lean
@@ -513,7 +513,7 @@ noncomputable def InitialSeg.leLT [IsWellOrder β s] [IsTrans γ t] (f : r ≼i
 @[simp]
 theorem InitialSeg.leLT_apply [IsWellOrder β s] [IsTrans γ t] (f : r ≼i s) (g : s ≺i t) (a : α) :
     (f.leLT g) a = g (f a) := by
-  delta InitialSeg.leLT; cases' h : f.ltOrEq with f' f'
+  delta InitialSeg.leLT; cases' f.ltOrEq with f' f'
   · simp only [PrincipalSeg.trans_apply, f.ltOrEq_apply_left]
   · simp only [PrincipalSeg.equivLT_apply, f.ltOrEq_apply_right]
 #align initial_seg.le_lt_apply InitialSeg.leLT_apply

diff --git a/Mathlib/RingTheory/Ideal/Norm.lean b/Mathlib/RingTheory/Ideal/Norm.lean
@@ -553,7 +553,7 @@ theorem spanNorm_localization (I : Ideal S) [Module.Finite R S] [Module.Free R S
     [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ]
     [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] :
     spanNorm Rₘ (I.map (algebraMap S Sₘ)) = (spanNorm R I).map (algebraMap R Rₘ) := by
-  cases h : subsingleton_or_nontrivial R
+  cases subsingleton_or_nontrivial R
   · haveI := IsLocalization.unique R Rₘ M
     simp [eq_iff_true_of_subsingleton]
   let b := Module.Free.chooseBasis R S

diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean
@@ -515,7 +515,7 @@ theorem sub_nfBelow : ∀ {o₁ o₂ b}, NFBelow o₁ b → NF o₂ → NFBelow
     · apply NFBelow.zero
     · simp only [h, Ordering.compares_eq] at this
       subst e₂
-      cases mn : (n₁ : ℕ) - n₂ <;> simp [sub]
+      cases (n₁ : ℕ) - n₂ <;> simp [sub]
       · by_cases en : n₁ = n₂ <;> simp [en]
         · exact h'.mono (le_of_lt h₁.lt)
         · exact NFBelow.zero