fixes for leanprover/lean4#5309

leanprover-community · Sep 12, 2024 · 8ec1a25 · 8ec1a25
1 parent dc7c7e8
commit 8ec1a25
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 7 deletions.
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
@@ -254,7 +254,7 @@ theorem iff_of_source_openCover [IsAffine Y] (𝒰 : X.OpenCover) [∀ i, IsAffi
 theorem iff_of_isAffine [IsAffine X] [IsAffine Y] :
     P f ↔ Q (f.app ⊤) := by
   rw [iff_of_source_openCover (P := P) (Scheme.openCoverOfIsIso.{u} (𝟙 _))]
-  simp
+  simp [forall_const]
 
 theorem Spec_iff {R S : CommRingCat.{u}} {φ : R ⟶ S} :
     P (Spec.map φ) ↔ Q φ := by

diff --git a/Mathlib/Analysis/Convex/EGauge.lean b/Mathlib/Analysis/Convex/EGauge.lean
@@ -69,7 +69,7 @@ variable (𝕜 : Type*) [NNNorm 𝕜] [Nonempty 𝕜] {E : Type*} [Zero E] [SMul
   {c : 𝕜} {s t : Set E} {x : E} {r : ℝ≥0∞}
 
 @[simp] lemma egauge_zero_left_eq_top : egauge 𝕜 0 x = ∞ ↔ x ≠ 0 := by
-  simp [egauge_eq_top]
+  simp [egauge_eq_top, forall_const]
 
 @[simp] alias ⟨_, egauge_zero_left⟩ := egauge_zero_left_eq_top
 

diff --git a/Mathlib/LinearAlgebra/Matrix/PosDef.lean b/Mathlib/LinearAlgebra/Matrix/PosDef.lean
@@ -124,7 +124,7 @@ protected theorem intCast [StarOrderedRing R] [DecidableEq n] (d : ℤ) (hd : 0
 protected theorem _root_.Matrix.posSemidef_intCast_iff
     [StarOrderedRing R] [DecidableEq n] [Nonempty n] [Nontrivial R] (d : ℤ) :
     PosSemidef (d : Matrix n n R) ↔ 0 ≤ d :=
-  posSemidef_diagonal_iff.trans <| by simp [Pi.le_def]
+  posSemidef_diagonal_iff.trans <| by simp [Pi.le_def, forall_const]
 
 protected lemma pow [StarOrderedRing R] [DecidableEq n]
     {M : Matrix n n R} (hM : M.PosSemidef) (k : ℕ) :
@@ -384,7 +384,7 @@ protected theorem natCast [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R]
 theorem _root_.Matrix.posDef_natCast_iff [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R]
     [Nonempty n] [Nontrivial R] {d : ℕ} :
     PosDef (d : Matrix n n R) ↔ 0 < d :=
-  posDef_diagonal_iff.trans <| by simp
+  posDef_diagonal_iff.trans <| by simp [forall_const]
 
 -- See note [no_index around OfNat.ofNat]
 protected theorem ofNat [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R]
@@ -404,7 +404,7 @@ protected theorem intCast [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R]
 theorem _root_.Matrix.posDef_intCast_iff [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R]
     [Nonempty n] [Nontrivial R] {d : ℤ} :
     PosDef (d : Matrix n n R) ↔ 0 < d :=
-  posDef_diagonal_iff.trans <| by simp
+  posDef_diagonal_iff.trans <| by simp [forall_const]
 
 protected lemma add_posSemidef [CovariantClass R R (· + ·) (· ≤ · )]
     {A : Matrix m m R} {B : Matrix m m R}

diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean
@@ -823,7 +823,7 @@ instance (priority := 100) IsHaarMeasure.noAtoms [TopologicalGroup G] [BorelSpac
     [WeaklyLocallyCompactSpace G] [(𝓝[≠] (1 : G)).NeBot] (μ : Measure G) [μ.IsHaarMeasure] :
     NoAtoms μ := by
   cases eq_or_ne (μ 1) 0 with
-  | inl h => constructor; simpa
+  | inl h => constructor; intro g; simpa
   | inr h =>
     obtain ⟨K, K_compact, K_nhds⟩ : ∃ K : Set G, IsCompact K ∧ K ∈ 𝓝 1 := exists_compact_mem_nhds 1
     have K_inf : Set.Infinite K := infinite_of_mem_nhds (1 : G) K_nhds

diff --git a/Mathlib/NumberTheory/ModularForms/Basic.lean b/Mathlib/NumberTheory/ModularForms/Basic.lean
@@ -302,7 +302,7 @@ theorem add_apply (f g : CuspForm Γ k) (z : ℍ) : (f + g) z = f z + g z :=
 instance instZero : Zero (CuspForm Γ k) :=
   ⟨ { toSlashInvariantForm := 0
       holo' := fun _ => mdifferentiableAt_const 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ)
-      zero_at_infty' := by simpa using Filter.zero_zeroAtFilter _ } ⟩
+      zero_at_infty' := fun _ => by simpa using Filter.zero_zeroAtFilter _ } ⟩
 
 @[simp]
 theorem coe_zero : ⇑(0 : CuspForm Γ k) = (0 : ℍ → ℂ) :=