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

State before:
a b c z : ℤω
⊢ OneHom.toFun (↑↑inclusion) z = 0 ↔ z = 0
Tactic:
constructor
State after:
case mp
a b c z : ℤω
⊢ OneHom.toFun (↑↑inclusion) z = 0 → z = 0

case mpr
a b c z : ℤω
⊢ z = 0 → OneHom.toFun (↑↑inclusion) z = 0

State before:
case mp
a b c z : ℤω
⊢ OneHom.toFun (↑↑inclusion) z = 0 → z = 0
Tactic:
intro h
State after:
case mp
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z = 0

State before:
case mp
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z = 0
Tactic:
ext
State after:
case mp.x
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z.x = 0.x

case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z.y = 0.y

State before:
case mp.x
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z.x = 0.x
Tactic:
have : (z.x : ℝ) = 0
State after:
case this
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ ↑z.x = 0

case mp.x
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.x = 0
⊢ z.x = 0.x

State before:
case this
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ ↑z.x = 0

case mp.x
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.x = 0
⊢ z.x = 0.x
Tactic:
rw [x_from_coe, h]
State after:
case this
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ 0.re + rt3⁻¹ * 0.im = 0

case mp.x
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.x = 0
⊢ z.x = 0.x

State before:
case this
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ 0.re + rt3⁻¹ * 0.im = 0

case mp.x
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.x = 0
⊢ z.x = 0.x
Tactic:
norm_num
State after:
case mp.x
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.x = 0
⊢ z.x = 0.x

State before:
case mp.x
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.x = 0
⊢ z.x = 0.x
Tactic:
exact_mod_cast this
State after:
no goals

State before:
case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z.y = 0.y
Tactic:
have : (z.y : ℝ) = 0
State after:
case this
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ ↑z.y = 0

case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.y = 0
⊢ z.y = 0.y

State before:
case this
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ ↑z.y = 0

case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.y = 0
⊢ z.y = 0.y
Tactic:
rw [y_from_coe, h]
State after:
case this
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ 2 * rt3⁻¹ * 0.im = 0

case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.y = 0
⊢ z.y = 0.y

State before:
case this
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ 2 * rt3⁻¹ * 0.im = 0

case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.y = 0
⊢ z.y = 0.y
Tactic:
norm_num
State after:
case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.y = 0
⊢ z.y = 0.y

State before:
case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.y = 0
⊢ z.y = 0.y
Tactic:
exact_mod_cast this
State after:
no goals

State before:
case mpr
a b c z : ℤω
⊢ z = 0 → OneHom.toFun (↑↑inclusion) z = 0
Tactic:
intro h
State after:
case mpr
a b c z : ℤω
h : z = 0
⊢ OneHom.toFun (↑↑inclusion) z = 0

State before:
case mpr
a b c z : ℤω
h : z = 0
⊢ OneHom.toFun (↑↑inclusion) z = 0
Tactic:
rw [h]
State after:
case mpr
a b c z : ℤω
h : z = 0
⊢ OneHom.toFun (↑↑inclusion) 0 = 0

State before:
case mpr
a b c z : ℤω
h : z = 0
⊢ OneHom.toFun (↑↑inclusion) 0 = 0
Tactic:
exact my_map_zero
State after:
no goals