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 : VectorBundle 𝕜 F V
cov : CovariantDerivative I F V
x : M
⊢ (↑cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x) 0 x = 0 x

Tactic:
simp [cov.isCovariantDerivativeOnUniv.zero]

Premises used: CovariantDerivative.isCovariantDerivativeOnUniv, IsCovariantDerivativeOn.zero
-- 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 : ι → 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)
hcov : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) cov (s i)
hs : Eq.{u_4 + 1} (α := Set M) (⋃ (i : ι), s i) Set.univ
⊢ (↑(of_isCovariantDerivativeOn_of_open_cover (V := V) (s := s) hcov hs) :
      ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x) =
    cov

Tactic:
rfl

Premises used: rfl
-- 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 : CovariantDerivative I F V
k : ℕ∞ω
⊢ ContMDiffCovariantDerivativeOn F (V := V) k (↑cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x) Set.univ ↔
    cov.ContMDiffCovariantDerivative (V := V) k

Tactic:
⟨fun h ↦ ⟨h⟩, fun h ↦ h.contMDiff⟩

Premises used: CovariantDerivative.ContMDiffCovariantDerivative.mk, Iff.intro, CovariantDerivative.ContMDiffCovariantDerivative.contMDiff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E (V := TangentSpace I) cov
x : M
Y : (x : M) → TangentSpace I x
f : M → 𝕜
σ : (x : M) → TangentSpace I x
hf : MDiffAt f x
hX : MDiffAt (T% σ) x
simp :
  HSMul.hSMul (β := TangentSpace I x) (f x)
          ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x) -
        (HSMul.hSMul (β := TangentSpace I x) (f x)
            ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x) +
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((d% f x : (a : TangentSpace I x) → 𝕜) (Y x) : 𝕜) (σ x)) -
      (-HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((d% f x : (a : TangentSpace I x) → 𝕜) (Y x) : 𝕜) (σ x) +
        f x • VectorField.mlieBracket I σ Y x) =
    f x •
      (HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x)
          ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x) -
        VectorField.mlieBracket I σ Y x)
⊢ torsionAux cov (f • σ) Y x = f x • torsionAux cov σ Y x

Tactic:
simp [torsionAux, hcov.leibniz hX hf, VectorField.mlieBracket_smul_left hf hX]

Premises used: VectorField.mlieBracket_smul_left, IsCovariantDerivativeOn.leibniz, _private.0.IsCovariantDerivativeOn.torsionAux
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E (V := TangentSpace I) cov
x : M
Y : (x : M) → TangentSpace I x
f : M → 𝕜
σ : (x : M) → TangentSpace I x
hf : MDiffAt f x
hX : MDiffAt (T% σ) x
⊢ HSMul.hSMul (β := TangentSpace I x) (f x)
          ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x) -
        (HSMul.hSMul (β := TangentSpace I x) (f x)
            ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x) +
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((d% f x : (a : TangentSpace I x) → 𝕜) (Y x) : 𝕜) (σ x)) -
      (-HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((d% f x : (a : TangentSpace I x) → 𝕜) (Y x) : 𝕜) (σ x) +
        f x • VectorField.mlieBracket I σ Y x) =
    f x •
      (HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x)
          ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x) -
        VectorField.mlieBracket I σ Y x)

