apply Eq.trans (Eq.trans (Eq.symm eq₂) eq₁) eq₃
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
eq₃ : s₃ ≃ s₂
⊢ (a₀, x₀) :: t ≃ s₂
no goals