feat: expand API around manifold derivatives (#18850)

Notably, prove that basic functions are differentiable in the manifold sense, and compute their derivatives.

Author: sgouezel

Mathlib/Geometry/Manifold/Algebra/Monoid.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicolò Cavalleri
 -/
 import Mathlib.Geometry.Manifold.ContMDiffMap
+import Mathlib.Geometry.Manifold.MFDeriv.Basic
 
 /-!
 # Smooth monoid
@@ -132,6 +133,28 @@ theorem smooth_mul_left {a : G} : Smooth I I fun b : G => a * b :=
 theorem smooth_mul_right {a : G} : Smooth I I fun b : G => b * a :=
   smooth_id.mul smooth_const
 
+theorem contMDiff_mul_left {a : G} : ContMDiff I I n (a * ·) := smooth_mul_left.contMDiff
+
+theorem contMDiffAt_mul_left {a b : G} : ContMDiffAt I I n (a * ·) b :=
+  contMDiff_mul_left.contMDiffAt
+
+theorem mdifferentiable_mul_left {a : G} : MDifferentiable I I (a * ·) :=
+  contMDiff_mul_left.mdifferentiable le_rfl
+
+theorem mdifferentiableAt_mul_left {a b : G} : MDifferentiableAt I I (a * ·) b :=
+  contMDiffAt_mul_left.mdifferentiableAt le_rfl
+
+theorem contMDiff_mul_right {a : G} : ContMDiff I I n (· * a) := smooth_mul_right.contMDiff
+
+theorem contMDiffAt_mul_right {a b : G} : ContMDiffAt I I n (· * a) b :=
+  contMDiff_mul_right.contMDiffAt
+
+theorem mdifferentiable_mul_right {a : G} : MDifferentiable I I (· * a) :=
+  contMDiff_mul_right.mdifferentiable le_rfl
+
+theorem mdifferentiableAt_mul_right {a b : G} : MDifferentiableAt I I (· * a) b :=
+  contMDiffAt_mul_right.mdifferentiableAt le_rfl
+
 end
 
 variable (I) (g h : G)

Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean

@@ -257,4 +257,96 @@ theorem mdifferentiableOn_extChartAt_symm :
   intro y hy
   exact (mdifferentiableWithinAt_extChartAt_symm hy).mono (extChartAt_target_subset_range x)
 
+/-- The composition of the derivative of `extChartAt` with the derivative of the inverse of
+`extChartAt` gives the identity.
+Version where the basepoint belongs to `(extChartAt I x).target`. -/
+lemma mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm {x : M}
+    {y : E} (hy : y ∈ (extChartAt I x).target) :
+    (mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y)) ∘L
+      (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y) = ContinuousLinearMap.id _ _ := by
+  have U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range ↑I) y := by
+    apply I.uniqueMDiffOn
+    exact extChartAt_target_subset_range x hy
+  have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target hy
+  have h''y : (extChartAt I x).symm y ∈ (chartAt H x).source := by
+    rwa [← extChartAt_source (I := I)]
+  rw [← mfderiv_comp_mfderivWithin]; rotate_left
+  · apply mdifferentiableAt_extChartAt h''y
+  · exact mdifferentiableWithinAt_extChartAt_symm hy
+  · exact U
+  rw [← mfderivWithin_id U]
+  apply Filter.EventuallyEq.mfderivWithin_eq U
+  · filter_upwards [extChartAt_target_mem_nhdsWithin_of_mem hy] with z hz
+    simp only [Function.comp_def, PartialEquiv.right_inv (extChartAt I x) hz, id_eq]
+  · simp only [Function.comp_def, PartialEquiv.right_inv (extChartAt I x) hy, id_eq]
+
+/-- The composition of the derivative of `extChartAt` with the derivative of the inverse of
+`extChartAt` gives the identity.
+Version where the basepoint belongs to `(extChartAt I x).source`. -/
+lemma mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm' {x : M}
+    {y : M} (hy : y ∈ (extChartAt I x).source) :
+    (mfderiv I 𝓘(𝕜, E) (extChartAt I x) y) ∘L
+      (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) (extChartAt I x y))
+    = ContinuousLinearMap.id _ _ := by
+  have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm
+  convert mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm ((extChartAt I x).map_source hy)
+
+/-- The composition of the derivative of the inverse of `extChartAt` with the derivative of
+`extChartAt` gives the identity.
+Version where the basepoint belongs to `(extChartAt I x).target`. -/
+lemma mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt
+    {y : E} (hy : y ∈ (extChartAt I x).target) :
+    (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y) ∘L
+      (mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y))
+      = ContinuousLinearMap.id _ _ := by
+  have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target hy
+  have h''y : (extChartAt I x).symm y ∈ (chartAt H x).source := by
+    rwa [← extChartAt_source (I := I)]
+  have U' : UniqueMDiffWithinAt I (extChartAt I x).source ((extChartAt I x).symm y) :=
+    (isOpen_extChartAt_source x).uniqueMDiffWithinAt h'y
+  have : mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y)
+      = mfderivWithin I 𝓘(𝕜, E) (extChartAt I x) (extChartAt I x).source
+      ((extChartAt I x).symm y) := by
+    rw [mfderivWithin_eq_mfderiv U']
+    exact mdifferentiableAt_extChartAt h''y
+  rw [this, ← mfderivWithin_comp_of_eq]; rotate_left
+  · exact mdifferentiableWithinAt_extChartAt_symm hy
+  · exact (mdifferentiableAt_extChartAt h''y).mdifferentiableWithinAt
+  · intro z hz
+    apply extChartAt_target_subset_range x
+    exact PartialEquiv.map_source (extChartAt I x) hz
+  · exact U'
+  · exact PartialEquiv.right_inv (extChartAt I x) hy
+  rw [← mfderivWithin_id U']
+  apply Filter.EventuallyEq.mfderivWithin_eq U'
+  · filter_upwards [extChartAt_source_mem_nhdsWithin' h'y] with z hz
+    simp only [Function.comp_def, PartialEquiv.left_inv (extChartAt I x) hz, id_eq]
+  · simp only [Function.comp_def, PartialEquiv.right_inv (extChartAt I x) hy, id_eq]
+
+/-- The composition of the derivative of the inverse of `extChartAt` with the derivative of
+`extChartAt` gives the identity.
+Version where the basepoint belongs to `(extChartAt I x).source`. -/
+lemma mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt'
+    {y : M} (hy : y ∈ (extChartAt I x).source) :
+    (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) (extChartAt I x y)) ∘L
+      (mfderiv I 𝓘(𝕜, E) (extChartAt I x) y)
+      = ContinuousLinearMap.id _ _ := by
+  have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm
+  convert mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt ((extChartAt I x).map_source hy)
+
+lemma isInvertible_mfderivWithin_extChartAt_symm {y : E} (hy : y ∈ (extChartAt I x).target) :
+    (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y).IsInvertible :=
+  ContinuousLinearMap.IsInvertible.of_inverse
+    (mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt hy)
+    (mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm hy)
+
+lemma isInvertible_mfderiv_extChartAt {y : M} (hy : y ∈ (extChartAt I x).source) :
+    (mfderiv I 𝓘(𝕜, E) (extChartAt I x) y).IsInvertible := by
+  have h'y : extChartAt I x y ∈ (extChartAt I x).target := (extChartAt I x).map_source hy
+  have Z := ContinuousLinearMap.IsInvertible.of_inverse
+    (mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm h'y)
+    (mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt h'y)
+  have : (extChartAt I x).symm ((extChartAt I x) y) = y := (extChartAt I x).left_inv hy
+  rwa [this] at Z
+
 end extChartAt

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

@@ -26,14 +26,31 @@ section SpecificFunctions
 
 /-! ### Differentiability of specific functions -/
 
-variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+  -- 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] {E' : Type*}
-  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
+  [TopologicalSpace M] [ChartedSpace H M]
+  -- 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']
+  -- 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'']
+  -- declare a charted space `N` over the pair `(F, G)`.
+  {F : Type*}
+  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} [TopologicalSpace G]
+  {J : ModelWithCorners 𝕜 F G} {N : Type*} [TopologicalSpace N] [ChartedSpace G N]
+  -- declare a charted space `N'` over the pair `(F', G')`.
+  {F' : Type*}
+  [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type*} [TopologicalSpace G']
+  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type*} [TopologicalSpace N'] [ChartedSpace G' N']
+  -- F₁, F₂, F₃, F₄ are normed spaces
+  {F₁ : Type*}
+  [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type*} [NormedAddCommGroup F₂]
+  [NormedSpace 𝕜 F₂] {F₃ : Type*} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type*}
+  [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄]
 
 namespace ContinuousLinearMap
 
@@ -301,6 +318,128 @@ theorem mfderivWithin_snd {s : Set (M × M')} {x : M × M'}
       ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2) := by
   rw [MDifferentiable.mfderivWithin mdifferentiableAt_snd hxs]; exact mfderiv_snd
 
+theorem MDifferentiableWithinAt.fst {f : N → M × M'} {s : Set N} {x : N}
+    (hf : MDifferentiableWithinAt J (I.prod I') f s x) :
+    MDifferentiableWithinAt J I (fun x => (f x).1) s x :=
+  mdifferentiableAt_fst.comp_mdifferentiableWithinAt x hf
+
+theorem MDifferentiableAt.fst {f : N → M × M'} {x : N} (hf : MDifferentiableAt J (I.prod I') f x) :
+    MDifferentiableAt J I (fun x => (f x).1) x :=
+  mdifferentiableAt_fst.comp x hf
+
+theorem MDifferentiable.fst {f : N → M × M'} (hf : MDifferentiable J (I.prod I') f) :
+    MDifferentiable J I fun x => (f x).1 :=
+  mdifferentiable_fst.comp hf
+
+theorem MDifferentiableWithinAt.snd {f : N → M × M'} {s : Set N} {x : N}
+    (hf : MDifferentiableWithinAt J (I.prod I') f s x) :
+    MDifferentiableWithinAt J I' (fun x => (f x).2) s x :=
+  mdifferentiableAt_snd.comp_mdifferentiableWithinAt x hf
+
+theorem MDifferentiableAt.snd {f : N → M × M'} {x : N} (hf : MDifferentiableAt J (I.prod I') f x) :
+    MDifferentiableAt J I' (fun x => (f x).2) x :=
+  mdifferentiableAt_snd.comp x hf
+
+theorem MDifferentiable.snd {f : N → M × M'} (hf : MDifferentiable J (I.prod I') f) :
+    MDifferentiable J I' fun x => (f x).2 :=
+  mdifferentiable_snd.comp hf
+
+theorem mdifferentiableWithinAt_prod_iff (f : M → M' × N') :
+    MDifferentiableWithinAt I (I'.prod J') f s x ↔
+      MDifferentiableWithinAt I I' (Prod.fst ∘ f) s x
+      ∧ MDifferentiableWithinAt I J' (Prod.snd ∘ f) s x :=
+  ⟨fun h => ⟨h.fst, h.snd⟩, fun h => h.1.prod_mk h.2⟩
+
+theorem mdifferentiableWithinAt_prod_module_iff (f : M → F₁ × F₂) :
+    MDifferentiableWithinAt I 𝓘(𝕜, F₁ × F₂) f s x ↔
+      MDifferentiableWithinAt I 𝓘(𝕜, F₁) (Prod.fst ∘ f) s x ∧
+      MDifferentiableWithinAt I 𝓘(𝕜, F₂) (Prod.snd ∘ f) s x := by
+  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
+  exact mdifferentiableWithinAt_prod_iff f
+
+theorem mdifferentiableAt_prod_iff (f : M → M' × N') :
+    MDifferentiableAt I (I'.prod J') f x ↔
+      MDifferentiableAt I I' (Prod.fst ∘ f) x ∧ MDifferentiableAt I J' (Prod.snd ∘ f) x := by
+  simp_rw [← mdifferentiableWithinAt_univ]; exact mdifferentiableWithinAt_prod_iff f
+
+theorem mdifferentiableAt_prod_module_iff (f : M → F₁ × F₂) :
+    MDifferentiableAt I 𝓘(𝕜, F₁ × F₂) f x ↔
+      MDifferentiableAt I 𝓘(𝕜, F₁) (Prod.fst ∘ f) x
+      ∧ MDifferentiableAt I 𝓘(𝕜, F₂) (Prod.snd ∘ f) x := by
+  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
+  exact mdifferentiableAt_prod_iff f
+
+theorem mdifferentiableOn_prod_iff (f : M → M' × N') :
+    MDifferentiableOn I (I'.prod J') f s ↔
+      MDifferentiableOn I I' (Prod.fst ∘ f) s ∧ MDifferentiableOn I J' (Prod.snd ∘ f) s :=
+  ⟨fun h ↦ ⟨fun x hx ↦ ((mdifferentiableWithinAt_prod_iff f).1 (h x hx)).1,
+      fun x hx ↦ ((mdifferentiableWithinAt_prod_iff f).1 (h x hx)).2⟩ ,
+    fun h x hx ↦ (mdifferentiableWithinAt_prod_iff f).2 ⟨h.1 x hx, h.2 x hx⟩⟩
+
+theorem mdifferentiableOn_prod_module_iff (f : M → F₁ × F₂) :
+    MDifferentiableOn I 𝓘(𝕜, F₁ × F₂) f s ↔
+      MDifferentiableOn I 𝓘(𝕜, F₁) (Prod.fst ∘ f) s
+      ∧ MDifferentiableOn I 𝓘(𝕜, F₂) (Prod.snd ∘ f) s := by
+  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
+  exact mdifferentiableOn_prod_iff f
+
+theorem mdifferentiable_prod_iff (f : M → M' × N') :
+    MDifferentiable I (I'.prod J') f ↔
+      MDifferentiable I I' (Prod.fst ∘ f) ∧ MDifferentiable I J' (Prod.snd ∘ f) :=
+  ⟨fun h => ⟨h.fst, h.snd⟩, fun h => by convert h.1.prod_mk h.2⟩
+
+theorem mdifferentiable_prod_module_iff (f : M → F₁ × F₂) :
+    MDifferentiable I 𝓘(𝕜, F₁ × F₂) f ↔
+      MDifferentiable I 𝓘(𝕜, F₁) (Prod.fst ∘ f) ∧ MDifferentiable I 𝓘(𝕜, F₂) (Prod.snd ∘ f) := by
+  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
+  exact mdifferentiable_prod_iff f
+
+
+section prodMap
+
+variable {f : M → M'} {g : N → N'} {r : Set N} {y : N}
+
+/-- The product map of two `C^n` functions within a set at a point is `C^n`
+within the product set at the product point. -/
+theorem MDifferentiableWithinAt.prod_map' {p : M × N} (hf : MDifferentiableWithinAt I I' f s p.1)
+    (hg : MDifferentiableWithinAt J J' g r p.2) :
+    MDifferentiableWithinAt (I.prod J) (I'.prod J') (Prod.map f g) (s ×ˢ r) p :=
+  (hf.comp p mdifferentiableWithinAt_fst (prod_subset_preimage_fst _ _)).prod_mk <|
+    hg.comp p mdifferentiableWithinAt_snd (prod_subset_preimage_snd _ _)
+
+theorem MDifferentiableWithinAt.prod_map (hf : MDifferentiableWithinAt I I' f s x)
+    (hg : MDifferentiableWithinAt J J' g r y) :
+    MDifferentiableWithinAt (I.prod J) (I'.prod J') (Prod.map f g) (s ×ˢ r) (x, y) :=
+  MDifferentiableWithinAt.prod_map' hf hg
+
+theorem MDifferentiableAt.prod_map
+    (hf : MDifferentiableAt I I' f x) (hg : MDifferentiableAt J J' g y) :
+    MDifferentiableAt (I.prod J) (I'.prod J') (Prod.map f g) (x, y) := by
+  rw [← mdifferentiableWithinAt_univ] at *
+  convert hf.prod_map hg
+  exact univ_prod_univ.symm
+
+/-- Variant of `MDifferentiableAt.prod_map` in which the point in the product is given as `p`
+instead of a pair `(x, y)`. -/
+theorem MDifferentiableAt.prod_map' {p : M × N}
+    (hf : MDifferentiableAt I I' f p.1) (hg : MDifferentiableAt J J' g p.2) :
+    MDifferentiableAt (I.prod J) (I'.prod J') (Prod.map f g) p := by
+  rcases p with ⟨⟩
+  exact hf.prod_map hg
+
+theorem MDifferentiableOn.prod_map
+    (hf : MDifferentiableOn I I' f s) (hg : MDifferentiableOn J J' g r) :
+    MDifferentiableOn (I.prod J) (I'.prod J') (Prod.map f g) (s ×ˢ r) :=
+  (hf.comp mdifferentiableOn_fst (prod_subset_preimage_fst _ _)).prod_mk <|
+    hg.comp mdifferentiableOn_snd (prod_subset_preimage_snd _ _)
+
+theorem MDifferentiable.prod_map (hf : MDifferentiable I I' f) (hg : MDifferentiable J J' g) :
+    MDifferentiable (I.prod J) (I'.prod J') (Prod.map f g) := by
+  intro p
+  exact (hf p.1).prod_map' (hg p.2)
+
+end prodMap
+
 @[simp, mfld_simps]
 theorem tangentMap_prod_snd {p : TangentBundle (I.prod I') (M × M')} :
     tangentMap (I.prod I') I' Prod.snd p = ⟨p.proj.2, p.2.2⟩ := by
@@ -330,22 +469,30 @@ theorem mfderiv_prod_left {x₀ : M} {y₀ : M'} :
   refine (mdifferentiableAt_id.mfderiv_prod mdifferentiableAt_const).trans ?_
   rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inl]
 
+theorem tangentMap_prod_left {p : TangentBundle I M} {y₀ : M'} :
+    tangentMap I (I.prod I') (fun x => (x, y₀)) p = ⟨(p.1, y₀), (p.2, 0)⟩ := by
+  simp only [tangentMap, mfderiv_prod_left, TotalSpace.mk_inj]
+  rfl
+
 theorem mfderiv_prod_right {x₀ : M} {y₀ : M'} :
     mfderiv I' (I.prod I') (fun y => (x₀, y)) y₀ =
       ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) := by
   refine (mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_id).trans ?_
   rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inr]
 
+theorem tangentMap_prod_right {p : TangentBundle I' M'} {x₀ : M} :
+    tangentMap I' (I.prod I') (fun y => (x₀, y)) p = ⟨(x₀, p.1), (0, p.2)⟩ := by
+  simp only [tangentMap, mfderiv_prod_right, TotalSpace.mk_inj]
+  rfl
+
 /-- The total derivative of a function in two variables is the sum of the partial derivatives.
   Note that to state this (without casts) we need to be able to see through the definition of
   `TangentSpace`. -/
 theorem mfderiv_prod_eq_add {f : M × M' → M''} {p : M × M'}
     (hf : MDifferentiableAt (I.prod I') I'' f p) :
     mfderiv (I.prod I') I'' f p =
-      show E × E' →L[𝕜] E'' from
         mfderiv (I.prod I') I'' (fun z : M × M' => f (z.1, p.2)) p +
           mfderiv (I.prod I') I'' (fun z : M × M' => f (p.1, z.2)) p := by
-  dsimp only
   erw [mfderiv_comp_of_eq hf (mdifferentiableAt_fst.prod_mk mdifferentiableAt_const) rfl,
     mfderiv_comp_of_eq hf (mdifferentiableAt_const.prod_mk mdifferentiableAt_snd) rfl,
     ← ContinuousLinearMap.comp_add,
@@ -356,6 +503,42 @@ theorem mfderiv_prod_eq_add {f : M × M' → M''} {p : M × M'}
   convert ContinuousLinearMap.comp_id <| mfderiv (.prod I I') I'' f (p.1, p.2)
   exact ContinuousLinearMap.coprod_inl_inr
 
+/-- The total derivative of a function in two variables is the sum of the partial derivatives.
+  Note that to state this (without casts) we need to be able to see through the definition of
+  `TangentSpace`. Version in terms of the one-variable derivatives. -/
+theorem mfderiv_prod_eq_add_comp {f : M × M' → M''} {p : M × M'}
+    (hf : MDifferentiableAt (I.prod I') I'' f p) :
+    mfderiv (I.prod I') I'' f p =
+        (mfderiv I I'' (fun z : M => f (z, p.2)) p.1) ∘L (id (ContinuousLinearMap.fst 𝕜 E E') :
+          (TangentSpace (I.prod I') p) →L[𝕜] (TangentSpace I p.1)) +
+        (mfderiv I' I'' (fun z : M' => f (p.1, z)) p.2) ∘L (id (ContinuousLinearMap.snd 𝕜 E E') :
+          (TangentSpace (I.prod I') p) →L[𝕜] (TangentSpace I' p.2)) := by
+  rw [mfderiv_prod_eq_add hf]
+  congr
+  · have : (fun z : M × M' => f (z.1, p.2)) = (fun z : M => f (z, p.2)) ∘ Prod.fst := rfl
+    rw [this, mfderiv_comp (I' := I)]
+    · simp only [mfderiv_fst, id_eq]
+      rfl
+    · exact hf.comp _  (mdifferentiableAt_id.prod_mk mdifferentiableAt_const)
+    · exact mdifferentiableAt_fst
+  · have : (fun z : M × M' => f (p.1, z.2)) = (fun z : M' => f (p.1, z)) ∘ Prod.snd := rfl
+    rw [this, mfderiv_comp (I' := I')]
+    · simp only [mfderiv_snd, id_eq]
+      rfl
+    · exact hf.comp _ (mdifferentiableAt_const.prod_mk mdifferentiableAt_id)
+    · exact mdifferentiableAt_snd
+
+/-- The total derivative of a function in two variables is the sum of the partial derivatives.
+  Note that to state this (without casts) we need to be able to see through the definition of
+  `TangentSpace`. Version in terms of the one-variable derivatives. -/
+theorem mfderiv_prod_eq_add_apply {f : M × M' → M''} {p : M × M'} {v : TangentSpace (I.prod I') p}
+    (hf : MDifferentiableAt (I.prod I') I'' f p) :
+    mfderiv (I.prod I') I'' f p v =
+      mfderiv I I'' (fun z : M => f (z, p.2)) p.1 v.1 +
+      mfderiv I' I'' (fun z : M' => f (p.1, z)) p.2 v.2 := by
+  rw [mfderiv_prod_eq_add_comp hf]
+  rfl
+
 end Prod
 
 section Arithmetic