Theorem: ℤω.my_quotient_zero (Mordell4/Eisenstein.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, 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 * rt3⁻¹ * 0.im);
    { x := round (0.re + 2⁻¹ * ↑y), y := y }) =
    0

State before:
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ (let y := round (2 * rt3⁻¹ * 0.im);
    { x := round (0.re + 2⁻¹ * ↑y), y := y }) =
    0
Tactic:
ext <;> dsimp <;> simp only [MulZeroClass.mul_zero, round_zero, algebraMap.coe_zero, add_zero]
State after:
case x
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ round (0 + 2⁻¹ * ↑0) = 0.x

State before:
case x
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ round (0 + 2⁻¹ * ↑0) = 0.x
Tactic:
simp only [cast_zero, mul_zero, add_zero, round_zero]
State after:
no goals