Theorem: ℤω.my_mul_assoc (Mordell4/Eisenstein.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 : ℤω
x✝ y✝ : ℤ
⊢ mul (mul { x := x✝, y := y✝ } b) c = mul { x := x✝, y := y✝ } (mul b c)

State before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul (mul { x := x✝, y := y✝ } b) c = mul { x := x✝, y := y✝ } (mul b c)
Tactic:
cases b
State after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) c = mul { x := x✝¹, y := y✝¹ } (mul { x := x✝, y := y✝ } c)

State before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) c = mul { x := x✝¹, y := y✝¹ } (mul { x := x✝, y := y✝ } c)
Tactic:
cases c
State after:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (mul { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) { x := x✝, y := y✝ } =
    mul { x := x✝², y := y✝² } (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ })

State before:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (mul { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) { x := x✝, y := y✝ } =
    mul { x := x✝², y := y✝² } (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ })
Tactic:
simp only [mul]
State after:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ { x := (x✝² * x✝¹ - y✝² * y✝¹) * x✝ - (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * y✝,
      y :=
        (x✝² * x✝¹ - y✝² * y✝¹) * y✝ + (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * x✝ -
          (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * y✝ } =
    { x := x✝² * (x✝¹ * x✝ - y✝¹ * y✝) - y✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝),
      y :=
        x✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) + y✝² * (x✝¹ * x✝ - y✝¹ * y✝) - y✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) }

State before:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ { x := (x✝² * x✝¹ - y✝² * y✝¹) * x✝ - (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * y✝,
      y :=
        (x✝² * x✝¹ - y✝² * y✝¹) * y✝ + (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * x✝ -
          (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * y✝ } =
    { x := x✝² * (x✝¹ * x✝ - y✝¹ * y✝) - y✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝),
      y :=
        x✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) + y✝² * (x✝¹ * x✝ - y✝¹ * y✝) - y✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) }
Tactic:
ring
State after:
no goals