Theorem: GroupRing.mul_monom_invariant (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
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]
State after:
no goals

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

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 ((0, g) :: tail)) x₀ = coords (mulMonom b h tail) x₀
Tactic:
simp [mulMonom, coords,monom_coords_at_zero]
State after:
no goals

State before:
case addCoeffs
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
a₁ a₂ : R
x : G
tail : FormalSum R G
⊢ coords (mulMonom b h ((a₁, x) :: (a₂, x) :: tail)) x₀ = coords (mulMonom b h ((a₁ + a₂, x) :: tail)) x₀
Tactic:
simp [mulMonom, coords, right_distrib, monom_coords_hom, add_assoc]
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₁ s₂ : FormalSum R G
a : R
x : G
t₁ t₂ : FormalSum R G
a✝ : ElementaryMove R G t₁ t₂
step : coords (mulMonom b h t₁) x₀ = coords (mulMonom b h t₂) x₀
⊢ coords (mulMonom b h ((a, x) :: t₁)) x₀ = coords (mulMonom b h ((a, x) :: t₂)) x₀
Tactic:
simp [mulMonom, coords, step]
State after:
no goals

State before:
case swap
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
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
⊢ coords (mulMonom b h ((a₁, x₁) :: (a₂, x₂) :: tail)) x₀ = coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail)) x₀
Tactic:
simp [mulMonom, coords]
State after:
case swap
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
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)

State before:
case swap
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
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)
Tactic:
conv =>
  lhs
  rw [← add_assoc]
  arg 1
  rw [add_comm]
State after:
case swap
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
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
⊢ monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)

State before:
case swap
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
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
⊢ monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)
Tactic:
rw [← add_assoc]
State after:
no goals