-- 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
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j = v j.succ
H₂ : j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i = v i.castSucc
simp :
  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)
                    (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) -
      HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((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)
              (i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) =
    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)
                    (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) -
      HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((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)
⊢ 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:
simp only [pow_add, mul_smul, pow_one, neg_one_smul, smul_neg, smul_sub, ← sub_eq_add_neg,
    smul_comm ((-1 : ℤ) ^ (j : ℕ)), H₁, H₂]

Premises used: neg_one_smul, sub_eq_add_neg, pow_add, smul_neg, Fin.val, smul_sub, HPow.hPow, pow_one, SMulCommClass.smul_comm, OfNat.ofNat, SemigroupAction.mul_smul, Neg.neg