Theorem: ℤθ.my_add_assoc (Mordell4/CubicRing.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 : ℤθ
f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝, g := g✝, h := h✝ } b) c = add { f := f✝, g := g✝, h := h✝ } (add b c)

State before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝, g := g✝, h := h✝ } b) c = add { f := f✝, g := g✝, h := h✝ } (add b c)
Tactic:
cases b
State after:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) c =
    add { f := f✝¹, g := g✝¹, h := h✝¹ } (add { f := f✝, g := g✝, h := h✝ } c)

State before:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) c =
    add { f := f✝¹, g := g✝¹, h := h✝¹ } (add { f := f✝, g := g✝, h := h✝ } c)
Tactic:
cases c
State after:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝², g := g✝², h := h✝² } { f := f✝¹, g := g✝¹, h := h✝¹ }) { f := f✝, g := g✝, h := h✝ } =
    add { f := f✝², g := g✝², h := h✝² } (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ })

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