awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (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'
f : M → M'
x : M
⊢ ContinuousAt f x ∧
      DifferentiableWithinAtProp I I'
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
        ((↑(chartAt H x) : M → H) x) ↔
    ContinuousAt f x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have a : DifferentiableWithinAtProp I I'
    ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
    ((↑(chartAt H x) : M → H) x) ↔
  DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: congrm _ ∧ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.FDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
x : E
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x))
⊢ HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x f' ↔ HasFDerivAt f f' x
have rw : HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f Set.univ x f' ↔ HasFDerivAt f f' x
Tactic: rw [← hasMFDerivWithinAt_univ, hasMFDerivWithinAt_iff_hasFDerivWithinAt, hasFDerivWithinAt_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.FDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
x : E
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x))
rw : HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f Set.univ x f' ↔ HasFDerivAt f f' x
⊢ HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x f' ↔ HasFDerivAt f f' x
have rw₁ : HasFDerivWithinAt f f' Set.univ x ↔ HasFDerivAt f f' x
Tactic: rw [← hasMFDerivWithinAt_univ, hasMFDerivWithinAt_iff_hasFDerivWithinAt, hasFDerivWithinAt_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.FDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
x : E
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x))
rw : HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f Set.univ x f' ↔ HasFDerivAt f f' x
rw₁ : HasFDerivWithinAt f f' Set.univ x ↔ HasFDerivAt f f' x
⊢ HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x f' ↔ HasFDerivAt f f' x
have rw₂ : HasFDerivAt f f' x ↔ HasFDerivAt f f' x
Tactic: rw [← hasMFDerivWithinAt_univ, hasMFDerivWithinAt_iff_hasFDerivWithinAt, hasFDerivWithinAt_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.FDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
⊢ MDiffAt[s] f x ↔ DifferentiableWithinAt 𝕜 f s x
have simp : ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f s x
Tactic: simp only [mdifferentiableWithinAt_iff', mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.FDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
x : E
⊢ MDiffAt f x ↔ DifferentiableAt 𝕜 f x
have simp : ContinuousAt f x ∧ DifferentiableAt 𝕜 f x ↔ DifferentiableAt 𝕜 f x
Tactic: simp only [mdifferentiableAt_iff, differentiableWithinAt_univ, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.FDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x) (fderivWithin 𝕜 f s x)
have pos : ∀ (h : MDiffAt[s] f x),
  Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x) (fderivWithin 𝕜 f s x)
Tactic: by_cases h : MDiffAt[s] f x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.FDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
pos :
  ∀ (h : MDiffAt[s] f x),
    Eq (α :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
      (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x) (fderivWithin 𝕜 f s x)
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x) (fderivWithin 𝕜 f s x)
have neg : ∀ (h : ¬MDiffAt[s] f x),
  Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x) (fderivWithin 𝕜 f s x)
Tactic: by_cases h : MDiffAt[s] f x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.FDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : ¬MDiffAt[s] f x
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x) (fderivWithin 𝕜 f s x)
have neg : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
  0 (fderivWithin 𝕜 f s x)
Tactic: simp only [mfderivWithin, h, if_neg, not_false_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.FDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : ¬MDiffAt[s] f x
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x))) 0
    (fderivWithin 𝕜 f s x)
have h₁ : ¬DifferentiableWithinAt 𝕜 f s x
Tactic: rw [mdifferentiableWithinAt_iff_differentiableWithinAt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.FDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
x : E
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderiv% f x) (fderiv 𝕜 f x)
have rw : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
  (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f Set.univ x) (fderivWithin 𝕜 f Set.univ x)
