awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
cov cov' : ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
s : Set M
hcov : IsCovariantDerivativeOn F (V := V) cov s
hcov' : IsCovariantDerivativeOn F (V := V) cov' s
inst_15 : CompleteSpace 𝕜
inst_16 : FiniteDimensional 𝕜 F
inst_17 : VectorBundle 𝕜 F V
inst_18 : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∈ s
σ : (x : M) → V x
hσ : MDiffAt (T% σ) x
⊢ (TensorialAt.mkHom (V := V) (fun (x_1 : (x : M) → V x) ↦ differenceAux (V := V) cov cov' x_1 x) x ⋯ :
        (a : V x) → TangentSpace I x →L[𝕜] V x)
      (σ x) =
    cov σ x - cov' σ x
have rw : differenceAux (V := V) cov cov' σ x = cov σ x - cov' σ x
Tactic: rw [TensorialAt.mkHom_apply _ hσ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
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
⊢ (↑cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x) 0 = 0
have h : ∀ (x : M), (↑cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x) 0 x = 0 x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
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
⊢ torsionAux cov (f • σ) Y x = f x • torsionAux cov σ Y x
have 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)
Tactic: simp [torsionAux, hcov.leibniz hX hf, VectorField.mlieBracket_smul_left hf hX]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
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
⊢ torsionAux cov (σ + σ') Y x = torsionAux cov σ Y x + torsionAux cov σ' Y x
have 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)
Tactic: simp [torsionAux, hcov.add hX hX', VectorField.mlieBracket_add_left hX hX']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
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
⊢ torsionAux cov X (f • σ) x = f x • torsionAux cov X σ x
have 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)
Tactic: simp [torsionAux, hcov.leibniz hY hf, VectorField.mlieBracket_smul_right hf hY]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
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
⊢ torsionAux cov X (σ + σ') x = torsionAux cov X σ x + torsionAux cov X σ' x
have 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)
Tactic: simp [torsionAux, hcov.add hY hY', VectorField.mlieBracket_add_right hY hY']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
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
⊢ 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)
have 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)
Tactic: simp only [torsion_apply_eq_extend, neg_sub]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
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) 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)
have 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)
Tactic: rw [VectorField.mlieBracket_swap]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
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)
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (hypothesis)
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
⊢ 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
have 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)
Tactic: replace h := congr($h x (X x) (Y x))
Cleared hypotheses: h