awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.NormedSpace (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
f g : M → 𝕜
x : M
hf : MDiffAt f x
hg : MDiffAt g x
v : TangentSpace I x
⊢ Eq.{u_1 + 1} (α := 𝕜) ((d% (f * g) x : (a : TangentSpace I x) → 𝕜) v : 𝕜)
    ((HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x) 𝕜) (f x) (d% g x) +
            HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x) 𝕜) (g x)
              (d% f x) :
          (a : TangentSpace I x) → 𝕜)
        v :
      𝕜)
have h : Eq.{u_1 + 1} (α := 𝕜)
  (((↑(NormedSpace.fromTangentSpace ((f • g) x)) : TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x) →L[𝕜] 𝕜) ∘SL
          HAdd.hAdd (β :=
            ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x)
              (TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x)))
            (HSMul.hSMul (β :=
              ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                (TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x)))
              (f x)
              ((↑(ContinuousLinearEquiv.symm (NormedSpace.fromTangentSpace ((f • g) x))) :
                  𝕜 →L[𝕜] TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x)) ∘SL
                (↑(NormedSpace.fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, 𝕜) (g x) →L[𝕜] 𝕜) ∘SL mfderiv% g x))
            (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
                (ContinuousLinearMap.toSpanSingleton 𝕜
                    ((ContinuousLinearEquiv.symm (NormedSpace.fromTangentSpace ((f • g) x)) :
                        (a : 𝕜) → TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x))
                      (g x)) :
                  𝕜 →L[𝕜] TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x))
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := TangentSpace 𝓘(𝕜, 𝕜) (f x))
                    (↑(NormedSpace.fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) (mfderiv% f x) :
                  ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x) 𝕜) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                (TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x))) :
        (a : TangentSpace I x) → 𝕜)
      v :
    𝕜)
  ((HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x) 𝕜) (f x)
            ((↑(NormedSpace.fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, 𝕜) (g x) →L[𝕜] 𝕜) ∘SL mfderiv% g x) +
          HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x) 𝕜) (g x)
            ((↑(NormedSpace.fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) ∘SL mfderiv% f x) :
        (a : TangentSpace I x) → 𝕜)
      v :
    𝕜)
Tactic: simp only [mvfderiv, ← smul_eq_mul, mfderiv_smul hf hg]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.NormedSpace (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
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
x : M
⊢ HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (d% 0 x) (d% 0 x) =
    d% 0 x
have rw : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F)
  (d% (HAdd.hAdd (α := M → F) 0 0) x) (d% 0 x)
Tactic: rw [← mvfderiv_add (by exact mdifferentiable_const ..) (by exact mdifferentiable_const ..)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.NormedSpace (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
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
x : M
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (d% 0 x) 0
have this : HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (d% 0 x) (d% 0 x) = d% 0 x
Tactic: have : d% (0 : M → F) x + d% (0 : M → F) x = d% (0 : M → F) x := by
    rw [← mvfderiv_add (by exact mdifferentiable_const ..) (by exact mdifferentiable_const ..)]
    simp
-- 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
x : M
⊢ HasMFDerivAt I I id x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
have refine : HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range (↑I : H → E))
  ((↑(extChartAt I x) : M → E) x)
Tactic: refine ⟨continuousAt_id, ?_⟩
-- 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
x : M
⊢ ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y
have apply : (extChartAt I x).target ⊆
  {x_1 : E | (fun (y : E) ↦ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y) x_1}
Tactic: apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin x)
-- 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
x : M
⊢ (extChartAt I x).target ⊆
    {x_1 : E | (fun (y : E) ↦ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y) x_1}
have mfld_set_tac : ∀ ⦃my_y : E⦄,
  my_y ∈ (extChartAt I x).target →
    Membership.mem (γ := Set E)
      {x_1 : E | (fun (y : E) ↦ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y) x_1} my_y
Tactic: mfld_set_tac
-- 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
x : M
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ :
  ∀ ⦃my_y : E⦄,
    my_y ∈ (extChartAt I x).target →
      Membership.mem (γ := Set E)
        {x_1 : E | (fun (y : E) ↦ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y) x_1} my_y
⊢ (extChartAt I x).target ⊆
    {x_1 : E | (fun (y : E) ↦ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y) x_1}
