diff --git a/Mathlib/Data/FP/Basic.lean b/Mathlib/Data/FP/Basic.lean
index d1d2bb060cc8a..8bec271be9db9 100644
--- 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
index 06313430b3b7d..068ff7022be5c 100644
--- a/Mathlib/Data/List/MinMax.lean
+++ b/Mathlib/Data/List/MinMax.lean
@@ -345,7 +345,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
index 31072132ad0bc..b61c4dfa2c78f 100644
--- 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
index ee47afa0ec54e..5901731de0182 100644
--- 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
index 5fe3ed0d0456e..62579a65debf8 100644
--- 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/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean
index 573afc7088656..742ffde8dd441 100644
--- a/Mathlib/MeasureTheory/Integral/SetToL1.lean
+++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean
@@ -637,7 +637,7 @@ theorem setToSimpleFunc_const' [Nonempty α] (T : Set α → F →L[ℝ] F') (x
 
 theorem setToSimpleFunc_const (T : Set α → F →L[ℝ] F') (hT_empty : T ∅ = 0) (x : F)
     {m : MeasurableSpace α} : SimpleFunc.setToSimpleFunc T (SimpleFunc.const α x) = T univ x := by
-  cases hα : isEmpty_or_nonempty α
+  cases isEmpty_or_nonempty α
   · have h_univ_empty : (univ : Set α) = ∅ := Subsingleton.elim _ _
     rw [h_univ_empty, hT_empty]
     simp only [setToSimpleFunc, ContinuousLinearMap.zero_apply, sum_empty,
diff --git a/Mathlib/Order/Estimator.lean b/Mathlib/Order/Estimator.lean
index 763f956bfc634..364c8baeb69cb 100644
--- 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
index 67a77c84ab0bf..1062281ebc660 100644
--- 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
index 4100795d4f52f..f498dbb54e50f 100644
--- 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
index 113f6b9987dd5..9a9ca65077236 100644
--- 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