Theorem: ℤα.coe_eq_zero (Mordell4/Rt7Ring.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.z
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z.z = 0.z

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

State before:
case mp.w
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.w = 0
⊢ z.w = 0.w
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