have mfld_set_tac₃ : ∀ ⦃my_y : E⦄,
  my_y ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) my_y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target →
    Membership.mem (γ := Set E)
      {x_1 : E | (fun (y : E) ↦ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y) x_1} my_y
Tactic: mfld_set_tac
-- 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
x : M
⊢ HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)
have this : ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
  ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y
Tactic: have : ∀ᶠ y in 𝓝[range I] (extChartAt I x) x, (extChartAt I x ∘ (extChartAt I x).symm) y = y := by
    apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin x)
    mfld_set_tac
-- 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
x : M
this :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y
⊢ HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)
have apply : ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) ((↑(extChartAt I x) : M → E) x) =
  id ((↑(extChartAt I x) : M → E) x)
Tactic: apply HasFDerivWithinAt.congr_of_eventuallyEq (hasFDerivWithinAt_id _ _) 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
s : Set M
x : M
hxs : UniqueMDiffWithinAt I s x
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderivWithin I I id s x)
    (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
have rw : Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
Tactic: rw [MDifferentiable.mfderivWithin mdifferentiableAt_id hxs]
-- 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
⊢ Eq (α := TangentBundle I M → TangentBundle I M) (tangentMap I I id) id
have h : ∀ (x : M) (v : TangentSpace I x), tangentMap I I id ⟨x, v⟩ = id ⟨x, v⟩
Tactic: ext1 ⟨x, v⟩
-- 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
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
⊢ ⟨p.proj (E := TangentSpace I),
      (mfderivWithin I I id s (p.proj (E := TangentSpace I)) : (a : TangentSpace I p.proj) → TangentSpace I p.proj)
        (p.snd (E := TangentSpace I))⟩ =
    p
have rw : ⟨p.proj (E := TangentSpace I),
    (ContinuousLinearMap.id 𝕜 (TangentSpace I (p.proj (E := TangentSpace I))) :
        (a : TangentSpace I p.proj) → TangentSpace I p.proj)
      (p.snd (E := TangentSpace I))⟩ =
  p
Tactic: rw [mfderivWithin_id]
-- 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
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
⊢ ⟨p.proj (E := TangentSpace I),
      (ContinuousLinearMap.id 𝕜 (TangentSpace I (p.proj (E := TangentSpace I))) :
          (a : TangentSpace I p.proj) → TangentSpace I p.proj)
        (p.snd (E := TangentSpace I))⟩ =
    p
have rcases : ∀ (proj : M) (snd : TangentSpace I proj)
  (hs : UniqueMDiffWithinAt I s (TotalSpace.proj (F := E) (E := TangentSpace I) ⟨proj, snd⟩)),
  Eq (α := TangentBundle I M)
    ⟨TotalSpace.proj (F := E) (E := TangentSpace I) ⟨proj, snd⟩,
      (ContinuousLinearMap.id 𝕜 (TangentSpace I (TotalSpace.proj (F := E) (E := TangentSpace I) ⟨proj, snd⟩)) :
          (a : TangentSpace I ⟨proj, snd⟩.proj) → TangentSpace I ⟨proj, snd⟩.proj)
        (TotalSpace.snd (E := TangentSpace I) ⟨proj, snd⟩)⟩
    ⟨proj, snd⟩
Tactic: rcases p with ⟨⟩
Cleared hypotheses: p, hs
-- 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''
x : M
f : M → M'
g : M → M''
hf : MDiffAt f x
hg : MDiffAt g x
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
    ((mfderiv% fun (x : M) ↦ (f x, g x)) x : TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
    (ContinuousLinearMap.prod (mfderiv% f x) (mfderiv% g x) :
      TangentSpace I x →L[𝕜] Prod.{u_5, u_8} (TangentSpace I' (f x)) (TangentSpace I'' (g x)))
have simp_rw : Eq (α := TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
  (mfderivWithin I (I'.prod I'') (M' := M' × M'') (fun (x : M) ↦ (f x, g x)) univ x :
    TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
  (ContinuousLinearMap.prod (mfderivWithin I I' f univ x) (mfderivWithin I I'' g univ x) :
    TangentSpace I x →L[𝕜] Prod.{u_5, u_8} (TangentSpace I' (f x)) (TangentSpace I'' (g x)))
Tactic: simp_rw [← mfderivWithin_univ]
-- 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 × M'
⊢ HasMFDerivAt (I.prod I') I Prod.fst x (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
have refine : HasFDerivWithinAt (𝕜 := 𝕜) (writtenInExtChartAt (I.prod I') I x Prod.fst)
  (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
  (range (↑(I.prod I') : ModelProd H H' → E × E')) ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x)
Tactic: refine ⟨continuous_fst.continuousAt, ?_⟩
-- 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 × M'
⊢ ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1
have h : ∀ (y : E × E') (hy : y ∈ (extChartAt (I.prod I') x).target),
  ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1
Tactic: filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
-- 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'
x : M × M'
y : E × E'
hy : y ∈ (extChartAt (I.prod I') x).target
⊢ ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1
have hy₁ : y ∈ ((extChartAt I x.1).prod (extChartAt I' x.2)).target
Tactic: rw [extChartAt_prod] at hy
Cleared hypotheses: hy
-- 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'
x : M × M'
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (writtenInExtChartAt (I.prod I') I x Prod.fst)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
    (range (↑(I.prod I') : ModelProd H H' → E × E')) ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x)
have this : ∀ᶠ (y : E × E') in 𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
  ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1
Tactic: have :
    ∀ᶠ y in 𝓝[range (I.prod I')] extChartAt (I.prod I') x x,
      (extChartAt I x.1 ∘ Prod.fst ∘ (extChartAt (I.prod I') x).symm) y = y.1 := by
    /- porting note: was
    apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin (I.prod I') x)
    mfld_set_tac
    -/
    filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
    rw [extChartAt_prod] at hy
    exact (extChartAt I x.1).right_inv hy.1
-- 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 × M'
this :
  ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (writtenInExtChartAt (I.prod I') I x Prod.fst)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
    (range (↑(I.prod I') : ModelProd H H' → E × E')) ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x)
have apply : ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M'))
    ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x) =
  ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x).1
Tactic: apply HasFDerivWithinAt.congr_of_eventuallyEq hasFDerivWithinAt_fst 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
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'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
⊢ Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I x.1) (mfderivWithin (I.prod I') I Prod.fst s x)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
have rw : Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I x.1) (mfderiv% Prod.fst x)
  (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
Tactic: rw [MDifferentiable.mfderivWithin mdifferentiableAt_fst hxs]
-- 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.prod I') (M × M')
⊢ Eq (α := TangentBundle I M) (tangentMap (I.prod I') I Prod.fst p)
    ⟨p.proj (E := TangentSpace (I.prod I')).1, p.snd (E := TangentSpace (I.prod I')).1⟩
have simp : ((ContinuousLinearMap.fst 𝕜 (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
          (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
        Prod.{u_2, u_5} (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
            (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) →L[𝕜]
          TangentSpace I p.proj (E := TangentSpace (I.prod I')).1) :
      (a : TangentSpace (I.prod I') p.proj) → TangentSpace I p.proj.1)
    (p.snd (E := TangentSpace (I.prod I'))) =
  p.snd (E := TangentSpace (I.prod I')).1
Tactic: simp [tangentMap]
-- 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'
s : Set (M × M')
p : TangentBundle (I.prod I') (M × M')
hs : UniqueMDiffWithinAt (I.prod I') s (p.proj (E := TangentSpace (I.prod I')))
⊢ Eq (α := TangentBundle I M)
    ⟨p.proj (E := TangentSpace (I.prod I')).1,
      (mfderivWithin (I.prod I') I Prod.fst s (p.proj (E := TangentSpace (I.prod I'))) :
          (a : TangentSpace (I.prod I') p.proj) → TangentSpace I p.proj.1)
        (p.snd (E := TangentSpace (I.prod I')))⟩
    ⟨p.proj (E := TangentSpace (I.prod I')).1, p.snd (E := TangentSpace (I.prod I')).1⟩
have rw : Eq (α := TangentBundle I M)
  ⟨p.proj (E := TangentSpace (I.prod I')).1,
    ((ContinuousLinearMap.fst 𝕜 (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
            (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
          Prod.{u_2, u_5} (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
              (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) →L[𝕜]
            TangentSpace I p.proj (E := TangentSpace (I.prod I')).1) :
        (a : TangentSpace (I.prod I') p.proj) → TangentSpace I p.proj.1)
      (p.snd (E := TangentSpace (I.prod I')))⟩
  ⟨p.proj (E := TangentSpace (I.prod I')).1, p.snd (E := TangentSpace (I.prod I')).1⟩
Tactic: rw [mfderivWithin_fst]