Theorem: ℤθ.my_mul_comm (Mordell4/CubicRing.lean)

State before:
a b c : ℤθ
⊢ mul a b = mul b a
Tactic:
cases a
State after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝, g := g✝, h := h✝ } b = mul b { f := f✝, g := g✝, h := h✝ }

State before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝, g := g✝, h := h✝ } b = mul b { f := f✝, g := g✝, h := h✝ }
Tactic:
cases b
State after:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ } =
    mul { f := f✝, g := g✝, h := h✝ } { f := f✝¹, g := g✝¹, h := h✝¹ }

State before:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ } =
    mul { f := f✝, g := g✝, h := h✝ } { f := f✝¹, g := g✝¹, h := h✝¹ }
Tactic:
simp only [mul]
State after:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ { f := f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝,
      g := f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝,
      h := f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝ } =
    { f := f✝ * f✝¹ + 6 * h✝ * h✝¹ - 2 * g✝ * h✝¹ - 2 * h✝ * g✝¹,
      g := f✝ * g✝¹ + g✝ * f✝¹ + 16 * h✝ * h✝¹ - 6 * g✝ * h✝¹ - 6 * h✝ * g✝¹,
      h := f✝ * h✝¹ + h✝ * f✝¹ + g✝ * g✝¹ + 3 * h✝ * h✝¹ - 3 * g✝ * h✝¹ - 3 * h✝ * g✝¹ }

State before:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ { f := f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝,
      g := f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝,
      h := f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝ } =
    { f := f✝ * f✝¹ + 6 * h✝ * h✝¹ - 2 * g✝ * h✝¹ - 2 * h✝ * g✝¹,
      g := f✝ * g✝¹ + g✝ * f✝¹ + 16 * h✝ * h✝¹ - 6 * g✝ * h✝¹ - 6 * h✝ * g✝¹,
      h := f✝ * h✝¹ + h✝ * f✝¹ + g✝ * g✝¹ + 3 * h✝ * h✝¹ - 3 * g✝ * h✝¹ - 3 * h✝ * g✝¹ }
Tactic:
ring
State after:
no goals