no goals
R : Type u_1
inst✝¹² : Semiring R
M : Type u_2
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type ?u.689410
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type ?u.689440
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
M' : Type ?u.689470
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
N' : Type u_3
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_4
ι' : Type ?u.690249
ι'' : Type ?u.690252
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x => M) N'
v : ι → M
⊢ ↑(↑alternatization m) v = ∑ σ : Perm ι, ↑Perm.sign σ • ↑(domDomCongr σ m) v
simp only [alternatization_def, smul_apply, sum_apply]