chore: backports for leanprover/lean4#4814 (part 33) (#15605)

Mathlib/Algebra/Homology/DerivedCategory/Ext.lean

@@ -238,18 +238,7 @@ lemma mk₀_zero : mk₀ (0 : X ⟶ Y) = 0 := by
 
 section
 
-variable [HasDerivedCategory.{w'} C]
-
-variable (X Y n) in
-@[simp]
-lemma zero_hom : (0 : Ext X Y n).hom = 0 := by
-  let β : Ext 0 Y n := 0
-  have hβ : β.hom = 0 := by apply (Functor.map_isZero _ (isZero_zero C)).eq_of_src
-  have : (0 : Ext X Y n) = (0 : Ext X 0 0).comp β (zero_add n) := by simp [β]
-  rw [this, comp_hom, hβ, ShiftedHom.comp_zero]
-
-attribute [local instance] preservesBinaryBiproductsOfPreservesBiproducts
-
+attribute [local instance] preservesBinaryBiproductsOfPreservesBiproducts in
 lemma biprod_ext {X₁ X₂ : C} {α β : Ext (X₁ ⊞ X₂) Y n}
     (h₁ : (mk₀ biprod.inl).comp α (zero_add n) = (mk₀ biprod.inl).comp β (zero_add n))
     (h₂ : (mk₀ biprod.inr).comp α (zero_add n) = (mk₀ biprod.inr).comp β (zero_add n)) :
@@ -262,6 +251,16 @@ lemma biprod_ext {X₁ X₂ : C} {α β : Ext (X₁ ⊞ X₂) Y n}
       (BinaryBiproduct.isBilimit X₁ X₂)).isColimit
   all_goals assumption
 
+variable [HasDerivedCategory.{w'} C]
+
+variable (X Y n) in
+@[simp]
+lemma zero_hom : (0 : Ext X Y n).hom = 0 := by
+  let β : Ext 0 Y n := 0
+  have hβ : β.hom = 0 := by apply (Functor.map_isZero _ (isZero_zero C)).eq_of_src
+  have : (0 : Ext X Y n) = (0 : Ext X 0 0).comp β (zero_add n) := by simp [β]
+  rw [this, comp_hom, hβ, ShiftedHom.comp_zero]
+
 @[simp]
 lemma add_hom (α β : Ext X Y n) : (α + β).hom = α.hom + β.hom := by
   let α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α (zero_add n)

Mathlib/Algebra/Lie/CartanExists.lean

@@ -32,7 +32,7 @@ namespace LieAlgebra
 section CommRing
 
 variable {K R L M : Type*}
-variable [Field K] [CommRing R] [Nontrivial R]
+variable [Field K] [CommRing R]
 variable [LieRing L] [LieAlgebra K L] [LieAlgebra R L]
 variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
 variable [Module.Finite K L]
@@ -83,7 +83,7 @@ def lieCharpoly : Polynomial R[X] :=
 lemma lieCharpoly_monic : (lieCharpoly R M x y).Monic :=
   (polyCharpoly_monic _ _).map _
 
-lemma lieCharpoly_natDegree : (lieCharpoly R M x y).natDegree = finrank R M := by
+lemma lieCharpoly_natDegree [Nontrivial R] : (lieCharpoly R M x y).natDegree = finrank R M := by
   rw [lieCharpoly, (polyCharpoly_monic _ _).natDegree_map, polyCharpoly_natDegree]
 
 variable {R} in
@@ -97,7 +97,7 @@ lemma lieCharpoly_map_eval (r : R) :
     map_add, map_mul, aeval_C, Algebra.id.map_eq_id, RingHom.id_apply, aeval_X, aux,
     MvPolynomial.coe_aeval_eq_eval, polyCharpoly_map_eq_charpoly, LieHom.coe_toLinearMap]
 
-lemma lieCharpoly_coeff_natDegree (i j : ℕ) (hij : i + j = finrank R M) :
+lemma lieCharpoly_coeff_natDegree [Nontrivial R] (i j : ℕ) (hij : i + j = finrank R M) :
     ((lieCharpoly R M x y).coeff i).natDegree ≤ j := by
   classical
   rw [← mul_one j, lieCharpoly, coeff_map]

Mathlib/Algebra/Lie/Killing.lean

@@ -54,7 +54,7 @@ attribute [simp] IsKilling.killingCompl_top_eq_bot
 
 namespace IsKilling
 
-variable [Module.Free R L] [Module.Finite R L] [IsKilling R L]
+variable [IsKilling R L]
 
 @[simp] lemma ker_killingForm_eq_bot :
     LinearMap.ker (killingForm R L) = ⊥ := by
@@ -65,7 +65,8 @@ lemma killingForm_nondegenerate :
   simp [LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot]
 
 variable {R L} in
-lemma ideal_eq_bot_of_isLieAbelian [IsDomain R] [IsPrincipalIdealRing R]
+lemma ideal_eq_bot_of_isLieAbelian
+    [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R]
     (I : LieIdeal R L) [IsLieAbelian I] : I = ⊥ := by
   rw [eq_bot_iff, ← killingCompl_top_eq_bot]
   exact I.le_killingCompl_top_of_isLieAbelian
@@ -83,7 +84,9 @@ over fields with positive characteristic.
 
 Note that when the coefficients are a field this instance is redundant since we have
 `LieAlgebra.IsKilling.instSemisimple` and `LieAlgebra.IsSemisimple.instHasTrivialRadical`. -/
-instance instHasTrivialRadical [IsDomain R] [IsPrincipalIdealRing R] : HasTrivialRadical R L :=
+instance instHasTrivialRadical
+    [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] :
+    HasTrivialRadical R L :=
   (hasTrivialRadical_iff_no_abelian_ideals R L).mpr IsKilling.ideal_eq_bot_of_isLieAbelian
 
 end IsKilling

Mathlib/Algebra/Lie/Weights/Linear.lean

@@ -55,8 +55,7 @@ class LinearWeights [LieAlgebra.IsNilpotent R L] : Prop :=
 
 namespace Weight
 
-variable [LieAlgebra.IsNilpotent R L] [LinearWeights R L M]
-    [NoZeroSMulDivisors R M] [IsNoetherian R M] (χ : Weight R L M)
+variable [LieAlgebra.IsNilpotent R L] [LinearWeights R L M] (χ : Weight R L M)
 
 /-- A weight of a Lie module, bundled as a linear map. -/
 @[simps]
@@ -155,7 +154,7 @@ instance instLinearWeightsOfCharZero [CharZero R] :
 
 end FiniteDimensional
 
-variable [LieAlgebra.IsNilpotent R L] [LinearWeights R L M] (χ : L → R)
+variable [LieAlgebra.IsNilpotent R L] (χ : L → R)
 
 /-- A type synonym for the `χ`-weight space but with the action of `x : L` on `m : weightSpace M χ`,
 shifted to act as `⁅x, m⁆ - χ x • m`. -/
@@ -166,6 +165,8 @@ namespace shiftedWeightSpace
 private lemma aux [h : Nontrivial (shiftedWeightSpace R L M χ)] : weightSpace M χ ≠ ⊥ :=
   (LieSubmodule.nontrivial_iff_ne_bot _ _ _).mp h
 
+variable [LinearWeights R L M]
+
 instance : LieRingModule L (shiftedWeightSpace R L M χ) where
   bracket x m := ⁅x, m⁆ - χ x • m
   add_lie x y m := by
@@ -217,7 +218,7 @@ end shiftedWeightSpace
 /-- Given a Lie module `M` of a Lie algebra `L` with coefficients in `R`, if a function `χ : L → R`
 has a simultaneous generalized eigenvector for the action of `L` then it has a simultaneous true
 eigenvector, provided `M` is Noetherian and has linear weights. -/
-lemma exists_forall_lie_eq_smul [IsNoetherian R M] (χ : Weight R L M) :
+lemma exists_forall_lie_eq_smul [LinearWeights R L M] [IsNoetherian R M] (χ : Weight R L M) :
     ∃ m : M, m ≠ 0 ∧ ∀ x : L, ⁅x, m⁆ = χ x • m := by
   replace hχ : Nontrivial (shiftedWeightSpace R L M χ) :=
     (LieSubmodule.nontrivial_iff_ne_bot R L M).mpr χ.weightSpace_ne_bot

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unitary.lean

@@ -20,7 +20,7 @@ section Generic
 
 variable {R A : Type*} {p : A → Prop} [CommRing R] [StarRing R] [MetricSpace R]
 variable [TopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A]
-variable [Algebra R A] [StarModule R A] [ContinuousFunctionalCalculus R p]
+variable [Algebra R A] [ContinuousFunctionalCalculus R p]
 
 lemma cfc_unitary_iff (f : R → R) (a : A) (ha : p a := by cfc_tac)
     (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) :
@@ -35,7 +35,7 @@ end Generic
 section Complex
 
 variable {A : Type*} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A]
-  [StarModule ℂ A] [ContinuousFunctionalCalculus ℂ (IsStarNormal : A → Prop)]
+  [ContinuousFunctionalCalculus ℂ (IsStarNormal : A → Prop)]
 
 lemma unitary_iff_isStarNormal_and_spectrum_subset_unitary {u : A} :
     u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ unitary ℂ := by

Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

@@ -787,8 +787,7 @@ that the differentiability set `D` is measurable. -/
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace E]
   {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
-  {α : Type*} [TopologicalSpace α] [MeasurableSpace α] [MeasurableSpace E]
-  [OpensMeasurableSpace α] [OpensMeasurableSpace E]
+  {α : Type*} [TopologicalSpace α]
   {f : α → E → F} (K : Set (E →L[𝕜] F))
 
 namespace FDerivMeasurableAux
@@ -873,6 +872,8 @@ end FDerivMeasurableAux
 
 open FDerivMeasurableAux
 
+variable [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace E] [OpensMeasurableSpace E]
+
 theorem measurableSet_of_differentiableAt_of_isComplete_with_param
     (hf : Continuous f.uncurry) {K : Set (E →L[𝕜] F)} (hK : IsComplete K) :
     MeasurableSet {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} := by

Mathlib/Analysis/Fourier/AddCircle.lean

@@ -243,7 +243,7 @@ theorem coeFn_fourierLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (n : ℤ) :
 theorem span_fourierLp_closure_eq_top {p : ℝ≥0∞} [Fact (1 ≤ p)] (hp : p ≠ ∞) :
     (span ℂ (range (@fourierLp T _ p _))).topologicalClosure = ⊤ := by
   convert
-    (ContinuousMap.toLp_denseRange ℂ (@haarAddCircle T hT) hp ℂ).topologicalClosure_map_submodule
+    (ContinuousMap.toLp_denseRange ℂ (@haarAddCircle T hT) ℂ hp).topologicalClosure_map_submodule
       span_fourier_closure_eq_top
   erw [map_span, range_comp]
   simp only [ContinuousLinearMap.coe_coe]

Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean

@@ -75,8 +75,11 @@ theorem separate_convex_open_set [TopologicalSpace E] [AddCommGroup E] [Topologi
       one_le_gauge_of_not_mem (hs₁.starConvex hs₀)
         (absorbent_nhds_zero <| hs₂.mem_nhds hs₀).absorbs hx₀
 
-variable [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module ℝ E]
-  [ContinuousSMul ℝ E] {s t : Set E} {x y : E}
+variable [TopologicalSpace E] [AddCommGroup E] [Module ℝ E]
+  {s t : Set E} {x y : E}
+section
+
+variable [TopologicalAddGroup E] [ContinuousSMul ℝ E]
 
 /-- A version of the **Hahn-Banach theorem**: given disjoint convex sets `s`, `t` where `s` is open,
 there is a continuous linear functional which separates them. -/
@@ -203,6 +206,8 @@ theorem iInter_halfspaces_eq (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) :
   obtain ⟨y, hy, hxy⟩ := hx l
   exact ((hxy.trans_lt (hlA y hy)).trans hl).not_le le_rfl
 
+end
+
 namespace RCLike
 
 variable [RCLike 𝕜] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [IsScalarTower ℝ 𝕜 E]
@@ -218,12 +223,12 @@ noncomputable def extendTo𝕜'ₗ : (E →L[ℝ] ℝ) →ₗ[ℝ] (E →L[𝕜]
     map_smul' := by intros; ext; simp [h, real_smul_eq_coe_mul]; ring }
 
 @[simp]
-lemma re_extendTo𝕜'ₗ (g : E →L[ℝ] ℝ) (x : E) :  re ((extendTo𝕜'ₗ g) x : 𝕜) = g x := by
+lemma re_extendTo𝕜'ₗ (g : E →L[ℝ] ℝ) (x : E) : re ((extendTo𝕜'ₗ g) x : 𝕜) = g x := by
   have h g (x : E) : extendTo𝕜'ₗ g x = ((g x : 𝕜) - (I : 𝕜) * (g ((I : 𝕜) • x) : 𝕜)) := rfl
   simp only [h , map_sub, ofReal_re, mul_re, I_re, zero_mul, ofReal_im, mul_zero,
     sub_self, sub_zero]
 
