Merge remote-tracking branch 'upstream/master' into bump/v4.32.0

Author: mathlib4-bot

Archive/Examples/IfNormalization/Result.lean

@@ -24,9 +24,6 @@ We add some local simp lemmas so we can unfold the definitions of the normalizat
 attribute [local simp] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
   List.disjoint
 
-set_option warning.simp.varHead false in
-attribute [local simp] apply_ite ite_eq_iff'
-
 variable {b : Bool} {f : ℕ → Bool} {i : ℕ} {t e : IfExpr}
 
 /-!
@@ -74,7 +71,7 @@ def normalize (l : AList (fun _ : ℕ => Bool)) :
       ⟨if t' = e' then t' else .ite (var v) t' e', by
         refine ⟨fun f => ?_, ?_, fun w b => ?_⟩
         · -- eval = eval
-          simp? says simp only [apply_ite, eval_ite_var, ite_eq_iff']
+          simp only [apply_ite, eval_ite_var, ite_eq_iff']
           cases hfv : f v
           · simp_all
             congr

Archive/Imo/Imo2024Q6.lean

@@ -55,8 +55,6 @@ lemma Aquaesulian.injective : Function.Injective f := by
   · exact (h.eq_of_apply_eq_inl he.symm hc).symm
   · exact h.eq_of_apply_eq_inl he hc
 
-set_option warning.simp.varHead false in
-@[simp]
 lemma Aquaesulian.apply_zero : f 0 = 0 := by
   refine h.injective ?_
   convert! h.apply_apply_add 0 using 1 <;> simp
@@ -69,14 +67,12 @@ lemma Aquaesulian.apply_neg_apply_add (x : G) : f (-(f x)) + x = 0 := by
   · rw [add_neg_cancel, h.apply_zero] at hc
     exact hc.symm
 
-set_option warning.simp.varHead false in
-@[simp]
 lemma Aquaesulian.apply_neg_apply (x : G) : f (-(f x)) = -x := by
   rw [← add_eq_zero_iff_eq_neg]
   exact h.apply_neg_apply_add x
 
 lemma Aquaesulian.apply_neg_apply_neg (x : G) : f (-(f (-x))) = x := by
-  simp [h]
+  simp [h.apply_neg_apply]
 
 lemma Aquaesulian.apply_neg_of_apply_eq {x₁ x₂ : G} (hx : f x₁ = x₂) : f (-x₂) = -x₁ := by
   rw [← hx]

Mathlib/Algebra/CharP/Two.lean

@@ -64,9 +64,8 @@ theorem natCast_cases (n : ℕ) : (n : R) = 0 ∨ (n : R) = 1 :=
 theorem natCast_eq_mod (n : ℕ) : (n : R) = (n % 2 : ℕ) := by
   simp [natCast_eq_ite, Nat.even_iff]
 
-set_option warning.simp.varHead false in
 @[scoped simp]
-theorem ofNat_eq_mod (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R) = (ofNat(n) % 2 : ℕ) :=
+theorem ofNat_eq_mod (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n : R) = (ofNat(n) % 2 : ℕ) :=
   natCast_eq_mod n
 
 example : (37 : R) = 1 := by simp

Mathlib/Algebra/Group/Subgroup/Ker.lean

@@ -262,20 +262,6 @@ theorem comap_ker {P : Type*} [MulOneClass P] (g : N →* P) (f : G →* N) :
     g.ker.comap f = (g.comp f).ker :=
   rfl
 
-/-- The kernel of a homomorphism composed with an isomorphism is equal to the kernel of
-the homomorphism mapped by the inverse isomorphism. -/
-@[to_additive (attr := simp)]
-lemma ker_comp_mulEquiv {P : Type*} [MulOneClass P] (g : N →* P) (iso : G ≃* N) :
-    (g.comp iso).ker = map (iso.symm : N →* G) g.ker := by
-  rw [← comap_ker, comap_equiv_eq_map_symm]
-
-/-- Composing with an isomorphism on the codomain does not change the kernel. -/
-@[to_additive (attr := simp)]
-lemma ker_mulEquiv_comp {P : Type*} [MulOneClass P] (f : G →* N) (iso : N ≃* P) :
-    ((iso : N →* P).comp f).ker = f.ker := by
-  ext
-  simp
-
 @[to_additive (attr := simp)]
 theorem comap_bot (f : G →* N) : (⊥ : Subgroup N).comap f = f.ker :=
   rfl
@@ -312,13 +298,36 @@ theorem ker_eq_bot_iff (f : G →* M) : f.ker = ⊥ ↔ Function.Injective f :=
   ⟨fun h x y hxy => by rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy, fun h =>
     bot_unique fun _ hx => h (hx.trans f.map_one.symm)⟩
 
+@[to_additive]
+theorem ker_eq_bot (f : G →* M) (hf : Function.Injective f) : f.ker = ⊥ :=
+  f.ker_eq_bot_iff.mpr hf
+
+/-- The kernel of a homomorphism composed with an isomorphism is equal to the kernel of
+the homomorphism mapped by the inverse isomorphism. -/
+@[to_additive (attr := simp)]
+lemma ker_comp_mulEquiv {P : Type*} [MulOneClass P] (g : N →* P) (iso : G ≃* N) :
+    (g.comp iso).ker = map (iso.symm : N →* G) g.ker := by
+  rw [← comap_ker, comap_equiv_eq_map_symm]
+
+/-- Composing with an injective homomorphism on the codomain does not change the kernel. -/
+@[to_additive]
+lemma ker_comp_of_injective {P : Type*} [MulOneClass P] (f : G →* N) (g : N →* P)
+    (hg : Function.Injective g) : (g.comp f).ker = f.ker := by
+  rw [← comap_ker, g.ker_eq_bot hg, comap_bot]
+
+/-- Composing with an isomorphism on the codomain does not change the kernel. -/
+@[to_additive (attr := simp)]
+lemma ker_mulEquiv_comp {P : Type*} [MulOneClass P] (f : G →* N) (iso : N ≃* P) :
+    ((iso : N →* P).comp f).ker = f.ker :=
+  ker_comp_of_injective f iso.toMonoidHom iso.injective
+
 @[to_additive (attr := simp)]
 theorem _root_.Subgroup.ker_subtype (H : Subgroup G) : H.subtype.ker = ⊥ :=
-  H.subtype.ker_eq_bot_iff.mpr Subtype.coe_injective
+  H.subtype.ker_eq_bot Subtype.coe_injective
 
 @[to_additive (attr := simp)]
 theorem _root_.Subgroup.ker_inclusion {H K : Subgroup G} (h : H ≤ K) : (inclusion h).ker = ⊥ :=
-  (inclusion h).ker_eq_bot_iff.mpr (Set.inclusion_injective h)
+  (inclusion h).ker_eq_bot (Set.inclusion_injective h)
 
 @[to_additive ker_prod]
 theorem ker_prod {M N : Type*} [MulOneClass M] [MulOneClass N] (f : G →* M) (g : G →* N) :
@@ -386,7 +395,7 @@ theorem map_eq_bot_iff {f : G →* N} : H.map f = ⊥ ↔ H ≤ f.ker :=
 
 @[to_additive]
 theorem map_eq_bot_iff_of_injective {f : G →* N} (hf : Function.Injective f) :
-    H.map f = ⊥ ↔ H = ⊥ := by rw [map_eq_bot_iff, f.ker_eq_bot_iff.mpr hf, le_bot_iff]
+    H.map f = ⊥ ↔ H = ⊥ := by rw [map_eq_bot_iff, f.ker_eq_bot hf, le_bot_iff]
 
 open MonoidHom
 
@@ -453,7 +462,7 @@ theorem comap_map_eq_self {f : G →* N} {H : Subgroup G} (h : f.ker ≤ H) :
 @[to_additive]
 theorem comap_map_eq_self_of_injective {f : G →* N} (h : Function.Injective f) (H : Subgroup G) :
     comap f (map f H) = H :=
-  comap_map_eq_self (((ker_eq_bot_iff _).mpr h).symm ▸ bot_le)
+  comap_map_eq_self ((ker_eq_bot _ h).symm ▸ bot_le)
 
 @[to_additive]
 theorem map_le_map_iff {f : G →* N} {H K : Subgroup G} : H.map f ≤ K.map f ↔ H ≤ K ⊔ f.ker := by

Mathlib/AlgebraicGeometry/Modules/Tilde.lean

@@ -121,12 +121,12 @@ lemma isSMulRegular_of_le_basicOpen {f : R} (hle : U ≤ PrimeSpectrum.basicOpen
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
-lemma Scheme.Modules.restrictAppIso_smul_Spec {S : CommRingCat.{u}} (f : R ⟶ S)
+lemma restrictAppIso_smul_Spec {S : CommRingCat.{u}} (f : R ⟶ S)
     [IsOpenImmersion (Spec.map f)] {U : (Spec S).Opens} (r : R)
     (x : Γ(M.restrict (Spec.map f), U)) :
     dsimp% (M.restrictAppIso (Spec.map f) U).hom (f r • x) =
       r • (M.restrictAppIso (Spec.map f) U).hom x := by
-  rw [Scheme.Modules.smul_Spec_def, Scheme.Modules.smul_Spec_def]
+  rw [smul_Spec_def, smul_Spec_def]
   simp_rw [smul_restrictAppIso_hom_apply, ← ConcreteCategory.comp_apply, Category.assoc]
   have :
       f ≫ (ΓSpecIso S).inv ≫ (Spec S).presheaf.map U.leTop.op ≫ (Hom.appIso (Spec.map f) U).inv =
@@ -135,6 +135,10 @@ lemma Scheme.Modules.restrictAppIso_smul_Spec {S : CommRingCat.{u}} (f : R ⟶ S
     rfl
   rw [this]
 
+set_option linter.dupNamespace false in
+@[deprecated (since := "2026-06-04")]
+alias Scheme.Modules.restrictAppIso_smul_Spec := restrictAppIso_smul_Spec
+
 end Scheme.Modules
 
 /--

Mathlib/Analysis/Analytic/Composition.lean

@@ -850,31 +850,26 @@ lemma AnalyticOn.comp {f : F → G} {g : E → F} {s : Set F}
     AnalyticOn 𝕜 (f ∘ g) t :=
   fun x m ↦ (hf _ (h m)).comp (hg x m) h
 
+-- Allow `to_fun` to eta-expand `g ∘ f`. Ideally, `Function.comp_def` would be a global pull lemma
+-- instead, which is not supported yet: see https://github.com/leanprover-community/mathlib4/issues/40183.
+attribute [local push ←] Function.comp_def
 /-- If two functions `g` and `f` are analytic respectively at `f x` and `x`, then `g ∘ f` is
 analytic at `x`. -/
-@[fun_prop]
+@[to_fun (attr := fun_prop)]
 theorem AnalyticAt.comp {g : F → G} {f : E → F} {x : E} (hg : AnalyticAt 𝕜 g (f x))
     (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (g ∘ f) x := by
   rw [← analyticWithinAt_univ] at hg hf ⊢
   apply hg.comp hf (by simp)
 
-/-- If two functions `g` and `f` are analytic respectively at `f x` and `x`, then `g ∘ f` is
-analytic at `x`. -/
-@[fun_prop]
-theorem AnalyticAt.comp' {g : F → G} {f : E → F} {x : E} (hg : AnalyticAt 𝕜 g (f x))
-    (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (fun z ↦ g (f z)) x :=
-  hg.comp hf
+@[deprecated (since := "2026-01-24")] alias AnalyticAt.comp' := AnalyticAt.fun_comp
 
 /-- Version of `AnalyticAt.comp` where point equality is a separate hypothesis. -/
+@[to_fun]
 theorem AnalyticAt.comp_of_eq {g : F → G} {f : E → F} {y : F} {x : E} (hg : AnalyticAt 𝕜 g y)
     (hf : AnalyticAt 𝕜 f x) (hy : f x = y) : AnalyticAt 𝕜 (g ∘ f) x := by
   rw [← hy] at hg
   exact hg.comp hf
-
-/-- Version of `AnalyticAt.comp` where point equality is a separate hypothesis. -/
-theorem AnalyticAt.comp_of_eq' {g : F → G} {f : E → F} {y : F} {x : E} (hg : AnalyticAt 𝕜 g y)
-    (hf : AnalyticAt 𝕜 f x) (hy : f x = y) : AnalyticAt 𝕜 (fun z ↦ g (f z)) x := by
-  apply hg.comp_of_eq hf hy
+@[deprecated (since := "2026-05-18")] alias AnalyticAt.comp_of_eq' := AnalyticAt.fun_comp_of_eq
 
 theorem AnalyticAt.comp_analyticWithinAt {g : F → G} {f : E → F} {x : E} {s : Set E}
     (hg : AnalyticAt 𝕜 g (f x)) (hf : AnalyticWithinAt 𝕜 f s x) :
@@ -939,6 +934,7 @@ theorem HasFiniteFPowerSeriesAt.comp {m n : ℕ} {g : F → G} {f : E → F}
 
 /-- If two functions `g` and `f` are continuously polynomial respectively at `f x` and `x`,
 then `g ∘ f` is continuously polynomial at `x`. -/
+@[to_fun]
 theorem CPolynomialAt.comp {g : F → G} {f : E → F} {x : E}
     (hg : CPolynomialAt 𝕜 g (f x)) (hf : CPolynomialAt 𝕜 f x) :
     CPolynomialAt 𝕜 (g ∘ f) x := by
@@ -947,25 +943,13 @@ theorem CPolynomialAt.comp {g : F → G} {f : E → F} {x : E}
   refine ⟨q.comp p, m * (n + 1), ?_⟩
   exact hm.comp (hn.of_le (Nat.le_succ n)) (Nat.zero_lt_succ n)
 
-/-- If two functions `g` and `f` are continuously polynomial respectively at `f x` and `x`,
-then `g ∘ f` is continuously polynomial at `x`. -/
-theorem CPolynomialAt.fun_comp {g : F → G} {f : E → F} {x : E}
-    (hg : CPolynomialAt 𝕜 g (f x)) (hf : CPolynomialAt 𝕜 f x) :
-    CPolynomialAt 𝕜 (fun z ↦ g (f z)) x :=
-  hg.comp hf
-
 /-- Version of `CPolynomialAt.comp` where point equality is a separate hypothesis. -/
+@[to_fun]
 theorem CPolynomialAt.comp_of_eq {g : F → G} {f : E → F} {y : F} {x : E} (hg : CPolynomialAt 𝕜 g y)
     (hf : CPolynomialAt 𝕜 f x) (hy : f x = y) : CPolynomialAt 𝕜 (g ∘ f) x := by
   rw [← hy] at hg
   exact hg.comp hf
 
-/-- Version of `CPolynomialAt.comp` where point equality is a separate hypothesis. -/
-theorem CPolynomialAt.fun_comp_of_eq {g : F → G} {f : E → F} {y : F} {x : E}
-    (hg : CPolynomialAt 𝕜 g y) (hf : CPolynomialAt 𝕜 f x) (hy : f x = y) :
-    CPolynomialAt 𝕜 (fun z ↦ g (f z)) x :=
-  hg.comp_of_eq hf hy
-
 /-- If two functions `g` and `f` are continuously polynomial respectively on `s.image f` and `s`,
 then `g ∘ f` is continuously polynomial on `s`. -/
 theorem CPolynomialOn.comp' {s : Set E} {g : F → G} {f : E → F} (hg : CPolynomialOn 𝕜 g (s.image f))

Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean

@@ -250,7 +250,7 @@ theorem extDerivWithin_pullback {ω : F → F [⋀^Fin n]→L[𝕜] G} {f : E 
   rw [extDerivWithin,
     fderivWithin_continuousAlternatingMapCompContinuousLinearMap (by exact hω.comp x hdf hst) hd2f
       (hs x hxs),
-    alternatizeUncurryFin_add, fderivWithin_comp' _ hω hdf hst (hs x hxs), extDerivWithin,
+    alternatizeUncurryFin_add, fderivWithin_fun_comp _ hω hdf hst (hs x hxs), extDerivWithin,
     alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero, add_zero]
   · ext v
     simp +unfoldPartialApp [alternatizeUncurryFin_apply, Fin.removeNth, Function.comp_def]

Mathlib/Analysis/Calculus/FDeriv/Comp.lean

@@ -133,31 +133,24 @@ theorem DifferentiableAt.comp_differentiableWithinAt {g : F → G} (hg : Differe
     (hf : DifferentiableWithinAt 𝕜 f s x) : DifferentiableWithinAt 𝕜 (g ∘ f) s x :=
   hg.differentiableWithinAt.comp x hf (mapsTo_univ _ _)
 
+-- Allow `to_fun` to eta-expand `g ∘ f`. Ideally, `Function.comp_def` would be a global pull lemma
+-- instead, which is not supported yet: see https://github.com/leanprover-community/mathlib4/issues/40183.
+attribute [local push ←] Function.comp_def
+@[to_fun fderivWithin_fun_comp]
 theorem fderivWithin_comp {g : F → G} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x))
     (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) :
     fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x) :=
   (hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h).fderivWithin hxs
 
+@[to_fun fderivWithin_fun_comp_of_eq]
 theorem fderivWithin_comp_of_eq {g : F → G} {t : Set F} {y : F}
     (hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t)
     (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) :
     fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x) := by
   subst hy; exact fderivWithin_comp _ hg hf h hxs
 
-/-- A variant for the derivative of a composition, written without `∘`. -/
-theorem fderivWithin_comp' {g : F → G} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x))
-    (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) :
-    fderivWithin 𝕜 (fun y ↦ g (f y)) s x
-      = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x) :=
-  fderivWithin_comp _ hg hf h hxs
-
-/-- A variant for the derivative of a composition, written without `∘`. -/
-theorem fderivWithin_comp_of_eq' {g : F → G} {t : Set F} {y : F}
-    (hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t)
-    (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) :
-    fderivWithin 𝕜 (fun y ↦ g (f y)) s x
-      = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x) := by
-  subst hy; exact fderivWithin_comp _ hg hf h hxs
+@[deprecated (since := "2026-05-18")] alias fderivWithin_comp' := fderivWithin_fun_comp
+@[deprecated (since := "2026-05-18")] alias fderivWithin_comp_of_eq' := fderivWithin_fun_comp_of_eq
 
 /-- A version of `fderivWithin_comp` that is useful to rewrite the composition of two derivatives
   into a single derivative. This version always applies, but creates a new side-goal `f x = y`. -/
@@ -180,14 +173,11 @@ theorem fderivWithin_comp₃ {g' : G → G'} {g : F → G} {t : Set F} {u : Set
   exact (hg'.hasFDerivWithinAt.comp x (hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h2f) <|
     h2g.comp h2f).fderivWithin hxs
 
+@[to_fun fderiv_fun_comp]
 theorem fderiv_comp {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableAt 𝕜 f x) :
     fderiv 𝕜 (g ∘ f) x = (fderiv 𝕜 g (f x)).comp (fderiv 𝕜 f x) :=
   (hg.hasFDerivAt.comp x hf.hasFDerivAt).fderiv
-
-/-- A variant for the derivative of a composition, written without `∘`. -/
-theorem fderiv_comp' {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableAt 𝕜 f x) :
-    fderiv 𝕜 (fun y ↦ g (f y)) x = (fderiv 𝕜 g (f x)).comp (fderiv 𝕜 f x) :=
-  fderiv_comp x hg hf
+@[deprecated (since := "2026-05-18")] alias fderiv_comp' := fderiv_fun_comp
 
 theorem fderiv_comp_fderivWithin {g : F → G} (hg : DifferentiableAt 𝕜 g (f x))
     (hf : DifferentiableWithinAt 𝕜 f s x) (hxs : UniqueDiffWithinAt 𝕜 s x) :

Mathlib/Analysis/Calculus/VectorField.lean

@@ -636,8 +636,8 @@ lemma pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt
   have Af : DifferentiableWithinAt 𝕜 f s x := h'f.differentiableWithinAt two_ne_zero
   simp only [lieBracketWithin_eq, pullbackWithin_eq_of_fderivWithin_eq hMx, map_sub, AV, AW]
   rw [fderivWithin_clm_apply, fderivWithin_clm_apply]
-  · simp [fderivWithin_comp' x hW Af hst (hu x hx), ← hMx,
-      fderivWithin_comp' x hV Af hst (hu x hx), M_diff, hf.eq]
+  · simp [fderivWithin_fun_comp x hW Af hst (hu x hx), ← hMx,
+      fderivWithin_fun_comp x hV Af hst (hu x hx), M_diff, hf.eq]
   · exact hu x hx
   · exact M_symm_smooth.differentiableWithinAt one_ne_zero
   · exact hV.comp x Af hst

Mathlib/Analysis/MeanInequalities.lean

@@ -1012,9 +1012,10 @@ lemma inner_le_weight_mul_Lp_of_nonneg (s : Finset ι) {p : ℝ} (hp : 1 ≤ p)
   have := coe_le_coe.2 <| NNReal.inner_le_weight_mul_Lp s hp.le (fun i ↦ ENNReal.toNNReal (w i))
     fun i ↦ ENNReal.toNNReal (f i)
   rw [coe_mul] at this
-  simp_rw [coe_rpow_of_nonneg _ <| inv_nonneg.2 hp₀.le, coe_finsetSum, ← ENNReal.toNNReal_rpow,
+  simp_rw [coe_rpow_of_nonneg _ <| inv_nonneg.2 hp₀.le, ofNNReal_finsetSum, ← ENNReal.toNNReal_rpow,
     ← ENNReal.toNNReal_mul, sum_congr rfl fun i hi ↦ coe_toNNReal (H'.2 i hi)] at this
-  simp only [toNNReal_mul, coe_mul, sub_nonneg, hp₁.le, coe_rpow_of_nonneg, coe_finsetSum] at this
+  simp only [toNNReal_mul, coe_mul, sub_nonneg, hp₁.le, coe_rpow_of_nonneg, ofNNReal_finsetSum]
+    at this
   convert! this using 2 with i hi
   · obtain hw | hw := eq_or_ne (w i) 0
     · simp [hw]