-- 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 + 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
simp :
  Eq.{u_3 + 1} (α := F)
    (∑ x_1 : Fin (n + 2),
      ∑ x_2 : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑x_1 : ℕ))
          ((ω x : (a : Fin (n + 1) → E) → F)
              (Function.update (β := fun (a : Fin (n + 1)) ↦ E)
                (fun (x_3 : Fin (n + 1)) ↦
                  x_1.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x_4 : Fin (n + 1 + 1)) ↦ V x_4 x) x_3)
                x_2
                ((fderivWithin 𝕜
                      (fun (y : E) ↦
                        x_1.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) (fun (x : Fin (n + 1 + 1)) ↦ V x y) x_2)
                      s x :
                    (a : E) → E)
                  (V x_1 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))
⊢ 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:
simp only [extDerivWithin_apply,
    fderivWithin_continuousAlternatingMap_apply_const_apply,
    fderivWithin_continuousAlternatingMap_apply_apply hω (H₀ _) hsx, *,
    smul_add, sum_add_distrib, add_sub_assoc, add_eq_left, sub_eq_zero, smul_sum]

Premises used: add_sub_assoc, sub_eq_zero, Finset.sum_add_distrib, fderivWithin_continuousAlternatingMap_apply_const_apply, add_eq_left, fderivWithin_continuousAlternatingMap_apply_apply, Finset.smul_sum, extDerivWithin_apply, smul_add