case cons head' tail' =>
  let (b, h) := head'
  induction rel with
  | zeroCoeff tail g a hyp => 
    rw [hyp]
    simp [mul, mulMonom]
    apply funext; intro x₀
    rw [← append_coords]
    simp [coords, monom_coords_at_zero]
    rw [← append_coords]
    simp  
    let rel' : ElementaryMove R G ((0, g) :: tail)  tail := by 
      apply ElementaryMove.zeroCoeff
      rfl
    let prev  := first_arg_invariant  _ _ tail' rel' 
    let pl := congrFun prev x₀
    rw [pl]  
  | addCoeffs a₁ a₂ x tail => 
    simp [mul]
    apply funext; intro x₀
    rw [← append_coords]
    rw [← append_coords]
    simp [coords]
    rw [right_distrib]
    simp [monom_coords_hom]
    let rel' : ElementaryMove R G 
      ((a₁, x) :: (a₂, x) :: tail)
        ((a₁ + a₂, x) :: tail) := by 
        apply ElementaryMove.addCoeffs
    let prev  := first_arg_invariant  _ _ tail' rel' 
    let pl := congrFun prev x₀
    rw [pl]
    simp [add_assoc] 
  | cons a x s₁ s₂ r _ => 
    simp [mul]
    apply funext; intro x₀
    rw [← append_coords]
    rw [← append_coords]
    simp [coords]
    let rel' : ElementaryMove R G 
      ((a, x) :: s₁)
        ((a, x) :: s₂) := by 
        apply ElementaryMove.cons
        assumption 
    let prev  := first_arg_invariant  _ _ tail' rel' 
    let pl := congrFun prev x₀
    rw [pl]
    let ps := mul_monom_invariant b h x₀ s₁ s₂ r
    rw [ps]       
  | swap a₁ a₂ x₁ x₂ tail => 
    simp [mul]
    apply funext; intro x₀
    rw [← append_coords]
    rw [← append_coords]
    rw [mulMonom]
    rw [mulMonom]
    rw [coords]
    rw [coords]
    rw [mulMonom]
    rw [mulMonom]
    rw [coords]
    rw [coords]
    let rel' : ElementaryMove R G 
      ((a₁, x₁) :: (a₂, x₂) :: tail)
        ((a₂, x₂) :: (a₁, x₁) :: tail) := by 
        apply ElementaryMove.swap
    let prev  := first_arg_invariant  _ _ tail' rel' 
    let pl := congrFun prev x₀
    rw [pl]
    simp 
    rw [← add_assoc]
    rw [← add_assoc]
    simp
    conv =>
      lhs 
      rw [add_comm]
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
rel : ElementaryMove R G s₁ s₂
head' : R × G
tail' : List (R × G)
⊢ mul s₁ (head' :: tail') ≈ mul s₂ (head' :: tail')
no goals