awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
s : Set E
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
H₀ :
  ∀ (i : Fin (n + 2)) (j : Fin (n + 1)),
    DifferentiableWithinAt 𝕜 (F := E)
      (fun (y : E) ↦ i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y) j) s x
⊢ ((extDerivWithin ω s x : (a : Fin (n + 1 + 1) → E) → F) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x) =
    HSub.hSub (α := F)
      (∑ i : Fin (n + 2),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderivWithin 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin (n + 1) → E) → F)
                      (i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                        (i : Fin (n + 1)) → E))
                  s x :
                (a : E) → F)
              (V i x) :
            F))
      (∑ i : Fin (n + 1),
        ∑ j ∈ Ici i,
          HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
            ((ω x : (a : Fin (n + 1) → E) → F)
                (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
                  (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
                    (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                      (i : Fin (n + 1)) → E))) :
              F))
have symm : HSub.hSub (α := F)
    (∑ i : Fin (n + 2),
      HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
        ((fderivWithin 𝕜
                (fun (x : E) ↦
                  (ω x : (a : Fin (n + 1) → E) → F)
                    (i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                      (i : Fin (n + 1)) → E))
                s x :
              (a : E) → F)
            (V i x) :
          F))
    (∑ i : Fin (n + 1),
      ∑ j ∈ Ici i,
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
          ((ω x : (a : Fin (n + 1) → E) → F)
              (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
                (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
                  (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                    (i : Fin (n + 1)) → E))) :
            F)) =
  (extDerivWithin ω s x : (a : Fin (n + 1 + 1) → E) → F) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
s : Set E
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
H₀ :
  ∀ (i : Fin (n + 2)) (j : Fin (n + 1)),
    DifferentiableWithinAt 𝕜 (F := E)
      (fun (y : E) ↦ i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y) j) s x
i j : Fin (n + 1)
hj : j ∈ Ici i
⊢ HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i.castSucc : ℕ))
        ((ω x : (a : Fin (n + 1) → E) → F)
            (Function.update (β := fun (a : Fin (n + 1)) ↦ E)
              (fun (x_1 : Fin (n + 1)) ↦
                i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x_2 : Fin (n + 1 + 1)) ↦ V x_2 x) x_1)
              j
              ((fderivWithin 𝕜
                    (fun (y : E) ↦
                      i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y) j)
                    s x :
                  (a : E) → E)
                (V i.castSucc x))) :
          F) +
      HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑j.succ : ℕ))
        ((ω x : (a : Fin (n + 1) → E) → F)
            (Function.update (β := fun (a : Fin (n + 1)) ↦ E)
              (fun (x_1 : Fin (n + 1)) ↦
                j.succ.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x_2 : Fin (n + 1 + 1)) ↦ V x_2 x) x_1)
              i
              ((fderivWithin 𝕜
                    (fun (y : E) ↦
                      j.succ.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y) i)
                    s x :
                  (a : E) → E)
                (V j.succ x))) :
          F) =
    HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
      ((ω x : (a : Fin (n + 1) → E) → F)
          (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
            (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
              (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                (i : Fin (n + 1)) → E))) :
        F)
have hj₁ : i ≤ j
Tactic: rw [mem_Ici] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
s : Set E
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
H₀ :
  ∀ (i : Fin (n + 2)) (j : Fin (n + 1)),
    DifferentiableWithinAt 𝕜 (F := E)
      (fun (y : E) ↦ i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y) j) s x
i j : Fin (n + 1)
hj : i ≤ j
⊢ HPow.hPow (α := ℤ) (-1) (↑i.castSucc : ℕ) •
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((ω x : (a : Fin (n + 1) → E) → F)
              (Matrix.vecCons
                  ((fderivWithin 𝕜
                        (fun (y : E) ↦
                          i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y)
                            j)
                        s x :
                      (a : E) → E)
                    (V i.castSucc x))
                  (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) (j.predAbove i.castSucc)
                    ((i.castSucc.succAbove j).removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ E)
                        fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                      (i : Fin (n + 1)) → E)) :
                Fin n.succ → E) :
            F) +
      HPow.hPow (α := ℤ) (-1) (↑j.succ : ℕ) •
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((ω x : (a : Fin (n + 1) → E) → F)
              (Matrix.vecCons
                  ((fderivWithin 𝕜
                        (fun (y : E) ↦
                          j.succ.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y) i)
                        s x :
                      (a : E) → E)
                    (V j.succ x))
                  (i.removeNth (α := fun (a : Fin (n + 1)) ↦ E) fun (x_1 : Fin (n + 1)) ↦
                    j.succ.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x_2 : Fin (n + 1 + 1)) ↦ V x_2 x) x_1) :
                Fin n.succ → E) :
            F) =
    HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
      ((ω x : (a : Fin (n + 1) → E) → F)
          (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
            (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) (j.predAbove i.castSucc)
              ((i.castSucc.succAbove j).removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦
                  V x_1 x :
                (i : Fin (n + 1)) → E))) :
        F)
