-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
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))
⊢ 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)

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]

Premises used: Fin.sum_sum_eq_sum_triangle_add, Int.reduceNeg, AlternatingMap.alternatizeUncurryFin_apply, Fin.val_succ, LinearMap.coe_comp, Finset.smul_sum, Function.comp_apply, AlternatingMap.alternatizeUncurryFinLM_apply, Fin.val_castSucc