chore(UpperHalfPlane): redefine as a structure (leanprover-community#34597)

Make `UpperHalfPlane` into a two-field structure rather than a type alias for a subtype, to reduce defeq abuse.

Author: urkud

Mathlib/Analysis/Complex/IntegerCompl.lean

@@ -28,21 +28,29 @@ local notation "ℂ_ℤ" => integerComplement
 
 lemma integerComplement_eq : ℂ_ℤ = {z : ℂ | ¬ ∃ (n : ℤ), n = z} := rfl
 
-lemma integerComplement.mem_iff {x : ℂ} : x ∈ ℂ_ℤ ↔ ¬ ∃ (n : ℤ), n = x := Iff.rfl
+lemma mem_integerComplement_iff {x : ℂ} : x ∈ ℂ_ℤ ↔ ¬ ∃ (n : ℤ), n = x := Iff.rfl
 
+@[deprecated (since := "2026-01-29")]
+alias integerComplement.mem_iff := mem_integerComplement_iff
+
+@[simp]
 lemma _root_.UpperHalfPlane.coe_mem_integerComplement (z : ℍ) : ↑z ∈ ℂ_ℤ :=
-  not_exists.mpr fun x hx ↦ ne_int z x hx.symm
+  not_exists.mpr fun x hx ↦ ne_intCast z x hx.symm
 
-lemma integerComplement.add_coe_int_mem {x : ℂ} (a : ℤ) : x + (a : ℂ) ∈ ℂ_ℤ ↔ x ∈ ℂ_ℤ := by
-  simp only [mem_iff, not_iff_not]
+@[simp]
+lemma add_intCast_mem_integerComplement {x : ℂ} (a : ℤ) : x + (a : ℂ) ∈ ℂ_ℤ ↔ x ∈ ℂ_ℤ := by
+  simp only [mem_integerComplement_iff, not_iff_not]
   exact ⟨(Exists.elim · fun n hn ↦ ⟨n - a, by simp [hn]⟩),
     (Exists.elim · fun n hn ↦ ⟨n + a, by simp [hn]⟩)⟩
 
+@[deprecated (since := "2026-01-29")]
+alias integerComplement.add_coe_int_mem := add_intCast_mem_integerComplement
+
 lemma integerComplement.ne_zero {x : ℂ} (hx : x ∈ ℂ_ℤ) : x ≠ 0 :=
   fun hx' ↦ hx ⟨0, by exact_mod_cast hx'.symm⟩
 
 lemma integerComplement_add_ne_zero {x : ℂ} (hx : x ∈ ℂ_ℤ) (a : ℤ) : x + (a : ℂ) ≠ 0 :=
-  integerComplement.ne_zero ((integerComplement.add_coe_int_mem a).mpr hx)
+  integerComplement.ne_zero ((add_intCast_mem_integerComplement a).mpr hx)
 
 lemma integerComplement.ne_one {x : ℂ} (hx : x ∈ ℂ_ℤ) : x ≠ 1 :=
   fun hx' ↦ hx ⟨1, by exact_mod_cast hx'.symm⟩
@@ -54,14 +62,13 @@ lemma integerComplement_pow_two_ne_pow_two {x : ℂ} (hx : x ∈ ℂ_ℤ) (n : 
 
 lemma upperHalfPlane_inter_integerComplement :
     {z : ℂ | 0 < z.im} ∩ ℂ_ℤ = {z : ℂ | 0 < z.im} := by
-  ext z
-  simp only [Set.mem_inter_iff, Set.mem_setOf_eq, and_iff_left_iff_imp]
-  exact fun hz ↦ UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩
+  apply Set.inter_eq_self_of_subset_left
+  exact fun z hz ↦ UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩
 
 lemma _root_.UpperHalfPlane.int_div_mem_integerComplement (z : ℍ) {n : ℤ} (hn : n ≠ 0) :
     n / (z : ℂ) ∈ ℂ_ℤ := by
   rintro ⟨_, hm⟩
-  have : (n / (z : ℂ)).im ≠ 0 := by simp [div_im, hn, z.im_pos.ne', ne_zero z]
+  have : (n / (z : ℂ)).im ≠ 0 := by simp [div_im, z.ne_zero, hn, z.im_ne_zero]
   simpa [← hm]
 
 end Complex

Mathlib/Analysis/Complex/Periodic.lean

@@ -77,6 +77,11 @@ theorem norm_qParam_lt_iff (hh : 0 < h) (A : ℝ) (z : ℂ) :
 lemma qParam_ne_zero (z : ℂ) : 𝕢 h z ≠ 0 := by
   simp [qParam, exp_ne_zero]
 
+@[fun_prop]
+lemma continuous_qParam : Continuous (𝕢 h) := by
+  unfold qParam
+  fun_prop
+
 @[fun_prop]
 lemma differentiable_qParam : Differentiable ℂ (𝕢 h) := by
   unfold qParam

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -21,29 +21,41 @@ We define the notation `ℍ` for the upper half plane available in the locale
 noncomputable section
 
 /-- The open upper half plane, denoted as `ℍ` within the `UpperHalfPlane` namespace -/
-def UpperHalfPlane :=
-  { point : ℂ // 0 < point.im }
+@[ext]
+structure UpperHalfPlane where
+  /-- Canonical embedding of the upper half-plane into `ℂ`. -/
+  protected coe : ℂ
+  coe_im_pos : 0 < coe.im
 
 @[inherit_doc] scoped[UpperHalfPlane] notation "ℍ" => UpperHalfPlane
 
 open UpperHalfPlane
 
 namespace UpperHalfPlane
 
-/-- Canonical embedding of the upper half-plane into `ℂ`. -/
-@[coe] protected def coe (z : ℍ) : ℂ := z.1
+attribute [coe] UpperHalfPlane.coe
 
 instance : CoeOut ℍ ℂ := ⟨UpperHalfPlane.coe⟩
 
-instance : Inhabited ℍ :=
-  ⟨⟨Complex.I, by simp⟩⟩
+/-- Define I := √-1 as an element on the upper half plane. -/
+def I : ℍ := ⟨Complex.I, zero_lt_one⟩
+
+instance : Inhabited ℍ := ⟨.I⟩
+
+@[simp, norm_cast] theorem coe_inj {a b : ℍ} : (a : ℂ) = b ↔ a = b := UpperHalfPlane.ext_iff.symm
+
+@[deprecated (since := "2026-01-31")] alias ext_iff' := coe_inj
+
+theorem coe_injective : Function.Injective UpperHalfPlane.coe := fun _ _ ↦ UpperHalfPlane.ext
 
-@[ext] theorem ext {a b : ℍ} (h : (a : ℂ) = b) : a = b := Subtype.ext h
+instance canLift : CanLift ℂ ℍ ((↑) : ℍ → ℂ) fun z => 0 < z.im where
+  prf z hz := ⟨⟨z, hz⟩, rfl⟩
 
-@[simp, norm_cast] theorem ext_iff' {a b : ℍ} : (a : ℂ) = b ↔ a = b := UpperHalfPlane.ext_iff.symm
+protected theorem «forall» {P : ℍ → Prop} : (∀ z, P z) ↔ ∀ z hz, P ⟨z, hz⟩ :=
+  ⟨fun h z hz ↦ h ⟨z, hz⟩, fun h z ↦ h z.1 z.2⟩
 
-instance canLift : CanLift ℂ ℍ ((↑) : ℍ → ℂ) fun z => 0 < z.im :=
-  Subtype.canLift fun (z : ℂ) => 0 < z.im
+protected theorem «exists» {P : ℍ → Prop} : (∃ z, P z) ↔ ∃ z hz, P ⟨z, hz⟩ :=
+  ⟨fun ⟨⟨z, hz⟩, hP⟩ ↦ ⟨z, hz, hP⟩, fun ⟨z, hz, hP⟩ ↦ ⟨⟨z, hz⟩, hP⟩⟩
 
 /-- Imaginary part -/
 def im (z : ℍ) :=
@@ -54,13 +66,11 @@ def re (z : ℍ) :=
   (z : ℂ).re
 
 /-- Extensionality lemma in terms of `UpperHalfPlane.re` and `UpperHalfPlane.im`. -/
-theorem ext' {a b : ℍ} (hre : a.re = b.re) (him : a.im = b.im) : a = b :=
-  ext <| Complex.ext hre him
+theorem ext_re_im {a b : ℍ} (hre : a.re = b.re) (him : a.im = b.im) : a = b :=
+  UpperHalfPlane.ext <| Complex.ext hre him
 
-/-- Constructor for `UpperHalfPlane`. It is useful if `⟨z, h⟩` makes Lean use a wrong
-typeclass instance. -/
-def mk (z : ℂ) (h : 0 < z.im) : ℍ :=
-  ⟨z, h⟩
+@[deprecated (since := "2026-01-29")]
+alias ext' := ext_re_im
 
 @[simp]
 theorem coe_im (z : ℍ) : (z : ℂ).im = z.im :=
@@ -78,48 +88,38 @@ theorem mk_re (z : ℂ) (h : 0 < z.im) : (mk z h).re = z.re :=
 theorem mk_im (z : ℂ) (h : 0 < z.im) : (mk z h).im = z.im :=
   rfl
 
-@[simp]
 theorem coe_mk (z : ℂ) (h : 0 < z.im) : (mk z h : ℂ) = z :=
   rfl
 
 @[simp]
-lemma coe_mk_subtype {z : ℂ} (hz : 0 < z.im) :
-    UpperHalfPlane.coe ⟨z, hz⟩ = z := by
+theorem mk_coe (z : ℍ) (h : 0 < (z : ℂ).im := z.2) : mk z h = z :=
   rfl
 
-instance : Nontrivial ℍ := by
-  constructor
-  use ⟨Complex.I, by simp⟩, ⟨2 * Complex.I, by simp⟩
-  simp [ne_eq, UpperHalfPlane.ext_iff]
+@[simp]
+lemma I_im : I.im = 1 := rfl
 
 @[simp]
-theorem mk_coe (z : ℍ) (h : 0 < (z : ℂ).im := z.2) : mk z h = z :=
+lemma I_re : I.re = 0 := rfl
+
+@[simp, norm_cast]
+lemma coe_I : I = Complex.I := rfl
+
+@[deprecated coe_mk (since := "2026-01-29")]
+lemma coe_mk_subtype {z : ℂ} (hz : 0 < z.im) :
+    UpperHalfPlane.coe ⟨z, hz⟩ = z :=
   rfl
 
 theorem re_add_im (z : ℍ) : (z.re + z.im * Complex.I : ℂ) = z :=
   Complex.re_add_im z
 
-theorem im_pos (z : ℍ) : 0 < z.im :=
-  z.2
+theorem im_pos (z : ℍ) : 0 < z.im := z.coe_im_pos
 
 theorem im_ne_zero (z : ℍ) : z.im ≠ 0 :=
   z.im_pos.ne'
 
 theorem ne_zero (z : ℍ) : (z : ℂ) ≠ 0 :=
   mt (congr_arg Complex.im) z.im_ne_zero
 
-/-- Define I := √-1 as an element on the upper half plane. -/
-def I : ℍ := ⟨Complex.I, by simp⟩
-
-@[simp]
-lemma I_im : I.im = 1 := rfl
-
-@[simp]
-lemma I_re : I.re = 0 := rfl
-
-@[simp, norm_cast]
-lemma coe_I : I = Complex.I := rfl
-
 end UpperHalfPlane
 
 namespace Mathlib.Meta.Positivity
@@ -155,30 +155,31 @@ theorem normSq_ne_zero (z : ℍ) : Complex.normSq (z : ℂ) ≠ 0 :=
   (normSq_pos z).ne'
 
 theorem im_inv_neg_coe_pos (z : ℍ) : 0 < (-z : ℂ)⁻¹.im := by
-  simpa [neg_div] using div_pos z.property (normSq_pos z)
+  simpa [neg_div] using div_pos z.im_pos (normSq_pos z)
 
 lemma im_pnat_div_pos (n : ℕ) [NeZero n] (z : ℍ) : 0 < (-(n : ℂ) / z).im := by
   suffices 0 < n * z.im / Complex.normSq z by simpa [Complex.div_im, neg_div]
   positivity [NeZero.ne n, z.normSq_pos]
 
-lemma ne_nat (z : ℍ) : ∀ n : ℕ, z.1 ≠ n := by
-  intro n
-  have h1 := z.2
-  aesop
+lemma ne_ofReal (z : ℍ) (x : ℝ) : (z : ℂ) ≠ x :=
+  ne_of_apply_ne Complex.im <| by simp [im_ne_zero]
+
+lemma ne_intCast (z : ℍ) (n : ℤ) : (z : ℂ) ≠ n := mod_cast ne_ofReal z n
+
+@[deprecated (since := "2026-01-29")] alias ne_int := ne_intCast
 
-lemma ne_int (z : ℍ) : ∀ n : ℤ, z.1 ≠ n := by
-  intro n
-  have h1 := z.2
-  aesop
+lemma ne_natCast (z : ℍ) (n : ℕ) : (z : ℂ) ≠ n := mod_cast ne_intCast z n
+
+@[deprecated (since := "2026-01-29")] alias ne_nat := ne_natCast
 
 section PosRealAction
 
-instance posRealAction : MulAction { x : ℝ // 0 < x } ℍ where
-  smul x z := mk ((x : ℝ) • (z : ℂ)) <| by simpa using mul_pos x.2 z.2
-  one_smul _ := Subtype.ext <| one_smul _ _
-  mul_smul x y z := Subtype.ext <| mul_smul (x : ℝ) y (z : ℂ)
+instance posRealAction : MulAction {x : ℝ // 0 < x} ℍ where
+  smul x z := mk ((x : ℝ) • (z : ℂ)) <| by simpa using mul_pos x.2 z.im_pos
+  one_smul _ := UpperHalfPlane.ext <| one_smul _ _
+  mul_smul x y z := UpperHalfPlane.ext <| mul_smul (x : ℝ) y (z : ℂ)
 
-variable (x : { x : ℝ // 0 < x }) (z : ℍ)
+variable (x : {x : ℝ // 0 < x}) (z : ℍ)
 
 @[simp]
 theorem coe_pos_real_smul : ↑(x • z) = (x : ℝ) • (z : ℂ) :=
@@ -192,14 +193,19 @@ theorem pos_real_im : (x • z).im = x * z.im :=
 theorem pos_real_re : (x • z).re = x * z.re :=
   Complex.smul_re _ _
 
+theorem pos_real_smul_injective (z : ℍ) :
+    Function.Injective fun x : {x : ℝ // 0 < x} ↦ x • z := by
+  rintro ⟨x, hx⟩ ⟨y, hy⟩ h
+  simp_all [UpperHalfPlane.ext_iff, ne_zero]
+
 end PosRealAction
 
 section RealAddAction
 
 instance : AddAction ℝ ℍ where
   vadd x z := mk (x + z) <| by simpa using z.im_pos
-  zero_vadd _ := Subtype.ext <| by simp [HVAdd.hVAdd]
-  add_vadd x y z := Subtype.ext <| by simp [HVAdd.hVAdd, add_assoc]
+  zero_vadd _ := by simp [HVAdd.hVAdd]
+  add_vadd x y z := by simp [HVAdd.hVAdd, add_assoc]
 
 variable (x : ℝ) (z : ℍ)
 
@@ -215,18 +221,34 @@ theorem vadd_re : (x +ᵥ z).re = x + z.re :=
 theorem vadd_im : (x +ᵥ z).im = z.im :=
   zero_add _
 
+@[simp]
+protected theorem vadd_right_cancel_iff {x y : ℝ} (z : ℍ) : x +ᵥ z = y +ᵥ z ↔ x = y := by
+  simp [UpperHalfPlane.ext_iff]
+
+protected theorem vadd_left_injective (z : ℍ) : Function.Injective fun x : ℝ ↦ x +ᵥ z := by
+  simp [Function.Injective]
+
+instance : Infinite ℍ :=
+  .of_injective _ <| UpperHalfPlane.vadd_left_injective I
+
+instance : Nontrivial ℍ := inferInstance
+
 end RealAddAction
 
 section upperHalfPlaneSet
 
-/-- The upper half plane as a subset of `ℂ`. This is convenient for taking derivatives of functions
-on the upper half plane. -/
+/-- The upper half plane as a subset of `ℂ`.
+This is convenient for taking derivatives of functions on the upper half plane. -/
 abbrev upperHalfPlaneSet := {z : ℂ | 0 < z.im}
 
 local notation "ℍₒ" => upperHalfPlaneSet
 
 lemma isOpen_upperHalfPlaneSet : IsOpen ℍₒ := isOpen_lt continuous_const Complex.continuous_im
 
+@[simp]
+theorem range_coe : Set.range UpperHalfPlane.coe = ℍₒ := by
+  ext; simp [UpperHalfPlane.exists]
+
 end upperHalfPlaneSet
 
 end UpperHalfPlane

Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean

@@ -34,7 +34,7 @@ def atImInfty :=
 instance : atImInfty.NeBot := by
   refine comap_neBot_iff_frequently.mpr (Eventually.frequently ?_)
   filter_upwards [eventually_gt_atTop 0] with t ht
-    using ⟨⟨I * t, by simp [ht]⟩, by simp [← coe_im]⟩
+    using ⟨⟨I * t, by simp [ht]⟩, by simp⟩
 
 theorem atImInfty_basis : atImInfty.HasBasis (fun _ => True) fun i : ℝ => im ⁻¹' Set.Ici i :=
   Filter.HasBasis.comap UpperHalfPlane.im Filter.atTop_basis
@@ -80,7 +80,7 @@ lemma tendsto_comap_im_ofComplex :
   simp only [atImInfty, tendsto_comap_iff, Function.comp_def]
   refine tendsto_comap.congr' ?_
   filter_upwards [preimage_mem_comap (Ioi_mem_atTop 0)] with z hz
-  simp only [ofComplex_apply_of_im_pos hz, ← UpperHalfPlane.coe_im, coe_mk_subtype]
+  simp [ofComplex_apply_of_im_pos hz]
 
 lemma tendsto_coe_atImInfty :
     Tendsto UpperHalfPlane.coe atImInfty (comap Complex.im atTop) := by

Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean

@@ -124,9 +124,8 @@ lemma eq_zero_of_frequently {f : ℍ → ℂ} (hf : MDifferentiable 𝓘(ℂ) 
   rw [UpperHalfPlane.mdifferentiable_iff] at hf
   have := hf.analyticOnNhd isOpen_upperHalfPlaneSet
   ext w
-  convert this.eqOn_zero_of_preconnected_of_frequently_eq_zero (z₀ := ↑τ) ?_ τ.2 ?_ w.property
-  · rw [Function.comp_apply, ofComplex_apply_of_im_pos w.property]
-    rfl
+  convert this.eqOn_zero_of_preconnected_of_frequently_eq_zero (z₀ := ↑τ) ?_ τ.2 ?_ w.im_pos
+  · rw [Function.comp_apply, ofComplex_apply]
   · exact (Complex.isConnected_of_upperHalfPlane subset_rfl (by grind)).isPreconnected
   · contrapose! hτ
     rw [eventually_nhdsWithin_iff, ← isOpenEmbedding_coe.map_nhds_eq, eventually_map] at hτ

Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean

@@ -137,8 +137,8 @@ theorem center_im (z r) : (center z r).im = z.im * Real.cosh r :=
   rfl
 
 @[simp]
-theorem center_zero (z : ℍ) : center z 0 = z :=
-  ext' rfl <| by rw [center_im, Real.cosh_zero, mul_one]
+theorem center_zero (z : ℍ) : center z 0 = z := by
+  apply ext_re_im <;> simp
 
 theorem dist_coe_center_sq (z w : ℍ) (r : ℝ) : dist (z : ℂ) (w.center r) ^ 2 =
     2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2 := by
@@ -304,7 +304,7 @@ theorem image_coe_sphere (z : ℍ) (r : ℝ) :
 
 instance : ProperSpace ℍ := by
   refine ⟨fun z r => ?_⟩
-  rw [IsInducing.subtypeVal.isCompact_iff (f := ((↑) : ℍ → ℂ)), image_coe_closedBall]
+  rw [isEmbedding_coe.isCompact_iff (f := ((↑) : ℍ → ℂ)), image_coe_closedBall]
   apply isCompact_closedBall
 
 theorem isometry_vertical_line (a : ℝ) : Isometry fun y => mk ⟨a, exp y⟩ (exp_pos y) := by
@@ -327,9 +327,9 @@ instance : IsIsometricSMul SL(2, ℝ) ℍ :=
   ⟨fun g => by
     have h₀ : Isometry (fun z => ModularGroup.S • z : ℍ → ℍ) :=
       Isometry.of_dist_eq fun y₁ y₂ => by
-        have h₁ : 0 ≤ im y₁ * im y₂ := mul_nonneg y₁.property.le y₂.property.le
+        have h₁ : 0 ≤ im y₁ * im y₂ := by positivity
         have h₂ : ‖(y₁ * y₂ : ℂ)‖ ≠ 0 := by simp [y₁.ne_zero, y₂.ne_zero]
-        simp_rw [modular_S_smul, inv_neg, dist_eq, coe_mk, dist_neg_neg,
+        simp_rw [modular_S_smul, inv_neg, dist_eq, dist_neg_neg,
           dist_inv_inv₀ y₁.ne_zero y₂.ne_zero, mk_im, neg_im, inv_im, coe_im, neg_div, neg_neg,
           div_mul_div_comm, ← normSq_mul, Real.sqrt_div h₁, ← norm_def, mul_div (2 : ℝ)]
         rw [div_div_div_comm, ← norm_mul, div_self h₂, div_one]

Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean

@@ -221,7 +221,7 @@ lemma denom_cocycle_σ (g h : GL (Fin 2) ℝ) (z : ℍ) :
   denom_cocycle' g h z
 
 lemma glPos_smul_def {g : GL (Fin 2) ℝ} (hg : 0 < g.det.val) (z : ℍ) :
-    g • z = mk (num g z / denom g z) (coe_smul_of_det_pos hg z ▸ (g • z).property) := by
+    g • z = ⟨num g z / denom g z, coe_smul_of_det_pos hg z ▸ (g • z).im_pos⟩ := by
   ext; simp [coe_smul_of_det_pos hg]
 
 variable (g : GL (Fin 2) ℝ) (z : ℍ)
@@ -272,7 +272,7 @@ theorem specialLinearGroup_apply {R : Type*} [CommRing R] [Algebra R ℝ] (g : S
     g • z = mk
       (((algebraMap R ℝ (g 0 0) : ℂ) * z + (algebraMap R ℝ (g 0 1) : ℂ)) /
       ((algebraMap R ℝ (g 1 0) : ℂ) * z + (algebraMap R ℝ (g 1 1) : ℂ)))
-      (coe_specialLinearGroup_apply g z ▸ (g • z).property) := by
+      (coe_specialLinearGroup_apply g z ▸ (g • z).im_pos) := by
   ext; simp [coe_specialLinearGroup_apply]
 
 /- these next few lemmas are *not* flagged `@simp` because of the constructors on the RHS;