awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
p : TangentBundle I M
y₀ : M'
simp :
  Eq (α := TangentSpace (I.prod I') (p.proj (E := TangentSpace I), y₀))
    (((ContinuousLinearMap.inl 𝕜 (TangentSpace I (p.proj (E := TangentSpace I))) (TangentSpace I' y₀) :
            TangentSpace I (p.proj (E := TangentSpace I)) →L[𝕜]
              Prod.{u_2, u_5} (TangentSpace I (p.proj (E := TangentSpace I))) (TangentSpace I' y₀)) :
          (a : TangentSpace I p.proj) → TangentSpace (I.prod I') (p.proj, y₀))
        (p.snd (E := TangentSpace I)) :
      TangentSpace (I.prod I') (p.proj (E := TangentSpace I), y₀))
    ((p.snd (E := TangentSpace I), 0) : E × E')
⊢ Eq (α := TangentBundle (I.prod I') (M × M')) (tangentMap I (I.prod I') (fun (x : M) ↦ (x, y₀)) p)
    ⟨(p.proj (E := TangentSpace I), y₀), (p.snd (E := TangentSpace I), 0)⟩

Tactic:
simp only [tangentMap, mfderiv_prod_left, TotalSpace.mk_inj]

Premises used: Bundle.TotalSpace.mk_inj, mfderiv_prod_left, tangentMap
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
p : TangentBundle I M
y₀ : M'
⊢ Eq (α := TangentSpace (I.prod I') (p.proj (E := TangentSpace I), y₀))
    (((ContinuousLinearMap.inl 𝕜 (TangentSpace I (p.proj (E := TangentSpace I))) (TangentSpace I' y₀) :
            TangentSpace I (p.proj (E := TangentSpace I)) →L[𝕜]
              Prod.{u_2, u_5} (TangentSpace I (p.proj (E := TangentSpace I))) (TangentSpace I' y₀)) :
          (a : TangentSpace I p.proj) → TangentSpace (I.prod I') (p.proj, y₀))
        (p.snd (E := TangentSpace I)) :
      TangentSpace (I.prod I') (p.proj (E := TangentSpace I), y₀))
    ((p.snd (E := TangentSpace I), 0) : E × E')

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
x₀ : M
y₀ : M'
⊢ Eq (α := TangentSpace I' y₀ →L[𝕜] TangentSpace (I.prod I') (x₀, y₀)) ((mfderiv% fun (y : M') ↦ (x₀, y)) y₀)
    (ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀))

Tactic:
(mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_id).trans ?_

Premises used: MDifferentiableAt.mfderiv_prod, mdifferentiableAt_const, TangentSpace, mdifferentiableAt_id, Eq.trans
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
x₀ : M
y₀ : M'
refine :
  Eq (α := TangentSpace I' y₀ →L[𝕜] TangentSpace (I.prod I') (x₀, id y₀))
    (ContinuousLinearMap.prod ((mfderiv% fun (x : M') ↦ x₀) y₀) (mfderiv% id y₀) :
      TangentSpace I' y₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' (id y₀)))
    (ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) :
      TangentSpace I' y₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' y₀))
⊢ Eq (α := TangentSpace I' y₀ →L[𝕜] TangentSpace (I.prod I') (x₀, y₀)) ((mfderiv% fun (y : M') ↦ (x₀, y)) y₀)
    (ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀))

Tactic:
refine (mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_id).trans ?_

Premises used: MDifferentiableAt.mfderiv_prod, mdifferentiableAt_const, mdifferentiableAt_id, Eq.trans
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
x₀ : M
y₀ : M'
rw :
  Eq (α := TangentSpace I' y₀ →L[𝕜] TangentSpace (I.prod I') (x₀, id y₀))
    (ContinuousLinearMap.prod ((mfderiv% fun (x : M') ↦ x₀) y₀) (ContinuousLinearMap.id 𝕜 (TangentSpace I' y₀)) :
      TangentSpace I' y₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' (id y₀)))
    (ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) :
      TangentSpace I' y₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' y₀))
rw₁ :
  Eq (α := TangentSpace I' y₀ →L[𝕜] TangentSpace (I.prod I') (x₀, id y₀))
    (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace I' y₀)) :
      TangentSpace I' y₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' (id y₀)))
    (ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀))
rw₂ rw₃ :
  Eq (α := TangentSpace I' y₀ →L[𝕜] TangentSpace (I.prod I') (x₀, id y₀))
    (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace I' y₀)) :
      TangentSpace I' y₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' (id y₀)))
    (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace I' y₀)))
⊢ Eq (α := TangentSpace I' y₀ →L[𝕜] TangentSpace (I.prod I') (x₀, id y₀))
    (ContinuousLinearMap.prod ((mfderiv% fun (x : M') ↦ x₀) y₀) (mfderiv% id y₀) :
      TangentSpace I' y₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' (id y₀)))
    (ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) :
      TangentSpace I' y₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' y₀))

Tactic:
rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inr]

Premises used: ContinuousLinearMap.inr, mfderiv_const, mfderiv_id
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
p : TangentBundle I' M'
x₀ : M
simp :
  Eq (α := TangentSpace (I.prod I') (x₀, p.proj (E := TangentSpace I')))
    (((ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' (p.proj (E := TangentSpace I'))) :
            TangentSpace I' (p.proj (E := TangentSpace I')) →L[𝕜]
              Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' (p.proj (E := TangentSpace I')))) :
          (a : TangentSpace I' p.proj) → TangentSpace (I.prod I') (x₀, p.proj))
        (p.snd (E := TangentSpace I')) :
      TangentSpace (I.prod I') (x₀, p.proj (E := TangentSpace I')))
    ((0, p.snd (E := TangentSpace I')) : E × E')
⊢ Eq (α := TangentBundle (I.prod I') (M × M')) (tangentMap I' (I.prod I') (fun (y : M') ↦ (x₀, y)) p)
    ⟨(x₀, p.proj (E := TangentSpace I')), (0, p.snd (E := TangentSpace I'))⟩

Tactic:
simp only [tangentMap, mfderiv_prod_right, TotalSpace.mk_inj]

Premises used: Bundle.TotalSpace.mk_inj, mfderiv_prod_right, tangentMap
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
p : TangentBundle I' M'
x₀ : M
⊢ Eq (α := TangentSpace (I.prod I') (x₀, p.proj (E := TangentSpace I')))
    (((ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' (p.proj (E := TangentSpace I'))) :
            TangentSpace I' (p.proj (E := TangentSpace I')) →L[𝕜]
              Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' (p.proj (E := TangentSpace I')))) :
          (a : TangentSpace I' p.proj) → TangentSpace (I.prod I') (x₀, p.proj))
        (p.snd (E := TangentSpace I')) :
      TangentSpace (I.prod I') (x₀, p.proj (E := TangentSpace I')))
    ((0, p.snd (E := TangentSpace I')) : E × E')

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
hf : MDiffAt f p
erw :
  Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f p)) (mfderiv% f p)
    (mfderiv% f (p.1, p.2) ∘SL
      HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2)) (β :=
        TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2))
        (ContinuousLinearMap.prod (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) 0 :
          TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2))
        (ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) :
          TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2)))