Tactic: rw [← mfderivWithin_univ, ← fderivWithin_univ]
-- 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
s : Set M
x : M
F : Type u_18
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
f : M → F
inst_8 : IsManifold I 1 M
hf :
  DifferentiableWithinAt 𝕜 (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ MDiffAt[s] f x
have refine : MDiffAt[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (f ∘ (↑(extChartAt I x).symm : E → M))
  ((↑(extChartAt I x) : M → E) x)
Tactic: refine (mdifferentiableWithinAt_iff_source_of_mem_source (mem_chart_source H x)).2 ?_
-- 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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : MDiffAt[s] g x
hf : MDiffAt[s] f x
⊢ DifferentiableWithinAt 𝕜 (F := F₂) (fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2) univ (g x, f x)
have apply : Differentiable 𝕜 (F := F₂) fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2
Tactic: apply (Differentiable.differentiableAt _).differentiableWithinAt
-- 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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
x : M
hg : MDiffAt g x
hf : MDiffAt f x
⊢ DifferentiableWithinAt 𝕜 (F := F₂) (fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2) univ (g x, f x)
have apply : Differentiable 𝕜 (F := F₂) fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2
Tactic: apply (Differentiable.differentiableAt _).differentiableWithinAt
-- 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
x : M
V : Type u_18
inst_6 : NormedAddCommGroup V
inst_7 : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x) 𝕜
hs :
  HasMFDerivAt I 𝓘(𝕜, 𝕜) f x
    ((↑(ContinuousLinearEquiv.symm (fromTangentSpace (f x))) : 𝕜 →L[𝕜] TangentSpace 𝓘(𝕜, 𝕜) (f x)) ∘SL f')
g' : ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) V
hg :
  HasMFDerivAt I 𝓘(𝕜, V) g x
    ((↑(ContinuousLinearEquiv.symm (fromTangentSpace (g x))) : V →L[𝕜] TangentSpace 𝓘(𝕜, V) (g x)) ∘SL g')
⊢ HasMFDerivAt I 𝓘(𝕜, V) (f • g) x
    (HAdd.hAdd (β :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x)))
      (HSMul.hSMul (β :=
        ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x)))
        (f x)
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            (↑(ContinuousLinearEquiv.symm (fromTangentSpace ((f • g) x))) : V →L[𝕜] TangentSpace 𝓘(𝕜, V) ((f • g) x))
            g' :
          ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x)
            (TangentSpace 𝓘(𝕜, V) ((f • g) x))))
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          (toSpanSingleton 𝕜
            ((ContinuousLinearEquiv.symm (fromTangentSpace ((f • g) x)) : (a : V) → TangentSpace 𝓘(𝕜, V) ((f • g) x))
              (g x)))
          f' :
        ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x))))
have left : ContinuousAt (f • g) x
Tactic: constructor
-- 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
x : M
V : Type u_18
inst_6 : NormedAddCommGroup V
inst_7 : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x) 𝕜
hs :
  HasMFDerivAt I 𝓘(𝕜, 𝕜) f x
    ((↑(ContinuousLinearEquiv.symm (fromTangentSpace (f x))) : 𝕜 →L[𝕜] TangentSpace 𝓘(𝕜, 𝕜) (f x)) ∘SL f')
g' : ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) V
hg :
  HasMFDerivAt I 𝓘(𝕜, V) g x
    ((↑(ContinuousLinearEquiv.symm (fromTangentSpace (g x))) : V →L[𝕜] TangentSpace 𝓘(𝕜, V) (g x)) ∘SL g')
left : ContinuousAt (f • g) x
⊢ HasMFDerivAt I 𝓘(𝕜, V) (f • g) x
    (HAdd.hAdd (β :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x)))
      (HSMul.hSMul (β :=
        ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x)))
        (f x)
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            (↑(ContinuousLinearEquiv.symm (fromTangentSpace ((f • g) x))) : V →L[𝕜] TangentSpace 𝓘(𝕜, V) ((f • g) x))
            g' :
          ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x)
            (TangentSpace 𝓘(𝕜, V) ((f • g) x))))
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          (toSpanSingleton 𝕜
            ((ContinuousLinearEquiv.symm (fromTangentSpace ((f • g) x)) : (a : V) → TangentSpace 𝓘(𝕜, V) ((f • g) x))
              (g x)))
          f' :
        ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x))))
have right : HasFDerivWithinAt (writtenInExtChartAt I 𝓘(𝕜, V) x (f • g))
  (HAdd.hAdd (β :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x)))
    (HSMul.hSMul (β :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x)))
      (f x)
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          (↑(ContinuousLinearEquiv.symm (fromTangentSpace ((f • g) x))) : V →L[𝕜] TangentSpace 𝓘(𝕜, V) ((f • g) x)) g' :
        ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x))))
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        (toSpanSingleton 𝕜
          ((ContinuousLinearEquiv.symm (fromTangentSpace ((f • g) x)) : (a : V) → TangentSpace 𝓘(𝕜, V) ((f • g) x))
            (g x)))
        f' :
      ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x))))
  (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: constructor
-- 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
x : M
V : Type u_18
inst_6 : NormedAddCommGroup V
inst_7 : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
hf : MDiffAt f x
hg : MDiffAt g x
⊢ ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := TangentSpace 𝓘(𝕜, V) ((f • g) x))
      (↑(fromTangentSpace ((f • g) x)) : TangentSpace 𝓘(𝕜, V) ((f • g) x) →L[𝕜] V) (mfderiv% (f • g) x) =
    HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) V) (f x)
        ((↑(fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, V) (g x) →L[𝕜] V) ∘SL mfderiv% g x) +
      ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (toSpanSingleton 𝕜 (g x))
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := TangentSpace 𝓘(𝕜, 𝕜) (f x))
          (↑(fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) (mfderiv% f x))
