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

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
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

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
State after:
no goals

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]
State after:
no goals

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]
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

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
State after:
no goals

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]
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

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
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

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₀
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₀

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]
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₀

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]
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₀

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]
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₀

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]
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₀

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]
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

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
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

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]
State after:
no goals