-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Uncurry.Fin (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
⊢ Eq.{u_4 + 1} (α := N)
    (∑ x : Fin (n + 1),
      ∑ x_1 ∈ Finset.Ici x,
        (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) •
            HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑x_1 : ℕ))
              ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v x.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                          (a : M) → M [⋀^Fin n]→ₗ[R] N)
                        (x.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v x_1) :
                      M [⋀^Fin n]→ₗ[R] N) :
                    (a : Fin n → M) → N)
                  (x_1.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                    (x.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
                N) +
          HPow.hPow (α := ℤ) (-1) ((↑x_1 : ℕ) + 1) •
            HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑x : ℕ))
              ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v x_1.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                          (a : M) → M [⋀^Fin n]→ₗ[R] N)
                        (x_1.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v x) :
                      M [⋀^Fin n]→ₗ[R] N) :
                    (a : Fin n → M) → N)
                  (x.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                    (x_1.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
                N)))
    (∑ i : Fin (n + 1),
      ∑ j ∈ Finset.Ici i,
        HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)) •
          HSub.hSub (α := N) (β := N)
            ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                        (a : M) → M [⋀^Fin n]→ₗ[R] N)
                      (v j.succ) :
                    M [⋀^Fin n]→ₗ[R] N) :
                  (a : Fin n → M) → N)
                (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                  (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
              N)
            ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                        (a : M) → M [⋀^Fin n]→ₗ[R] N)
                      (v i.castSucc) :
                    M [⋀^Fin n]→ₗ[R] N) :
                  (a : Fin n → M) → N)
                (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                  (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
              N))
have refine : ∀ (i j : Fin (n + 1)) (hj : j ∈ Finset.Ici i),
  HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) +
      HPow.hPow (α := ℤ) (-1) ((↑j : ℕ) + 1) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) =
    HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)) •
      HSub.hSub (α := N) (β := N)
        ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                    (a : M) → M [⋀^Fin n]→ₗ[R] N)
                  (v j.succ) :
                M [⋀^Fin n]→ₗ[R] N) :
              (a : Fin n → M) → N)
            (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
              (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
          N)
        ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                    (a : M) → M [⋀^Fin n]→ₗ[R] N)
                  (v i.castSucc) :
                M [⋀^Fin n]→ₗ[R] N) :
              (a : Fin n → M) → N)
            (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
              (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
          N)
Tactic: refine Fintype.sum_congr _ _ fun i ↦ Finset.sum_congr rfl fun j hj ↦ ?_