Theorem: ℤα.my_left_distrib (Mordell4/Rt7Ring.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 : ℤα
z✝ w✝ : ℤ
⊢ mul { z := z✝, w := w✝ } (add b c) = add (mul { z := z✝, w := w✝ } b) (mul { z := z✝, w := w✝ } c)

State before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ mul { z := z✝, w := w✝ } (add b c) = add (mul { z := z✝, w := w✝ } b) (mul { z := z✝, w := w✝ } c)
Tactic:
cases b
State after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul { z := z✝¹, w := w✝¹ } (add { z := z✝, w := w✝ } c) =
    add (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) (mul { z := z✝¹, w := w✝¹ } c)

State before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul { z := z✝¹, w := w✝¹ } (add { z := z✝, w := w✝ } c) =
    add (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) (mul { z := z✝¹, w := w✝¹ } c)
Tactic:
cases c
State after:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul { z := z✝², w := w✝² } (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) =
    add (mul { z := z✝², w := w✝² } { z := z✝¹, w := w✝¹ }) (mul { z := z✝², w := w✝² } { z := z✝, w := w✝ })

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

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