-- Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
theorem domCoprod.summand_eq_zero_of_smul_invariant (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁)
    (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ}
    {i j : ιa ⊕ ιb} (hv : v i = v j) (hij : i ≠ j) :
    swap i j • σ = σ → domCoprod.summand a b σ v = 0

Proof state:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
⊢ swap i j • σ = σ → (summand a b σ) v = 0

Tactic:
refine Quotient.inductionOn' σ fun σ => ?_

Result:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
σ : Perm (ιa ⊕ ιb)
⊢ swap i j • Quotient.mk'' σ = Quotient.mk'' σ → (summand a b (Quotient.mk'' σ)) v = 0

Proof state:
case h.e'_2.h.e'_6
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
i' j' : ιb
hv : v (σ (Sum.inr i')) = v (σ (Sum.inr j'))
hij : σ (Sum.inr i') ≠ σ (Sum.inr j')
hσ✝ : swap (σ (Sum.inr i')) (σ (Sum.inr j')) • Quotient.mk'' σ = Quotient.mk'' σ
⊢ ((↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0

Tactic:
convert TensorProduct.tmul_zero (R := R') (M := N₁) N₂ _

Result:
case h.e'_2.h.e'_10
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
i' j' : ιb
hv : v (σ (Sum.inr i')) = v (σ (Sum.inr j'))
hij : σ (Sum.inr i') ≠ σ (Sum.inr j')
hσ✝ : swap (σ (Sum.inr i')) (σ (Sum.inr j')) • Quotient.mk'' σ = Quotient.mk'' σ
⊢ (↑b fun i => v (σ (Sum.inr i))) = 0

Proof state:
case intro.mk
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
i' : ιb
j' : ιa
hv✝ : v (σ (Sum.inr i')) = v (σ (Sum.inl j'))
hij✝ : σ (Sum.inr i') ≠ σ (Sum.inl j')
hσ✝ : swap (σ (Sum.inr i')) (σ (Sum.inl j')) • Quotient.mk'' σ = Quotient.mk'' σ
sl : Perm ιa
sr : Perm ιb
hσ : ((Perm.sumCongrHom ιa ιb) (sl, sr)) (Sum.inr i') = (swap (Sum.inr i') (Sum.inl j')) (Sum.inr i')
⊢ (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0

Tactic:
simp at hσ

Result:
no goals

Proof state:
case intro.mk
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
i' : ιa
j' : ιb
hv✝ : v (σ (Sum.inl i')) = v (σ (Sum.inr j'))
hij✝ : σ (Sum.inl i') ≠ σ (Sum.inr j')
hσ✝ : swap (σ (Sum.inl i')) (σ (Sum.inr j')) • Quotient.mk'' σ = Quotient.mk'' σ
sl : Perm ιa
sr : Perm ιb
hσ : ((Perm.sumCongrHom ιa ιb) (sl, sr)) (Sum.inl i') = (swap (Sum.inl i') (Sum.inr j')) (Sum.inl i')
⊢ (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0

Tactic:
simp at hσ

Result:
no goals

Proof state:
case h.e'_2.h.e'_9
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
i' j' : ιa
hv : v (σ (Sum.inl i')) = v (σ (Sum.inl j'))
hij : σ (Sum.inl i') ≠ σ (Sum.inl j')
hσ✝ : swap (σ (Sum.inl i')) (σ (Sum.inl j')) • Quotient.mk'' σ = Quotient.mk'' σ
⊢ (↑a fun i => v (σ (Sum.inl i))) = 0

Tactic:
exact AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)

Result:
no goals

Proof state:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
i' j' : ιb
hv : v (σ (Sum.inr i')) = v (σ (Sum.inr j'))
hij : σ (Sum.inr i') ≠ σ (Sum.inr j')
hσ✝ : swap (σ (Sum.inr i')) (σ (Sum.inr j')) • Quotient.mk'' σ = Quotient.mk'' σ
⊢ (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0

Tactic:
convert smul_zero (M := ℤˣ) (A := N₁ ⊗[R'] N₂) _

Result:
case h.e'_2.h.e'_6
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
i' j' : ιb
hv : v (σ (Sum.inr i')) = v (σ (Sum.inr j'))
hij : σ (Sum.inr i') ≠ σ (Sum.inr j')
hσ✝ : swap (σ (Sum.inr i')) (σ (Sum.inr j')) • Quotient.mk'' σ = Quotient.mk'' σ
⊢ ((↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0