Theorem: ℤα.my_add_assoc (Mordell4/Rt7Ring.lean)

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

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

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

State before:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ add (add { z := z✝², w := w✝² } { z := z✝¹, w := w✝¹ }) { z := z✝, w := w✝ } =
    add { z := z✝², w := w✝² } (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ })
Tactic:
simp only [add, add_assoc]
State after:
no goals