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

State before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
s : FormalSum R G
⊢ coords (mulMonom (b₁ + b₂) h s) x₀ = coords (mulMonom b₁ h s) x₀ + coords (mulMonom b₂ h s) x₀
Tactic:
induction s with
| nil => 
simp [mulMonom, coords]
| cons head tail ih => 
  let (a, g) := head
  simp [mulMonom, coords]
  rw [left_distrib]
  rw [monom_coords_hom]
  rw [ih]
  conv =>
    lhs
    rw [add_assoc]
    arg 2
    rw [← add_assoc]
    congr
    rw [add_comm]    
  conv =>
    rhs
    rw [add_assoc]
  conv =>
    rhs 
    arg 2
    skip 
    rw [← add_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₁ b₂ : R
h x₀ : G
⊢ coords (mulMonom (b₁ + b₂) h []) x₀ = coords (mulMonom b₁ h []) x₀ + coords (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₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
⊢ coords (mulMonom (b₁ + b₂) h (head :: tail)) x₀ =
    coords (mulMonom b₁ h (head :: tail)) x₀ + coords (mulMonom b₂ h (head :: tail)) x₀
Tactic:
let (a, g) := head
State after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ coords (mulMonom (b₁ + b₂) h ((a, g) :: tail)) x₀ =
    coords (mulMonom b₁ h ((a, g) :: tail)) x₀ + coords (mulMonom b₂ h ((a, g) :: tail)) x₀

State before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ coords (mulMonom (b₁ + b₂) h ((a, g) :: tail)) x₀ =
    coords (mulMonom b₁ h ((a, g) :: tail)) x₀ + coords (mulMonom b₂ h ((a, g) :: tail)) x₀
Tactic:
simp [mulMonom, coords]
State after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * (b₁ + b₂), g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (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₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * (b₁ + b₂), g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Tactic:
rw [left_distrib]
State after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁ + a * b₂, g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (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₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁ + a * b₂, g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Tactic:
rw [monom_coords_hom]
State after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) + monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (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₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) + monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (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₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) + monomCoeff R G x₀ (a * b₂, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀) =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (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₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) + monomCoeff R G x₀ (a * b₂, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀) =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Tactic:
conv =>
  lhs
  rw [add_assoc]
  arg 2
  rw [← add_assoc]
  congr
  rw [add_comm]
State after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀) =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (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₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀) =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)
Tactic:
conv =>
  rhs
  rw [add_assoc]
State after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀) =
    monomCoeff R G x₀ (a * b₁, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + (monomCoeff R G x₀ (a * b₂, g * h) + coords (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₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * b₁, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀) =
    monomCoeff R G x₀ (a * b₁, g * h) +
      (coords (mulMonom b₁ h tail) x₀ + (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀))
Tactic:
conv =>
  rhs 
  arg 2
  skip 
  rw [← add_assoc]
State after:
no goals