awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw :
  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) Y₀) (extend E (E := TangentSpace I) X₀)) 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)
⊢ 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)

Tactic:
rw [VectorField.mlieBracket_swap]

Premises used: VectorField.mlieBracket_swap
-- 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
dsimp :
  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) Y₀) (extend E (E := TangentSpace I) X₀) 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)
⊢ 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) Y₀) (extend E (E := TangentSpace I) X₀)) 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)

Tactic:
dsimp
-- 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
⊢ 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) Y₀) (extend E (E := TangentSpace I) X₀) 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)

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
x : M
inst_6 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
hσ : MDiffAt (T% X) x
hτ : MDiffAt (T% Y) x
⊢ ((((TensorialAt.mkHom₂.{u_1, u_2, u_3, u_4, u_2, u_2, u_2, u_2, u_2} (E := E) (H := H) (I := I) (F := E) (V :=
                  TangentSpace I) (F' := E) (V' := TangentSpace I)
                  (fun (x1 x2 : (x : M) → TangentSpace I x) ↦
                    IsCovariantDerivativeOn.torsionAux
                      (↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) x1 x2 x)
                  x ⋯ ⋯ :
                TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] TangentSpace I 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 : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
              (a : TangentSpace I x) → TangentSpace I x)
            (X x) :
          TangentSpace I x)
        (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
              (a : TangentSpace I x) → TangentSpace I x)
            (Y x) :
          TangentSpace I x) -
      mlieBracket I X Y x

Tactic:
apply TensorialAt.mkHom₂_apply

Premises used: 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
x : M
inst_6 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
⊢ MDiffAt (T% X) x

Tactic:
hX
-- 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 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
⊢ MDiffAt (T% Y) x

Tactic:
hY
-- 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 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
⊢ MDiffAt (T% X) x

Tactic:
exacts [hX, hY]
-- 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 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
X₀ Y₀ : TangentSpace I x
⊢ ((((TensorialAt.mkHom₂.{u_1, u_2, u_3, u_4, u_2, u_2, u_2, u_2, u_2} (E := E) (H := H) (I := I) (F := E) (V :=
                  TangentSpace I) (F' := E) (V' := TangentSpace I)
                  (fun (x1 x2 : (x : M) → TangentSpace I x) ↦
                    IsCovariantDerivativeOn.torsionAux
                      (↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) x1 x2 x)
                  x ⋯ ⋯ :
                TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] TangentSpace I 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 : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x)
                (extend E (E := TangentSpace I) Y₀) x :
              (a : TangentSpace I x) → TangentSpace I x)
            (extend E (E := TangentSpace I) X₀ x) :
          TangentSpace I x)
        (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x)
                (extend E (E := TangentSpace I) X₀) x :
              (a : TangentSpace I x) → TangentSpace I x)
            (extend E (E := TangentSpace I) Y₀ x) :
          TangentSpace I x) -
      mlieBracket I (extend E (E := TangentSpace I) X₀) (extend E (E := TangentSpace I) Y₀) x

Tactic:
apply TensorialAt.mkHom₂_apply_eq_extend

