chore: define Complex.UnitDisc using Subsemigroup.unitBall (#39385)

The motivation is to have some local consistency between the definitions of `Circle` and `Complex.UnitDisc`. At the moment, there is a mild style inconsistency since `Circle` uses `Submonoid.unitSphere` whereas `Complex.UnitDisc` uses a raw `Metric.ball`.

The background is that we are about to add `Complex.closedUnitDisc` and so the question arose about which pattern to follow. I decided that we should follow `Circle` and bring `Complex.UnitDisc` in line.

Author: ocfnash

Mathlib/Analysis/Complex/UnitDisc/Basic.lean

@@ -27,7 +27,7 @@ namespace Complex
 
 /-- The complex unit disc, denoted as `𝔻` within the Complex namespace -/
 def UnitDisc : Type :=
-  ball (0 : ℂ) 1 deriving TopologicalSpace
+  Subsemigroup.unitBall ℂ deriving TopologicalSpace
 
 @[inherit_doc] scoped[Complex.UnitDisc] notation "𝔻" => Complex.UnitDisc
 open UnitDisc

Mathlib/Analysis/Normed/Field/UnitBall.lean

@@ -35,6 +35,10 @@ def Subsemigroup.unitBall (𝕜 : Type*) [NonUnitalSeminormedRing 𝕜] : Subsem
     rw [mem_ball_zero_iff] at *
     exact (norm_mul_le _ _).trans_lt (mul_lt_one_of_nonneg_of_lt_one_left (norm_nonneg _) hx hy.le)
 
+@[simp] lemma Subsemigroup.mem_unitBall (𝕜 : Type*) [NonUnitalSeminormedRing 𝕜] {x : 𝕜} :
+    x ∈ Subsemigroup.unitBall 𝕜 ↔ ‖x‖ < 1 := by
+  simp [Subsemigroup.unitBall]
+
 instance Metric.unitBall.instSemigroup [NonUnitalSeminormedRing 𝕜] : Semigroup (ball (0 : 𝕜) 1) :=
   inferInstanceAs <| Semigroup (Subsemigroup.unitBall 𝕜)