have H₁ : i.castSucc.succAbove j = j.succ
Tactic: have H₁ : i.castSucc.succAbove j = j.succ := by simp [Fin.succAbove_of_le_castSucc, hj]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
s : Set E
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
H₀ :
  ∀ (i : Fin (n + 2)) (j : Fin (n + 1)),
    DifferentiableWithinAt 𝕜 (F := E)
      (fun (y : E) ↦ i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y) j) s x
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.succAbove j = j.succ
⊢ HPow.hPow (α := ℤ) (-1) (↑i.castSucc : ℕ) •
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((ω x : (a : Fin (n + 1) → E) → F)
              (Matrix.vecCons
                  ((fderivWithin 𝕜
                        (fun (y : E) ↦
                          i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y)
                            j)
                        s x :
                      (a : E) → E)
                    (V i.castSucc x))
                  (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) (j.predAbove i.castSucc)
                    ((i.castSucc.succAbove j).removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ E)
                        fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                      (i : Fin (n + 1)) → E)) :
                Fin n.succ → E) :
            F) +
      HPow.hPow (α := ℤ) (-1) (↑j.succ : ℕ) •
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((ω x : (a : Fin (n + 1) → E) → F)
              (Matrix.vecCons
                  ((fderivWithin 𝕜
                        (fun (y : E) ↦
                          j.succ.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y) i)
                        s x :
                      (a : E) → E)
                    (V j.succ x))
                  (i.removeNth (α := fun (a : Fin (n + 1)) ↦ E) fun (x_1 : Fin (n + 1)) ↦
                    j.succ.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x_2 : Fin (n + 1 + 1)) ↦ V x_2 x) x_1) :
                Fin n.succ → E) :
            F) =
    HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
      ((ω x : (a : Fin (n + 1) → E) → F)
          (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
            (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) (j.predAbove i.castSucc)
              ((i.castSucc.succAbove j).removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦
                  V x_1 x :
                (i : Fin (n + 1)) → E))) :
        F)
have H₂ : j.predAbove i.castSucc = i
Tactic: have H₂ : j.predAbove i.castSucc = i := by simp [Fin.predAbove_of_le_castSucc, hj]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
s : Set E
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
H₀ :
  ∀ (i : Fin (n + 2)) (j : Fin (n + 1)),
    DifferentiableWithinAt 𝕜 (F := E)
      (fun (y : E) ↦ i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y) j) s x
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.succAbove j = j.succ
H₂ : j.predAbove i.castSucc = i
⊢ HPow.hPow (α := ℤ) (-1) (↑i.castSucc : ℕ) •
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((ω x : (a : Fin (n + 1) → E) → F)
              (Matrix.vecCons
                  ((fderivWithin 𝕜
                        (fun (y : E) ↦
                          i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y)
                            j)
                        s x :
                      (a : E) → E)
                    (V i.castSucc x))
                  (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) (j.predAbove i.castSucc)
                    ((i.castSucc.succAbove j).removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ E)
                        fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                      (i : Fin (n + 1)) → E)) :
                Fin n.succ → E) :
            F) +
      HPow.hPow (α := ℤ) (-1) (↑j.succ : ℕ) •
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((ω x : (a : Fin (n + 1) → E) → F)
              (Matrix.vecCons
                  ((fderivWithin 𝕜
                        (fun (y : E) ↦
                          j.succ.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y) i)
                        s x :
                      (a : E) → E)
                    (V j.succ x))
                  (i.removeNth (α := fun (a : Fin (n + 1)) ↦ E) fun (x_1 : Fin (n + 1)) ↦
                    j.succ.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x_2 : Fin (n + 1 + 1)) ↦ V x_2 x) x_1) :
                Fin n.succ → E) :
            F) =
    HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
      ((ω x : (a : Fin (n + 1) → E) → F)
          (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
            (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) (j.predAbove i.castSucc)
              ((i.castSucc.succAbove j).removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦
                  V x_1 x :
                (i : Fin (n + 1)) → E))) :
        F)
