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

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

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

State before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑(x✝¹ * x✝ - y✝¹ * y✝) + ↑(x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) * complexω =
    (↑x✝¹ + ↑y✝¹ * complexω) * (↑x✝ + ↑y✝ * complexω)
Tactic:
norm_num
State after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑x✝¹ * ↑x✝ - ↑y✝¹ * ↑y✝ + (↑x✝¹ * ↑y✝ + ↑y✝¹ * ↑x✝ - ↑y✝¹ * ↑y✝) * complexω =
    (↑x✝¹ + ↑y✝¹ * complexω) * (↑x✝ + ↑y✝ * complexω)

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

State before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑x✝¹ * ↑x✝ + ↑x✝¹ * ↑y✝ * complexω + ↑x✝ * ↑y✝¹ * complexω + (-(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω) =
    ↑x✝¹ * ↑x✝ + ↑x✝¹ * ↑y✝ * complexω + ↑x✝ * ↑y✝¹ * complexω + ↑y✝¹ * ↑y✝ * complexω ^ 2
Tactic:
congr
State after:
case mk.mk.e_a
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ -(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω = ↑y✝¹ * ↑y✝ * complexω ^ 2

State before:
case mk.mk.e_a
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ -(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω = ↑y✝¹ * ↑y✝ * complexω ^ 2
Tactic:
rw [complexω_sq]
State after:
case mk.mk.e_a
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ -(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω = ↑y✝¹ * ↑y✝ * (-complexω - 1)

State before:
case mk.mk.e_a
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ -(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω = ↑y✝¹ * ↑y✝ * (-complexω - 1)
Tactic:
sorry
State after:
no goals