Theorem: ℤω.my_map_add (Mordell4/Eisenstein.lean)

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

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

State before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ toℂ (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) = toℂ { x := x✝¹, y := y✝¹ } + toℂ { x := x✝, y := y✝ }
Tactic:
simp only [add, toℂ, complexω]
State after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑(x✝¹ + x✝) + ↑(y✝¹ + y✝) * { re := -1 / 2, im := rt3 / 2 } =
    ↑x✝¹ + ↑y✝¹ * { re := -1 / 2, im := rt3 / 2 } + (↑x✝ + ↑y✝ * { re := -1 / 2, im := rt3 / 2 })

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