Premises used: TensorialAt.mkHom₂_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 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
X₀ : TangentSpace I x
⊢ Eq (α := TangentSpace I x)
    ((((cov.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:
cov.isCovariantDerivativeOn.torsion_self ..

Premises used: CovariantDerivative.isCovariantDerivativeOn, IsCovariantDerivativeOn.torsion_self
-- 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 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
X₀ Y₀ : TangentSpace I x
⊢ Eq (α := TangentSpace I x)
    ((((cov.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)
    (-(((cov.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:
cov.isCovariantDerivativeOn.torsion_antisymm ..

Premises used: CovariantDerivative.isCovariantDerivativeOn, IsCovariantDerivativeOn.torsion_antisymm
-- 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 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
mp :
  cov.torsion = 0 →
    ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
      MDiffAt (T% X) x →
        MDiffAt (T% Y) x →
          HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
              (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
                    (a : TangentSpace I x) → TangentSpace I x)
                  (X x) :
                TangentSpace I x)
              (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
                    (a : TangentSpace I x) → TangentSpace I x)
                  (Y x) :
                TangentSpace I x) =
            mlieBracket I X Y x
mpr :
  (∀ {X Y : (x : M) → TangentSpace I x} {x : M},
      MDiffAt (T% X) x →
        MDiffAt (T% Y) x →
          HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
              (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
                    (a : TangentSpace I x) → TangentSpace I x)
                  (X x) :
                TangentSpace I x)
              (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
                    (a : TangentSpace I x) → TangentSpace I x)
                  (Y x) :
                TangentSpace I x) =
            mlieBracket I X Y x) →
    cov.torsion = 0
⊢ cov.torsion = 0 ↔
    ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
      MDiffAt (T% X) x →
        MDiffAt (T% Y) x →
          HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
              (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
                    (a : TangentSpace I x) → TangentSpace I x)
                  (X x) :
                TangentSpace I x)
              (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
                    (a : TangentSpace I x) → TangentSpace I x)
                  (Y x) :
                TangentSpace I x) =
            mlieBracket I X Y x

Tactic:
constructor
-- 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 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
h : cov.torsion = 0
X Y : (x : M) → TangentSpace I x
x : M
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
⊢ Eq (α := TangentSpace I x)
    ((((cov.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) :
      TangentSpace I x)
    ((((0 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) :
      TangentSpace I x)

Tactic:
replace h := congr($h x (X x) (Y x))
-- 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 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
x : M
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
h :
  Eq (α := TangentSpace I x)
    ((((cov.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) :
      TangentSpace I x)
    ((((0 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) :
      TangentSpace I x)
⊢ HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
        (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
              (a : TangentSpace I x) → TangentSpace I x)
            (X x) :
          TangentSpace I x)
        (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
              (a : TangentSpace I x) → TangentSpace I x)
            (Y x) :
          TangentSpace I x) -
      mlieBracket I X Y x =
    (((0 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)

Tactic:
rw [cov.torsion_apply hX hY] at h

Premises used: CovariantDerivative.torsion_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 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
x : M
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
h :
  HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
        (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
              (a : TangentSpace I x) → TangentSpace I x)
            (X x) :
          TangentSpace I x)
        (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
              (a : TangentSpace I x) → TangentSpace I x)
            (Y x) :
          TangentSpace I x) -
      mlieBracket I X Y x =
    (((0 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 : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
            (a : TangentSpace I x) → TangentSpace I x)
          (X x) :
        TangentSpace I x)
      (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
            (a : TangentSpace I x) → TangentSpace I x)
          (Y x) :
        TangentSpace I x) =
    mlieBracket I X Y x

Tactic:
simpa [sub_eq_iff_eq_add'] using h

Premises used: sub_eq_iff_eq_add'
-- 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 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
h :
  ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
    MDiffAt (T% X) x →
      MDiffAt (T% Y) x →
        HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
            (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
                  (a : TangentSpace I x) → TangentSpace I x)
                (X x) :
              TangentSpace I x)
            (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
                  (a : TangentSpace I x) → TangentSpace I x)
                (Y x) :
              TangentSpace I x) =
          mlieBracket I X Y x
mpr :
  ∀ (x : M) (u v : TangentSpace I x),
    Eq (α := TangentSpace I x)
      ((((cov.torsion x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
              TangentSpace I x →L[𝕜] TangentSpace I x) :
            (a : TangentSpace I x) → TangentSpace I x)
          v :
        TangentSpace I x)
      ((((0 x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
              TangentSpace I x →L[𝕜] TangentSpace I x) :
            (a : TangentSpace I x) → TangentSpace I x)
          v :
        TangentSpace I x)
⊢ cov.torsion = 0

Tactic:
ext x u v