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

State before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x : G
a b : R
h x₀ : G
s : FormalSum R G
⊢ coords (mulMonom b h (mulMonom a x s)) x₀ = coords (mulMonom (a * b) (x * h) s) x₀
Tactic:
induction s with
| nil => 
  simp [mulMonom, coords]
| cons head tail ih =>
  let (a₁, x₁) := head
  simp [mulMonom, coords, mul_assoc]
  rw [ih]
State after:
no goals

State before:
case nil
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x : G
a b : R
h x₀ : G
⊢ coords (mulMonom b h (mulMonom a x [])) x₀ = coords (mulMonom (a * b) (x * 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
x : G
a b : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
⊢ coords (mulMonom b h (mulMonom a x (head :: tail))) x₀ = coords (mulMonom (a * b) (x * 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
x : G
a b : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
a₁ : R
x₁ : G
⊢ coords (mulMonom b h (mulMonom a x ((a₁, x₁) :: tail))) x₀ = coords (mulMonom (a * b) (x * 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
x : G
a b : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
a₁ : R
x₁ : G
⊢ coords (mulMonom b h (mulMonom a x ((a₁, x₁) :: tail))) x₀ = coords (mulMonom (a * b) (x * h) ((a₁, x₁) :: tail)) x₀
Tactic:
simp [mulMonom, coords, mul_assoc]
State after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x : G
a b : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
a₁ : R
x₁ : G
⊢ coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀

State before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x : G
a b : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
a₁ : R
x₁ : G
⊢ coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
Tactic:
rw [ih]
State after:
no goals