awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
⊢ mfderiv% (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))
            ((↑(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)))

Tactic:
(hf.hasMFDerivAt.smul hg.hasMFDerivAt).mfderiv

Premises used: HasMFDerivAt.smul, HasMFDerivAt.mfderiv, MDifferentiableAt.hasMFDerivAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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 𝕜)
      (↑(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:
rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
⊢ (↑(fromTangentSpace (f x • g x)) : TangentSpace 𝓘(𝕜, V) (f x • g x) →L[𝕜] V) ∘SL 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))

Tactic:
fromTangentSpace_mfderiv_smul hf hg

Premises used: fromTangentSpace_mfderiv_smul, TangentSpace
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
v : TangentSpace I x
⊢ ((fromTangentSpace ((f • g) x) : TangentSpace 𝓘(𝕜, V) ((f • g) x) ≃L[𝕜] V) :
        (a : TangentSpace 𝓘(𝕜, V) ((f • g) x)) → V)
      (((mfderiv% (f • g) x :
              ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x)
                (TangentSpace 𝓘(𝕜, V) ((f • g) x))) :
            (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, V) ((f • g) x))
          v :
        TangentSpace 𝓘(𝕜, V) ((f • g) x)) =
    HSMul.hSMul (β := V) (f x)
        ((fromTangentSpace (g x) : (a : TangentSpace 𝓘(𝕜, V) (g x)) → V)
            (((mfderiv% g x :
                    ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x)
                      (TangentSpace 𝓘(𝕜, V) (g x))) :
                  (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, V) (g x))
                v :
              TangentSpace 𝓘(𝕜, V) (g x)) :
          V) +
      HSMul.hSMul (α := 𝕜)
        ((fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
            (((mfderiv% f x :
                    ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                      (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                  (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
                v :
              TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
          𝕜)
        (g x)

Tactic:
simpa using congr($(fromTangentSpace_mfderiv_smul hf hg) v)
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
v : TangentSpace I x
⊢ (fromTangentSpace (f x • g x) : (a : TangentSpace 𝓘(𝕜, V) (f x • g x)) → V)
      (((mfderiv% (f • g) x :
              ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x)
                (TangentSpace 𝓘(𝕜, V) ((f • g) x))) :
            (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, V) ((f • g) x))
          v :
        TangentSpace 𝓘(𝕜, V) ((f • g) x)) =
    HSMul.hSMul (β := V) (f x)
        ((fromTangentSpace (g x) : (a : TangentSpace 𝓘(𝕜, V) (g x)) → V)
            (((mfderiv% g x :
                    ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x)
                      (TangentSpace 𝓘(𝕜, V) (g x))) :
                  (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, V) (g x))
                v :
              TangentSpace 𝓘(𝕜, V) (g x)) :
          V) +
      HSMul.hSMul (α := 𝕜)
        ((fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
            (((mfderiv% f x :
                    ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                      (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                  (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
                v :
              TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
          𝕜)
        (g x)

Tactic:
fromTangentSpace_mfderiv_smul_apply hf hg v

Premises used: fromTangentSpace_mfderiv_smul_apply
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
c : F
x : M
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) ((d% fun (x : M) ↦ c) x) 0

Tactic:
simp [mvfderiv, mfderiv_const]

Premises used: mvfderiv, mfderiv_const
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
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)
⊢ 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)

Tactic:
simp [mvfderiv, mfderiv_add hg hg']

Premises used: mvfderiv, mfderiv_add
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
⊢ 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:
rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
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)
⊢ 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)

Tactic:
simp [mvfderiv, mfderiv_sub hg hg']

Premises used: mvfderiv, mfderiv_sub
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
⊢ 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:
rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
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)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (d% (-g) x) (-d% g x)

Tactic:
simp [mvfderiv, mfderiv_neg]

Premises used: mvfderiv, mfderiv_neg
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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)
    ((↑(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:
rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
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)
⊢ 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)

Tactic:
ext v
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
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:
simp [mvfderiv, -Pi.smul_apply', fromTangentSpace_mfderiv_smul_apply ha hg]

Premises used: fromTangentSpace_mfderiv_smul_apply, mvfderiv, Pi.smul_apply'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
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 :
        𝕜)
⊢ 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)

Tactic:
ext v
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
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 :
      𝕜)
⊢ 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:
simp only [mvfderiv, ← smul_eq_mul, mfderiv_smul hf hg]

Premises used: mvfderiv, mfderiv_smul, smul_eq_mul