Theorem: GroupRing.first_arg_invariant (UnitConjecture/GroupRing.lean)

State before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ t : FormalSum R G
rel : ElementaryMove R G s₁ s₂
⊢ mul s₁ t ≈ mul s₂ t
Tactic:
cases t
State after:
case nil
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₂
⊢ mul s₁ [] ≈ mul s₂ []

case cons
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✝)

State before:
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₂
⊢ mul s₁ [] ≈ mul s₂ []
Tactic:
case nil => 
  simp [mul]
  rfl
State after:
no goals

State before:
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')
Tactic:
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]
State after:
no goals

State before:
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₂
⊢ mul s₁ [] ≈ mul s₂ []
Tactic:
simp [mul]
State after:
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₂
⊢ [] ≈ []

State before:
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₂
⊢ [] ≈ []
Tactic:
rfl
State after:
no goals

State before:
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')
Tactic:
let (b, h) := head'
State after:
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')

State before:
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')
Tactic:
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]
State after:
no goals

State before:
case zeroCoeff
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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
⊢ mul ((a, g) :: tail) ((b, h) :: tail') ≈ mul tail ((b, h) :: tail')
Tactic:
rw [hyp]
State after:
case zeroCoeff
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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
⊢ mul ((0, g) :: tail) ((b, h) :: tail') ≈ mul tail ((b, h) :: tail')

