mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E cov
x : M
Y σ✝ σ'✝ : (x : M) → TangentSpace I x
hX : MDiffAt (T% σ✝) x
hX' : MDiffAt (T% σ'✝) x
⊢ torsionAux cov (σ✝ + σ'✝) Y x = torsionAux cov σ✝ Y x + torsionAux cov σ'✝ Y x

Tactic:
by

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
ι : 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✝ = ∑ i ∈ s, f i x✝ • cov i σ✝ x✝ + ∑ i ∈ s, f i x✝ • cov i σ'✝ x✝

Tactic:
by

Goal state after:
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
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E cov
x : M
X : (x : M) → TangentSpace I x
f✝ : M → 𝕜
σ✝ : (x : M) → TangentSpace I x
hf : MDiffAt f✝ x
hY : MDiffAt (T% σ✝) x
⊢ torsionAux cov X (f✝ • σ✝) x = f✝ x • torsionAux cov X σ✝ x

Tactic:
by

Goal state after:
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
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E cov
x : M
X σ✝ σ'✝ : (x : M) → TangentSpace I x
hY : MDiffAt (T% σ✝) x
hY' : MDiffAt (T% σ'✝) x
⊢ torsionAux cov X (σ✝ + σ'✝) x = torsionAux cov X σ✝ x + torsionAux cov X σ'✝ x

Tactic:
by

Goal state after:
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
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 : M
X₀ Y₀ : TangentSpace I x
⊢ ((hcov.torsion x) X₀) Y₀ =
    (cov (extend E Y₀) x) X₀ - (cov (extend E X₀) x) Y₀ - VectorField.mlieBracket I (extend E X₀) (extend E Y₀) x

Tactic:
by

Goal state after:
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₀ : TangentSpace I x
⊢ ((hcov.torsion x) X₀) X₀ = 0

Tactic:
by

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
ι : 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 ∈ s, f i x • cov i (g • σ) x = ∑ i ∈ s, (g x • f i x • cov i σ x + f i x • (d% g x).smulRight (σ x))

Tactic:
by

Goal state after:
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
⊢ ((hcov.torsion x) X₀) Y₀ = -((hcov.torsion x) Y₀) X₀

Tactic:
by

Goal state after:
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✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
⊢ ((cov.torsion x) (X x)) (Y x) = (↑cov Y x) (X x) - (↑cov X x) (Y x) - mlieBracket I X Y x

Tactic:
by

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
ι : 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 ∈ s, (g x • f i x • cov i σ x + f i x • (d% g x).smulRight (σ x)) =
    g x • ∑ i ∈ s, f i x • cov i σ x + (∑ i ∈ s, f i) x • (d% g x).smulRight (σ x)

Tactic:
by

Goal state after:
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✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
X₀ Y₀ : TangentSpace I x
⊢ ((cov.torsion x) X₀) Y₀ =
    (↑cov (extend E Y₀) x) (extend E X₀ x) - (↑cov (extend E X₀) x) (extend E Y₀ x) -
      mlieBracket I (extend E X₀) (extend E Y₀) x

Tactic:
unfold torsion IsCovariantDerivativeOn.torsion
  apply TensorialAt.mkHom₂_apply_eq_extend

Goal state after:
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✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
X₀ Y₀ : TangentSpace I x
⊢ ((cov.torsion x) X₀) Y₀ =
    (↑cov (extend E Y₀) x) (extend E X₀ x) - (↑cov (extend E X₀) x) (extend E Y₀ x) -
      mlieBracket I (extend E X₀) (extend E Y₀) x

Tactic:
by

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
ι : 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
⊢ g x • ∑ i ∈ s, f i x • cov i σ x + (∑ i ∈ s, f i) x • (d% g x).smulRight (σ x) =
    g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x)

Tactic:
rw [hf]; simp

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
ι : 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
⊢ g x • ∑ i ∈ s, f i x • cov i σ x + (∑ i ∈ s, f i) x • (d% g x).smulRight (σ x) =
    g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x)

Tactic:
by

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
ι : 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 ∈ s, f i x • cov i (g • σ) x = g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x)

