exact
  if h₁ : (0 = s₁.coords x) then
    if h₂ : (0 = s₂.coords x) then by
      rw [← h₁, h₂]
    else by
      have lem : x ∈ s₂.support := by
        apply nonzero_coord_in_support
        assumption
      let lem' := eq_mem_of_equalOnList s₂.support s₁.coords s₂.coords x lem ch₂
      exact lem'
  else by
    have lem : x ∈ s₁.support := by
      apply nonzero_coord_in_support
      assumption
    let lem' := eq_mem_of_equalOnList s₁.support s₁.coords s₂.coords x lem ch₁
    exact lem'
case a.h
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₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x
no goals