internlm/Lean-Github huggingface dataset:
Theorem: GroupRing.mul_monom_assoc
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mulMonom a x s₁ ++ mul s₁ tail)) x₀ =
    coords (mulMonom (a * b) (x * h) s₁ ++ mul s₁ (mulMonom b h tail)) x₀
Tactic:
rw [← append_coords]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mulMonom a x s₁ ++ mul s₁ tail)) x₀ =
    coords (mulMonom (a * b) (x * h) s₁) x₀ + coords (mul s₁ (mulMonom b h tail)) x₀
Theorem: GroupRing.mul_monom_assoc
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mulMonom a x s₁ ++ mul s₁ tail)) x₀ =
    coords (mulMonom (a * b) (x * h) s₁) x₀ + coords (mul s₁ (mulMonom b h tail)) x₀
Tactic:
rw [mul_monom_dist]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mulMonom a x s₁)) x₀ + coords (mulMonom b h (mul s₁ tail)) x₀ =
    coords (mulMonom (a * b) (x * h) s₁) x₀ + coords (mul s₁ (mulMonom b h tail)) x₀
Theorem: GroupRing.mul_monom_assoc
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mulMonom a x s₁)) x₀ + coords (mulMonom b h (mul s₁ tail)) x₀ =
    coords (mulMonom (a * b) (x * h) s₁) x₀ + coords (mul s₁ (mulMonom b h tail)) x₀
Tactic:
rw [ih]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mulMonom a x s₁)) x₀ + coords (mul s₁ (mulMonom b h tail)) x₀ =
    coords (mulMonom (a * b) (x * h) s₁) x₀ + coords (mul s₁ (mulMonom b h tail)) x₀
Theorem: GroupRing.mul_monom_assoc
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mulMonom a x s₁)) x₀ + coords (mul s₁ (mulMonom b h tail)) x₀ =
    coords (mulMonom (a * b) (x * h) s₁) x₀ + coords (mul s₁ (mulMonom b h tail)) x₀
Tactic:
simp [add_assoc, mulMonom]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mulMonom a x s₁)) x₀ = coords (mulMonom (a * b) (x * h) s₁) x₀
Theorem: GroupRing.mul_monom_assoc
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mulMonom a x s₁)) x₀ = coords (mulMonom (a * b) (x * h) s₁) x₀
Tactic:
rw [mul_monom_monom_assoc]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_add
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
s : FormalSum R G
⊢ coords (mulMonom (b₁ + b₂) h s) x₀ = coords (mulMonom b₁ h s) x₀ + coords (mulMonom b₂ h s) x₀
Tactic:
induction s with
| nil => 
simp [mulMonom, coords]
| cons head tail ih => 
  let (a, g) := head
  simp [mulMonom, coords]
  rw [left_distrib]
  rw [monom_coords_hom]
  rw [ih]
  conv =>
    lhs
    rw [add_assoc]
    arg 2
    rw [← add_assoc]
    congr
    rw [add_comm]    
  conv =>
    rhs
    rw [add_assoc]
  conv =>
    rhs 
    arg 2
    skip 
    rw [← add_assoc]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_add
Proof state before:
case nil
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
⊢ coords (mulMonom (b₁ + b₂) h []) x₀ = coords (mulMonom b₁ h []) x₀ + coords (mulMonom b₂ h []) x₀
Tactic:
simp [mulMonom, coords]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_add
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
⊢ coords (mulMonom (b₁ + b₂) h (head :: tail)) x₀ =
    coords (mulMonom b₁ h (head :: tail)) x₀ + coords (mulMonom b₂ h (head :: tail)) x₀
Tactic:
let (a, g) := head
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ coords (mulMonom (b₁ + b₂) h ((a, g) :: tail)) x₀ =
    coords (mulMonom b₁ h ((a, g) :: tail)) x₀ + coords (mulMonom b₂ h ((a, g) :: tail)) x₀
Theorem: GroupRing.mul_monom_add
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ coords (mulMonom (b₁ + b₂) h ((a, g) :: tail)) x₀ =
    coords (mulMonom b₁ h ((a, g) :: tail)) x₀ + coords (mulMonom b₂ h ((a, g) :: tail)) x₀
