R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ : 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
refine Quotient.inductionOn' σ fun σ => ?_
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
dsimp only [Quotient.liftOn'_mk'', Quotient.map'_mk'', MultilinearMap.smul_apply,
  MultilinearMap.domDomCongr_apply, MultilinearMap.domCoprod_apply, domCoprod.summand]
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
σ : Perm (ιa ⊕ ιb)
hσ : 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
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
intro hσ
case inl.inl
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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

case inl.inr
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val : ιa) (val_1 : ιb),
    v (↑σ (Sum.inl val)) = v (↑σ (Sum.inr val_1)) →
      ↑σ (Sum.inl val) ≠ ↑σ (Sum.inr val_1) →
        swap (↑σ (Sum.inl val)) (↑σ (Sum.inr val_1)) • Quotient.mk'' σ = Quotient.mk'' σ →
          (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0

case inr.inl
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val : ιb) (val_1 : ιa),
    v (↑σ (Sum.inr val)) = v (↑σ (Sum.inl val_1)) →
      ↑σ (Sum.inr val) ≠ ↑σ (Sum.inl val_1) →
        swap (↑σ (Sum.inr 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

case inr.inr
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val val_1 : ιb),
    v (↑σ (Sum.inr val)) = v (↑σ (Sum.inr val_1)) →
      ↑σ (Sum.inr val) ≠ ↑σ (Sum.inr val_1) →
        swap (↑σ (Sum.inr val)) (↑σ (Sum.inr val_1)) • Quotient.mk'' σ = Quotient.mk'' σ →
          (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
σ : Perm (ιa ⊕ ιb)
hσ : 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
cases' hi : σ⁻¹ i with val val <;> cases' hj : σ⁻¹ j with val_1 val_1 <;>
  rw [Perm.inv_eq_iff_eq] at hi hj <;> substs hi hj <;> revert val val_1
case inl.inl
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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

case inr.inl
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val : ιb) (val_1 : ιa),
    v (↑σ (Sum.inr val)) = v (↑σ (Sum.inl val_1)) →
      ↑σ (Sum.inr val) ≠ ↑σ (Sum.inl val_1) →
        swap (↑σ (Sum.inr 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

case inr.inr
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val val_1 : ιb),
    v (↑σ (Sum.inr val)) = v (↑σ (Sum.inr val_1)) →
      ↑σ (Sum.inr val) ≠ ↑σ (Sum.inr val_1) →
        swap (↑σ (Sum.inr val)) (↑σ (Sum.inr val_1)) • Quotient.mk'' σ = Quotient.mk'' σ →
          (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
case inl.inl
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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

case inl.inr
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val : ιa) (val_1 : ιb),
    v (↑σ (Sum.inl val)) = v (↑σ (Sum.inr val_1)) →
      ↑σ (Sum.inl val) ≠ ↑σ (Sum.inr val_1) →
        swap (↑σ (Sum.inl val)) (↑σ (Sum.inr val_1)) • Quotient.mk'' σ = Quotient.mk'' σ →
          (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0

case inr.inl
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val : ιb) (val_1 : ιa),
    v (↑σ (Sum.inr val)) = v (↑σ (Sum.inl val_1)) →
      ↑σ (Sum.inr val) ≠ ↑σ (Sum.inl val_1) →
        swap (↑σ (Sum.inr 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

case inr.inr
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val val_1 : ιb),
    v (↑σ (Sum.inr val)) = v (↑σ (Sum.inr val_1)) →
      ↑σ (Sum.inr val) ≠ ↑σ (Sum.inr val_1) →
        swap (↑σ (Sum.inr val)) (↑σ (Sum.inr val_1)) • Quotient.mk'' σ = Quotient.mk'' σ →
          (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
case inl.inr =>
  intro i' j' _ _ hσ
  obtain ⟨⟨sl, sr⟩, hσ⟩ := QuotientGroup.leftRel_apply.mp (Quotient.exact' hσ)
  replace hσ := Equiv.congr_fun hσ (Sum.inl i')
  dsimp only at hσ
  rw [smul_eq_mul, ← mul_swap_eq_swap_mul, mul_inv_rev, swap_inv, inv_mul_cancel_right] at hσ
  simp at hσ
case inl.inl
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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

case inr.inr
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val val_1 : ιb),
    v (↑σ (Sum.inr val)) = v (↑σ (Sum.inr val_1)) →
      ↑σ (Sum.inr val) ≠ ↑σ (Sum.inr val_1) →
        swap (↑σ (Sum.inr val)) (↑σ (Sum.inr val_1)) • Quotient.mk'' σ = Quotient.mk'' σ →
          (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
case inl.inl
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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

case inr.inl
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val : ιb) (val_1 : ιa),
    v (↑σ (Sum.inr val)) = v (↑σ (Sum.inl val_1)) →
      ↑σ (Sum.inr val) ≠ ↑σ (Sum.inl val_1) →
        swap (↑σ (Sum.inr 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

case inr.inr
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val val_1 : ιb),
    v (↑σ (Sum.inr val)) = v (↑σ (Sum.inr val_1)) →
      ↑σ (Sum.inr val) ≠ ↑σ (Sum.inr val_1) →
        swap (↑σ (Sum.inr val)) (↑σ (Sum.inr val_1)) • Quotient.mk'' σ = Quotient.mk'' σ →
          (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
case inr.inl =>
  intro i' j' _ _ hσ
  obtain ⟨⟨sl, sr⟩, hσ⟩ := QuotientGroup.leftRel_apply.mp (Quotient.exact' hσ)
  replace hσ := Equiv.congr_fun hσ (Sum.inr i')
  dsimp only at hσ
  rw [smul_eq_mul, ← mul_swap_eq_swap_mul, mul_inv_rev, swap_inv, inv_mul_cancel_right] at hσ
  simp at hσ
case inl.inl
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
case inl.inl
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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

case inr.inr
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val val_1 : ιb),
    v (↑σ (Sum.inr val)) = v (↑σ (Sum.inr val_1)) →
      ↑σ (Sum.inr val) ≠ ↑σ (Sum.inr val_1) →
        swap (↑σ (Sum.inr val)) (↑σ (Sum.inr val_1)) • Quotient.mk'' σ = Quotient.mk'' σ →
          (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
case inr.inr =>
  intro i' j' hv hij _
  convert smul_zero (M := ℤˣ) (A := N₁ ⊗[R'] N₂) _
  convert TensorProduct.tmul_zero (R := R') (M := N₁) N₂ _
  exact AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)
no goals
case inl.inl
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
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)
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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'' σ
⊢ (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val : ιa) (val_1 : ιb),
    v (↑σ (Sum.inl val)) = v (↑σ (Sum.inr val_1)) →
      ↑σ (Sum.inl val) ≠ ↑σ (Sum.inr val_1) →
        swap (↑σ (Sum.inl val)) (↑σ (Sum.inr val_1)) • Quotient.mk'' σ = Quotient.mk'' σ →
          (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
intro i' j' _ _ hσ
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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) = ((fun x x_1 => x • x_1) (swap (↑σ (Sum.inl i')) (↑σ (Sum.inr j'))) σ)⁻¹ * σ
⊢ (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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'' σ
⊢ (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
obtain ⟨⟨sl, sr⟩, hσ⟩ := QuotientGroup.leftRel_apply.mp (Quotient.exact' hσ)
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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') =
    ↑(((fun x x_1 => x • x_1) (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
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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) = ((fun x x_1 => x • x_1) (swap (↑σ (Sum.inl i')) (↑σ (Sum.inr j'))) σ)⁻¹ * σ
⊢ (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
replace hσ := Equiv.congr_fun hσ (Sum.inl i')
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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') =
    ↑(((fun x x_1 => x • x_1) (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
dsimp only at hσ
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
rw [smul_eq_mul, ← mul_swap_eq_swap_mul, mul_inv_rev, swap_inv, inv_mul_cancel_right] at hσ
no goals
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
simp at hσ
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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'' σ
⊢ (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val : ιb) (val_1 : ιa),
    v (↑σ (Sum.inr val)) = v (↑σ (Sum.inl val_1)) →
      ↑σ (Sum.inr val) ≠ ↑σ (Sum.inl val_1) →
        swap (↑σ (Sum.inr 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
intro i' j' _ _ hσ
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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 x_1 => x • x_1) (swap (↑σ (Sum.inr i')) (↑σ (Sum.inl j'))) σ)⁻¹ * σ
⊢ (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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'' σ
⊢ (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
obtain ⟨⟨sl, sr⟩, hσ⟩ := QuotientGroup.leftRel_apply.mp (Quotient.exact' hσ)
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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 x_1 => x • x_1) (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
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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 x_1 => x • x_1) (swap (↑σ (Sum.inr i')) (↑σ (Sum.inl j'))) σ)⁻¹ * σ
⊢ (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
replace hσ := Equiv.congr_fun hσ (Sum.inr i')
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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 x_1 => x • x_1) (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
dsimp only at hσ
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
rw [smul_eq_mul, ← mul_swap_eq_swap_mul, mul_inv_rev, swap_inv, inv_mul_cancel_right] at hσ
no goals
case intro.mk
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
simp at hσ
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
⊢ ∀ (val val_1 : ιb),
    v (↑σ (Sum.inr val)) = v (↑σ (Sum.inr val_1)) →
      ↑σ (Sum.inr val) ≠ ↑σ (Sum.inr val_1) →
        swap (↑σ (Sum.inr val)) (↑σ (Sum.inr val_1)) • Quotient.mk'' σ = Quotient.mk'' σ →
          (↑Perm.sign σ • (↑↑a fun i => v (↑σ (Sum.inl i))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
intro i' j' hv hij _
case h.e'_2.h.e'_6
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
convert smul_zero (M := ℤˣ) (A := N₁ ⊗[R'] N₂) _
case h.e'_2.h.e'_10
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
case h.e'_2.h.e'_6
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
convert TensorProduct.tmul_zero (R := R') (M := N₁) N₂ _
no goals
case h.e'_2.h.e'_10
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
exact AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
intro i' j' hv hij _
case h.e'_2.h.e'_6
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
convert smul_zero (M := ℤˣ) (A := N₁ ⊗[R'] N₂) _
case h.e'_2.h.e'_9
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
case h.e'_2.h.e'_6
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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))) ⊗ₜ[R'] ↑↑b fun i => v (↑σ (Sum.inr i))) = 0
convert TensorProduct.zero_tmul (R := R') N₁ (N := N₂) _
no goals
case h.e'_2.h.e'_9
R : Type ?u.948464
inst✝²¹ : Semiring R
M : Type ?u.948470
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
N : Type ?u.948502
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : Module R N
P : Type ?u.948532
inst✝¹⁶ : AddCommMonoid P
inst✝¹⁵ : Module R P
M' : Type ?u.948562
inst✝¹⁴ : AddCommGroup M'
inst✝¹³ : Module R M'
N' : Type ?u.948950
inst✝¹² : AddCommGroup N'
inst✝¹¹ : Module R N'
ι : Type ?u.949338
ι' : Type ?u.949341
ι'' : Type ?u.949344
ιa : Type u_4
ιb : Type u_6
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_1
Mᵢ : Type u_2
N₁ : Type u_3
N₂ : Type u_5
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 : AlternatingMap R' Mᵢ N₁ ιa
b : AlternatingMap R' Mᵢ N₂ ιb
σ✝ : 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
exact AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)