-- 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
σ : Perm (ιa ⊕ ιb)
⊢ swap i j • Quotient.mk'' σ = Quotient.mk'' σ → (summand a b (Quotient.mk'' σ)) v = 0

Tactic:
dsimp only [Quotient.liftOn'_mk'', Quotient.map'_mk'', MultilinearMap.smul_apply,
  MultilinearMap.domDomCongr_apply, MultilinearMap.domCoprod_apply, domCoprod.summand]

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'' σ →
    (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑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') =
    (((fun x => swap (σ (Sum.inr i')) (σ (Sum.inl j')) • x) σ)⁻¹ * σ) (Sum.inr i')
⊢ (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0

Tactic:
dsimp only at hσ

Result:
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

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)
⊢ ∀ (val val_1 : ιa),
    v (σ (Sum.inl val)) = v (σ (Sum.inl val_1)) →
      σ (Sum.inl val) ≠ σ (Sum.inl val_1) →
        swap (σ (Sum.inl val)) (σ (Sum.inl val_1)) • Quotient.mk'' σ = Quotient.mk'' σ →
          (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0

Tactic:
intro i' j' hv hij _

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ᵢ
σ : 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'' σ
⊢ (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0

Proof state:
case inl.inl
ι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)
⊢ ∀ (val val_1 : ιa),
    v (σ (Sum.inl val)) = v (σ (Sum.inl val_1)) →
      σ (Sum.inl val) ≠ σ (Sum.inl val_1) →
        swap (σ (Sum.inl val)) (σ (Sum.inl val_1)) • Quotient.mk'' σ = Quotient.mk'' σ →
          (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0

Tactic:
case inl.inl =>
  intro i' j' hv hij _
  convert smul_zero (M := ℤˣ) (A := N₁ ⊗[R'] N₂) _
  convert TensorProduct.zero_tmul (R := R') N₁ (N := N₂) _
  exact AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)

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' : ι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) = ((fun x => swap (σ (Sum.inr i')) (σ (Sum.inl j')) • x) σ)⁻¹ * σ
⊢ (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0

Tactic:
replace hσ := Equiv.congr_fun hσ (Sum.inr i')

Result:
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') =
    (((fun x => swap (σ (Sum.inr i')) (σ (Sum.inl j')) • x) σ)⁻¹ * σ) (Sum.inr i')
⊢ (Perm.sign σ • (↑a fun i => v (σ (Sum.inl i))) ⊗ₜ[R'] ↑b fun i => v (σ (Sum.inr i))) = 0