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

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

State before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ toℂ (mul { 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ℂ (mul { 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ℂ (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) = toℂ { z := z✝¹, w := w✝¹ } * toℂ { z := z✝, w := w✝ }
Tactic:
simp only [mul, toℂ]
State after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑(z✝¹ * z✝ - 2 * w✝¹ * w✝) + ↑(z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝) * complexα =
    (↑z✝¹ + ↑w✝¹ * complexα) * (↑z✝ + ↑w✝ * complexα)

State before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑(z✝¹ * z✝ - 2 * w✝¹ * w✝) + ↑(z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝) * complexα =
    (↑z✝¹ + ↑w✝¹ * complexα) * (↑z✝ + ↑w✝ * complexα)
Tactic:
norm_num
State after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ - 2 * ↑w✝¹ * ↑w✝ + (↑z✝¹ * ↑w✝ + ↑w✝¹ * ↑z✝ + ↑w✝¹ * ↑w✝) * complexα =
    (↑z✝¹ + ↑w✝¹ * complexα) * (↑z✝ + ↑w✝ * complexα)

State before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ - 2 * ↑w✝¹ * ↑w✝ + (↑z✝¹ * ↑w✝ + ↑w✝¹ * ↑z✝ + ↑w✝¹ * ↑w✝) * complexα =
    (↑z✝¹ + ↑w✝¹ * complexα) * (↑z✝ + ↑w✝ * complexα)
Tactic:
ring_nf
State after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + (↑z✝ * ↑w✝¹ * complexα - ↑w✝¹ * ↑w✝ * 2) + ↑w✝¹ * ↑w✝ * complexα =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * ↑w✝¹ * complexα + ↑w✝¹ * ↑w✝ * complexα ^ 2

State before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + (↑z✝ * ↑w✝¹ * complexα - ↑w✝¹ * ↑w✝ * 2) + ↑w✝¹ * ↑w✝ * complexα =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * ↑w✝¹ * complexα + ↑w✝¹ * ↑w✝ * complexα ^ 2
Tactic:
ring
State after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + (↑w✝ * complexα * ↑w✝¹ - ↑w✝ * ↑w✝¹ * 2) =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + ↑w✝ * complexα ^ 2 * ↑w✝¹

State before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + (↑w✝ * complexα * ↑w✝¹ - ↑w✝ * ↑w✝¹ * 2) =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + ↑w✝ * complexα ^ 2 * ↑w✝¹
Tactic:
rw [complexα_sq]
State after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + (↑w✝ * complexα * ↑w✝¹ - ↑w✝ * ↑w✝¹ * 2) =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + ↑w✝ * (complexα - 2) * ↑w✝¹

State before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + (↑w✝ * complexα * ↑w✝¹ - ↑w✝ * ↑w✝¹ * 2) =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + ↑w✝ * (complexα - 2) * ↑w✝¹
Tactic:
congr
State after:
case mk.mk.e_a
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑w✝ * complexα * ↑w✝¹ - ↑w✝ * ↑w✝¹ * 2 = ↑w✝ * (complexα - 2) * ↑w✝¹

State before:
case mk.mk.e_a
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑w✝ * complexα * ↑w✝¹ - ↑w✝ * ↑w✝¹ * 2 = ↑w✝ * (complexα - 2) * ↑w✝¹
Tactic:
ring
State after:
no goals