let ch₁ := eql_on_support_of_true c₁
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