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

State before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
g x₀ : G
s : FormalSum R G
⊢ coords (mulMonom 0 g s) x₀ = 0
Tactic:
induction s with
| nil =>  
  simp [mulMonom, coords]
| cons h t ih => 
  simp [mulMonom, coords, monom_coords_at_zero]
  assumption
State after:
no goals

State before:
case nil
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
g x₀ : G
⊢ coords (mulMonom 0 g []) x₀ = 0
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
g x₀ : G
h : R × G
t : List (R × G)
ih : coords (mulMonom 0 g t) x₀ = 0
⊢ coords (mulMonom 0 g (h :: t)) x₀ = 0
Tactic:
simp [mulMonom, coords, monom_coords_at_zero]
State after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
g x₀ : G
h : R × G
t : List (R × G)
ih : coords (mulMonom 0 g t) x₀ = 0
⊢ coords (mulMonom 0 g t) x₀ = 0

State before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
g x₀ : G
h : R × G
t : List (R × G)
ih : coords (mulMonom 0 g t) x₀ = 0
⊢ coords (mulMonom 0 g t) x₀ = 0
Tactic:
assumption
State after:
no goals