-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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]→L[𝕜] F
V : Fin (n + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
hcomm : Pairwise fun (i j : Fin (n + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
zero :
  ∀ {ω : E → E [⋀^Fin 0]→L[𝕜] F} {V : Fin (HAdd.hAdd (α := ℕ) 0 1) → E → E} (hω : DifferentiableWithinAt 𝕜 ω s x)
    (hV : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), DifferentiableWithinAt 𝕜 (V i) s x)
    (hcomm : Pairwise fun (i j : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0),
    Eq.{u_3 + 1} (α := F)
      ((extDerivWithin ω s x : (a : Fin (0 + 1) → E) → F) fun (x_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ V x_1 x : F)
      (∑ i : Fin (0 + 1),
          HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
            ((fderivWithin 𝕜
                    (fun (x : E) ↦
                      (ω x : (a : Fin 0 → E) → F)
                        (i.removeNth (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E)
                            fun (x_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ V x_1 x :
                          (i : Fin 0) → E))
                    s x :
                  (a : E) → F)
                (V i x) :
              F) :
        F)
succ :
  ∀ (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)
⊢ Eq.{u_3 + 1} (α := F) ((extDerivWithin ω s x : (a : Fin (n + 1) → E) → F) fun (x_1 : Fin (n + 1)) ↦ V x_1 x : F)
    (∑ i : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderivWithin 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin n → E) → F)
                      (i.removeNth (α := fun (x : Fin (n + 1)) ↦ E) fun (x_1 : Fin (n + 1)) ↦ V x_1 x :
                        (i : Fin n) → E))
                  s x :
                (a : E) → F)
              (V i x) :
            F) :
      F)

Tactic:
cases n with
  | zero =>
    simp [extDerivWithin_apply, fderivWithin_continuousAlternatingMap_apply_const_apply,
      fderivWithin_continuousAlternatingMap_apply_apply, *]
  | succ n =>
    rw [extDerivWithin_apply_vectorField hω hV hsx, sub_eq_self]
    refine Fintype.sum_eq_zero _ fun i ↦ sum_eq_zero fun j hj ↦ ?_
    rw [hcomm (ne_of_lt <| by simpa using hj), (ω x).map_coord_zero 0] <;>
      simp

Premises used: Fintype.sum_eq_zero, Finset.sum_eq_zero, fderivWithin_continuousAlternatingMap_apply_const_apply, sub_eq_self, fderivWithin_continuousAlternatingMap_apply_apply, extDerivWithin_apply, ne_of_lt