State before:
case zeroCoeff
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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
⊢ mul ((0, g) :: tail) ((b, h) :: tail') ≈ mul tail ((b, h) :: tail')
Tactic:
simp [mul, mulMonom]
State after:
case zeroCoeff
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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
⊢ (0, g * h) :: (mulMonom b h tail ++ mul ((0, g) :: tail) tail') ≈ mulMonom b h tail ++ mul tail tail'

State before:
case zeroCoeff
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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
⊢ (0, g * h) :: (mulMonom b h tail ++ mul ((0, g) :: tail) tail') ≈ mulMonom b h tail ++ mul tail tail'
Tactic:
apply funext
State after:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
⊢ ∀ (x : G),
    coords ((0, g * h) :: (mulMonom b h tail ++ mul ((0, g) :: tail) tail')) x =
      coords (mulMonom b h tail ++ mul tail tail') x

State before:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
⊢ ∀ (x : G),
    coords ((0, g * h) :: (mulMonom b h tail ++ mul ((0, g) :: tail) tail')) x =
      coords (mulMonom b h tail ++ mul tail tail') x
Tactic:
intro x₀
State after:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ coords ((0, g * h) :: (mulMonom b h tail ++ mul ((0, g) :: tail) tail')) x₀ =
    coords (mulMonom b h tail ++ mul tail tail') x₀

State before:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ coords ((0, g * h) :: (mulMonom b h tail ++ mul ((0, g) :: tail) tail')) x₀ =
    coords (mulMonom b h tail ++ mul tail tail') x₀
Tactic:
rw [← append_coords]
State after:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ coords ((0, g * h) :: (mulMonom b h tail ++ mul ((0, g) :: tail) tail')) x₀ =
    coords (mulMonom b h tail) x₀ + coords (mul tail tail') x₀

State before:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ coords ((0, g * h) :: (mulMonom b h tail ++ mul ((0, g) :: tail) tail')) x₀ =
    coords (mulMonom b h tail) x₀ + coords (mul tail tail') x₀
Tactic:
simp [coords, monom_coords_at_zero]
State after:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ coords (mulMonom b h tail ++ mul ((0, g) :: tail) tail') x₀ =
    coords (mulMonom b h tail) x₀ + coords (mul tail tail') x₀

State before:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ coords (mulMonom b h tail ++ mul ((0, g) :: tail) tail') x₀ =
    coords (mulMonom b h tail) x₀ + coords (mul tail tail') x₀
Tactic:
rw [← append_coords]
State after:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ coords (mulMonom b h tail) x₀ + coords (mul ((0, g) :: tail) tail') x₀ =
    coords (mulMonom b h tail) x₀ + coords (mul tail tail') x₀

State before:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ coords (mulMonom b h tail) x₀ + coords (mul ((0, g) :: tail) tail') x₀ =
    coords (mulMonom b h tail) x₀ + coords (mul tail tail') x₀
Tactic:
simp
State after:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀

State before:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀
Tactic:
let rel' : ElementaryMove R G ((0, g) :: tail)  tail := by 
  apply ElementaryMove.zeroCoeff
  rfl
State after:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
rel' : ElementaryMove R G ((0, g) :: tail) tail := zeroCoeff tail g 0 (Eq.refl 0)
⊢ coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀

State before:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
rel' : ElementaryMove R G ((0, g) :: tail) tail := zeroCoeff tail g 0 (Eq.refl 0)
⊢ coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀
Tactic:
let prev  := first_arg_invariant  _ _ tail' rel'
State after:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
rel' : ElementaryMove R G ((0, g) :: tail) tail := zeroCoeff tail g 0 (Eq.refl 0)
prev : mul ((0, g) :: tail) tail' ≈ mul tail tail' := first_arg_invariant ((0, g) :: tail) tail tail' rel'
⊢ coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀

State before:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
rel' : ElementaryMove R G ((0, g) :: tail) tail := zeroCoeff tail g 0 (Eq.refl 0)
prev : mul ((0, g) :: tail) tail' ≈ mul tail tail' := first_arg_invariant ((0, g) :: tail) tail tail' rel'
⊢ coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀
Tactic:
let pl := congrFun prev x₀
State after:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
rel' : ElementaryMove R G ((0, g) :: tail) tail := zeroCoeff tail g 0 (Eq.refl 0)
prev : mul ((0, g) :: tail) tail' ≈ mul tail tail' := first_arg_invariant ((0, g) :: tail) tail tail' rel'
pl : coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀ := congrFun prev x₀
⊢ coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀

State before:
case zeroCoeff.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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
rel' : ElementaryMove R G ((0, g) :: tail) tail := zeroCoeff tail g 0 (Eq.refl 0)
prev : mul ((0, g) :: tail) tail' ≈ mul tail tail' := first_arg_invariant ((0, g) :: tail) tail tail' rel'
pl : coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀ := congrFun prev x₀
⊢ coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀
Tactic:
rw [pl]
State after:
no goals

State before:
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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ ElementaryMove R G ((0, g) :: tail) tail
Tactic:
apply ElementaryMove.zeroCoeff
State after:
case 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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ 0 = 0

State before:
case 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
tail : FormalSum R G
g : G
a : R
hyp : a = 0
x₀ : G
⊢ 0 = 0
Tactic:
rfl
State after:
no goals

State before:
case addCoeffs
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 : G
tail : FormalSum R G
⊢ mul ((a₁, x) :: (a₂, x) :: tail) ((b, h) :: tail') ≈ mul ((a₁ + a₂, x) :: tail) ((b, h) :: tail')
Tactic:
simp [mul]
State after:
case addCoeffs
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 : G
tail : FormalSum R G
⊢ mulMonom b h ((a₁, x) :: (a₂, x) :: tail) ++ mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈
    mulMonom b h ((a₁ + a₂, x) :: tail) ++ mul ((a₁ + a₂, x) :: tail) tail'

State before:
case addCoeffs
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 : G
tail : FormalSum R G
⊢ mulMonom b h ((a₁, x) :: (a₂, x) :: tail) ++ mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈
    mulMonom b h ((a₁ + a₂, x) :: tail) ++ mul ((a₁ + a₂, x) :: tail) tail'
Tactic:
apply funext
State after:
case addCoeffs.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 : G
tail : FormalSum R G
⊢ ∀ (x_1 : G),
    coords (mulMonom b h ((a₁, x) :: (a₂, x) :: tail) ++ mul ((a₁, x) :: (a₂, x) :: tail) tail') x_1 =
      coords (mulMonom b h ((a₁ + a₂, x) :: tail) ++ mul ((a₁ + a₂, x) :: tail) tail') x_1

State before:
case addCoeffs.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 : G
tail : FormalSum R G
⊢ ∀ (x_1 : G),
    coords (mulMonom b h ((a₁, x) :: (a₂, x) :: tail) ++ mul ((a₁, x) :: (a₂, x) :: tail) tail') x_1 =
      coords (mulMonom b h ((a₁ + a₂, x) :: tail) ++ mul ((a₁ + a₂, x) :: tail) tail') x_1
Tactic:
intro x₀
State after:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
⊢ coords (mulMonom b h ((a₁, x) :: (a₂, x) :: tail) ++ mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₁ + a₂, x) :: tail) ++ mul ((a₁ + a₂, x) :: tail) tail') x₀

State before:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
⊢ coords (mulMonom b h ((a₁, x) :: (a₂, x) :: tail) ++ mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₁ + a₂, x) :: tail) ++ mul ((a₁ + a₂, x) :: tail) tail') x₀
Tactic:
rw [← append_coords]
State after:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
⊢ coords (mulMonom b h ((a₁, x) :: (a₂, x) :: tail)) x₀ + coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₁ + a₂, x) :: tail) ++ mul ((a₁ + a₂, x) :: tail) tail') x₀

State before:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
⊢ coords (mulMonom b h ((a₁, x) :: (a₂, x) :: tail)) x₀ + coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₁ + a₂, x) :: tail) ++ mul ((a₁ + a₂, x) :: tail) tail') x₀
Tactic:
rw [← append_coords]
State after:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
⊢ coords (mulMonom b h ((a₁, x) :: (a₂, x) :: tail)) x₀ + coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₁ + a₂, x) :: tail)) x₀ + coords (mul ((a₁ + a₂, x) :: tail) tail') x₀

State before:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
⊢ coords (mulMonom b h ((a₁, x) :: (a₂, x) :: tail)) x₀ + coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₁ + a₂, x) :: tail)) x₀ + coords (mul ((a₁ + a₂, x) :: tail) tail') x₀
Tactic:
simp [coords]
State after:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
⊢ 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₁ + a₂) * b, x * h) + coords (mulMonom b h tail) x₀ +
      coords (mul ((a₁ + a₂, x) :: tail) tail') x₀

State before:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
⊢ 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₁ + a₂) * b, x * h) + coords (mulMonom b h tail) x₀ +
      coords (mul ((a₁ + a₂, x) :: tail) tail') x₀
Tactic:
rw [right_distrib]
State after:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
⊢ 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 + a₂ * b, x * h) + coords (mulMonom b h tail) x₀ +
      coords (mul ((a₁ + a₂, x) :: tail) tail') x₀

State before:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
⊢ 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 + a₂ * b, x * h) + coords (mulMonom b h tail) x₀ +
      coords (mul ((a₁ + a₂, x) :: tail) tail') x₀
Tactic:
simp [monom_coords_hom]
State after:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
⊢ 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₁ + a₂, x) :: tail) tail') x₀

State before:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
⊢ 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₁ + a₂, x) :: tail) tail') x₀
Tactic:
let rel' : ElementaryMove R G 
  ((a₁, x) :: (a₂, x) :: tail)
    ((a₁ + a₂, x) :: tail) := by 
    apply ElementaryMove.addCoeffs
State after:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) := addCoeffs a₁ a₂ x tail
⊢ 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₁ + a₂, x) :: tail) tail') x₀

State before:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) := addCoeffs a₁ a₂ x tail
⊢ 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₁ + a₂, x) :: tail) tail') x₀
Tactic:
let prev  := first_arg_invariant  _ _ tail' rel'
State after:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) := addCoeffs a₁ a₂ x tail
prev : mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈ mul ((a₁ + a₂, x) :: tail) tail' :=
  first_arg_invariant ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) tail' rel'
⊢ 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₁ + a₂, x) :: tail) tail') x₀

State before:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) := addCoeffs a₁ a₂ x tail
prev : mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈ mul ((a₁ + a₂, x) :: tail) tail' :=
  first_arg_invariant ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) tail' rel'
⊢ 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₁ + a₂, x) :: tail) tail') x₀
Tactic:
let pl := congrFun prev x₀
State after:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) := addCoeffs a₁ a₂ x tail
prev : mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈ mul ((a₁ + a₂, x) :: tail) tail' :=
  first_arg_invariant ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) tail' rel'
