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
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
apply : Differentiable 𝕜 (F := F₂) fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2
⊢ DifferentiableWithinAt 𝕜 (F := F₂) (fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2) univ (g x, f x)

Tactic:
apply (Differentiable.differentiableAt _).differentiableWithinAt

Premises used: Differentiable.differentiableAt, DifferentiableAt.differentiableWithinAt
-- 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_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
⊢ Differentiable 𝕜 (F := F₂) fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2

Tactic:
differentiable_fst.clm_apply differentiable_snd

Premises used: differentiable_snd, Differentiable.clm_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_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
⊢ Differentiable 𝕜 (F := F₂) fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2

Tactic:
exact differentiable_fst.clm_apply differentiable_snd

Premises used: Differentiable.clm_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_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
⊢ MapsTo (β := (F₁ →L[𝕜] F₂) × F₁) (fun (x : M) ↦ (g x, f x)) univ univ

Tactic:
simp_rw [mapsTo_univ]

Premises used: Set.mapsTo_univ
-- 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_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
hg : MDiff[s] g
hf : MDiff[s] f
⊢ MDiff[s] fun (x : M) ↦ (g x : (a : F₁) → F₂) (f x)

Tactic:
fun x hx ↦ (hg x hx).clm_apply (hf x hx)

Premises used: MDifferentiableOn, MDifferentiableWithinAt.clm_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_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₁
hg : MDiff g
hf : MDiff f
⊢ MDiff fun (x : M) ↦ (g x : (a : F₁) → F₂) (f x)

Tactic:
fun x ↦ (hg x).clm_apply (hf x)

Premises used: MDifferentiable, MDifferentiableAt.clm_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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_17
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
f : M → F₁ ≃L[𝕜] F₂
g : M → F₃ ≃L[𝕜] F₄
s : Set M
x : M
hf : (MDiffAt[s] fun (x : M) ↦ (↑(f x).symm : F₂ →L[𝕜] F₁)) x
hg : (MDiffAt[s] fun (x : M) ↦ (↑(g x) : F₃ →L[𝕜] F₄)) x
⊢ (MDiffAt[s] fun (y : M) ↦ (↑((f y).arrowCongr (g y)) : (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) x

Tactic:
show MDifferentiableWithinAt I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄))
    (fun y ↦ (((f y).symm : F₂ →L[𝕜] F₁).precomp F₄).comp ((g y : F₃ →L[𝕜] F₄).postcomp F₁)) s x
  from hf.clm_precomp (F₃ := F₄) |>.clm_comp <| hg.clm_postcomp (F₁ := F₁)

Premises used: ContinuousLinearMap.comp, MDifferentiableWithinAt.clm_precomp, MDifferentiableWithinAt.clm_comp, MDifferentiableWithinAt.clm_postcomp, ContinuousLinearEquiv.toContinuousLinearMap
-- 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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_17
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
f : M → F₁ ≃L[𝕜] F₂
g : M → F₃ ≃L[𝕜] F₄
x : M
hf : (MDiffAt fun (x : M) ↦ (↑(f x).symm : F₂ →L[𝕜] F₁)) x
hg : (MDiffAt fun (x : M) ↦ (↑(g x) : F₃ →L[𝕜] F₄)) x
⊢ (MDiffAt fun (y : M) ↦ (↑((f y).arrowCongr (g y)) : (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) x

Tactic:
show MDifferentiableAt I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄))
    (fun y ↦ (((f y).symm : F₂ →L[𝕜] F₁).precomp F₄).comp ((g y : F₃ →L[𝕜] F₄).postcomp F₁)) x
  from hf.clm_precomp (F₃ := F₄) |>.clm_comp <| hg.clm_postcomp (F₁ := F₁)