-variable [ContinuousSMul ℝ E]
+variable [TopologicalAddGroup E] [ContinuousSMul ℝ E]
 
 theorem separate_convex_open_set {s : Set E}
     (hs₀ : (0 : E) ∈ s) (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) {x₀ : E} (hx₀ : x₀ ∉ s) :

Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

@@ -28,7 +28,14 @@ open Finset Matrix
 namespace SimpleGraph
 
 variable {V : Type*} (R : Type*)
-variable [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
+variable [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
+
+theorem degree_eq_sum_if_adj {R : Type*} [AddCommMonoidWithOne R] (i : V) :
+    (G.degree i : R) = ∑ j : V, if G.Adj i j then 1 else 0 := by
+  unfold degree neighborFinset neighborSet
+  rw [sum_boole, Set.toFinset_setOf]
+
+variable [DecidableEq V]
 
 /-- The diagonal matrix consisting of the degrees of the vertices in the graph. -/
 def degMatrix [AddMonoidWithOne R] : Matrix V V R := Matrix.diagonal (G.degree ·)
@@ -64,11 +71,6 @@ theorem dotProduct_mulVec_degMatrix [CommRing R] (x : V → R) :
 
 variable (R)
 
-theorem degree_eq_sum_if_adj [AddCommMonoidWithOne R] (i : V) :
-    (G.degree i : R) = ∑ j : V, if G.Adj i j then 1 else 0 := by
-  unfold degree neighborFinset neighborSet
-  rw [sum_boole, Set.toFinset_setOf]
-
 /-- Let $L$ be the graph Laplacian and let $x \in \mathbb{R}$, then
 $$x^{\top} L x = \sum_{i \sim j} (x_{i}-x_{j})^{2}$$,
 where $\sim$ denotes the adjacency relation -/

Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean

@@ -19,11 +19,10 @@ open Set ChartedSpace SmoothManifoldWithCorners
 open scoped Topology Manifold
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
-  -- declare a smooth manifold `M` over the pair `(E, H)`.
+  -- declare a charted space `M` over the pair `(E, H)`.
   {E : Type*}
   [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
   {I : ModelWithCorners 𝕜 E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
-  [SmoothManifoldWithCorners I M]
   -- declare a smooth manifold `M'` over the pair `(E', H')`.
   {E' : Type*}
   [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
@@ -120,49 +119,6 @@ theorem ContinuousLinearMap.contMDiffOn (L : E →L[𝕜] F) {s} : ContMDiffOn 
 
 theorem ContinuousLinearMap.smooth (L : E →L[𝕜] F) : Smooth 𝓘(𝕜, E) 𝓘(𝕜, F) L := L.contMDiff
 
-theorem ContMDiffWithinAt.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M} {x : M}
-    (hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s x)
-    (hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s x) :
-    ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) s x :=
-  ContDiff.comp_contMDiffWithinAt (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₁) => x.1.comp x.2)
-    (f := fun x => (g x, f x)) (contDiff_fst.clm_comp contDiff_snd) (hg.prod_mk_space hf)
-
-theorem ContMDiffAt.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {x : M}
-    (hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g x) (hf : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f x) :
-    ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) x :=
-  (hg.contMDiffWithinAt.clm_comp hf.contMDiffWithinAt).contMDiffAt Filter.univ_mem
-
-theorem ContMDiffOn.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M}
-    (hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s) (hf : ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s) :
-    ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) s := fun x hx =>
-  (hg x hx).clm_comp (hf x hx)
-
-theorem ContMDiff.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁}
-    (hg : ContMDiff I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g) (hf : ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f) :
-    ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₃) n fun x => (g x).comp (f x) := fun x => (hg x).clm_comp (hf x)
-
-theorem ContMDiffWithinAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M}
-    (hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x)
-    (hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x) :
-    ContMDiffWithinAt I 𝓘(𝕜, F₂) n (fun x => g x (f x)) s x :=
-  @ContDiffWithinAt.comp_contMDiffWithinAt _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
-    (fun x : (F₁ →L[𝕜] F₂) × F₁ => x.1 x.2) (fun x => (g x, f x)) s _ x
-    (by apply ContDiff.contDiffAt; exact contDiff_fst.clm_apply contDiff_snd) (hg.prod_mk_space hf)
-    (by simp_rw [preimage_univ, subset_univ])
-
-nonrec theorem ContMDiffAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M}
-    (hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g x) (hf : ContMDiffAt I 𝓘(𝕜, F₁) n f x) :
-    ContMDiffAt I 𝓘(𝕜, F₂) n (fun x => g x (f x)) x :=
-  hg.clm_apply hf
-
-theorem ContMDiffOn.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M}
-    (hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s) (hf : ContMDiffOn I 𝓘(𝕜, F₁) n f s) :
-    ContMDiffOn I 𝓘(𝕜, F₂) n (fun x => g x (f x)) s := fun x hx => (hg x hx).clm_apply (hf x hx)
-
-theorem ContMDiff.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁}
-    (hg : ContMDiff I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g) (hf : ContMDiff I 𝓘(𝕜, F₁) n f) :
-    ContMDiff I 𝓘(𝕜, F₂) n fun x => g x (f x) := fun x => (hg x).clm_apply (hf x)
-
 theorem ContMDiffWithinAt.clm_precomp {f : M → F₁ →L[𝕜] F₂} {s : Set M} {x : M}
     (hf : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n f s x) :
     ContMDiffWithinAt I 𝓘(𝕜, (F₂ →L[𝕜] F₃) →L[𝕜] (F₁ →L[𝕜] F₃)) n
