rw [pl]
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