apply Eq.trans eqn₄
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)]
⊢ sum [(a₀, x₀), (coords t x₀, x₀)] = sum []
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)]
⊢ sum [(a₀ + coords t x₀, x₀)] = sum []