-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
inst_5 : DecidableEq ι
inst_6 : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
a₁ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ σ : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
            (MultilinearMap.domDomCongr σ (↑a : MultilinearMap R (fun (x : ι) ↦ M) N'))) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₂ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (↑(domDomCongr x a) : MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₃ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (↑(HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ) a) :
              MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₄ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
              (↑a : MultilinearMap R (fun (x : ι) ↦ M) N'))) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₅ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HMul.hMul (α := ℤˣ) (β := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
              (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ) •
            (↑a : MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₆ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι, HSMul.hSMul (α := ℤˣ) 1 (↑a : MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₇ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι, (↑a : MultilinearMap R (fun (x : ι) ↦ M) N')) : (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₈ :
  Eq (α := (a : ι → M) → N')
    (⇑(Finset.card.{u_7} (α := Equiv.Perm ι) Finset.univ • (↑a : MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₉ :
  Eq (α := (a : ι → M) → N')
    (⇑(Fintype.card.{u_7} (Equiv.Perm ι) • (↑a : MultilinearMap R (fun (x : ι) ↦ M) N')) : (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₁₀ :
  Eq (α := (a : ι → M) → N')
    (⇑((Fintype.card ι).factorial • (↑a : MultilinearMap R (fun (x : ι) ↦ M) N')) : (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₁₁ :
  Eq (α := (a : ι → M) → N')
    (⇑((Fintype.card ι).factorial • (↑a : MultilinearMap R (fun (x : ι) ↦ M) N')) : (a : (i : ι) → M) → N')
    (⇑(↑((Fintype.card ι).factorial • a) : MultilinearMap R (fun (x : ι) ↦ M) N') : (a : (i : ι) → M) → N')
⊢ Eq (α := (a : ι → M) → N')
    (⇑((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N')
            (↑a : MultilinearMap R (fun (x : ι) ↦ M) N') :
          M [⋀^ι]→ₗ[R] N') :
      (a : ι → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')

Tactic:
simp_rw [MultilinearMap.alternatization_def, ← coe_domDomCongr, domDomCongr_perm, coe_smul,
    smul_smul, Int.units_mul_self, one_smul, Finset.sum_const, Finset.card_univ, Fintype.card_perm,
    ← coe_multilinearMap, coe_smul]

Premises used: Finset.card_univ, Fintype.card_perm, AlternatingMap.coe_smul, smul_smul, AlternatingMap.coe_domDomCongr, one_smul, AlternatingMap.coe_multilinearMap, AlternatingMap.domDomCongr_perm, MultilinearMap.alternatization_def, Finset.sum_const, Int.units_mul_self