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

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

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

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

State before:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul (mul { f := f✝², g := g✝², h := h✝² } { f := f✝¹, g := g✝¹, h := h✝¹ }) { f := f✝, g := g✝, h := h✝ } =
    mul { 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.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ {
      f :=
        (f✝² * f✝¹ + 6 * h✝² * h✝¹ - 2 * g✝² * h✝¹ - 2 * h✝² * g✝¹) * f✝ +
              6 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * h✝ -
            2 * (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * h✝ -
          2 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * g✝,
      g :=
        (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✝¹) * f✝ +
              16 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * h✝ -
            6 * (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * h✝ -
          6 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * g✝,
      h :=
        (f✝² * f✝¹ + 6 * h✝² * h✝¹ - 2 * g✝² * h✝¹ - 2 * h✝² * g✝¹) * h✝ +
                  (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * f✝ +
                (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * g✝ +
              3 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * h✝ -
            3 * (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * h✝ -
          3 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * g✝ } =
    {
      f :=
        f✝² * (f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝) +
              6 * h✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
            2 * g✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
          2 * h✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝),
      g :=
        f✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝) +
                g✝² * (f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝) +
              16 * h✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
            6 * g✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
          6 * h✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝),
      h :=
        f✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) +
                  h✝² * (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✝) +
              3 * h✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
            3 * g✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
          3 * h✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝) }

State before:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ {
      f :=
        (f✝² * f✝¹ + 6 * h✝² * h✝¹ - 2 * g✝² * h✝¹ - 2 * h✝² * g✝¹) * f✝ +
              6 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * h✝ -
            2 * (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * h✝ -
          2 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * g✝,
      g :=
        (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✝¹) * f✝ +
              16 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * h✝ -
            6 * (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * h✝ -
          6 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * g✝,
      h :=
        (f✝² * f✝¹ + 6 * h✝² * h✝¹ - 2 * g✝² * h✝¹ - 2 * h✝² * g✝¹) * h✝ +
                  (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * f✝ +
                (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * g✝ +
              3 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * h✝ -
            3 * (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * h✝ -
          3 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * g✝ } =
    {
      f :=
        f✝² * (f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝) +
              6 * h✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
            2 * g✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
          2 * h✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝),
      g :=
        f✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝) +
                g✝² * (f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝) +
              16 * h✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
            6 * g✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
          6 * h✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝),
      h :=
        f✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) +
                  h✝² * (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✝) +
              3 * h✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
            3 * g✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
          3 * h✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝) }
Tactic:
ring
State after:
no goals