diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean
index 383594bd1b22c..4b89eb8b537c7 100644
--- a/Mathlib/Algebra/Group/Subgroup/Basic.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Basic.lean
@@ -1511,7 +1511,7 @@ variable {H K : Subgroup G}
 
 @[to_additive]
 instance (priority := 100) normal_of_comm {G : Type*} [CommGroup G] (H : Subgroup G) : H.Normal :=
-  ⟨by simp [mul_comm, mul_left_comm]⟩
+  ⟨by simp [mul_comm, mul_left_comm, forall_const]⟩
 
 namespace Normal
 
diff --git a/Mathlib/CategoryTheory/Sites/Types.lean b/Mathlib/CategoryTheory/Sites/Types.lean
index fca7e5d973986..962a6f8a389ca 100644
--- a/Mathlib/CategoryTheory/Sites/Types.lean
+++ b/Mathlib/CategoryTheory/Sites/Types.lean
@@ -172,6 +172,6 @@ theorem typesGrothendieckTopology_eq_canonical :
   have : (fun _ => ULift.up true) = fun _ => ULift.up false :=
     (hs PUnit fun _ => x).isSeparatedFor.ext
       fun β f hf => funext fun y => hsx.elim <| S.2 hf fun _ => y
-  simp [Function.funext_iff] at this
+  simp [Function.funext_iff, forall_const] at this
 
 end CategoryTheory
diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
index 8de6f50777720..6a5951d3c6539 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Clique.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
@@ -328,7 +328,7 @@ theorem CliqueFree.comap {H : SimpleGraph β} (f : H ↪g G) : G.CliqueFree n 
   obtain (hle | hlt) := le_or_lt n 1
   · obtain (rfl | rfl) := Nat.le_one_iff_eq_zero_or_eq_one.1 hle
     · simp [CliqueFree]
-    simp [CliqueFree, show ∃ (_ : β), True from ⟨f (Classical.arbitrary _), trivial⟩]
+    simp [CliqueFree, show ∃ (_ : β), True from ⟨f (Classical.arbitrary _), trivial⟩, forall_const]
   simp [CliqueFree, isNClique_map_iff hlt]
 
 /-- See `SimpleGraph.cliqueFree_of_chromaticNumber_lt` for a tighter bound. -/
diff --git a/Mathlib/Data/Fintype/Prod.lean b/Mathlib/Data/Fintype/Prod.lean
index 2a5dfcdbbbf59..99f2fd78f11f6 100644
--- a/Mathlib/Data/Fintype/Prod.lean
+++ b/Mathlib/Data/Fintype/Prod.lean
@@ -44,7 +44,7 @@ variable [Fintype α] [Fintype β] {s : Finset α} {t : Finset β}
 @[simp] lemma univ_product_univ : univ ×ˢ univ = (univ : Finset (α × β)) := rfl
 
 @[simp] lemma product_eq_univ [Nonempty α] [Nonempty β] : s ×ˢ t = univ ↔ s = univ ∧ t = univ := by
-  simp [eq_univ_iff_forall, forall_and]
+  simp [eq_univ_iff_forall, forall_and, forall_const]
 
 end Finset
 
diff --git a/Mathlib/Data/Set/Prod.lean b/Mathlib/Data/Set/Prod.lean
index 07ef12d57509b..c38042e8181d3 100644
--- a/Mathlib/Data/Set/Prod.lean
+++ b/Mathlib/Data/Set/Prod.lean
@@ -89,7 +89,7 @@ theorem univ_prod {t : Set β} : (univ : Set α) ×ˢ t = Prod.snd ⁻¹' t := b
 theorem prod_univ {s : Set α} : s ×ˢ (univ : Set β) = Prod.fst ⁻¹' s := by simp [prod_eq]
 
 @[simp] lemma prod_eq_univ [Nonempty α] [Nonempty β] : s ×ˢ t = univ ↔ s = univ ∧ t = univ := by
-  simp [eq_univ_iff_forall, forall_and]
+  simp [eq_univ_iff_forall, forall_and, forall_const]
 
 @[simp]
 theorem singleton_prod : ({a} : Set α) ×ˢ t = Prod.mk a '' t := by
@@ -647,7 +647,8 @@ theorem pi_eq_empty_iff : s.pi t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧
   rw [← not_nonempty_iff_eq_empty, pi_nonempty_iff]
   push_neg
   refine exists_congr fun i => ?_
-  cases isEmpty_or_nonempty (α i) <;> simp [*, forall_and, eq_empty_iff_forall_not_mem]
+  cases isEmpty_or_nonempty (α i) <;>
+    simp [*, forall_and, forall_const, eq_empty_iff_forall_not_mem]
 
 @[simp]
 theorem univ_pi_eq_empty_iff : pi univ t = ∅ ↔ ∃ i, t i = ∅ := by