pl : coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = coords (mul ((a₁ + 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₁ + a₂, x) :: tail) tail') x₀

State before:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) := addCoeffs a₁ a₂ x tail
prev : mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈ mul ((a₁ + a₂, x) :: tail) tail' :=
  first_arg_invariant ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) tail' rel'
pl : coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = coords (mul ((a₁ + 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₁ + a₂, x) :: tail) tail') x₀
Tactic:
rw [pl]
State after:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) := addCoeffs a₁ a₂ x tail
prev : mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈ mul ((a₁ + a₂, x) :: tail) tail' :=
  first_arg_invariant ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) tail' rel'
pl : coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = coords (mul ((a₁ + 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₁ + 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₁ + a₂, x) :: tail) tail') x₀

State before:
case addCoeffs.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 : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) := addCoeffs a₁ a₂ x tail
prev : mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈ mul ((a₁ + a₂, x) :: tail) tail' :=
  first_arg_invariant ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) tail' rel'
pl : coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = coords (mul ((a₁ + 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₁ + 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₁ + a₂, x) :: tail) tail') x₀
Tactic:
simp [add_assoc]
State after:
no goals

State before:
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 : G
tail : FormalSum R G
x₀ : G
⊢ ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail)
Tactic:
apply ElementaryMove.addCoeffs
State after:
no goals

