rw [← ls, ← lt]
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
ls : coords s₁ x₀ = coords s₂ x₀
lt : coords t₁ x₀ = coords t₂ x₀
⊢ coords s₁ x₀ + coords t₁ x₀ = coords s₂ x₀ + coords t₂ x₀
no goals