From da6d609bc61e561be97b1998d95c0c0f30c63364 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 5 Jan 2024 12:10:08 +1100 Subject: [PATCH 1/2] chore: rmeove unused cases' names --- Mathlib/Data/FP/Basic.lean | 4 ++-- Mathlib/Data/List/MinMax.lean | 2 +- Mathlib/Data/PFunctor/Univariate/M.lean | 4 ++-- Mathlib/Data/QPF/Univariate/Basic.lean | 2 +- Mathlib/Logic/Encodable/Basic.lean | 2 +- Mathlib/Order/Estimator.lean | 2 +- Mathlib/Order/InitialSeg.lean | 2 +- Mathlib/RingTheory/Ideal/Norm.lean | 2 +- Mathlib/SetTheory/Ordinal/Notation.lean | 2 +- Mathlib/Tactic/Positivity/Core.lean | 2 +- 10 files changed, 12 insertions(+), 12 deletions(-) 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 b83e55c766e29..8989dbe286f68 100644 --- 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 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 9f3873f283372..7daa034066022 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/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 500ebe4ccb616..0b72971ea4213 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 3e30da76b787b..4247cccfcd67b 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 diff --git a/Mathlib/Tactic/Positivity/Core.lean b/Mathlib/Tactic/Positivity/Core.lean index 755eb8cbe93ee..6df2444342089 100644 --- a/Mathlib/Tactic/Positivity/Core.lean +++ b/Mathlib/Tactic/Positivity/Core.lean @@ -74,7 +74,7 @@ initialize positivityExt : PersistentEnvExtension Entry (Entry × PositivityExt) (List Entry × DiscrTree PositivityExt) ← -- we only need this to deduplicate entries in the DiscrTree have : BEq PositivityExt := ⟨fun _ _ => false⟩ - let insert kss v dt := kss.foldl (fun dt ks => dt.insertCore ks v discrTreeConfig) dt + let insert kss v dt := kss.foldl (fun dt ks => dt.insertCore ks v) dt registerPersistentEnvExtension { mkInitial := pure ([], {}) addImportedFn := fun s => do From 2893621497948bbc2fc5274bde5d810f752bc972 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 5 Jan 2024 12:16:02 +1100 Subject: [PATCH 2/2] revert stray change --- Mathlib/Tactic/Positivity/Core.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Tactic/Positivity/Core.lean b/Mathlib/Tactic/Positivity/Core.lean index 6df2444342089..755eb8cbe93ee 100644 --- a/Mathlib/Tactic/Positivity/Core.lean +++ b/Mathlib/Tactic/Positivity/Core.lean @@ -74,7 +74,7 @@ initialize positivityExt : PersistentEnvExtension Entry (Entry × PositivityExt) (List Entry × DiscrTree PositivityExt) ← -- we only need this to deduplicate entries in the DiscrTree have : BEq PositivityExt := ⟨fun _ _ => false⟩ - let insert kss v dt := kss.foldl (fun dt ks => dt.insertCore ks v) dt + let insert kss v dt := kss.foldl (fun dt ks => dt.insertCore ks v discrTreeConfig) dt registerPersistentEnvExtension { mkInitial := pure ([], {}) addImportedFn := fun s => do