Tactic:
simp [mulMonom, coords]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * (b₁ + b₂), g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Theorem: GroupRing.mul_monom_add
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * (b₁ + b₂), g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Tactic:
rw [left_distrib]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁ + a * b₂, g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Theorem: GroupRing.mul_monom_add
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁ + a * b₂, g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Tactic:
rw [monom_coords_hom]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) + monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Theorem: GroupRing.mul_monom_add
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) + monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Tactic:
rw [ih]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) + monomCoeff R G x₀ (a * b₂, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀) =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Theorem: GroupRing.mul_monom_add
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) + monomCoeff R G x₀ (a * b₂, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀) =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Tactic:
conv =>
  lhs
  rw [add_assoc]
  arg 2
  rw [← add_assoc]
  congr
  rw [add_comm]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀) =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Theorem: GroupRing.mul_monom_add
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀) =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Tactic:
conv =>
  rhs
  rw [add_assoc]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀) =
    monomCoeff R G x₀ (a * b₁, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀))
Theorem: GroupRing.mul_monom_add
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀) =
    monomCoeff R G x₀ (a * b₁, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀))
Tactic:
conv =>
  rhs 
  arg 2
  skip 
  rw [← add_assoc]
Proof state after:
no goals
Theorem: GroupRing.mul_zero_cons
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
s t : FormalSum R G
⊢ mul s ((0, h) :: t) ≈ mul s t
Tactic:
induction s
Proof state after:
case nil
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
⊢ mul [] ((0, h) :: t) ≈ mul [] t

case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head✝ : R × G
tail✝ : List (R × G)
tail_ih✝ : mul tail✝ ((0, h) :: t) ≈ mul tail✝ t
⊢ mul (head✝ :: tail✝) ((0, h) :: t) ≈ mul (head✝ :: tail✝) t
Theorem: GroupRing.mul_zero_cons
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
⊢ mul [] ((0, h) :: t) ≈ mul [] t
Tactic:
case nil =>
  simp [mul, mulMonom]
  apply eqlCoords.refl
Proof state after:
no goals
Theorem: GroupRing.mul_zero_cons
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
⊢ mul (head :: tail) ((0, h) :: t) ≈ mul (head :: tail) t
Tactic:
case cons head tail _ =>
  simp [mul, mulMonom]
  apply funext ; intro x₀
  simp [coords]
  rw [monom_coords_at_zero]
  rw [zero_add]
  rw [← append_coords]
  simp [coords, mul]
  let l := mul_monom_zero h x₀ tail
  rw [l]
Proof state after:
no goals
Theorem: GroupRing.mul_zero_cons
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
⊢ mul [] ((0, h) :: t) ≈ mul [] t
Tactic:
simp [mul, mulMonom]
Proof state after:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
⊢ mul [] t ≈ mul [] t
Theorem: GroupRing.mul_zero_cons
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
⊢ mul [] t ≈ mul [] t
Tactic:
apply eqlCoords.refl
Proof state after:
no goals
Theorem: GroupRing.mul_zero_cons
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
⊢ mul (head :: tail) ((0, h) :: t) ≈ mul (head :: tail) t
Tactic:
simp [mul, mulMonom]
Proof state after:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
⊢ (0, head.2 * h) :: (mulMonom 0 h tail ++ mul (head :: tail) t) ≈ mul (head :: tail) t
Theorem: GroupRing.mul_zero_cons
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
⊢ (0, head.2 * h) :: (mulMonom 0 h tail ++ mul (head :: tail) t) ≈ mul (head :: tail) t
Tactic:
apply funext
Proof state after:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
⊢ ∀ (x : G), coords ((0, head.2 * h) :: (mulMonom 0 h tail ++ mul (head :: tail) t)) x = coords (mul (head :: tail) t) x
Theorem: GroupRing.mul_zero_cons
Proof state before:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
⊢ ∀ (x : G), coords ((0, head.2 * h) :: (mulMonom 0 h tail ++ mul (head :: tail) t)) x = coords (mul (head :: tail) t) x
Tactic:
intro x₀
Proof state after:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
⊢ coords ((0, head.2 * h) :: (mulMonom 0 h tail ++ mul (head :: tail) t)) x₀ = coords (mul (head :: tail) t) x₀
Theorem: GroupRing.mul_zero_cons
Proof state before:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
⊢ coords ((0, head.2 * h) :: (mulMonom 0 h tail ++ mul (head :: tail) t)) x₀ = coords (mul (head :: tail) t) x₀
Tactic:
simp [coords]
Proof state after:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
⊢ monomCoeff R G x₀ (0, head.2 * h) + coords (mulMonom 0 h tail ++ mul (head :: tail) t) x₀ =
    coords (mul (head :: tail) t) x₀
