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

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

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

State before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ } = add { z := z✝, w := w✝ } { z := z✝¹, w := w✝¹ }
Tactic:
simp only [add, add_comm]
State after:
no goals