State before:
case cons
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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
⊢ mul ((a, x) :: s₁) ((b, h) :: tail') ≈ mul ((a, x) :: s₂) ((b, h) :: tail')
Tactic:
simp [mul]
State after:
case cons
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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
⊢ mulMonom b h ((a, x) :: s₁) ++ mul ((a, x) :: s₁) tail' ≈ mulMonom b h ((a, x) :: s₂) ++ mul ((a, x) :: s₂) tail'

State before:
case cons
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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
⊢ mulMonom b h ((a, x) :: s₁) ++ mul ((a, x) :: s₁) tail' ≈ mulMonom b h ((a, x) :: s₂) ++ mul ((a, x) :: s₂) tail'
Tactic:
apply funext
State after:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
⊢ ∀ (x_1 : G),
    coords (mulMonom b h ((a, x) :: s₁) ++ mul ((a, x) :: s₁) tail') x_1 =
      coords (mulMonom b h ((a, x) :: s₂) ++ mul ((a, x) :: s₂) tail') x_1

State before:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
⊢ ∀ (x_1 : G),
    coords (mulMonom b h ((a, x) :: s₁) ++ mul ((a, x) :: s₁) tail') x_1 =
      coords (mulMonom b h ((a, x) :: s₂) ++ mul ((a, x) :: s₂) tail') x_1
Tactic:
intro x₀
State after:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
⊢ coords (mulMonom b h ((a, x) :: s₁) ++ mul ((a, x) :: s₁) tail') x₀ =
    coords (mulMonom b h ((a, x) :: s₂) ++ mul ((a, x) :: s₂) tail') x₀

State before:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
⊢ coords (mulMonom b h ((a, x) :: s₁) ++ mul ((a, x) :: s₁) tail') x₀ =
    coords (mulMonom b h ((a, x) :: s₂) ++ mul ((a, x) :: s₂) tail') x₀
Tactic:
rw [← append_coords]
State after:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
⊢ coords (mulMonom b h ((a, x) :: s₁)) x₀ + coords (mul ((a, x) :: s₁) tail') x₀ =
    coords (mulMonom b h ((a, x) :: s₂) ++ mul ((a, x) :: s₂) tail') x₀

State before:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
⊢ coords (mulMonom b h ((a, x) :: s₁)) x₀ + coords (mul ((a, x) :: s₁) tail') x₀ =
    coords (mulMonom b h ((a, x) :: s₂) ++ mul ((a, x) :: s₂) tail') x₀
Tactic:
rw [← append_coords]
State after:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
⊢ coords (mulMonom b h ((a, x) :: s₁)) x₀ + coords (mul ((a, x) :: s₁) tail') x₀ =
    coords (mulMonom b h ((a, x) :: s₂)) x₀ + coords (mul ((a, x) :: s₂) tail') x₀

State before:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
⊢ coords (mulMonom b h ((a, x) :: s₁)) x₀ + coords (mul ((a, x) :: s₁) tail') x₀ =
    coords (mulMonom b h ((a, x) :: s₂)) x₀ + coords (mul ((a, x) :: s₂) tail') x₀
Tactic:
simp [coords]
State after:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
⊢ monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₁) x₀ + coords (mul ((a, x) :: s₁) tail') x₀ =
    monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₂) x₀ + coords (mul ((a, x) :: s₂) tail') x₀

State before:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
⊢ monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₁) x₀ + coords (mul ((a, x) :: s₁) tail') x₀ =
    monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₂) x₀ + coords (mul ((a, x) :: s₂) tail') x₀
Tactic:
let rel' : ElementaryMove R G 
  ((a, x) :: s₁)
    ((a, x) :: s₂) := by 
    apply ElementaryMove.cons
    assumption
State after:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
rel' : ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂) := cons a x s₁ s₂ r
⊢ monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₁) x₀ + coords (mul ((a, x) :: s₁) tail') x₀ =
    monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₂) x₀ + coords (mul ((a, x) :: s₂) tail') x₀

State before:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
rel' : ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂) := cons a x s₁ s₂ r
⊢ monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₁) x₀ + coords (mul ((a, x) :: s₁) tail') x₀ =
    monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₂) x₀ + coords (mul ((a, x) :: s₂) tail') x₀
Tactic:
let prev  := first_arg_invariant  _ _ tail' rel'
State after:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
rel' : ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂) := cons a x s₁ s₂ r
prev : mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail' :=
  first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel'
⊢ monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₁) x₀ + coords (mul ((a, x) :: s₁) tail') x₀ =
    monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₂) x₀ + coords (mul ((a, x) :: s₂) tail') x₀

State before:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
rel' : ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂) := cons a x s₁ s₂ r
prev : mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail' :=
  first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel'
⊢ monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₁) x₀ + coords (mul ((a, x) :: s₁) tail') x₀ =
    monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₂) x₀ + coords (mul ((a, x) :: s₂) tail') x₀
Tactic:
let pl := congrFun prev x₀
State after:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
rel' : ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂) := cons a x s₁ s₂ r
prev : mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail' :=
  first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel'
pl : coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀ := congrFun prev x₀
⊢ monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₁) x₀ + coords (mul ((a, x) :: s₁) tail') x₀ =
    monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₂) x₀ + coords (mul ((a, x) :: s₂) tail') x₀

State before:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
rel' : ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂) := cons a x s₁ s₂ r
prev : mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail' :=
  first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel'
pl : coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀ := congrFun prev x₀
⊢ monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₁) x₀ + coords (mul ((a, x) :: s₁) tail') x₀ =
    monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₂) x₀ + coords (mul ((a, x) :: s₂) tail') x₀
Tactic:
rw [pl]
State after:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
rel' : ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂) := cons a x s₁ s₂ r
prev : mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail' :=
  first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel'
pl : coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀ := congrFun prev x₀
⊢ monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₁) x₀ + coords (mul ((a, x) :: s₂) tail') x₀ =
    monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₂) x₀ + coords (mul ((a, x) :: s₂) tail') x₀

State before:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
rel' : ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂) := cons a x s₁ s₂ r
prev : mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail' :=
  first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel'
pl : coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀ := congrFun prev x₀
⊢ monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₁) x₀ + coords (mul ((a, x) :: s₂) tail') x₀ =
    monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₂) x₀ + coords (mul ((a, x) :: s₂) tail') x₀
Tactic:
let ps := mul_monom_invariant b h x₀ s₁ s₂ r
State after:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
rel' : ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂) := cons a x s₁ s₂ r
prev : mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail' :=
  first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel'
pl : coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀ := congrFun prev x₀
ps : coords (mulMonom b h s₁) x₀ = coords (mulMonom b h s₂) x₀ := mul_monom_invariant b h x₀ s₁ s₂ r
⊢ monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₁) x₀ + coords (mul ((a, x) :: s₂) tail') x₀ =
    monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₂) x₀ + coords (mul ((a, x) :: s₂) tail') x₀

State before:
case cons.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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
rel' : ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂) := cons a x s₁ s₂ r
prev : mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail' :=
  first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel'
pl : coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀ := congrFun prev x₀
ps : coords (mulMonom b h s₁) x₀ = coords (mulMonom b h s₂) x₀ := mul_monom_invariant b h x₀ s₁ s₂ r
⊢ monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₁) x₀ + coords (mul ((a, x) :: s₂) tail') x₀ =
    monomCoeff R G x₀ (a * b, x * h) + coords (mulMonom b h s₂) x₀ + coords (mul ((a, x) :: s₂) tail') x₀
Tactic:
rw [ps]
State after:
no goals

State before:
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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
⊢ ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂)
Tactic:
apply ElementaryMove.cons
State after:
case a
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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
⊢ ElementaryMove R G s₁ s₂

State before:
case a
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 : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
⊢ ElementaryMove R G s₁ s₂
Tactic:
assumption
State after:
no goals

State before:
case swap
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
⊢ mul ((a₁, x₁) :: (a₂, x₂) :: tail) ((b, h) :: tail') ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) ((b, h) :: tail')
Tactic:
simp [mul]
State after:
case swap
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
⊢ mulMonom b h ((a₁, x₁) :: (a₂, x₂) :: tail) ++ mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈
    mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail) ++ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'

State before:
case swap
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
⊢ mulMonom b h ((a₁, x₁) :: (a₂, x₂) :: tail) ++ mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈
    mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail) ++ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
Tactic:
apply funext
State after:
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),
    coords (mulMonom b h ((a₁, x₁) :: (a₂, x₂) :: tail) ++ mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x =
      coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail) ++ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x

State before:
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),
    coords (mulMonom b h ((a₁, x₁) :: (a₂, x₂) :: tail) ++ mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x =
      coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail) ++ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x
Tactic:
intro x₀
State after:
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
⊢ coords (mulMonom b h ((a₁, x₁) :: (a₂, x₂) :: tail) ++ mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail) ++ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀

State before:
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
⊢ coords (mulMonom b h ((a₁, x₁) :: (a₂, x₂) :: tail) ++ mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail) ++ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
rw [← append_coords]
State after:
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
⊢ coords (mulMonom b h ((a₁, x₁) :: (a₂, x₂) :: tail)) x₀ + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail) ++ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀

State before:
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
⊢ coords (mulMonom b h ((a₁, x₁) :: (a₂, x₂) :: tail)) x₀ + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail) ++ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
rw [← append_coords]
State after:
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
⊢ coords (mulMonom b h ((a₁, x₁) :: (a₂, x₂) :: tail)) x₀ + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail)) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀

State before:
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
⊢ coords (mulMonom b h ((a₁, x₁) :: (a₂, x₂) :: tail)) x₀ + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail)) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
rw [mulMonom]
State after:
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
⊢ coords ((a₁ * b, x₁ * h) :: mulMonom b h ((a₂, x₂) :: tail)) x₀ +
      coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail)) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀

State before:
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
⊢ coords ((a₁ * b, x₁ * h) :: mulMonom b h ((a₂, x₂) :: tail)) x₀ +
      coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail)) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
rw [mulMonom]
State after:
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
⊢ coords ((a₁ * b, x₁ * h) :: (a₂ * b, x₂ * h) :: mulMonom b h tail) x₀ +
      coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail)) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀

