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

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

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

State before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul { x := x✝¹, y := y✝¹ } (add { x := x✝, y := y✝ } c) =
    add (mul { x := x✝¹, y := y✝¹ } { 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 { x := x✝², y := y✝² } (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) =
    add (mul { x := x✝², y := y✝² } { 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 { x := x✝², y := y✝² } (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) =
    add (mul { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) (mul { x := x✝², y := y✝² } { x := x✝, y := y✝ })
Tactic:
simp only [mul, add]
State after:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ { x := x✝² * (x✝¹ + x✝) - y✝² * (y✝¹ + y✝), y := x✝² * (y✝¹ + y✝) + y✝² * (x✝¹ + x✝) - y✝² * (y✝¹ + y✝) } =
    { x := x✝² * x✝¹ - y✝² * y✝¹ + (x✝² * x✝ - y✝² * y✝),
      y := x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹ + (x✝² * y✝ + y✝² * x✝ - y✝² * y✝) }

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