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

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
⊢ coords (mulMonom b h (mul s₁ s₂)) x₀ = coords (mul s₁ (mulMonom b h s₂)) x₀
Tactic:
induction s₂ with
| nil => 
  simp [mulMonom, coords]
| cons head tail ih =>
  let (a, x) := head
  simp [mulMonom, coords, mul]
  rw [← append_coords]
  rw [mul_monom_dist]
  rw [ih]
  simp [add_assoc, mulMonom]
  rw [mul_monom_monom_assoc]
State after:
no goals

State before:
case nil
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
⊢ coords (mulMonom b h (mul s₁ [])) x₀ = coords (mul s₁ (mulMonom b h [])) x₀
Tactic:
simp [mulMonom, coords]
State after:
no goals

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₀
⊢ coords (mulMonom b h (mul s₁ (head :: tail))) x₀ = coords (mul s₁ (mulMonom b h (head :: tail))) x₀
Tactic:
let (a, x) := head
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 (mul s₁ ((a, x) :: tail))) x₀ = coords (mul s₁ (mulMonom b h ((a, x) :: tail))) x₀

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 (mul s₁ ((a, x) :: tail))) x₀ = coords (mul s₁ (mulMonom b h ((a, x) :: tail))) x₀
Tactic:
simp [mulMonom, coords, mul]
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₁ ++ mul s₁ (mulMonom b h tail)) x₀

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

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

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

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

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