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'
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)))
    ((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 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)))
Tactic: rw [this, mfderiv_comp (I' := I)]
-- 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
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)))
⊢ 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 e_a₁ : (MDiffAt fun (z : M) ↦ f (z, p.2)) p.1
Tactic: rw [this, mfderiv_comp (I' := I)]
-- 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
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
⊢ 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 e_a₂ : MDiffAt Prod.fst p
Tactic: rw [this, mfderiv_comp (I' := I)]
-- 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
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 (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)))
have 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)))
Tactic: simp only [mfderiv_fst, id_eq]
-- 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 (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')))
have this : 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
-- 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
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)))
    ((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')))
have 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)))
Tactic: rw [this, mfderiv_comp (I' := I')]
-- 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
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)))
⊢ 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')))
have e_a₁ : (MDiffAt fun (z : M') ↦ f (p.1, z)) p.2
Tactic: rw [this, mfderiv_comp (I' := I')]
-- 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
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
⊢ 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')))
have e_a₂ : MDiffAt Prod.snd p
Tactic: rw [this, mfderiv_comp (I' := I')]
-- 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
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 (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)))
have 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)))
Tactic: simp only [mfderiv_snd, id_eq]
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
y : E
hy : y ∈ t
⊢ writtenInExtChartAt (M := M ⊕ M') I I (Sum.inl x) Sum.swap y = id y
have simp : Function.comp (β := M' ⊕ M)
    (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I) : M' ⊕ M → E)
    (Sum.swap ∘
      (↑(PartialEquiv.symm
            (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I)) :
        E → M ⊕ M'))
    y =
  id y
Tactic: simp only [writtenInExtChartAt, extChartAt, Sum.swap_inl,
          ChartedSpace.sum_chartAt_inl, ChartedSpace.sum_chartAt_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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
y : E
hy : y ∈ t
⊢ Function.comp (β := M' ⊕ M)
      (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M' ⊕ M → E)
      (Sum.swap ∘
        (↑(PartialEquiv.symm
              (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
          E → M ⊕ M'))
      y =
    id y
have dsimp : (↑I : H → E)
    (Function.extend Sum.inr (↑(chartAt H x) : M → H) (fun (x_1 : M' ⊕ M) ↦ Classical.arbitrary H)
      (Sum.inr ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y)))) =
  y
Tactic: dsimp
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
y : E
hy : y ∈ t
⊢ (↑I : H → E)
      (Function.extend Sum.inr (↑(chartAt H x) : M → H) (fun (x_1 : M' ⊕ M) ↦ Classical.arbitrary H)
        (Sum.inr ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y)))) =
    y
have rw : (↑I : H → E) ((↑I.symm : E → H) y) = y
Tactic: rw [Sum.inr_injective.extend_apply, (chartAt H x).right_inv (by grind)]
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
⊢ writtenInExtChartAt (M := M ⊕ M') I I (Sum.inl x)
      Sum.swap =ᶠ[𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))]
    id
have this : EqOn (writtenInExtChartAt (M := M ⊕ M') I I (Sum.inl x) Sum.swap) id t
Tactic: have : EqOn (writtenInExtChartAt I I (Sum.inl x) (@Sum.swap M M')) id t := by
        intro y hy
        simp only [writtenInExtChartAt, extChartAt, Sum.swap_inl,
          ChartedSpace.sum_chartAt_inl, ChartedSpace.sum_chartAt_inr]
        dsimp
        rw [Sum.inr_injective.extend_apply, (chartAt H x).right_inv (by grind)]
        exact I.right_inv (by grind)
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
this : EqOn (writtenInExtChartAt (M := M ⊕ M') I I (Sum.inl x) Sum.swap) id t
⊢ writtenInExtChartAt (M := M ⊕ M') I I (Sum.inl x)
      Sum.swap =ᶠ[𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))]
    id
have apply : t ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))
Tactic: apply Filter.eventually_of_mem ?_ this
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
this : EqOn (writtenInExtChartAt (M := M ⊕ M') I I (Sum.inl x) Sum.swap) id t
⊢ t ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))
have rw : (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x)) ∧
  range (↑I : H → E) ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))
Tactic: rw [Filter.inter_mem_iff]
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
this : EqOn (writtenInExtChartAt (M := M ⊕ M') I I (Sum.inl x) Sum.swap) id t
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
      𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x)) ∧
    range (↑I : H → E) ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))
have refine : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
  𝓝 ((↑I.symm : E → H) ((↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))))
Tactic: refine ⟨I.continuousWithinAt_symm.preimage_mem_nhdsWithin ?_, self_mem_nhdsWithin⟩