have H₃ : j.succ.succAbove i = i.castSucc
Tactic: have H₃ : j.succ.succAbove i = i.castSucc := by simp [Fin.succAbove_of_castSucc_lt, hj]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableAt 𝕜 ω x
hV : ∀ (i : Fin (n + 2)), DifferentiableAt 𝕜 (V i) x
⊢ ((extDeriv ω x : (a : Fin (n + 1 + 1) → E) → F) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x) =
    HSub.hSub (α := F)
      (∑ i : Fin (n + 2),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderiv 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin (n + 1) → E) → F)
                      (i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                        (i : Fin (n + 1)) → E))
                  x :
                (a : E) → F)
              (V i x) :
            F))
      (∑ i : Fin (n + 1),
        ∑ j ∈ Ici i,
          HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
            ((ω x : (a : Fin (n + 1) → E) → F)
                (Matrix.vecCons (lieBracket 𝕜 (V i.castSucc) (V j.succ) x)
                  (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
                    (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                      (i : Fin (n + 1)) → E))) :
              F))
have simp : ∀ (hω : DifferentiableWithinAt 𝕜 ω Set.univ x) (hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) Set.univ x),
  ((extDerivWithin ω Set.univ x : (a : Fin (n + 1 + 1) → E) → F) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x) =
    HSub.hSub (α := F)
      (∑ x_1 : Fin (n + 2),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑x_1 : ℕ))
          ((fderivWithin 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin (n + 1) → E) → F)
                      (x_1.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_2 : Fin (n + 1 + 1)) ↦ V x_2 x :
                        (i : Fin (n + 1)) → E))
                  Set.univ x :
                (a : E) → F)
              (V x_1 x) :
            F))
      (∑ x_1 : Fin (n + 1),
        ∑ x_2 ∈ Ici x_1,
          HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑x_1 : ℕ) + (↑x_2 : ℕ)))
            ((ω x : (a : Fin (n + 1) → E) → F)
                (Matrix.vecCons (lieBracketWithin 𝕜 (V x_1.castSucc) (V x_2.succ) Set.univ x)
                  (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) x_2
                    (x_1.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_3 : Fin (n + 1 + 1)) ↦ V x_3 x :
                      (i : Fin (n + 1)) → E))) :
              F))
Tactic: simp only [← differentiableWithinAt_univ, ← extDerivWithin_univ, ← fderivWithin_univ,
    ← lieBracketWithin_univ] at *
Cleared hypotheses: hω, hV
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun (i j : Fin (n + 1 + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
⊢ Eq.{u_3 + 1} (α := F)
    ((extDerivWithin ω s x : (a : Fin (n + 1 + 1) → E) → F) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x : F)
    (∑ i : Fin (n + 1 + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderivWithin 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin (n + 1) → E) → F)
                      (i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                        (i : Fin (n + 1)) → E))
                  s x :
                (a : E) → F)
              (V i x) :
            F) :
      F)
have succ : Eq.{u_3 + 1} (α := F)
  (∑ i : Fin (n + 1),
    ∑ j ∈ Ici i,
      HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
        ((ω x : (a : Fin (n + 1) → E) → F)
            (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
              (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
                (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                  (i : Fin (n + 1)) → E))) :
          F))
  0
Tactic: rw [extDerivWithin_apply_vectorField hω hV hsx, sub_eq_self]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun (i j : Fin (n + 1 + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
⊢ Eq.{u_3 + 1} (α := F)
    (∑ i : Fin (n + 1),
      ∑ j ∈ Ici i,
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
          ((ω x : (a : Fin (n + 1) → E) → F)
              (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
                (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
                  (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                    (i : Fin (n + 1)) → E))) :
            F))
    0
have succ : ∀ (i j : Fin (n + 1)) (hj : j ∈ Ici i),
  HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
      ((ω x : (a : Fin (n + 1) → E) → F)
          (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
            (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
              (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                (i : Fin (n + 1)) → E))) :
        F) =
    0
Tactic: refine Fintype.sum_eq_zero _ fun i ↦ sum_eq_zero fun j hj ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun (i j : Fin (n + 1 + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
i j : Fin (n + 1)
hj : j ∈ Ici i
⊢ HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
      ((ω x : (a : Fin (n + 1) → E) → F)
          (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
            (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
              (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                (i : Fin (n + 1)) → E))) :
        F) =
    0
have succ : HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ))) 0 = 0
Tactic: rw [hcomm (ne_of_lt <| by simpa using hj), (ω x).map_coord_zero 0]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun (i j : Fin (n + 1 + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
i j : Fin (n + 1)
hj : j ∈ Ici i
succ : HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ))) 0 = 0
⊢ HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
      ((ω x : (a : Fin (n + 1) → E) → F)
          (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
            (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
              (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                (i : Fin (n + 1)) → E))) :
        F) =
    0
have succ₁ : Eq.{u_2 + 1} (α := E)
  (Matrix.vecCons (n := n) 0
    (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
      (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
        (i : Fin (n + 1)) → E))
    0)
  0
Tactic: rw [hcomm (ne_of_lt <| by simpa using hj), (ω x).map_coord_zero 0]