R : Type ?u.810983
inst✝²⁰ : Semiring R
M : Type ?u.810989
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
N : Type ?u.811021
inst✝¹⁷ : AddCommMonoid N
inst✝¹⁶ : Module R N
P : Type ?u.811051
inst✝¹⁵ : AddCommMonoid P
inst✝¹⁴ : Module R P
M' : Type ?u.811081
inst✝¹³ : AddCommGroup M'
inst✝¹² : Module R M'
N' : Type ?u.811469
inst✝¹¹ : AddCommGroup N'
inst✝¹⁰ : Module R N'
ι : Type ?u.811857
ι' : Type ?u.811860
ι'' : Type ?u.811863
ιa : Type ?u.811866
ιb : Type ?u.811869
inst✝⁹ : Fintype ιa
inst✝⁸ : Fintype ιb
R' : Type ?u.811878
Mᵢ : Type ?u.811881
N₁ : Type ?u.811884
N₂ : Type ?u.811887
inst✝⁷ : CommSemiring R'
inst✝⁶ : AddCommGroup N₁
inst✝⁵ : Module R' N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R' N₂
inst✝² : AddCommMonoid Mᵢ
inst✝¹ : Module R' Mᵢ
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α ⊕ β)
i j : α ⊕ β
σ✝ : ModSumCongr α β
σ : Perm (α ⊕ β)
⊢ SMul.smul (swap i j) (SMul.smul (swap i j) (Quotient.mk'' σ)) = Quotient.mk'' σ
R : Type ?u.810983
inst✝²⁰ : Semiring R
M : Type ?u.810989
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
N : Type ?u.811021
inst✝¹⁷ : AddCommMonoid N
inst✝¹⁶ : Module R N
P : Type ?u.811051
inst✝¹⁵ : AddCommMonoid P
inst✝¹⁴ : Module R P
M' : Type ?u.811081
inst✝¹³ : AddCommGroup M'
inst✝¹² : Module R M'
N' : Type ?u.811469
inst✝¹¹ : AddCommGroup N'
inst✝¹⁰ : Module R N'
ι : Type ?u.811857
ι' : Type ?u.811860
ι'' : Type ?u.811863
ιa : Type ?u.811866
ιb : Type ?u.811869
inst✝⁹ : Fintype ιa
inst✝⁸ : Fintype ιb
R' : Type ?u.811878
Mᵢ : Type ?u.811881
N₁ : Type ?u.811884
N₂ : Type ?u.811887
inst✝⁷ : CommSemiring R'
inst✝⁶ : AddCommGroup N₁
inst✝⁵ : Module R' N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R' N₂
inst✝² : AddCommMonoid Mᵢ
inst✝¹ : Module R' Mᵢ
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α ⊕ β)
i j : α ⊕ β
σ : ModSumCongr α β
⊢ SMul.smul (swap i j) (SMul.smul (swap i j) σ) = σ
refine Quotient.inductionOn' σ fun σ => ?_
no goals
R : Type ?u.810983
inst✝²⁰ : Semiring R
M : Type ?u.810989
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
N : Type ?u.811021
inst✝¹⁷ : AddCommMonoid N
inst✝¹⁶ : Module R N
P : Type ?u.811051
inst✝¹⁵ : AddCommMonoid P
inst✝¹⁴ : Module R P
M' : Type ?u.811081
inst✝¹³ : AddCommGroup M'
inst✝¹² : Module R M'
N' : Type ?u.811469
inst✝¹¹ : AddCommGroup N'
inst✝¹⁰ : Module R N'
ι : Type ?u.811857
ι' : Type ?u.811860
ι'' : Type ?u.811863
ιa : Type ?u.811866
ιb : Type ?u.811869
inst✝⁹ : Fintype ιa
inst✝⁸ : Fintype ιb
R' : Type ?u.811878
Mᵢ : Type ?u.811881
N₁ : Type ?u.811884
N₂ : Type ?u.811887
inst✝⁷ : CommSemiring R'
inst✝⁶ : AddCommGroup N₁
inst✝⁵ : Module R' N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R' N₂
inst✝² : AddCommMonoid Mᵢ
inst✝¹ : Module R' Mᵢ
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α ⊕ β)
i j : α ⊕ β
σ✝ : ModSumCongr α β
σ : Perm (α ⊕ β)
⊢ SMul.smul (swap i j) (SMul.smul (swap i j) (Quotient.mk'' σ)) = Quotient.mk'' σ
exact _root_.congr_arg Quotient.mk'' (Equiv.swap_mul_involutive i j σ)