Premises used: ContinuousLinearMap.comp, MDifferentiableAt.clm_postcomp, MDifferentiableAt.clm_comp, MDifferentiableAt.clm_precomp, ContinuousLinearEquiv.toContinuousLinearMap
-- 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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_17
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
f : M → F₁ ≃L[𝕜] F₂
g : M → F₃ ≃L[𝕜] F₄
s : Set M
hf : MDiff[s] fun (x : M) ↦ (↑(f x).symm : F₂ →L[𝕜] F₁)
hg : MDiff[s] fun (x : M) ↦ (↑(g x) : F₃ →L[𝕜] F₄)
⊢ MDiff[s] fun (y : M) ↦ (↑((f y).arrowCongr (g y)) : (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)

Tactic:
fun x hx ↦
  (hf x hx).cle_arrowCongr (hg x hx)

Premises used: MDifferentiableWithinAt.cle_arrowCongr, MDifferentiableOn
-- 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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_17
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
f : M → F₁ ≃L[𝕜] F₂
g : M → F₃ ≃L[𝕜] F₄
hf : MDiff fun (x : M) ↦ (↑(f x).symm : F₂ →L[𝕜] F₁)
hg : MDiff fun (x : M) ↦ (↑(g x) : F₃ →L[𝕜] F₄)
⊢ MDiff fun (y : M) ↦ (↑((f y).arrowCongr (g y)) : (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)

Tactic:
fun x ↦
  (hf x).cle_arrowCongr (hg x)

Premises used: MDifferentiableAt.cle_arrowCongr, MDifferentiable
-- 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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_17
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₄
s : Set M
x : M
hg : MDiffAt[s] g x
hf : MDiffAt[s] f x
⊢ (MDiffAt[s] fun (x : M) ↦ (g x).prodMap (f x)) x

Tactic:
Differentiable.comp_mdifferentiableWithinAt
    (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₄) => x.1.prodMap x.2)
    (f := fun x => (g x, f x)) (ContinuousLinearMap.prodMapL 𝕜 F₁ F₃ F₂ F₄).differentiable
    (hg.prodMk_space hf)

Premises used: MDifferentiableWithinAt.prodMk_space, setOf, ContinuousLinearMap.prodMap, ContinuousLinearMap.differentiable, Differentiable.comp_mdifferentiableWithinAt, ContinuousLinearMap.prod, ContinuousLinearMap.prodMapL
-- 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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_17
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₄
x : M
hg : MDiffAt g x
hf : MDiffAt f x
⊢ (MDiffAt fun (x : M) ↦ (g x).prodMap (f x)) x

Tactic:
Differentiable.comp_mdifferentiableWithinAt
    (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₄) => x.1.prodMap x.2)
    (f := fun x => (g x, f x)) (ContinuousLinearMap.prodMapL 𝕜 F₁ F₃ F₂ F₄).differentiable
    (hg.prodMk_space hf)

Premises used: setOf, MDifferentiableAt, ContinuousLinearMap.prodMap, ContinuousLinearMap.differentiable, MDifferentiableAt.prodMk_space, Differentiable.comp_mdifferentiableWithinAt, ContinuousLinearMap.prod, ContinuousLinearMap.prodMapL, ChartedSpace.LiftPropAt
-- 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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_17
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₄
s : Set M
hg : MDiff[s] g
hf : MDiff[s] f
⊢ MDiff[s] fun (x : M) ↦ (g x).prodMap (f x)

Tactic:
fun x hx ↦ (hg x hx).clm_prodMap (hf x hx)

Premises used: MDifferentiableOn, MDifferentiableWithinAt.clm_prodMap
-- 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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_17
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₄
hg : MDiff g
hf : MDiff f
⊢ MDiff fun (x : M) ↦ (g x).prodMap (f x)

Tactic:
fun x ↦ (hg x).clm_prodMap (hf x)

Premises used: MDifferentiableAt.clm_prodMap, MDifferentiable
-- 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
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
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)
⊢ 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))))

Tactic:
constructor
-- 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
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')
⊢ ContinuousAt (f • g) x

Tactic:
hs.1.smul hg.1

Premises used: ContinuousAt.smul, And.left
-- 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
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')
⊢ ContinuousAt (f • g) x

Tactic:
exact hs.1.smul hg.1

Premises used: ContinuousAt.smul, And.left
-- 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
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')
⊢ 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:
simpa using hs.2.smul hg.2

Premises used: And.right, HasFDerivWithinAt.smul
-- 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
s : Set M
x : M
V : Type u_18
inst_6 : NormedAddCommGroup V
inst_7 : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
⊢ (MDiffAt[s] fun (p : M) ↦ f p • g p) x

Tactic:
((contMDiff_smul.of_le le_top).mdifferentiable one_ne_zero _).comp_mdifferentiableWithinAt x
    (hf.prodMk hg)

Premises used: MDifferentiableAt.comp_mdifferentiableWithinAt, ContMDiff.mdifferentiable, MDifferentiableWithinAt.prodMk, le_top, ContMDiffSMul.contMDiff_smul, ContMDiff.of_le, one_ne_zero
-- 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
⊢ (MDiffAt fun (p : M) ↦ f p • g p) x

Tactic:
((contMDiff_smul.of_le le_top).mdifferentiable one_ne_zero _).comp x (hf.prodMk hg)

Premises used: MDifferentiableAt.prodMk, ContMDiff.mdifferentiable, le_top, ContMDiffSMul.contMDiff_smul, ContMDiff.of_le, MDifferentiableAt.comp, one_ne_zero
-- 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
s : Set M
V : Type u_18
inst_6 : NormedAddCommGroup V
inst_7 : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
hf : MDiff[s] f
hg : MDiff[s] g
⊢ MDiff[s] fun (p : M) ↦ f p • g p

Tactic:
fun x hx ↦ (hf x hx).smul (hg x hx)

Premises used: MDifferentiableOn, MDifferentiableWithinAt.smul
-- 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
V : Type u_18
inst_6 : NormedAddCommGroup V
inst_7 : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
hf : MDiff f
hg : MDiff g
⊢ MDiff fun (p : M) ↦ f p • g p

Tactic:
fun x ↦ (hf x).smul (hg x)

Premises used: MDifferentiableAt.smul, MDifferentiable