internlm/Lean-Github huggingface dataset:
Theorem: GroupRing.first_arg_invariant
Proof 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]
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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]
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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]
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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]
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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]
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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'
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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₀
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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]
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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]
Proof state after:
no goals
Theorem: GroupRing.first_arg_invariant
Proof 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
Proof state after:
no goals
Theorem: GroupRing.first_arg_invariant
Proof 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]
Proof 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'
Theorem: GroupRing.first_arg_invariant
Proof 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
Proof 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
Theorem: GroupRing.first_arg_invariant
Proof 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₀
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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]
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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]
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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]
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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'
Proof 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₀
Theorem: GroupRing.first_arg_invariant
Proof 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₀
Proof 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₀