State before:
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
⊢ coords ((a₁ * b, x₁ * h) :: (a₂ * b, x₂ * h) :: mulMonom b h tail) x₀ +
      coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail)) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
rw [coords]
State after:
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
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords ((a₂ * b, x₂ * h) :: mulMonom b h tail) x₀ +
      coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail)) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀

State before:
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
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords ((a₂ * b, x₂ * h) :: mulMonom b h tail) x₀ +
      coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail)) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
rw [coords]
State after:
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
⊢ 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₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail)) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀

State before:
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
⊢ 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₀ =
    coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail)) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
rw [mulMonom]
State after:
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
⊢ 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₀ =
    coords ((a₂ * b, x₂ * h) :: mulMonom b h ((a₁, x₁) :: tail)) x₀ +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀

State before:
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
⊢ 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₀ =
    coords ((a₂ * b, x₂ * h) :: mulMonom b h ((a₁, x₁) :: tail)) x₀ +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
rw [mulMonom]
State after:
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
⊢ 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₀ =
    coords ((a₂ * b, x₂ * h) :: (a₁ * b, x₁ * h) :: mulMonom b h tail) x₀ +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀

State before:
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
⊢ 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₀ =
    coords ((a₂ * b, x₂ * h) :: (a₁ * b, x₁ * h) :: mulMonom b h tail) x₀ +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