Theorem: GroupRing.mul_zero_cons
Proof state before:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
⊢ monomCoeff R G x₀ (0, head.2 * h) + coords (mulMonom 0 h tail ++ mul (head :: tail) t) x₀ =
    coords (mul (head :: tail) t) x₀
Tactic:
rw [monom_coords_at_zero]
Proof state after:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
⊢ 0 + coords (mulMonom 0 h tail ++ mul (head :: tail) t) x₀ = coords (mul (head :: tail) t) x₀
Theorem: GroupRing.mul_zero_cons
Proof state before:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
⊢ 0 + coords (mulMonom 0 h tail ++ mul (head :: tail) t) x₀ = coords (mul (head :: tail) t) x₀
Tactic:
rw [zero_add]
Proof state after:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
⊢ coords (mulMonom 0 h tail ++ mul (head :: tail) t) x₀ = coords (mul (head :: tail) t) x₀
Theorem: GroupRing.mul_zero_cons
Proof state before:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
⊢ coords (mulMonom 0 h tail ++ mul (head :: tail) t) x₀ = coords (mul (head :: tail) t) x₀
Tactic:
rw [← append_coords]
Proof state after:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
⊢ coords (mulMonom 0 h tail) x₀ + coords (mul (head :: tail) t) x₀ = coords (mul (head :: tail) t) x₀
Theorem: GroupRing.mul_zero_cons
Proof state before:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
⊢ coords (mulMonom 0 h tail) x₀ + coords (mul (head :: tail) t) x₀ = coords (mul (head :: tail) t) x₀
Tactic:
simp [coords, mul]
Proof state after:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
⊢ coords (mulMonom 0 h tail) x₀ = 0
Theorem: GroupRing.mul_zero_cons
Proof state before:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
⊢ coords (mulMonom 0 h tail) x₀ = 0
Tactic:
let l := mul_monom_zero h x₀ tail
Proof state after:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
l : coords (mulMonom 0 h tail) x₀ = 0 := mul_monom_zero h x₀ tail
⊢ coords (mulMonom 0 h tail) x₀ = 0
Theorem: GroupRing.mul_zero_cons
Proof state before:
case h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
x₀ : G
l : coords (mulMonom 0 h tail) x₀ = 0 := mul_monom_zero h x₀ tail
⊢ coords (mulMonom 0 h tail) x₀ = 0
Tactic:
rw [l]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_invariant
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ s₂ : FormalSum R G
rel : ElementaryMove R G s₁ s₂
⊢ coords (mulMonom b h s₁) x₀ = coords (mulMonom b h s₂) x₀
Tactic:
induction rel with
| zeroCoeff tail g a hyp => 
  rw [hyp]
  simp [mulMonom, coords,monom_coords_at_zero]
| addCoeffs a₁ a₂ x tail => 
  simp [mulMonom, coords, right_distrib, monom_coords_hom, add_assoc]
  
| cons a x t₁ t₂ _ step => 
  simp [mulMonom, coords, step]
| swap a₁ a₂ x₁ x₂ tail => 
  simp [mulMonom, coords]
  conv =>
    lhs
    rw [← add_assoc]
    arg 1
    rw [add_comm]
  rw [← add_assoc]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_invariant
Proof state before:
case zeroCoeff
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ s₂ tail : FormalSum R G
g : G
a : R
hyp : a = 0
⊢ coords (mulMonom b h ((a, g) :: tail)) x₀ = coords (mulMonom b h tail) x₀
Tactic:
rw [hyp]
Proof state after:
case zeroCoeff
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ s₂ tail : FormalSum R G
g : G
a : R
hyp : a = 0
⊢ coords (mulMonom b h ((0, g) :: tail)) x₀ = coords (mulMonom b h tail) x₀