mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

Goal state before:
pp: 𝕜 : Type u_1
inst✝³¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³⁰ : NormedAddCommGroup E
inst✝²⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝²⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝²⁷ : TopologicalSpace M
inst✝²⁶ : ChartedSpace H M
F : Type u_5
inst✝²⁵ : NormedAddCommGroup F
inst✝²⁴ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝²³ : TopologicalSpace (TotalSpace F V)
inst✝²² : (x : M) → AddCommGroup (V x)
inst✝²¹ : (x : M) → Module 𝕜 (V x)
inst✝²⁰ : (x : M) → TopologicalSpace (V x)
inst✝¹⁹ : FiberBundle F V
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
inst✝¹⁶ : TopologicalSpace (TotalSpace F' V')
inst✝¹⁵ : (x : M) → AddCommGroup (V' x)
inst✝¹⁴ : (x : M) → Module 𝕜 (V' x)
inst✝¹³ : (x : M) → TopologicalSpace (V' x)
inst✝¹² : FiberBundle F' V'
A : Type u_9
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Module 𝕜 A
Φ✝ : ((x : M) → V x) → A
x✝ : M
inst✝⁹ : VectorBundle 𝕜 F V
inst✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
this✝² : T2Space (V x)
this✝¹ : FiniteDimensional 𝕜 (V x)
this✝ : IsTopologicalAddGroup (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V x)
v₁ v₂ : V x
⊢ Φ (extend F (v₁ + v₂)) = Φ (extend F v₁ + extend F v₂)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³⁰ : NormedAddCommGroup E
inst✝²⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝²⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝²⁷ : TopologicalSpace M
inst✝²⁶ : ChartedSpace H M
F : Type u_5
inst✝²⁵ : NormedAddCommGroup F
inst✝²⁴ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝²³ : TopologicalSpace (TotalSpace F V)
inst✝²² : (x : M) → AddCommGroup (V x)
inst✝²¹ : (x : M) → Module 𝕜 (V x)
inst✝²⁰ : (x : M) → TopologicalSpace (V x)
inst✝¹⁹ : FiberBundle F V
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
inst✝¹⁶ : TopologicalSpace (TotalSpace F' V')
inst✝¹⁵ : (x : M) → AddCommGroup (V' x)
inst✝¹⁴ : (x : M) → Module 𝕜 (V' x)
inst✝¹³ : (x : M) → TopologicalSpace (V' x)
inst✝¹² : FiberBundle F' V'
A : Type u_9
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Module 𝕜 A
Φ✝ : ((x : M) → V x) → A
x✝ : M
inst✝⁹ : VectorBundle 𝕜 F V
inst✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
this✝² : T2Space (V x)
this✝¹ : FiniteDimensional 𝕜 (V x)
this✝ : IsTopologicalAddGroup (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V x)
v₁ v₂ : V x
⊢ Φ (extend F (v₁ + v₂)) = Φ (extend F v₁ + extend F v₂)
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

Goal state before:
pp: 𝕜 : Type u_1
inst✝³¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³⁰ : NormedAddCommGroup E
inst✝²⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝²⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝²⁷ : TopologicalSpace M
inst✝²⁶ : ChartedSpace H M
F : Type u_5
inst✝²⁵ : NormedAddCommGroup F
inst✝²⁴ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝²³ : TopologicalSpace (TotalSpace F V)
inst✝²² : (x : M) → AddCommGroup (V x)
inst✝²¹ : (x : M) → Module 𝕜 (V x)
inst✝²⁰ : (x : M) → TopologicalSpace (V x)
inst✝¹⁹ : FiberBundle F V
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
inst✝¹⁶ : TopologicalSpace (TotalSpace F' V')
inst✝¹⁵ : (x : M) → AddCommGroup (V' x)
inst✝¹⁴ : (x : M) → Module 𝕜 (V' x)
inst✝¹³ : (x : M) → TopologicalSpace (V' x)
inst✝¹² : FiberBundle F' V'
A : Type u_9
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Module 𝕜 A
Φ✝ : ((x : M) → V x) → A
x✝ : M
inst✝⁹ : VectorBundle 𝕜 F V
inst✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
this✝² : T2Space (V x)
this✝¹ : FiniteDimensional 𝕜 (V x)
this✝ : IsTopologicalAddGroup (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V x)
c : 𝕜
v : V x
⊢ Φ (extend F (c • v)) = Φ ((fun x ↦ c) • extend F v)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³⁰ : NormedAddCommGroup E
inst✝²⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝²⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝²⁷ : TopologicalSpace M
inst✝²⁶ : ChartedSpace H M
F : Type u_5
inst✝²⁵ : NormedAddCommGroup F
inst✝²⁴ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝²³ : TopologicalSpace (TotalSpace F V)
inst✝²² : (x : M) → AddCommGroup (V x)
inst✝²¹ : (x : M) → Module 𝕜 (V x)
inst✝²⁰ : (x : M) → TopologicalSpace (V x)
inst✝¹⁹ : FiberBundle F V
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
inst✝¹⁶ : TopologicalSpace (TotalSpace F' V')
inst✝¹⁵ : (x : M) → AddCommGroup (V' x)
inst✝¹⁴ : (x : M) → Module 𝕜 (V' x)
inst✝¹³ : (x : M) → TopologicalSpace (V' x)
inst✝¹² : FiberBundle F' V'
A : Type u_9
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Module 𝕜 A
Φ✝ : ((x : M) → V x) → A
x✝ : M
inst✝⁹ : VectorBundle 𝕜 F V
inst✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
this✝² : T2Space (V x)
this✝¹ : FiniteDimensional 𝕜 (V x)
this✝ : IsTopologicalAddGroup (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V x)
c : 𝕜
v : V x
⊢ Φ (extend F (c • v)) = Φ ((fun x ↦ c) • extend F v)
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
hgy : ((g y) v) v = ((g' y) w) w
hgx : ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) = ((g' x) w) w
⊢ ((g' x) w) w ≤ r' ^ 2 * ((g' y) w) w

Tactic:
]

Goal state after:
B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
hgy : ((g y) v) v = ((g' y) w) w
hgx : ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) = ((g' x) w) w
⊢ ((g' x) w) w ≤ r' ^ 2 * ((g' y) w) w
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Goal state before:
pp: E : Type u_1
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
H : Type u_2
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
V : M → Type u_5
inst✝³ : TopologicalSpace (TotalSpace F V)
inst✝² : (x : M) → NormedAddCommGroup (V x)
inst✝¹ : (x : M) → InnerProductSpace ℝ (V x)
inst✝ : FiberBundle F V
cov : CovariantDerivative I F V
σ τ : (x : M) → V x
x : M
X₀ : TangentSpace I x
⊢ (derivMetricTensorAux I cov σ τ x) X₀ =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) X₀ - inner ℝ (τ x) ((↑cov σ x) X₀) - inner ℝ (σ x) ((↑cov τ x) X₀)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
H : Type u_2
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
V : M → Type u_5
inst✝³ : TopologicalSpace (TotalSpace F V)
inst✝² : (x : M) → NormedAddCommGroup (V x)
inst✝¹ : (x : M) → InnerProductSpace ℝ (V x)
inst✝ : FiberBundle F V
cov : CovariantDerivative I F V
σ τ : (x : M) → V x
x : M
X₀ : TangentSpace I x
⊢ (derivMetricTensorAux I cov σ τ x) X₀ =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) X₀ - inner ℝ (τ x) ((↑cov σ x) X₀) - inner ℝ (σ x) ((↑cov τ x) X₀)
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
hgy : ((g y) v) v = ((g' y) w) w
hgx : ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) = ((g' x) w) w
⊢ ((g' x - g' y) w) w + ((g' y) w) w ≤ ((g' x - g' y) w) w + ((g' y) w) w

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H✝ : Type u_3
inst✝¹¹ : TopologicalSpace H✝
I : ModelWithCorners 𝕜 E H✝
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H✝ M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : M → 𝕜 := fun x' ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
H : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : HasMFDerivAt% ψ x 0
this : cov (ψ • σ) x = ψ x • cov σ x + (d% ψ x).smulRight (σ x)
⊢ cov (ψ • σ') x = cov (ψ • σ') x

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Goal state before:
pp: E : Type u_1
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
H : Type u_2
inst✝¹² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → NormedAddCommGroup (V x)
inst✝⁵ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁴ : FiberBundle F V
σ τ : (x : M) → V x
cov : CovariantDerivative I F V
inst✝³ : VectorBundle ℝ F V
inst✝² : IsContMDiffRiemannianBundle I 1 F V
X : (x : M) → TangentSpace I x
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : FiniteDimensional ℝ F
x : M
hσ : MDiffAt (T% σ) x
hτ : MDiffAt (T% τ) x
⊢ ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) - inner ℝ ((↑cov σ x) (X x)) (τ x) - inner ℝ (σ x) ((↑cov τ x) (X x)) =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) - (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x -
      (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∃ v ∈ 𝓝 x, ∀ y ∈ v, σ y = σ' y
⊢ cov σ x = cov σ' x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∃ v ∈ 𝓝 x, ∀ y ∈ v, σ y = σ' y
⊢ cov σ x = cov σ' x
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ✝ σ'✝ : (x : M) → V x
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hσ' : MDiffAt (T% σ'✝) x✝
hx : x✝ ∈ u
⊢ ∑ i ∈ s, f i x✝ • cov i (σ✝ + σ'✝) x✝ = ∑ x ∈ s, (f x x✝ • cov x σ✝ x✝ + f x x✝ • cov x σ'✝ x✝)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ✝ σ'✝ : (x : M) → V x
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hσ' : MDiffAt (T% σ'✝) x✝
hx : x✝ ∈ u
⊢ ∑ i ∈ s, f i x✝ • cov i (σ✝ + σ'✝) x✝ = ∑ x ∈ s, (f x x✝ • cov x σ✝ x✝ + f x x✝ • cov x σ'✝ x✝)
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: case e_f
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ✝ σ'✝ : (x : M) → V x
x✝¹ : M
hσ : MDiffAt (T% σ✝) x✝¹
hσ' : MDiffAt (T% σ'✝) x✝¹
hx : x✝¹ ∈ u
i : ι
x✝ : TangentSpace I x✝¹
⊢ (f i x✝¹ • (cov i σ✝ x✝¹ + cov i σ'✝ x✝¹)) x✝ = (f i x✝¹ • (cov i σ✝ x✝¹ + cov i σ'✝ x✝¹)) x✝

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: case a
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ 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 + (d% g x).smulRight (σ x)) = g x • f i x • cov i σ x + f i x • (d% g x).smulRight (σ x)

Tactic:
]

Goal state after:
case a
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ 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 + (d% g x).smulRight (σ x)) = g x • f i x • cov i σ x + f i x • (d% g x).smulRight (σ x)
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
x : M
inst✝³ : IsManifold I 2 M
inst✝² : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
hcov : IsCovariantDerivativeOn E cov
X₀ Y₀ : TangentSpace I x
⊢ (cov (extend E Y₀) x) X₀ - (cov (extend E X₀) x) Y₀ - (-VectorField.mlieBracket I (extend E Y₀) (extend E X₀)) x =
    VectorField.mlieBracket I (extend E Y₀) (extend E X₀) x - ((cov (extend E X₀) x) Y₀ - (cov (extend E Y₀) x) X₀)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
x : M
inst✝³ : IsManifold I 2 M
inst✝² : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
hcov : IsCovariantDerivativeOn E cov
X₀ Y₀ : TangentSpace I x
⊢ (cov (extend E Y₀) x) X₀ - (cov (extend E X₀) x) Y₀ - (-VectorField.mlieBracket I (extend E Y₀) (extend E X₀)) x =
    VectorField.mlieBracket I (extend E Y₀) (extend E X₀) x - ((cov (extend E X₀) x) Y₀ - (cov (extend E Y₀) x) X₀)