Theorem: ℤω.my_mul_comm (Mordell4/Eisenstein.lean)

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

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

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

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