R : Type u_1
inst✝¹² : Semiring R
M : Type u_2
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type ?u.568657
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type ?u.568687
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
M' : Type ?u.568717
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
N' : Type u_3
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_4
ι' : Type ?u.569496
ι'' : Type ?u.569499
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x => M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
⊢ ∑ a : Perm ι, ↑(↑Perm.sign a • domDomCongr a m) v = 0
R : Type u_1
inst✝¹² : Semiring R
M : Type u_2
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type ?u.568657
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type ?u.568687
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
M' : Type ?u.568717
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
N' : Type u_3
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_4
ι' : Type ?u.569496
ι'' : Type ?u.569499
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x => M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
⊢ ↑(∑ σ : Perm ι, ↑Perm.sign σ • domDomCongr σ m) v = 0
rw [sum_apply]
no goals
R : Type u_1
inst✝¹² : Semiring R
M : Type u_2
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type ?u.568657
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type ?u.568687
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
M' : Type ?u.568717
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
N' : Type u_3
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_4
ι' : Type ?u.569496
ι'' : Type ?u.569499
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x => M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
⊢ ∑ a : Perm ι, ↑(↑Perm.sign a • domDomCongr a m) v = 0
exact
  Finset.sum_involution (fun σ _ => swap i j * σ)
    (fun σ _ => by simp [Perm.sign_swap i_ne_j, apply_swap_eq_self hv, -Equiv.Perm.sign_swap'])
    (fun σ _ _ => (not_congr swap_mul_eq_iff).mpr i_ne_j) (fun σ _ => Finset.mem_univ _)
    fun σ _ => swap_mul_involutive i j σ
no goals
R : Type u_1
inst✝¹² : Semiring R
M : Type u_2
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type ?u.568657
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type ?u.568687
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
M' : Type ?u.568717
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
N' : Type u_3
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_4
ι' : Type ?u.569496
ι'' : Type ?u.569499
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x => M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
σ : Perm ι
x✝ : σ ∈ Finset.univ
⊢ ↑(↑Perm.sign σ • domDomCongr σ m) v +
      ↑(↑Perm.sign ((fun σ x => swap i j * σ) σ x✝) • domDomCongr ((fun σ x => swap i j * σ) σ x✝) m) v =
    0
simp [Perm.sign_swap i_ne_j, apply_swap_eq_self hv, -Equiv.Perm.sign_swap']