[GOAL]
⊢ CommSemigroup 𝔻
[PROOFSTEP]
unfold UnitDisc
[GOAL]
⊢ CommSemigroup ↑(ball 0 1)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ HasDistribNeg 𝔻
[PROOFSTEP]
unfold UnitDisc
[GOAL]
⊢ HasDistribNeg ↑(ball 0 1)
[PROOFSTEP]
infer_instance
[GOAL]
z : 𝔻
⊢ ↑normSq ↑z < 1
[PROOFSTEP]
convert (Real.sqrt_lt' one_pos).1 z.abs_lt_one
[GOAL]
case h.e'_4
z : 𝔻
⊢ 1 = 1 ^ 2
[PROOFSTEP]
exact (one_pow 2).symm
[GOAL]
z : 𝔻
⊢ ↑abs ↑z ≠ ↑abs (-1)
[PROOFSTEP]
rw [abs.map_neg, map_one]
[GOAL]
z : 𝔻
⊢ ↑abs ↑z ≠ 1
[PROOFSTEP]
exact z.abs_ne_one