diff --git a/Mathlib/Data/W/Basic.lean b/Mathlib/Data/W/Basic.lean
index aec104886a43b..93975201a133b 100644
--- a/Mathlib/Data/W/Basic.lean
+++ b/Mathlib/Data/W/Basic.lean
@@ -103,7 +103,7 @@ theorem infinite_of_nonempty_of_isEmpty (a b : α) [ha : Nonempty (β a)] [he :
     · cases' m with m
       · simp_all
       · refine congr_arg Nat.succ (ih ?_)
-        simp_all [Function.funext_iff]⟩
+        simp_all [Function.funext_iff, forall_const]⟩
 
 variable [∀ a : α, Fintype (β a)]
 
diff --git a/Mathlib/GroupTheory/HNNExtension.lean b/Mathlib/GroupTheory/HNNExtension.lean
index d4c6a1677d248..70362e141ba3f 100644
--- a/Mathlib/GroupTheory/HNNExtension.lean
+++ b/Mathlib/GroupTheory/HNNExtension.lean
@@ -259,7 +259,7 @@ theorem group_smul_head (g : G) (w : NormalWord d) : (g • w).head = g * w.head
 @[simp]
 theorem group_smul_toList (g : G) (w : NormalWord d) : (g • w).toList = w.toList := rfl
 
-instance : FaithfulSMul G (NormalWord d) := ⟨by simp [group_smul_def]⟩
+instance : FaithfulSMul G (NormalWord d) := ⟨by simp [group_smul_def, forall_const]⟩
 
 /-- A constructor to append an element `g` of `G` and `u : ℤˣ` to a word `w` with sufficient
 hypotheses that no normalization or cancellation need take place for the result to be in normal form
diff --git a/Mathlib/GroupTheory/PushoutI.lean b/Mathlib/GroupTheory/PushoutI.lean
index ab561721ed4f6..c94f6ce8a0ca7 100644
--- a/Mathlib/GroupTheory/PushoutI.lean
+++ b/Mathlib/GroupTheory/PushoutI.lean
@@ -574,10 +574,10 @@ instance : FaithfulSMul (PushoutI φ) (NormalWord d) :=
   ⟨fun h => by simpa using congr_arg prod (h empty)⟩
 
 instance (i : ι) : FaithfulSMul (G i) (NormalWord d) :=
-  ⟨by simp [summand_smul_def']⟩
+  ⟨by simp [summand_smul_def', forall_const]⟩
 
 instance : FaithfulSMul H (NormalWord d) :=
-  ⟨by simp [base_smul_def']⟩
+  ⟨by simp [base_smul_def', forall_const]⟩
 
 end NormalWord
 
diff --git a/Mathlib/ModelTheory/Algebra/Field/Basic.lean b/Mathlib/ModelTheory/Algebra/Field/Basic.lean
index dba9790f9c93a..b5c346bb1525a 100644
--- a/Mathlib/ModelTheory/Algebra/Field/Basic.lean
+++ b/Mathlib/ModelTheory/Algebra/Field/Basic.lean
@@ -83,7 +83,7 @@ theorem FieldAxiom.realize_toSentence_iff_toProp {K : Type*}
     (ax : FieldAxiom) :
     (K ⊨ (ax.toSentence : Sentence Language.ring)) ↔ ax.toProp K := by
   cases ax <;>
-  simp [Sentence.Realize, Formula.Realize, Fin.snoc]
+  simp [Sentence.Realize, Formula.Realize, Fin.snoc, forall_const]
 
 theorem FieldAxiom.toProp_of_model {K : Type*}
     [Add K] [Mul K] [Neg K] [Zero K] [One K] [CompatibleRing K]
diff --git a/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean b/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
index 6ade04820260d..decdc706ce706 100644
--- a/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
+++ b/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
@@ -245,7 +245,7 @@ instance : EuclideanDomain ℤ[i] :=
     GaussianInt.instNontrivial with
     quotient := (· / ·)
     remainder := (· % ·)
-    quotient_zero := by simp [div_def]; rfl
+    quotient_zero := fun _ => by simp [div_def]; rfl
     quotient_mul_add_remainder_eq := fun _ _ => by simp [mod_def]
     r := _
     r_wellFounded := (measure (Int.natAbs ∘ norm)).wf
diff --git a/Mathlib/Order/Filter/Ultrafilter.lean b/Mathlib/Order/Filter/Ultrafilter.lean
index 3d1ae9a87f5fc..b34032253c955 100644
--- a/Mathlib/Order/Filter/Ultrafilter.lean
+++ b/Mathlib/Order/Filter/Ultrafilter.lean
@@ -118,7 +118,7 @@ theorem diff_mem_iff (f : Ultrafilter α) : s \ t ∈ f ↔ s ∈ f ∧ t ∉ f
 `Ultrafilter.compl_not_mem_iff`. -/
 def ofComplNotMemIff (f : Filter α) (h : ∀ s, sᶜ ∉ f ↔ s ∈ f) : Ultrafilter α where
   toFilter := f
-  neBot' := ⟨fun hf => by simp [hf] at h⟩
+  neBot' := ⟨fun hf => by simp [hf, forall_const] at h⟩
   le_of_le g hg hgf s hs := (h s).1 fun hsc => compl_not_mem hs (hgf hsc)
 
 /-- If `f : Filter α` is an atom, then it is an ultrafilter. -/
diff --git a/Mathlib/Order/OmegaCompletePartialOrder.lean b/Mathlib/Order/OmegaCompletePartialOrder.lean
index 911cd139607e1..dcda735f2eed4 100644
--- a/Mathlib/Order/OmegaCompletePartialOrder.lean
+++ b/Mathlib/Order/OmegaCompletePartialOrder.lean
@@ -363,7 +363,9 @@ theorem id_continuous' : Continuous' (@id α) :=
 
 @[deprecated ωScottContinuous.const (since := "2024-05-29")]
 theorem continuous_const (x : β) : Continuous (OrderHom.const α x) := fun c =>
-  eq_of_forall_ge_iff fun z => by rw [ωSup_le_iff, Chain.map_coe, OrderHom.const_coe_coe]; simp
+  eq_of_forall_ge_iff fun z => by
+    rw [ωSup_le_iff, Chain.map_coe, OrderHom.const_coe_coe]
+    simp [forall_const]
 
 @[deprecated ωScottContinuous.const (since := "2024-05-29")]
 theorem const_continuous' (x : β) : Continuous' (Function.const α x) :=
@@ -567,7 +569,7 @@ lemma ωScottContinuous.sup (hf : ωScottContinuous f) (hg : ωScottContinuous g
 
 lemma ωScottContinuous.top : ωScottContinuous (⊤ : α → β) :=
   ωScottContinuous.of_monotone_map_ωSup
-    ⟨monotone_const, fun c ↦ eq_of_forall_ge_iff fun a ↦ by simp⟩
+    ⟨monotone_const, fun c ↦ eq_of_forall_ge_iff fun a ↦ by simp [forall_const]⟩
 
 lemma ωScottContinuous.bot : ωScottContinuous (⊥ : α → β) := by
   rw [← sSup_empty]; exact ωScottContinuous.sSup (by simp)
diff --git a/Mathlib/SetTheory/Game/Impartial.lean b/Mathlib/SetTheory/Game/Impartial.lean
index fea623654ef44..d1b3b3e05b150 100644
--- a/Mathlib/SetTheory/Game/Impartial.lean
+++ b/Mathlib/SetTheory/Game/Impartial.lean
@@ -52,7 +52,7 @@ instance impartial_zero : Impartial 0 := by
 
 instance impartial_star : Impartial star := by
   rw [impartial_def]
-  simpa using Impartial.impartial_zero
+  simpa [forall_const] using Impartial.impartial_zero
 
 theorem neg_equiv_self (G : PGame) [h : G.Impartial] : G ≈ -G :=
   (impartial_def.1 h).1
diff --git a/Mathlib/SetTheory/Surreal/Dyadic.lean b/Mathlib/SetTheory/Surreal/Dyadic.lean
index f47d76361786e..e2ec14b15ad2d 100644
--- a/Mathlib/SetTheory/Surreal/Dyadic.lean
+++ b/Mathlib/SetTheory/Surreal/Dyadic.lean
@@ -79,7 +79,7 @@ theorem numeric_powHalf (n) : (powHalf n).Numeric := by
   | zero => exact numeric_one
   | succ n hn =>
     constructor
-    · simpa using hn.moveLeft_lt default
+    · intros; simpa using hn.moveLeft_lt default
     · exact ⟨fun _ => numeric_zero, fun _ => hn⟩
 
 theorem powHalf_succ_lt_powHalf (n : ℕ) : powHalf (n + 1) < powHalf n :=
diff --git a/Mathlib/Topology/Algebra/Group/Basic.lean b/Mathlib/Topology/Algebra/Group/Basic.lean
index ad1294ce4d9e6..1b23a76935427 100644
--- a/Mathlib/Topology/Algebra/Group/Basic.lean
+++ b/Mathlib/Topology/Algebra/Group/Basic.lean
@@ -817,7 +817,7 @@ theorem TopologicalGroup.of_comm_of_nhds_one {G : Type u} [CommGroup G] [Topolog
     (hmul : Tendsto (uncurry ((· * ·) : G → G → G)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
     (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1))
     (hleft : ∀ x₀ : G, 𝓝 x₀ = map (x₀ * ·) (𝓝 1)) : TopologicalGroup G :=
-  TopologicalGroup.of_nhds_one hmul hinv hleft (by simpa using tendsto_id)
+  TopologicalGroup.of_nhds_one hmul hinv hleft (fun _ => by simpa using tendsto_id)
 
 variable (G) in
 /-- Any first countable topological group has an antitone neighborhood basis `u : ℕ → Set G` for