⊢ mfderiv% f p =
    HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
      ((mfderiv% fun (z : M × M') ↦ f (z.1, p.2)) p) ((mfderiv% fun (z : M × M') ↦ f (p.1, z.2)) p)

Tactic:
erw [mfderiv_comp_of_eq hf (mdifferentiableAt_fst.prodMk mdifferentiableAt_const) rfl,
    mfderiv_comp_of_eq hf (mdifferentiableAt_const.prodMk mdifferentiableAt_snd) rfl,
    ← ContinuousLinearMap.comp_add,
    mdifferentiableAt_fst.mfderiv_prod mdifferentiableAt_const,
    mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_snd, mfderiv_fst,
    mfderiv_snd, mfderiv_const, mfderiv_const]

Premises used: MDifferentiableAt.mfderiv_prod, mfderiv_comp_of_eq, ContinuousLinearMap.comp_add, mdifferentiableAt_fst, MDifferentiableAt.prodMk, mdifferentiableAt_snd, mfderiv_snd, mdifferentiableAt_const, mfderiv_const, mfderiv_fst, rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
hf : MDiffAt f p
symm :
  Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f p))
    (mfderiv% f (p.1, p.2) ∘SL
      HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2)) (β :=
        TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2))
        (ContinuousLinearMap.prod (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) 0 :
          TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2))
        (ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) :
          TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2)))
    (mfderiv% f p)
