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

State before:
a b c : ℤα
⊢ div a 0 = 0
Tactic:
unfold div
State after:
a b c : ℤα
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0

State before:
a b c : ℤα
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0
Tactic:
have : ((0 : ℤα) : ℂ) = 0 := my_map_zero
State after:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0

State before:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0
Tactic:
rw [this]
State after:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / 0) = 0

State before:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / 0) = 0
Tactic:
rw [div_zero]
State after:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα 0 = 0

State before:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα 0 = 0
Tactic:
unfold nearestℤα
State after:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ (let y := round (2 * rt7⁻¹ * 0.im);
    { z := round (0.re - 2⁻¹ * ↑y), w := y }) =
    0

State before:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ (let y := round (2 * rt7⁻¹ * 0.im);
    { z := round (0.re - 2⁻¹ * ↑y), w := y }) =
    0
Tactic:
ext <;> dsimp <;> simp only [MulZeroClass.mul_zero, round_zero, algebraMap.coe_zero, sub_zero] <;>
norm_num
State after:
no goals