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'
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
e_a :
  Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
    ((mfderiv% fun (z : M × M') ↦ f (z.1, p.2)) p)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := TangentSpace I p.1) ((mfderiv% fun (z : M) ↦ f (z, p.2)) p.1)
      (id (ContinuousLinearMap.fst 𝕜 E E')))
e_a₁ :
  Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
    ((mfderiv% fun (z : M × M') ↦ f (p.1, z.2)) p)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := TangentSpace I' p.2)
      ((mfderiv% fun (z : M') ↦ f (p.1, z)) p.2) (id (ContinuousLinearMap.snd 𝕜 E E')))
⊢ 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)))

Tactic:
congr
-- 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 (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (z.1, p.2)) ((fun (z : M) ↦ f (z, p.2)) ∘ Prod.fst)

Tactic:
have : (fun z : M × M' ↦ f (z.1, p.2)) = (fun z : M ↦ f (z, p.2)) ∘ Prod.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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (z.1, p.2)) ((fun (z : M) ↦ f (z, p.2)) ∘ Prod.fst)
e_a :
  Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I p.1) ((mfderiv% fun (z : M) ↦ f (z, p.2)) p.1)
        (mfderiv% Prod.fst p) :
      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)))
e_a₁ : (MDiffAt fun (z : M) ↦ f (z, p.2)) p.1
e_a₂ : MDiffAt Prod.fst p
⊢ Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
    ((mfderiv% fun (z : M × M') ↦ f (z.1, p.2)) p)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := TangentSpace I p.1) ((mfderiv% fun (z : M) ↦ f (z, p.2)) p.1)
      (id (ContinuousLinearMap.fst 𝕜 E E')))

Tactic:
rw [this, mfderiv_comp (I' := I)]

Premises used: mfderiv_comp
-- 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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (z.1, p.2)) ((fun (z : M) ↦ f (z, p.2)) ∘ Prod.fst)
e_a :
  Eq (α := 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)
        (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' 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)
        (ContinuousLinearMap.fst 𝕜 E E') :
      TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
⊢ Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I p.1) ((mfderiv% fun (z : M) ↦ f (z, p.2)) p.1)
        (mfderiv% Prod.fst p) :
      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)))

Tactic:
simp only [mfderiv_fst, id_eq]

Premises used: mfderiv_fst, id_eq
-- 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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (z.1, p.2)) ((fun (z : M) ↦ f (z, p.2)) ∘ Prod.fst)
⊢ Eq (α := 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)
        (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' 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)
        (ContinuousLinearMap.fst 𝕜 E E') :
      TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))

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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (z.1, p.2)) ((fun (z : M) ↦ f (z, p.2)) ∘ Prod.fst)
⊢ (MDiffAt fun (z : M) ↦ f (z, p.2)) p.1

Tactic:
hf.comp _ (mdifferentiableAt_id.prodMk mdifferentiableAt_const)

Premises used: MDifferentiableAt.prodMk, mdifferentiableAt_const, mdifferentiableAt_id, MDifferentiableAt.comp
-- 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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (z.1, p.2)) ((fun (z : M) ↦ f (z, p.2)) ∘ Prod.fst)
⊢ (MDiffAt fun (z : M) ↦ f (z, p.2)) p.1

Tactic:
exact hf.comp _ (mdifferentiableAt_id.prodMk mdifferentiableAt_const)

Premises used: MDifferentiableAt.prodMk, mdifferentiableAt_const, mdifferentiableAt_id, MDifferentiableAt.comp
-- 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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (z.1, p.2)) ((fun (z : M) ↦ f (z, p.2)) ∘ Prod.fst)
⊢ MDiffAt Prod.fst p

Tactic:
mdifferentiableAt_fst

Premises used: mdifferentiableAt_fst
-- 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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (z.1, p.2)) ((fun (z : M) ↦ f (z, p.2)) ∘ Prod.fst)
⊢ MDiffAt Prod.fst p

Tactic:
exact mdifferentiableAt_fst

Premises used: mdifferentiableAt_fst
-- 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 (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (p.1, z.2)) ((fun (z : M') ↦ f (p.1, z)) ∘ Prod.snd)

Tactic:
have : (fun z : M × M' ↦ f (p.1, z.2)) = (fun z : M' ↦ f (p.1, z)) ∘ Prod.snd := 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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (p.1, z.2)) ((fun (z : M') ↦ f (p.1, z)) ∘ Prod.snd)
e_a :
  Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' p.2) ((mfderiv% fun (z : M') ↦ f (p.1, z)) p.2)
        (mfderiv% Prod.snd p) :
      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)))
e_a₁ : (MDiffAt fun (z : M') ↦ f (p.1, z)) p.2
e_a₂ : MDiffAt Prod.snd p
⊢ Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
    ((mfderiv% fun (z : M × M') ↦ f (p.1, z.2)) p)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := TangentSpace I' p.2)
      ((mfderiv% fun (z : M') ↦ f (p.1, z)) p.2) (id (ContinuousLinearMap.snd 𝕜 E E')))

Tactic:
rw [this, mfderiv_comp (I' := I')]

Premises used: mfderiv_comp
-- 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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (p.1, z.2)) ((fun (z : M') ↦ f (p.1, z)) ∘ Prod.snd)
e_a :
  Eq (α := 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)
        (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) :
      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) (ContinuousLinearMap.snd 𝕜 E E') :
      TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
⊢ Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' p.2) ((mfderiv% fun (z : M') ↦ f (p.1, z)) p.2)
        (mfderiv% Prod.snd p) :
      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:
simp only [mfderiv_snd, id_eq]

Premises used: mfderiv_snd, id_eq
-- 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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (p.1, z.2)) ((fun (z : M') ↦ f (p.1, z)) ∘ Prod.snd)
⊢ Eq (α := 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)
        (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) :
      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) (ContinuousLinearMap.snd 𝕜 E E') :
      TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))

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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (p.1, z.2)) ((fun (z : M') ↦ f (p.1, z)) ∘ Prod.snd)
⊢ (MDiffAt fun (z : M') ↦ f (p.1, z)) p.2

Tactic:
hf.comp _ (mdifferentiableAt_const.prodMk mdifferentiableAt_id)

Premises used: MDifferentiableAt.prodMk, mdifferentiableAt_const, mdifferentiableAt_id, MDifferentiableAt.comp
-- 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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (p.1, z.2)) ((fun (z : M') ↦ f (p.1, z)) ∘ Prod.snd)
⊢ (MDiffAt fun (z : M') ↦ f (p.1, z)) p.2

Tactic:
exact hf.comp _ (mdifferentiableAt_const.prodMk mdifferentiableAt_id)

Premises used: MDifferentiableAt.prodMk, mdifferentiableAt_const, mdifferentiableAt_id, MDifferentiableAt.comp
-- 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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (p.1, z.2)) ((fun (z : M') ↦ f (p.1, z)) ∘ Prod.snd)
⊢ MDiffAt Prod.snd p

Tactic:
mdifferentiableAt_snd

Premises used: mdifferentiableAt_snd
-- 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
this : Eq (α := (z : M × M') → M'') (fun (z : M × M') ↦ f (p.1, z.2)) ((fun (z : M') ↦ f (p.1, z)) ∘ Prod.snd)
⊢ MDiffAt Prod.snd p

Tactic:
exact mdifferentiableAt_snd

Premises used: mdifferentiableAt_snd