have rw : ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(fromTangentSpace ((f • g) x)) : TangentSpace 𝓘(𝕜, V) ((f • g) x) →L[𝕜] V)
    (HAdd.hAdd (β :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x)))
      (HSMul.hSMul (β :=
        ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x)))
        (f x)
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            (↑(ContinuousLinearEquiv.symm (fromTangentSpace ((f • g) x))) : V →L[𝕜] TangentSpace 𝓘(𝕜, V) ((f • g) x))
            ((↑(fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, V) (g x) →L[𝕜] V) ∘SL mfderiv% g x) :
          ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x)
            (TangentSpace 𝓘(𝕜, V) ((f • g) x))))
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          (toSpanSingleton 𝕜
              ((ContinuousLinearEquiv.symm (fromTangentSpace ((f • g) x)) : (a : V) → TangentSpace 𝓘(𝕜, V) ((f • g) x))
                (g x)) :
            ContinuousLinearMap.{u_1, u_1, u_1, u_18} (RingHom.id 𝕜) 𝕜 (TangentSpace 𝓘(𝕜, V) ((f • g) x)))
          (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := TangentSpace 𝓘(𝕜, 𝕜) (f x))
              (↑(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_18} (RingHom.id 𝕜) (TangentSpace I x)
          (TangentSpace 𝓘(𝕜, V) ((f • g) x)))) =
  HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) V) (f x)
      ((↑(fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, V) (g x) →L[𝕜] V) ∘SL mfderiv% g x) +
    ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (toSpanSingleton 𝕜 (g x))
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := TangentSpace 𝓘(𝕜, 𝕜) (f x))
        (↑(fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) (mfderiv% f x))
Tactic: rw [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
g g' : M → F
x : M
hg : MDiffAt g x
hg' : MDiffAt g' x
⊢ d% (g + g') x =
    HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (d% g x) (d% g' x)
have simp : HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F)
    ((↑(NormedSpace.fromTangentSpace (g x + g' x)) : TangentSpace 𝓘(𝕜, F) (g x + g' x) →L[𝕜] F) ∘SL mfderiv% g x)
    ((↑(NormedSpace.fromTangentSpace (g x + g' x)) : TangentSpace 𝓘(𝕜, F) (g x + g' x) →L[𝕜] F) ∘SL mfderiv% g' x) =
  HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F)
    ((↑(NormedSpace.fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, F) (g x) →L[𝕜] F) ∘SL mfderiv% g x)
    ((↑(NormedSpace.fromTangentSpace (g' x)) : TangentSpace 𝓘(𝕜, F) (g' x) →L[𝕜] F) ∘SL mfderiv% g' x)
Tactic: simp [mvfderiv, mfderiv_add hg 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
g g' : M → F
x : M
hg : MDiffAt g x
hg' : MDiffAt g' x
⊢ d% (g - g') x =
    HSub.hSub (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (d% g x) (d% g' x)
have simp : HSub.hSub (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F)
    ((↑(NormedSpace.fromTangentSpace (g x - g' x)) : TangentSpace 𝓘(𝕜, F) (g x - g' x) →L[𝕜] F) ∘SL mfderiv% g x)
    ((↑(NormedSpace.fromTangentSpace (g x - g' x)) : TangentSpace 𝓘(𝕜, F) (g x - g' x) →L[𝕜] F) ∘SL mfderiv% g' x) =
  HSub.hSub (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F)
    ((↑(NormedSpace.fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, F) (g x) →L[𝕜] F) ∘SL mfderiv% g x)
    ((↑(NormedSpace.fromTangentSpace (g' x)) : TangentSpace 𝓘(𝕜, F) (g' x) →L[𝕜] F) ∘SL mfderiv% g' x)
Tactic: simp [mvfderiv, mfderiv_sub hg 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
g : M → F
x : M
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (d% (-g) x) (-d% g x)
have simp : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F)
  ((↑(NormedSpace.fromTangentSpace (-g x)) : TangentSpace 𝓘(𝕜, F) (-g x) →L[𝕜] F) ∘SL (-mfderiv% g x))
  (-(↑(NormedSpace.fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, F) (g x) →L[𝕜] F) ∘SL mfderiv% g x)
Tactic: simp [mvfderiv, mfderiv_neg]
-- 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
a : M → 𝕜
ha : MDiffAt a x
g : M → F
hg : MDiffAt g x
⊢ d% (a • g) x =
    HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (a x) (d% g x) +
      ContinuousLinearMap.smulRight (S := 𝕜) (d% a x) (g x)
have h : ∀ (v : TangentSpace I x),
  Eq.{u_8 + 1} (α := F) ((d% (a • g) x : (a : TangentSpace I x) → F) v : F)
    ((HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (a x) (d% g x) +
            ContinuousLinearMap.smulRight (S := 𝕜) (d% a x) (g x) :
          (a : TangentSpace I x) → F)
        v :
      F)
Tactic: ext v
-- 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
⊢ d% (f * g) x =
    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)
have h : ∀ (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 :
      𝕜)
Tactic: ext v