-- 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
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))
                  (j.removeNth (α := 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) :
                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
              (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 rw : 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)
Tactic: rw [Fin.removeNth_removeNth_eq_swap]