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)
b : R
h : G
⊢ mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
no goals