Tactic:
by

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
inst✝¹ : IsManifold I 1 M
n : ℕ∞ω
inst✝ : VectorBundle 𝕜 F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : ∀ i ∈ s, ContMDiffCovariantDerivativeOn F n (cov i) u
f : ι → M → 𝕜
hf : ∀ i ∈ s, ContMDiffOn I 𝓘(𝕜, 𝕜) n (f i) u
σ : (x : M) → V x
hσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (n + 1) (fun x ↦ ⟨x, σ x⟩) u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, E →L[𝕜] F)) n (fun x ↦ ⟨x, ∑ i ∈ s, f i x • cov i σ x⟩) u

Tactic:
by

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
s : Set M
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : IsCovariantDerivativeOn F cov s
A : (x : M) → V x →L[𝕜] TangentSpace I x →L[𝕜] V x
σ✝ σ'✝ : (x : M) → V x
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hσ' : MDiffAt (T% σ'✝) x✝
hx : x✝ ∈ s
⊢ cov (σ✝ + σ'✝) x✝ + (A x✝) ((σ✝ + σ'✝) x✝) = cov σ✝ x✝ + (A x✝) (σ✝ x✝) + (cov σ'✝ x✝ + (A x✝) (σ'✝ x✝))

Tactic:
by

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
s : Set M
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : IsCovariantDerivativeOn F cov s
A : (x : M) → V x →L[𝕜] TangentSpace I x →L[𝕜] V x
σ✝ : (x : M) → V x
g✝ : M → 𝕜
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hg : MDiffAt g✝ x✝
hx : x✝ ∈ s
⊢ cov (g✝ • σ✝) x✝ + (A x✝) ((g✝ • σ✝) x✝) = g✝ x✝ • (cov σ✝ x✝ + (A x✝) (σ✝ x✝)) + (d% g✝ x✝).smulRight (σ✝ x✝)

Tactic:
by

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 cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
hcov' : IsCovariantDerivativeOn F cov' s
x : M
hx : x ∈ s
f✝ : M → 𝕜
σ✝ : (x : M) → V x
hf : MDiffAt f✝ x
hσ : MDiffAt (T% σ✝) x
⊢ differenceAux cov cov' (f✝ • σ✝) x = f✝ x • differenceAux cov cov' σ✝ x

Tactic:
by

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 cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
hcov' : IsCovariantDerivativeOn F cov' s
x : M
hx : x ∈ s
σ✝ σ'✝ : (x : M) → V x
hσ : MDiffAt (T% σ✝) x
hσ' : MDiffAt (T% σ'✝) x
⊢ differenceAux cov cov' (σ✝ + σ'✝) x = differenceAux cov cov' σ✝ x + differenceAux cov cov' σ'✝ x

Tactic:
by

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 cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
hcov' : IsCovariantDerivativeOn F cov' s
inst✝³ : CompleteSpace 𝕜
inst✝² : FiniteDimensional 𝕜 F
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∈ s
σ : (x : M) → V x
hσ : MDiffAt (T% σ) x
⊢ (hcov.difference hcov' x) (σ x) = cov σ x - cov' σ x

Tactic:
by

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
inst✝ : VectorBundle 𝕜 F V
cov : CovariantDerivative I F V
⊢ ↑cov 0 = 0

Tactic:
by

Goal state after:
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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
⊢ cov.torsion = 0 ↔
    ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
      MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x

Tactic:
by

Goal state after:
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 ≤ δ * ‖w‖ ^ 2 + ((g' y) w) w

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Pullback

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B) → AddCommMonoid (E x)
inst✝¹⁷ : (x : B) → Module 𝕜 (E x)
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : TopologicalSpace (TotalSpace F E)
inst✝¹³ : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst✝¹² : NormedAddCommGroup EB
inst✝¹¹ : NormedSpace 𝕜 EB
HB : Type u_7
inst✝¹⁰ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁹ : TopologicalSpace B
inst✝⁸ : ChartedSpace HB B
EB' : Type u_8
inst✝⁷ : NormedAddCommGroup EB'
inst✝⁶ : NormedSpace 𝕜 EB'
HB' : Type u_9
inst✝⁵ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁴ : TopologicalSpace B'
inst✝³ : ChartedSpace HB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
⊢ ∀ (e e' : Trivialization F TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'],
    ContMDiffOn IB' 𝓘(𝕜, F →L[𝕜] F) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

Tactic:
by

Goal state after: