-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
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')
⊢ 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')
have 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')
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]