-- 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) ((alternatizeUncurryFin (alternatizeUncurryFinLM ∘ₗ f) : (a : Fin (n + 1 + 1) → M) → N) 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) :
      N)
have simp : 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))
Tactic: simp only [alternatizeUncurryFin_apply, Int.reduceNeg, LinearMap.coe_comp, comp_apply,
    alternatizeUncurryFinLM_apply, Finset.smul_sum, sum_sum_eq_sum_triangle_add, val_castSucc,
    val_succ]