chore(analysis/complex/upper_half_plane): don't use abbreviation (#12679)

Some day we should add Poincaré metric as a `metric_space` instance on `upper_half_plane`.
In the meantime, make sure that Lean doesn't use `subtype` instances for `uniform_space` and/or `metric_space`.

Author: urkud

src/analysis/complex/upper_half_plane.lean

@@ -35,13 +35,15 @@ local attribute [-instance] matrix.special_linear_group.has_coe_to_fun
 local prefix `↑ₘ`:1024 := @coe _ (matrix (fin 2) (fin 2) _) _
 
 /-- The open upper half plane -/
-abbreviation upper_half_plane :=
-{point : ℂ // 0 < point.im}
+@[derive [topological_space, λ α, has_coe α ℂ]]
+def upper_half_plane := {point : ℂ // 0 < point.im}
 
 localized "notation `ℍ` := upper_half_plane" in upper_half_plane
 
 namespace upper_half_plane
 
+instance : inhabited ℍ := ⟨⟨complex.I, by simp⟩⟩
+
 /-- Imaginary part -/
 def im (z : ℍ) := (z : ℂ).im