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

State before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₂ s₃ : FormalSum R G
⊢ coords (mul s₁ (s₂ ++ s₃)) x₀ = coords (mul s₁ s₂) x₀ + coords (mul s₁ s₃) x₀
Tactic:
induction s₂ with
| nil => 
  simp [mulMonom, coords]
| cons head tail ih =>
  simp [mulMonom, coords, mul]
  rw [← append_coords]
  rw [← append_coords]
  rw [ih]
  simp [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
x₀ : G
s₁ s₃ : FormalSum R G
⊢ coords (mul s₁ ([] ++ s₃)) x₀ = coords (mul s₁ []) x₀ + coords (mul s₁ s₃) 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
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mul s₁ (head :: tail ++ s₃)) x₀ = coords (mul s₁ (head :: tail)) x₀ + coords (mul s₁ s₃) 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
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁ ++ mul s₁ (tail ++ s₃)) x₀ =
    coords (mulMonom head.1 head.2 s₁ ++ mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀

State before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁ ++ mul s₁ (tail ++ s₃)) x₀ =
    coords (mulMonom head.1 head.2 s₁ ++ mul s₁ tail) x₀ + coords (mul s₁ s₃) 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
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ (tail ++ s₃)) x₀ =
    coords (mulMonom head.1 head.2 s₁ ++ mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀

State before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ (tail ++ s₃)) x₀ =
    coords (mulMonom head.1 head.2 s₁ ++ mul s₁ tail) x₀ + coords (mul s₁ s₃) 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
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ (tail ++ s₃)) x₀ =
    coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀

State before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ (tail ++ s₃)) x₀ =
    coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
Tactic:
rw [ih]
State after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁) x₀ + (coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀) =
    coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀

State before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁) x₀ + (coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀) =
    coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
Tactic:
simp [add_assoc]
State after:
no goals