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

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

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

State before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ toℂ (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) = toℂ { z := z✝¹, w := w✝¹ } + toℂ { z := z✝, w := w✝ }
Tactic:
simp only [add, toℂ, complexα]
State after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑(z✝¹ + z✝) + ↑(w✝¹ + w✝) * { re := 1 / 2, im := rt7 / 2 } =
    ↑z✝¹ + ↑w✝¹ * { re := 1 / 2, im := rt7 / 2 } + (↑z✝ + ↑w✝ * { re := 1 / 2, im := rt7 / 2 })

State before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑(z✝¹ + z✝) + ↑(w✝¹ + w✝) * { re := 1 / 2, im := rt7 / 2 } =
    ↑z✝¹ + ↑w✝¹ * { re := 1 / 2, im := rt7 / 2 } + (↑z✝ + ↑w✝ * { re := 1 / 2, im := rt7 / 2 })
Tactic:
ext <;> dsimp <;> norm_num <;> ring
State after:
no goals