rw [coords]
State after:
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
⊢ 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) + coords ((a₁ * b, x₁ * h) :: mulMonom b h tail) x₀ +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀

State before:
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
⊢ 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) + coords ((a₁ * b, x₁ * h) :: mulMonom b h tail) x₀ +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
rw [coords]
State after:
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
⊢ 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₀

State before:
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
⊢ 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₀
Tactic:
let rel' : ElementaryMove R G 
  ((a₁, x₁) :: (a₂, x₂) :: tail)
    ((a₂, x₂) :: (a₁, x₁) :: tail) := by 
    apply ElementaryMove.swap
State after:
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
⊢ 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₀

State before:
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
⊢ 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₀
Tactic:
let prev  := first_arg_invariant  _ _ tail' rel'
State after:
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'
⊢ 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₀

State before:
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'
⊢ 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₀
Tactic:
let pl := congrFun prev x₀
State after:
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₀

State before:
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₀
Tactic:
rw [pl]
State after:
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₀

State before:
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₀
Tactic:
simp
State after:
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₀) =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)

State before:
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₀) =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)
Tactic:
rw [← add_assoc]
State after:
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₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)

State before:
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₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)
Tactic:
rw [← add_assoc]
State after:
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₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀

State before:
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₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀
Tactic:
simp
State after:
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) =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)

State before:
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) =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)
Tactic:
conv =>
  lhs 
  rw [add_comm]
State after:
no goals

State before:
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
⊢ ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
Tactic:
apply ElementaryMove.swap
State after:
no goals