@@ -211,6 +167,52 @@ theorem ContMDiff.clm_postcomp {f : M → F₂ →L[𝕜] F₃} (hf : ContMDiff
       (fun y ↦ (f y).postcomp F₁ : M → (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃)) := fun x ↦
   (hf x).clm_postcomp
 
+-- Now make `M` a smooth manifold.
+variable [SmoothManifoldWithCorners I M]
+
+theorem ContMDiffWithinAt.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M} {x : M}
+    (hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s x)
+    (hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s x) :
+    ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) s x :=
+  ContDiff.comp_contMDiffWithinAt (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₁) => x.1.comp x.2)
+    (f := fun x => (g x, f x)) (contDiff_fst.clm_comp contDiff_snd) (hg.prod_mk_space hf)
+
+theorem ContMDiffAt.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {x : M}
+    (hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g x) (hf : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f x) :
+    ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) x :=
+  (hg.contMDiffWithinAt.clm_comp hf.contMDiffWithinAt).contMDiffAt Filter.univ_mem
+
+theorem ContMDiffOn.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M}
+    (hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s) (hf : ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s) :
+    ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) s := fun x hx =>
+  (hg x hx).clm_comp (hf x hx)
+
+theorem ContMDiff.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁}
+    (hg : ContMDiff I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g) (hf : ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f) :
+    ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₃) n fun x => (g x).comp (f x) := fun x => (hg x).clm_comp (hf x)
+
+theorem ContMDiffWithinAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M}
+    (hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x)
+    (hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x) :
+    ContMDiffWithinAt I 𝓘(𝕜, F₂) n (fun x => g x (f x)) s x :=
+  ContDiffWithinAt.comp_contMDiffWithinAt
+    (g := fun x : (F₁ →L[𝕜] F₂) × F₁ => x.1 x.2)
+    (by apply ContDiff.contDiffAt; exact contDiff_fst.clm_apply contDiff_snd) (hg.prod_mk_space hf)
+    (by simp_rw [preimage_univ, subset_univ])
+
+nonrec theorem ContMDiffAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M}
+    (hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g x) (hf : ContMDiffAt I 𝓘(𝕜, F₁) n f x) :
+    ContMDiffAt I 𝓘(𝕜, F₂) n (fun x => g x (f x)) x :=
+  hg.clm_apply hf
+
+theorem ContMDiffOn.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M}
+    (hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s) (hf : ContMDiffOn I 𝓘(𝕜, F₁) n f s) :
+    ContMDiffOn I 𝓘(𝕜, F₂) n (fun x => g x (f x)) s := fun x hx => (hg x hx).clm_apply (hf x hx)
+
+theorem ContMDiff.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁}
+    (hg : ContMDiff I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g) (hf : ContMDiff I 𝓘(𝕜, F₁) n f) :
+    ContMDiff I 𝓘(𝕜, F₂) n fun x => g x (f x) := fun x => (hg x).clm_apply (hf x)
+
 theorem ContMDiffWithinAt.cle_arrowCongr {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄}
     {s : Set M} {x : M}
     (hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n (fun x ↦ ((f x).symm : F₂ →L[𝕜] F₁)) s x)