⊢ Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f p)) (mfderiv% f p)
    (mfderiv% f (p.1, p.2) ∘SL
      HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2)) (β :=
        TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2))
        (ContinuousLinearMap.prod (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) 0 :
          TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2))
        (ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) :
          TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2)))

Tactic:
symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
hf : MDiffAt f p
⊢ Eq (α := TangentSpace (I.prod I') (p.1, p.2) →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
    (mfderiv% f (p.1, p.2) ∘SL ContinuousLinearMap.id 𝕜 (TangentSpace (I.prod I') (p.1, p.2))) (mfderiv% f (p.1, p.2))

Tactic:
ContinuousLinearMap.comp_id <| mfderiv% f (p.1, p.2)

Premises used: mfderiv, Prod.mk, Prod.fst, Prod.snd, ContinuousLinearMap.comp_id, ModelWithCorners.prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
hf : MDiffAt f p
h :
  HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2)) (β :=
      TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2))
      (ContinuousLinearMap.prod (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) 0 :
        TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2))
      (ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) :
        TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace (I.prod I') (p.1, p.2))
⊢ Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f p))
    (mfderiv% f (p.1, p.2) ∘SL
      HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2)) (β :=
        TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2))
        (ContinuousLinearMap.prod (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) 0 :
          TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2))
        (ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) :
          TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2)))
    (mfderiv% f p)

Tactic:
convert! ContinuousLinearMap.comp_id <| mfderiv% f (p.1, p.2)

Premises used: mfderiv, Prod.mk, Prod.fst, Prod.snd, ContinuousLinearMap.comp_id, ModelWithCorners.prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
hf : MDiffAt f p
⊢ HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2)) (β :=
      TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2))
      (ContinuousLinearMap.prod (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) 0 :
        TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2))
      (ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) :
        TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace (I.prod I') (p.1, p.2))

Tactic:
ContinuousLinearMap.coprod_inl_inr

Premises used: LinearMap.coprod, setOf, instModuleTangentSpace._aux_1, ContinuousLinearMap.coprod, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4, ContinuousLinearMap.coprod_inl_inr
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
hf : MDiffAt f p
⊢ HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2)) (β :=
      TangentSpace (I.prod I') p →L[𝕜] TangentSpace (I.prod I') (p.1, p.2))
      (ContinuousLinearMap.prod (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) 0 :
        TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2))
      (ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) :
        TangentSpace (I.prod I') p →L[𝕜] Prod.{u_2, u_5} (TangentSpace I p.1) (TangentSpace I' p.2)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace (I.prod I') (p.1, p.2))

Tactic:
exact ContinuousLinearMap.coprod_inl_inr

Premises used: ContinuousLinearMap.coprod_inl_inr
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
hf : MDiffAt f p
rw :
  HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
      ((mfderiv% fun (z : M × M') ↦ f (z.1, p.2)) p) ((mfderiv% fun (z : M × M') ↦ f (p.1, z.2)) p) =
    HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2))) (β :=
      TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := TangentSpace I p.1)
          ((mfderiv% fun (z : M) ↦ f (z, p.2)) p.1) (id (ContinuousLinearMap.fst 𝕜 E E')) :
        TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := TangentSpace I' p.2)
          ((mfderiv% fun (z : M') ↦ f (p.1, z)) p.2) (id (ContinuousLinearMap.snd 𝕜 E E')) :
        TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
⊢ mfderiv% f p =
    HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2))) (β :=
      TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := TangentSpace I p.1)
          ((mfderiv% fun (z : M) ↦ f (z, p.2)) p.1) (id (ContinuousLinearMap.fst 𝕜 E E')) :
        TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := TangentSpace I' p.2)
          ((mfderiv% fun (z : M') ↦ f (p.1, z)) p.2) (id (ContinuousLinearMap.snd 𝕜 E E')) :
        TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))

Tactic:
rw [mfderiv_prod_eq_add hf]

Premises used: mfderiv_prod_eq_add