awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
inst_15 : IsManifold I 1 M
inst_16 : VectorBundle 𝕜 F V
cov cov' : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
u : Set M
f : M → 𝕜
n : ℕ∞ω
hf : ContMDiffOn I 𝓘(𝕜, 𝕜) n f u
Hcov : ContMDiffCovariantDerivativeOn F (V := V) n cov u
Hcov' : ContMDiffCovariantDerivativeOn F (V := V) n cov' u
σ : (x : M) → V x
hσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) (n + 1) (fun (x : M) ↦ ⟨x, σ x⟩) u
hs :
  ContMDiffOn I (E' := E × (E →L[𝕜] F)) (I.prod 𝓘(𝕜, E →L[𝕜] F)) (M' :=
    TotalSpace (E →L[𝕜] F) fun (x : M) ↦
      ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    n (fun (x : M) ↦ ⟨x, (f • cov σ) x⟩) u
ht :
  ContMDiffOn I (E' := E × (E →L[𝕜] F)) (I.prod 𝓘(𝕜, E →L[𝕜] F)) (M' :=
    TotalSpace (E →L[𝕜] F) fun (x : M) ↦
      ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    n (fun (x : M) ↦ ⟨x, ((1 - f) • cov' σ) x⟩) u
⊢ ContMDiffOn I (E' := E × (E →L[𝕜] F)) (I.prod 𝓘(𝕜, E →L[𝕜] F)) (M' :=
    TotalSpace (E →L[𝕜] F) fun (x : M) ↦
      ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    n (fun (x : M) ↦ ⟨x, (f • cov σ + (1 - f) • cov' σ) x⟩) u

Tactic:
apply ContMDiffOn.add_section

Premises used: ContMDiffOn.add_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
inst_15 : IsManifold I 1 M
inst_16 : VectorBundle 𝕜 F V
cov cov' : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
u : Set M
f : M → 𝕜
n : ℕ∞ω
hf : ContMDiffOn I 𝓘(𝕜, 𝕜) n f u
Hcov : ContMDiffCovariantDerivativeOn F (V := V) n cov u
Hcov' : ContMDiffCovariantDerivativeOn F (V := V) n cov' u
σ : (x : M) → V x
hσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) (n + 1) (fun (x : M) ↦ ⟨x, σ x⟩) u
⊢ ContMDiffOn I (E' := E × (E →L[𝕜] F)) (I.prod 𝓘(𝕜, E →L[𝕜] F)) (M' :=
    TotalSpace (E →L[𝕜] F) fun (x : M) ↦
      ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    n (fun (x : M) ↦ ⟨x, (f • cov σ) x⟩) u

Tactic:
hf.smul_section <| Hcov.contMDiff hσ

Premises used: ContMDiffCovariantDerivativeOn.contMDiff, ContMDiffOn.smul_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
inst_15 : IsManifold I 1 M
inst_16 : VectorBundle 𝕜 F V
cov cov' : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
u : Set M
f : M → 𝕜
n : ℕ∞ω
hf : ContMDiffOn I 𝓘(𝕜, 𝕜) n f u
Hcov : ContMDiffCovariantDerivativeOn F (V := V) n cov u
Hcov' : ContMDiffCovariantDerivativeOn F (V := V) n cov' u
σ : (x : M) → V x
hσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) (n + 1) (fun (x : M) ↦ ⟨x, σ x⟩) u
⊢ ContMDiffOn I (E' := E × (E →L[𝕜] F)) (I.prod 𝓘(𝕜, E →L[𝕜] F)) (M' :=
    TotalSpace (E →L[𝕜] F) fun (x : M) ↦
      ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    n (fun (x : M) ↦ ⟨x, (f • cov σ) x⟩) u

Tactic:
exact hf.smul_section <| Hcov.contMDiff hσ

Premises used: ContMDiffCovariantDerivativeOn.contMDiff, ContMDiffOn.smul_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
inst_15 : IsManifold I 1 M
inst_16 : VectorBundle 𝕜 F V
cov cov' : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
u : Set M
f : M → 𝕜
n : ℕ∞ω
hf : ContMDiffOn I 𝓘(𝕜, 𝕜) n f u
Hcov : ContMDiffCovariantDerivativeOn F (V := V) n cov u
Hcov' : ContMDiffCovariantDerivativeOn F (V := V) n cov' u
σ : (x : M) → V x
hσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) (n + 1) (fun (x : M) ↦ ⟨x, σ x⟩) u
⊢ ContMDiffOn I (E' := E × (E →L[𝕜] F)) (I.prod 𝓘(𝕜, E →L[𝕜] F)) (M' :=
    TotalSpace (E →L[𝕜] F) fun (x : M) ↦
      ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    n (fun (x : M) ↦ ⟨x, ((1 - f) • cov' σ) x⟩) u

Tactic:
(contMDiffOn_const.sub hf).smul_section <| Hcov'.contMDiff hσ

Premises used: ContMDiffCovariantDerivativeOn.contMDiff, contMDiffOn_const, ContMDiffOn.sub, ContMDiffOn.smul_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
inst_15 : IsManifold I 1 M
inst_16 : VectorBundle 𝕜 F V
cov cov' : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
u : Set M
f : M → 𝕜
n : ℕ∞ω
hf : ContMDiffOn I 𝓘(𝕜, 𝕜) n f u
Hcov : ContMDiffCovariantDerivativeOn F (V := V) n cov u
Hcov' : ContMDiffCovariantDerivativeOn F (V := V) n cov' u
σ : (x : M) → V x
hσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) (n + 1) (fun (x : M) ↦ ⟨x, σ x⟩) u
⊢ ContMDiffOn I (E' := E × (E →L[𝕜] F)) (I.prod 𝓘(𝕜, E →L[𝕜] F)) (M' :=
    TotalSpace (E →L[𝕜] F) fun (x : M) ↦
      ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    n (fun (x : M) ↦ ⟨x, ((1 - f) • cov' σ) x⟩) u

Tactic:
exact (contMDiffOn_const.sub hf).smul_section <| Hcov'.contMDiff hσ

Premises used: ContMDiffCovariantDerivativeOn.contMDiff, contMDiffOn_const, ContMDiffOn.sub, ContMDiffOn.smul_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hx : x ∈ u
rw :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    (∑ i ∈ s, f i x • cov i (σ + σ') x) (∑ x_1 ∈ s, (f x_1 x • cov x_1 σ x + f x_1 x • cov x_1 σ' x))
⊢ ∑ i ∈ s, f i x • cov i (σ + σ') x =
    HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
      (∑ i ∈ s, f i x • cov i σ x) (∑ i ∈ s, f i x • cov i σ' x)

Tactic:
rw [← Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hx : x ∈ u
e_f :
  Eq (α := ι → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    (fun (i : ι) ↦ f i x • cov i (σ + σ') x) fun (x_1 : ι) ↦ f x_1 x • cov x_1 σ x + f x_1 x • cov x_1 σ' x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    (∑ i ∈ s, f i x • cov i (σ + σ') x) (∑ x_1 ∈ s, (f x_1 x • cov x_1 σ x + f x_1 x • cov x_1 σ' x))

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hx : x ∈ u
e_f :
  ∀ (i : ι) (x_1 : TangentSpace I x),
    Eq.{u_6 + 1} (α := V x) ((f i x • cov i (σ + σ') x : (a : TangentSpace I x) → V x) x_1 : V x)
      ((f i x • cov i σ x + f i x • cov i σ' x : (a : TangentSpace I x) → V x) x_1 : V x)
⊢ Eq (α := ι → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    (fun (i : ι) ↦ f i x • cov i (σ + σ') x) fun (x_1 : ι) ↦ f x_1 x • cov x_1 σ x + f x_1 x • cov x_1 σ' x

Tactic:
ext i
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hx : x ∈ u
i : ι
x_1 : TangentSpace I x
e_f :
  Eq.{u_6 + 1} (α := V x) ((f i x • cov i (σ + σ') x : (a : TangentSpace I x) → V x) x_1 : V x)
    ((f i x • (cov i σ x + cov i σ' x) : (a : TangentSpace I x) → V x) x_1 : V x)
e_f₁ e_f₂ :
  Eq.{u_6 + 1} (α := V x) ((f i x • (cov i σ x + cov i σ' x) : (a : TangentSpace I x) → V x) x_1 : V x)
    ((f i x • (cov i σ x + cov i σ' x) : (a : TangentSpace I x) → V x) x_1 : V x)
⊢ Eq.{u_6 + 1} (α := V x) ((f i x • cov i (σ + σ') x : (a : TangentSpace I x) → V x) x_1 : V x)
    ((f i x • cov i σ x + f i x • cov i σ' x : (a : TangentSpace I x) → V x) x_1 : V x)

Tactic:
rw [← smul_add, (h i).add hσ hσ' hx]

Premises used: IsCovariantDerivativeOn.add, smul_add
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
a :
  ∀ (i : ι) (hi : i ∈ s),
    f i x • cov i (g • σ) x =
      g x • f i x • cov i σ x +
        HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f i x)
          (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    (∑ i ∈ s, f i x • cov i (g • σ) x)
    (∑ i ∈ s,
      (g x • f i x • cov i σ x +
        HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f i x)
          (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))))

Tactic:
congr! 1 with i hi
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
i : ι
hi : i ∈ s
a :
  f i x • (g x • cov i σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x)) =
    g x • f i x • cov i σ x +
      HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f i x)
        (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))
⊢ f i x • cov i (g • σ) x =
    g x • f i x • cov i σ x +
      HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f i x)
        (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))

Tactic:
rw [(h i).leibniz hσ hg]

Premises used: IsCovariantDerivativeOn.leibniz
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
i : ι
hi : i ∈ s
a : f i x • g x • cov i σ x = g x • f i x • cov i σ x
⊢ f i x • (g x • cov i σ x + ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x)) =
    g x • f i x • cov i σ x +
      HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f i x)
        (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))

Tactic:
simp [mvfderiv]

Premises used: mvfderiv
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
i : ι
hi : i ∈ s
⊢ f i x • g x • cov i σ x = g x • f i x • cov i σ x

Tactic:
module
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
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_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
rw :
  HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (g x)
        (∑ i ∈ s, f i x • cov i σ x) +
      HSMul.hSMul (α := 𝕜) (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (1 x)
        (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x)) =
    HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (g x)
        (∑ i ∈ s, f i x • cov i σ x) +
      ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x)
⊢ HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (g x)
        (∑ i ∈ s, f i x • cov i σ x) +
      HSMul.hSMul (α := 𝕜) (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
        ((∑ i ∈ s, f i) x) (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x)) =
    HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (g x)
        (∑ i ∈ s, f i x • cov i σ x) +
      ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x)

Tactic:
rw [hf]