awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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 (α := 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)⟩
have 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')
Tactic: simp only [tangentMap, mfderiv_prod_left, TotalSpace.mk_inj]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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₀))
have 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₀))
Tactic: refine (mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_id).trans ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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₀, 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₀))
have 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₀))
Tactic: rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inr]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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₀))
⊢ 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₀))
have 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₀))
Tactic: rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inr]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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₀))
⊢ 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₀))
have 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₀)))
Tactic: rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inr]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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 (α := 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'))⟩
have 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')
Tactic: simp only [tangentMap, mfderiv_prod_right, TotalSpace.mk_inj]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
⊢ 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)
have 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)))
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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 →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)))
have 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)
Tactic: symm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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 →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)
have 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))
Tactic: convert! ContinuousLinearMap.comp_id <| mfderiv% f (p.1, p.2)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
⊢ 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)))
have 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)))
Tactic: rw [mfderiv_prod_eq_add hf]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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'' (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)))
have 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')))
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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')))
⊢ 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)))
have 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')))
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (hypothesis)
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 →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')))
have this : 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