Tactic:
module
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E (V := TangentSpace I) cov
x : M
Y σ σ' : (x : M) → TangentSpace I x
hX : MDiffAt (T% σ) x
hX' : MDiffAt (T% σ') x
simp :
  HAdd.hAdd (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x)
          ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (σ' x) : TangentSpace I x) -
        HAdd.hAdd (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x)
          ((cov σ' x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x) -
      (VectorField.mlieBracket I σ Y x + VectorField.mlieBracket I σ' Y x) =
    HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x)
          ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x) -
        VectorField.mlieBracket I σ Y x +
      (HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (σ' x) : TangentSpace I x)
          ((cov σ' x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x) -
        VectorField.mlieBracket I σ' Y x)
⊢ torsionAux cov (σ + σ') Y x = torsionAux cov σ Y x + torsionAux cov σ' Y x

Tactic:
simp [torsionAux, hcov.add hX hX', VectorField.mlieBracket_add_left hX hX']

Premises used: VectorField.mlieBracket_add_left, IsCovariantDerivativeOn.add, _private.0.IsCovariantDerivativeOn.torsionAux
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E (V := TangentSpace I) cov
x : M
Y σ σ' : (x : M) → TangentSpace I x
hX : MDiffAt (T% σ) x
hX' : MDiffAt (T% σ') x
⊢ HAdd.hAdd (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x)
          ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (σ' x) : TangentSpace I x) -
        HAdd.hAdd (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x)
          ((cov σ' x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x) -
      (VectorField.mlieBracket I σ Y x + VectorField.mlieBracket I σ' Y x) =
    HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x)
          ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x) -
        VectorField.mlieBracket I σ Y x +
      (HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (σ' x) : TangentSpace I x)
          ((cov σ' x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x) -
        VectorField.mlieBracket I σ' Y x)

Tactic:
module
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E (V := TangentSpace I) cov
x : M
X : (x : M) → TangentSpace I x
f : M → 𝕜
σ : (x : M) → TangentSpace I x
hf : MDiffAt f x
hY : MDiffAt (T% σ) x
simp :
  HSMul.hSMul (β := TangentSpace I x) (f x)
            ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x) +
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((d% f x : (a : TangentSpace I x) → 𝕜) (X x) : 𝕜) (σ x) -
        HSMul.hSMul (β := TangentSpace I x) (f x)
          ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x) -
      (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((d% f x : (a : TangentSpace I x) → 𝕜) (X x) : 𝕜) (σ x) +
        f x • VectorField.mlieBracket I X σ x) =
    f x •
      (HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x)
          ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x) -
        VectorField.mlieBracket I X σ x)
⊢ torsionAux cov X (f • σ) x = f x • torsionAux cov X σ x

Tactic:
simp [torsionAux, hcov.leibniz hY hf, VectorField.mlieBracket_smul_right hf hY]

Premises used: IsCovariantDerivativeOn.leibniz, _private.0.IsCovariantDerivativeOn.torsionAux, VectorField.mlieBracket_smul_right
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E (V := TangentSpace I) cov
x : M
X : (x : M) → TangentSpace I x
f : M → 𝕜
σ : (x : M) → TangentSpace I x
hf : MDiffAt f x
hY : MDiffAt (T% σ) x
⊢ HSMul.hSMul (β := TangentSpace I x) (f x)
            ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x) +
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((d% f x : (a : TangentSpace I x) → 𝕜) (X x) : 𝕜) (σ x) -
        HSMul.hSMul (β := TangentSpace I x) (f x)
          ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x) -
      (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((d% f x : (a : TangentSpace I x) → 𝕜) (X x) : 𝕜) (σ x) +
        f x • VectorField.mlieBracket I X σ x) =
    f x •
      (HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x)
          ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x) -
        VectorField.mlieBracket I X σ x)

Tactic:
module
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E (V := TangentSpace I) cov
x : M
X σ σ' : (x : M) → TangentSpace I x
hY : MDiffAt (T% σ) x
hY' : MDiffAt (T% σ') x
simp :
  HAdd.hAdd (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x)
          ((cov σ' x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x) -
        HAdd.hAdd (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x)
          ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (σ' x) : TangentSpace I x) -
      (VectorField.mlieBracket I X σ x + VectorField.mlieBracket I X σ' x) =
    HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x)
          ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x) -
        VectorField.mlieBracket I X σ x +
      (HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov σ' x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x)
          ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (σ' x) : TangentSpace I x) -
        VectorField.mlieBracket I X σ' x)
⊢ torsionAux cov X (σ + σ') x = torsionAux cov X σ x + torsionAux cov X σ' x

Tactic:
simp [torsionAux, hcov.add hY hY', VectorField.mlieBracket_add_right hY hY']

Premises used: VectorField.mlieBracket_add_right, IsCovariantDerivativeOn.add, _private.0.IsCovariantDerivativeOn.torsionAux
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E (V := TangentSpace I) cov
x : M
X σ σ' : (x : M) → TangentSpace I x
hY : MDiffAt (T% σ) x
hY' : MDiffAt (T% σ') x
⊢ HAdd.hAdd (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x)
          ((cov σ' x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x) -
        HAdd.hAdd (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x)
          ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (σ' x) : TangentSpace I x) -
      (VectorField.mlieBracket I X σ x + VectorField.mlieBracket I X σ' x) =
    HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov σ x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x)
          ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (σ x) : TangentSpace I x) -
        VectorField.mlieBracket I X σ x +
      (HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
          ((cov σ' x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x)
          ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (σ' x) : TangentSpace I x) -
        VectorField.mlieBracket I X σ' x)

Tactic:
module
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
inst_8 : CompleteSpace 𝕜
inst_9 : FiniteDimensional 𝕜 E
hcov : IsCovariantDerivativeOn E (V := TangentSpace I) cov
x : M
X : (x : M) → TangentSpace I x
hX : MDiffAt (T% X) x
Y : (x : M) → TangentSpace I x
hY : MDiffAt (T% Y) x
⊢ (((hcov.torsion x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) (X x) :
          TangentSpace I x →L[𝕜] TangentSpace I x) :
        (a : TangentSpace I x) → TangentSpace I x)
      (Y x) =
    HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
        ((cov Y x : (a : TangentSpace I x) → TangentSpace I x) (X x) : TangentSpace I x)
        ((cov X x : (a : TangentSpace I x) → TangentSpace I x) (Y x) : TangentSpace I x) -
      VectorField.mlieBracket I X Y x

Tactic:
TensorialAt.mkHom₂_apply _ _ hX hY

Premises used: _private.0.IsCovariantDerivativeOn.torsionAux, TensorialAt.mkHom₂_apply
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
inst_8 : CompleteSpace 𝕜
inst_9 : FiniteDimensional 𝕜 E
hcov : IsCovariantDerivativeOn E (V := TangentSpace I) cov
x : M
X₀ Y₀ : TangentSpace I x
⊢ (((hcov.torsion x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) X₀ :
          TangentSpace I x →L[𝕜] TangentSpace I x) :
        (a : TangentSpace I x) → TangentSpace I x)
      Y₀ =
    HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
        ((cov (extend E (E := TangentSpace I) Y₀) x : (a : TangentSpace I x) → TangentSpace I x) X₀ : TangentSpace I x)
        ((cov (extend E (E := TangentSpace I) X₀) x : (a : TangentSpace I x) → TangentSpace I x) Y₀ :
          TangentSpace I x) -
      VectorField.mlieBracket I (extend E (E := TangentSpace I) X₀) (extend E (E := TangentSpace I) Y₀) x

Tactic:
simp [torsion, torsionAux, TensorialAt.mkHom₂_apply_eq_extend]

Premises used: _private.0.IsCovariantDerivativeOn.torsionAux, TensorialAt.mkHom₂_apply_eq_extend, IsCovariantDerivativeOn.torsion
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
inst_8 : CompleteSpace 𝕜
inst_9 : FiniteDimensional 𝕜 E
hcov : IsCovariantDerivativeOn E (V := TangentSpace I) cov
X₀ : TangentSpace I x
⊢ Eq (α := TangentSpace I x)
    ((((hcov.torsion x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) X₀ :
            TangentSpace I x →L[𝕜] TangentSpace I x) :
          (a : TangentSpace I x) → TangentSpace I x)
        X₀ :
      TangentSpace I x)
    (0 : TangentSpace I x)

Tactic:
simp [torsion_apply_eq_extend]

Premises used: IsCovariantDerivativeOn.torsion_apply_eq_extend
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
inst_8 : CompleteSpace 𝕜
inst_9 : FiniteDimensional 𝕜 E
hcov : IsCovariantDerivativeOn E (V := TangentSpace I) cov
X₀ Y₀ : TangentSpace I x
simp :
  HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
        ((cov (extend E (E := TangentSpace I) Y₀) x : (a : TangentSpace I x) → TangentSpace I x) X₀ : TangentSpace I x)
        ((cov (extend E (E := TangentSpace I) X₀) x : (a : TangentSpace I x) → TangentSpace I x) Y₀ :
          TangentSpace I x) -
      VectorField.mlieBracket I (extend E (E := TangentSpace I) X₀) (extend E (E := TangentSpace I) Y₀) x =
    VectorField.mlieBracket I (extend E (E := TangentSpace I) Y₀) (extend E (E := TangentSpace I) X₀) x -
      HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
        ((cov (extend E (E := TangentSpace I) X₀) x : (a : TangentSpace I x) → TangentSpace I x) Y₀ : TangentSpace I x)
        ((cov (extend E (E := TangentSpace I) Y₀) x : (a : TangentSpace I x) → TangentSpace I x) X₀ : TangentSpace I x)
⊢ Eq (α := TangentSpace I x)
    ((((hcov.torsion x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) X₀ :
            TangentSpace I x →L[𝕜] TangentSpace I x) :
          (a : TangentSpace I x) → TangentSpace I x)
        Y₀ :
      TangentSpace I x)
    (-(((hcov.torsion x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) Y₀ :
              TangentSpace I x →L[𝕜] TangentSpace I x) :
            (a : TangentSpace I x) → TangentSpace I x)
          X₀ :
      TangentSpace I x)

Tactic:
simp only [torsion_apply_eq_extend, neg_sub]

Premises used: neg_sub, IsCovariantDerivativeOn.torsion_apply_eq_extend