Theorem: ℤα.my_mul_comm (Mordell4/Rt7Ring.lean)

State before:
a b c : ℤα
⊢ mul a b = mul b a
Tactic:
cases a
State after:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ mul { z := z✝, w := w✝ } b = mul b { z := z✝, w := w✝ }

State before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ mul { z := z✝, w := w✝ } b = mul b { z := z✝, w := w✝ }
Tactic:
cases b
State after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ } = mul { z := z✝, w := w✝ } { z := z✝¹, w := w✝¹ }

State before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ } = mul { z := z✝, w := w✝ } { z := z✝¹, w := w✝¹ }
Tactic:
simp only [mul]
State after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ { z := z✝¹ * z✝ - 2 * w✝¹ * w✝, w := z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝ } =
    { z := z✝ * z✝¹ - 2 * w✝ * w✝¹, w := z✝ * w✝¹ + w✝ * z✝¹ + w✝ * w✝¹ }

State before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ { z := z✝¹ * z✝ - 2 * w✝¹ * w✝, w := z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝ } =
    { z := z✝ * z✝¹ - 2 * w✝ * w✝¹, w := z✝ * w✝¹ + w✝ * z✝¹ + w✝ * w✝¹ }
Tactic:
ring
State after:
no goals