From e5b2bf4863321b22a9905ece08336b34d955ee27 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 28 Dec 2025 15:11:08 -0600
Subject: [PATCH 1/8] feat: weaken assumptions in Schwarz lemma

---
 Mathlib/Analysis/Complex/Schwarz.lean | 93 ++++++++++++---------------
 1 file changed, 41 insertions(+), 52 deletions(-)

diff --git a/Mathlib/Analysis/Complex/Schwarz.lean b/Mathlib/Analysis/Complex/Schwarz.lean
index c3a57049f6d95e..1f2019cd323929 100644
--- a/Mathlib/Analysis/Complex/Schwarz.lean
+++ b/Mathlib/Analysis/Complex/Schwarz.lean
@@ -14,21 +14,21 @@ public import Mathlib.Analysis.Complex.RemovableSingularity
 In this file we prove several versions of the Schwarz lemma.
 
 * `Complex.norm_deriv_le_div_of_mapsTo_ball`, `Complex.abs_deriv_le_div_of_mapsTo_ball`: if
-  `f : ℂ → E` sends an open disk with center `c` and a positive radius `R₁` to an open ball with
+  `f : ℂ → E` sends an open disk with center `c` and a positive radius `R₁` to a closed ball with
   center `f c` and radius `R₂`, then the norm of the derivative of `f` at `c` is at most
   the ratio `R₂ / R₁`;
 
 * `Complex.dist_le_div_mul_dist_of_mapsTo_ball`: if `f : ℂ → E` sends an open disk with center `c`
-  and radius `R₁` to an open disk with center `f c` and radius `R₂`, then for any `z` in the former
+  and radius `R₁` to a closed disk with center `f c` and radius `R₂`, then for any `z` in the former
   disk we have `dist (f z) (f c) ≤ (R₂ / R₁) * dist z c`;
 
-* `Complex.abs_deriv_le_one_of_mapsTo_ball`: if `f : ℂ → ℂ` sends an open disk of positive radius
-  to itself and the center of this disk to itself, then the norm of the derivative of `f`
-  at the center of this disk is at most `1`;
+* `Complex.abs_deriv_le_one_of_mapsTo_ball`: if `f : ℂ → ℂ` sends a point `c` to itself
+  and it maps an open disk with center `c` to the closed disk with the same center and radius,
+  then the norm of the derivative of `f` at the center of this disk is at most `1`;
 
-* `Complex.dist_le_dist_of_mapsTo_ball_self`: if `f : ℂ → ℂ` sends an open disk to itself and the
-  center `c` of this disk to itself, then for any point `z` of this disk we have
-  `dist (f z) c ≤ dist z c`;
+* `Complex.dist_le_dist_of_mapsTo_ball_self`: if `f : ℂ → ℂ` sends a point `c` to itself
+  and it maps an open disk with center `c` to the closed disk with the same center and radius,
+  then for any point `z` of this disk we have `dist (f z) c ≤ dist z c`;
 
 * `Complex.norm_le_norm_of_mapsTo_ball_self`: if `f : ℂ → ℂ` sends an open disk with center `0` to
   itself, then for any point `z` of this disk we have `abs (f z) ≤ abs z`.
@@ -40,8 +40,6 @@ over complex numbers.
 
 ## TODO
 
-* Prove that these inequalities are strict unless `f` is an affine map.
-
 * Prove that any diffeomorphism of the unit disk to itself is a Möbius map.
 
 ## Tags
@@ -49,23 +47,16 @@ over complex numbers.
 Schwarz lemma
 -/
 
-@[expose] public section
-
-
 open Metric Set Function Filter TopologicalSpace
 
-open scoped Topology
-
-namespace Complex
-
-section Space
+open scoped Topology ComplexConjugate
 
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E}
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {R R₁ R₂ : ℝ} {f : ℂ → E}
   {c z z₀ : ℂ}
 
 /-- An auxiliary lemma for `Complex.norm_dslope_le_div_of_mapsTo_ball`. -/
-theorem schwarz_aux {f : ℂ → ℂ} (hd : DifferentiableOn ℂ f (ball c R₁))
-    (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
+private theorem Complex.schwarz_aux {f : ℂ → ℂ} (hd : DifferentiableOn ℂ f (ball c R₁))
+    (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)) (hz : z ∈ ball c R₁) :
     ‖dslope f c z‖ ≤ R₂ / R₁ := by
   have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
   suffices ∀ᶠ r in 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r by
@@ -84,39 +75,42 @@ theorem schwarz_aux {f : ℂ → ℂ} (hd : DifferentiableOn ℂ f (ball c R₁)
     intro z hz
     have hz' : z ≠ c := ne_of_mem_sphere hz hr₀.ne'
     rw [dslope_of_ne _ hz', slope_def_module, norm_smul, norm_inv, mem_sphere_iff_norm.1 hz, ←
-      div_eq_inv_mul, div_le_div_iff_of_pos_right hr₀, ← dist_eq_norm]
-    exact le_of_lt (h_maps (mem_ball.2 (by rw [mem_sphere.1 hz]; exact hr.2)))
+      div_eq_inv_mul, div_le_div_iff_of_pos_right hr₀, ← mem_closedBall_iff_norm]
+    exact h_maps <| mem_ball.2 <| by rw [mem_sphere.1 hz]; exact hr.2
   · rw [closure_ball c hr₀.ne', mem_closedBall]
     exact hr.1.le
 
+@[expose] public section
+
+namespace Complex
+
 /-- Two cases of the **Schwarz Lemma** (derivative and distance), merged together. -/
 theorem norm_dslope_le_div_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
-    (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
+    (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)) (hz : z ∈ ball c R₁) :
     ‖dslope f c z‖ ≤ R₂ / R₁ := by
   have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
-  have hR₂ : 0 < R₂ := nonempty_ball.1 ⟨f z, h_maps hz⟩
+  have hR₂ : 0 ≤ R₂ := nonempty_closedBall.mp ⟨f z, h_maps hz⟩
   rcases eq_or_ne (dslope f c z) 0 with hc | hc
-  · rw [hc, norm_zero]; exact div_nonneg hR₂.le hR₁.le
+  · rw [hc, norm_zero]; exact div_nonneg hR₂ hR₁.le
   rcases exists_dual_vector ℂ _ hc with ⟨g, hg, hgf⟩
   have hg' : ‖g‖₊ = 1 := NNReal.eq hg
-  have hg₀ : ‖g‖₊ ≠ 0 := by simpa only [hg'] using one_ne_zero
   calc
     ‖dslope f c z‖ = ‖dslope (g ∘ f) c z‖ := by
       rw [g.dslope_comp, hgf, RCLike.norm_ofReal, abs_norm]
       exact fun _ => hd.differentiableAt (ball_mem_nhds _ hR₁)
     _ ≤ R₂ / R₁ := by
       refine schwarz_aux (g.differentiable.comp_differentiableOn hd) (MapsTo.comp ?_ h_maps) hz
-      simpa only [hg', NNReal.coe_one, one_mul] using g.lipschitz.mapsTo_ball hg₀ (f c) R₂
+      simpa only [hg', NNReal.coe_one, one_mul] using g.lipschitz.mapsTo_closedBall (f c) R₂
 
 /-- Equality case in the **Schwarz Lemma**: in the setup of `norm_dslope_le_div_of_mapsTo_ball`, if
 `‖dslope f c z₀‖ = R₂ / R₁` holds at a point in the ball then the map `f` is affine. -/
 theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div [CompleteSpace E] [StrictConvexSpace ℝ E]
-    (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : Set.MapsTo f (ball c R₁) (ball (f c) R₂))
+    (hd : DifferentiableOn ℂ f (ball c R₁))
+    (h_maps : Set.MapsTo f (ball c R₁) (closedBall (f c) R₂))
     (h_z₀ : z₀ ∈ ball c R₁) (h_eq : ‖dslope f c z₀‖ = R₂ / R₁) :
     Set.EqOn f (fun z => f c + (z - c) • dslope f c z₀) (ball c R₁) := by
   set g := dslope f c
   rintro z hz
-  by_cases h : z = c; · simp [h]
   have h_R₁ : 0 < R₁ := nonempty_ball.mp ⟨_, h_z₀⟩
   have g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁ := fun z hz =>
     norm_dslope_le_div_of_mapsTo_ball hd h_maps hz
@@ -131,7 +125,7 @@ theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div [CompleteSpace E] [St
 
 theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div' [CompleteSpace E]
     [StrictConvexSpace ℝ E] (hd : DifferentiableOn ℂ f (ball c R₁))
-    (h_maps : Set.MapsTo f (ball c R₁) (ball (f c) R₂))
+    (h_maps : Set.MapsTo f (ball c R₁) (closedBall (f c) R₂))
     (h_z₀ : ∃ z₀ ∈ ball c R₁, ‖dslope f c z₀‖ = R₂ / R₁) :
     ∃ C : E, ‖C‖ = R₂ / R₁ ∧ Set.EqOn f (fun z => f c + (z - c) • C) (ball c R₁) :=
   let ⟨z₀, h_z₀, h_eq⟩ := h_z₀
@@ -141,46 +135,41 @@ theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div' [CompleteSpace E]
 `R₁` to an open ball with center `f c` and radius `R₂`, then the norm of the derivative of
 `f` at `c` is at most the ratio `R₂ / R₁`. -/
 theorem norm_deriv_le_div_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
-    (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (h₀ : 0 < R₁) : ‖deriv f c‖ ≤ R₂ / R₁ := by
+    (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)) (h₀ : 0 < R₁) :
+    ‖deriv f c‖ ≤ R₂ / R₁ := by
   simpa only [dslope_same] using norm_dslope_le_div_of_mapsTo_ball hd h_maps (mem_ball_self h₀)
 
-/-- The **Schwarz Lemma**: if `f : ℂ → E` sends an open disk with center `c` and radius `R₁` to an
-open ball with center `f c` and radius `R₂`, then for any `z` in the former disk we have
+/-- The **Schwarz Lemma**: if `f : ℂ → E` sends an open disk with center `c` and radius `R₁` to a
+closed ball with center `f c` and radius `R₂`, then for any `z` in the former disk we have
 `dist (f z) (f c) ≤ (R₂ / R₁) * dist z c`. -/
 theorem dist_le_div_mul_dist_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
-    (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
+    (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)) (hz : z ∈ ball c R₁) :
     dist (f z) (f c) ≤ R₂ / R₁ * dist z c := by
   rcases eq_or_ne z c with (rfl | hne)
   · simp only [dist_self, mul_zero, le_rfl]
   simpa only [dslope_of_ne _ hne, slope_def_module, norm_smul, norm_inv, ← div_eq_inv_mul, ←
     dist_eq_norm, div_le_iff₀ (dist_pos.2 hne)] using norm_dslope_le_div_of_mapsTo_ball hd h_maps hz
 
-end Space
-
-variable {f : ℂ → ℂ} {c z : ℂ} {R R₁ R₂ : ℝ}
-
 /-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk of positive radius to itself and the
 center of this disk to itself, then the norm of the derivative of `f` at the center of
 this disk is at most `1`. -/
 theorem norm_deriv_le_one_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R))
-    (h_maps : MapsTo f (ball c R) (ball c R)) (hc : f c = c) (h₀ : 0 < R) : ‖deriv f c‖ ≤ 1 :=
-  (norm_deriv_le_div_of_mapsTo_ball hd (by rwa [hc]) h₀).trans_eq (div_self h₀.ne')
+    (h_maps : MapsTo f (ball c R) (closedBall (f c) R)) (h₀ : 0 < R) : ‖deriv f c‖ ≤ 1 :=
+  (norm_deriv_le_div_of_mapsTo_ball hd h_maps h₀).trans_eq (div_self h₀.ne')
 
 /-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk to itself and the center `c` of this
 disk to itself, then for any point `z` of this disk we have `dist (f z) c ≤ dist z c`. -/
 theorem dist_le_dist_of_mapsTo_ball_self (hd : DifferentiableOn ℂ f (ball c R))
-    (h_maps : MapsTo f (ball c R) (ball c R)) (hc : f c = c) (hz : z ∈ ball c R) :
-    dist (f z) c ≤ dist z c := by
-  have := dist_le_div_mul_dist_of_mapsTo_ball hd (by rwa [hc]) hz
-  rwa [hc, div_self, one_mul] at this
-  exact (nonempty_ball.1 ⟨z, hz⟩).ne'
-
-/-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk with center `0` to itself, then for any
-point `z` of this disk we have `‖f z‖ ≤ ‖z‖`. -/
+    (h_maps : MapsTo f (ball c R) (closedBall (f c) R)) (hz : z ∈ ball c R) :
+    dist (f z) (f c) ≤ dist z c := by
+  simpa [(nonempty_ball.1 ⟨z, hz⟩).ne'] using dist_le_div_mul_dist_of_mapsTo_ball hd h_maps hz
+
+/-- The **Schwarz Lemma**: if `f : ℂ → E` sends an open disk with center `0`
+to the closed ball with center `0` of the same radius,
+then for any point `z` of this disk we have `‖f z‖ ≤ ‖z‖`. -/
 theorem norm_le_norm_of_mapsTo_ball_self (hd : DifferentiableOn ℂ f (ball 0 R))
-    (h_maps : MapsTo f (ball 0 R) (ball 0 R)) (h₀ : f 0 = 0) (hz : ‖z‖ < R) :
+    (h_maps : MapsTo f (ball 0 R) (closedBall 0 R)) (h₀ : f 0 = 0) (hz : ‖z‖ < R) :
     ‖f z‖ ≤ ‖z‖ := by
-  replace hz : z ∈ ball (0 : ℂ) R := mem_ball_zero_iff.2 hz
-  simpa only [dist_zero_right] using dist_le_dist_of_mapsTo_ball_self hd h_maps h₀ hz
+  simpa [h₀] using dist_le_dist_of_mapsTo_ball_self hd (by rwa [h₀]) (mem_ball_zero_iff.mpr hz)
 
 end Complex

From d862c6bbd4792026a50e87991e87371c956c167d Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 28 Dec 2025 19:17:40 -0600
Subject: [PATCH 2/8] feat: define `Complex.UnitDisc.shift`

---
 Mathlib/Analysis/Complex/UnitDisc/Basic.lean | 107 ++++++++----
 Mathlib/Analysis/Complex/UnitDisc/Shift.lean | 172 +++++++++++++++++++
 2 files changed, 242 insertions(+), 37 deletions(-)
 create mode 100644 Mathlib/Analysis/Complex/UnitDisc/Shift.lean

diff --git a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean
index bd1f33f30887b8..7eeeaa12d68fdd 100644
--- a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean
+++ b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean
@@ -17,20 +17,18 @@ introduce some basic operations on this disc.
 
 @[expose] public section
 
-
 open Set Function Metric
+open scoped ComplexConjugate
 
 noncomputable section
 
-local notation "conj'" => starRingEnd ℂ
-
 namespace Complex
 
 /-- The complex unit disc, denoted as `𝔻` withinin the Complex namespace -/
 def UnitDisc : Type :=
   ball (0 : ℂ) 1 deriving TopologicalSpace
 
-@[inherit_doc] scoped[UnitDisc] notation "𝔻" => Complex.UnitDisc
+@[inherit_doc] scoped[Complex.UnitDisc] notation "𝔻" => Complex.UnitDisc
 open UnitDisc
 
 namespace UnitDisc
@@ -44,6 +42,7 @@ instance instIsCancelMulZero : IsCancelMulZero UnitDisc := by unfold UnitDisc; i
 instance instHasDistribNeg : HasDistribNeg UnitDisc := by unfold UnitDisc; infer_instance
 instance instCoe : Coe UnitDisc ℂ := ⟨UnitDisc.coe⟩
 
+@[ext]
 theorem coe_injective : Injective ((↑) : 𝔻 → ℂ) :=
   Subtype.coe_injective
 
@@ -73,11 +72,25 @@ theorem one_add_coe_ne_zero (z : 𝔻) : (1 + z : ℂ) ≠ 0 :=
 theorem coe_mul (z w : 𝔻) : ↑(z * w) = (z * w : ℂ) :=
   rfl
 
+@[simp, norm_cast]
+theorem coe_neg (z : 𝔻) : ↑(-z) = (-z : ℂ) := rfl
+
 /-- A constructor that assumes `‖z‖ < 1` instead of `dist z 0 < 1` and returns an element
 of `𝔻` instead of `↥Metric.ball (0 : ℂ) 1`. -/
 def mk (z : ℂ) (hz : ‖z‖ < 1) : 𝔻 :=
   ⟨z, mem_ball_zero_iff.2 hz⟩
 
+/-- A cases eliminator that makes `cases z` use `UnitDisc.mk` instead of `Subtype.mk`. -/
+@[elab_as_elim, cases_eliminator]
+protected def casesOn {motive : 𝔻 → Sort*} (mk : ∀ z hz, motive (.mk z hz)) (z : 𝔻) :
+    motive z :=
+  mk z z.norm_lt_one
+
+@[simp]
+theorem casesOn_mk {motive : 𝔻 → Sort*} (mk' : ∀ z hz, motive (.mk z hz)) {z : ℂ} (hz : ‖z‖ < 1) :
+    (mk z hz).casesOn mk' = mk' z hz :=
+  rfl
+
 @[simp]
 theorem coe_mk (z : ℂ) (hz : ‖z‖ < 1) : (mk z hz : ℂ) = z :=
   rfl
@@ -104,39 +117,42 @@ theorem coe_eq_zero {z : 𝔻} : (z : ℂ) = 0 ↔ z = 0 :=
 instance : Inhabited 𝔻 :=
   ⟨0⟩
 
-instance circleAction : MulAction Circle 𝔻 :=
+instance instMulActionCircle : MulAction Circle 𝔻 :=
   mulActionSphereBall
 
-instance isScalarTower_circle_circle : IsScalarTower Circle Circle 𝔻 :=
+instance instIsScalarTower_circle_circle : IsScalarTower Circle Circle 𝔻 :=
   isScalarTower_sphere_sphere_ball
 
-instance isScalarTower_circle : IsScalarTower Circle 𝔻 𝔻 :=
+instance instIsScalarTower_circle : IsScalarTower Circle 𝔻 𝔻 :=
   isScalarTower_sphere_ball_ball
 
-instance instSMulCommClass_circle : SMulCommClass Circle 𝔻 𝔻 :=
+instance instSMulCommClass_circle_left : SMulCommClass Circle 𝔻 𝔻 :=
   instSMulCommClass_sphere_ball_ball
 
-instance instSMulCommClass_circle' : SMulCommClass 𝔻 Circle 𝔻 :=
+instance instSMulCommClass_circle_right : SMulCommClass 𝔻 Circle 𝔻 :=
   SMulCommClass.symm _ _ _
 
 @[simp, norm_cast]
-theorem coe_smul_circle (z : Circle) (w : 𝔻) : ↑(z • w) = (z * w : ℂ) :=
+theorem coe_circle_smul (z : Circle) (w : 𝔻) : ↑(z • w) = (z * w : ℂ) :=
   rfl
 
-instance closedBallAction : MulAction (closedBall (0 : ℂ) 1) 𝔻 :=
+@[deprecated (since := "2025-04-21")]
+alias Complex.UnitDisc.coe_smul_circle := coe_circle_smul
+
+instance instMulActionClosedBall : MulAction (closedBall (0 : ℂ) 1) 𝔻 :=
   mulActionClosedBallBall
 
-instance isScalarTower_closedBall_closedBall :
+instance instIsScalarTower_closedBall_closedBall :
     IsScalarTower (closedBall (0 : ℂ) 1) (closedBall (0 : ℂ) 1) 𝔻 :=
   isScalarTower_closedBall_closedBall_ball
 
-instance isScalarTower_closedBall : IsScalarTower (closedBall (0 : ℂ) 1) 𝔻 𝔻 :=
+instance instIsScalarTower_closedBall : IsScalarTower (closedBall (0 : ℂ) 1) 𝔻 𝔻 :=
   isScalarTower_closedBall_ball_ball
 
-instance instSMulCommClass_closedBall : SMulCommClass (closedBall (0 : ℂ) 1) 𝔻 𝔻 :=
+instance instSMulCommClass_closedBall_left : SMulCommClass (closedBall (0 : ℂ) 1) 𝔻 𝔻 :=
   ⟨fun _ _ _ => Subtype.ext <| mul_left_comm _ _ _⟩
 
-instance instSMulCommClass_closedBall' : SMulCommClass 𝔻 (closedBall (0 : ℂ) 1) 𝔻 :=
+instance instSMulCommClass_closedBall_right : SMulCommClass 𝔻 (closedBall (0 : ℂ) 1) 𝔻 :=
   SMulCommClass.symm _ _ _
 
 instance instSMulCommClass_circle_closedBall : SMulCommClass Circle (closedBall (0 : ℂ) 1) 𝔻 :=
@@ -146,9 +162,12 @@ instance instSMulCommClass_closedBall_circle : SMulCommClass (closedBall (0 : 
   SMulCommClass.symm _ _ _
 
 @[simp, norm_cast]
-theorem coe_smul_closedBall (z : closedBall (0 : ℂ) 1) (w : 𝔻) : ↑(z • w) = (z * w : ℂ) :=
+theorem coe_closedBall_smul (z : closedBall (0 : ℂ) 1) (w : 𝔻) : ↑(z • w) = (z * w : ℂ) :=
   rfl
 
+@[deprecated (since := "2025-12-25")]
+alias coe_smul_closedBall := coe_closedBall_smul
+
 /-- Real part of a point of the unit disc. -/
 def re (z : 𝔻) : ℝ :=
   Complex.re z
@@ -174,36 +193,50 @@ theorem im_neg (z : 𝔻) : (-z).im = -z.im :=
   rfl
 
 /-- Conjugate point of the unit disc. -/
-def conj (z : 𝔻) : 𝔻 :=
-  mk (conj' ↑z) <| (norm_conj z).symm ▸ z.norm_lt_one
+instance : Star 𝔻 where
+  star z := mk (conj z) <| (norm_conj z).symm ▸ z.norm_lt_one
 
-@[simp]
-theorem coe_conj (z : 𝔻) : (z.conj : ℂ) = conj' ↑z :=
-  rfl
+@[deprecated star (since := "2025-12-28")]
+protected def «conj» (z : 𝔻) := star z
 
-@[simp]
-theorem conj_zero : conj 0 = 0 :=
-  coe_injective (map_zero conj')
+@[simp] theorem coe_star (z : 𝔻) : (↑(star z) : ℂ) = conj ↑z := rfl
 
-@[simp]
-theorem conj_conj (z : 𝔻) : conj (conj z) = z :=
-  coe_injective <| Complex.conj_conj (z : ℂ)
+@[deprecated (since := "2025-12-28")]
+alias coe_conj := coe_star
 
 @[simp]
-theorem conj_neg (z : 𝔻) : (-z).conj = -z.conj :=
-  rfl
+protected theorem star_eq_zero {z : 𝔻} : star z = 0 ↔ z = 0 := by
+  simp [← coe_eq_zero]
 
 @[simp]
-theorem re_conj (z : 𝔻) : z.conj.re = z.re :=
-  rfl
+protected theorem star_zero : star (0 : 𝔻) = 0 := by simp
 
-@[simp]
-theorem im_conj (z : 𝔻) : z.conj.im = -z.im :=
-  rfl
+instance : InvolutiveStar 𝔻 where
+  star_involutive z := by ext; simp
 
-@[simp]
-theorem conj_mul (z w : 𝔻) : (z * w).conj = z.conj * w.conj :=
-  Subtype.ext <| map_mul _ _ _
+@[deprecated star_star (since := "2025-12-28")]
+theorem conj_conj (z : 𝔻) : star (star z) = z := star_star z
+
+@[simp] protected theorem star_neg (z : 𝔻) : star (-z) = -(star z) := rfl
+
+@[deprecated (since := "2025-12-28")]
+alias conj_neg := UnitDisc.star_neg
+
+@[simp] protected theorem re_star (z : 𝔻) : (star z).re = z.re := rfl
+
+@[deprecated (since := "2025-12-28")]
+alias re_conj := UnitDisc.re_star
+
+@[simp] protected theorem im_star (z : 𝔻) : (star z).im = -z.im := rfl
+
+@[deprecated (since := "2025-12-28")] alias im_conj := UnitDisc.im_star
+
+instance : StarMul 𝔻 where
+  star_mul z w := coe_injective <| by simp [mul_comm]
+
+@[deprecated star_mul' (since := "2025-12-28")]
+theorem conj_mul (z w : 𝔻) : star (z * w) = star z * star w :=
+  star_mul' z w
 
 end UnitDisc
 
diff --git a/Mathlib/Analysis/Complex/UnitDisc/Shift.lean b/Mathlib/Analysis/Complex/UnitDisc/Shift.lean
new file mode 100644
index 00000000000000..adabfdd0ed575c
--- /dev/null
+++ b/Mathlib/Analysis/Complex/UnitDisc/Shift.lean
@@ -0,0 +1,172 @@
+/-
+Copyright (c) 2025 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+
+module
+public import Mathlib.Analysis.Complex.UnitDisc.Basic
+
+/-!
+# Shift on the unit disc
+
+In this file we define `Complex.UnitDisc.shift z` to be the automorphism of the unit disc
+that sends `0` to `z` and preserves the diameter joining `0` to `z`.
+
+We also prove basic properties of this function.
+-/
+
+open Set Function Metric
+open scoped ComplexConjugate
+
+noncomputable section
+
+namespace Complex.UnitDisc
+
+public section
+
+lemma shift_den_ne_zero (z w : 𝔻) : 1 + conj (z : ℂ) * w ≠ 0 :=
+  (star z * w).one_add_coe_ne_zero
+
+lemma shift_den_ne_zero' (z w : 𝔻) : 1 + z * conj (w : ℂ) ≠ 0 :=
+  (z * star w).one_add_coe_ne_zero
+
+end
+
+/-- Auxiliary definition for `shift` below. This function is not a part of the public API. -/
+def shiftFun (z w : 𝔻) : 𝔻 :=
+  mk ((z + w : ℂ) / (1 + conj ↑z * w)) <| by
+    suffices ‖(z + w : ℂ)‖ < ‖1 + conj (z : ℂ) * w‖ by
+      rwa [norm_div, div_lt_one]
+      exact (norm_nonneg _).trans_lt this
+    dsimp only [Complex.norm_def]
+    gcongr
+    · apply normSq_nonneg -- TODO: add a `positivity` extension
+    · rw [← sub_pos]
+      convert mul_pos (sub_pos.2 z.normSq_lt_one) (sub_pos.2 w.normSq_lt_one) using 1
+      simp [normSq]
+      ring
+
+theorem coe_shiftFun (z w : 𝔻) : (shiftFun z w : ℂ) = (z + w) / (1 + conj ↑z * w) := rfl
+
+theorem shiftFun_eq_iff {z w u : 𝔻} : shiftFun z w = u ↔ (z + w : ℂ) = u + u * conj ↑z * w := by
+  rw [← coe_inj, coe_shiftFun, div_eq_iff (shift_den_ne_zero _ _)]
+  ring_nf
+
+theorem shiftFun_neg_apply_shiftFun (z w : 𝔻) : shiftFun (-z) (shiftFun z w) = w := by
+  rw [shiftFun_eq_iff, coe_shiftFun, add_div_eq_mul_add_div, ← mul_div_assoc,
+    add_div_eq_mul_add_div]
+  · simp; ring
+  all_goals exact shift_den_ne_zero z w
+
+public section
+
+/-- The automorphism of the unit disc that sends zero to `z`. -/
+def shift (z : 𝔻) : 𝔻 ≃ 𝔻 where
+  toFun := shiftFun z
+  invFun := shiftFun (-z)
+  left_inv := shiftFun_neg_apply_shiftFun _
+  right_inv := by simpa using shiftFun_neg_apply_shiftFun (-z)
+
+/-- An explicit formula for `shift z w`.
+
+Note that the definition of `shift` is not exposed, so this is not a `dsimp` lemma. -/
+theorem coe_shift (z w : 𝔻) : (shift z w : ℂ) = (z + w) / (1 + conj ↑z * w) := by rfl
+
+theorem shift_eq_iff {z w u : 𝔻} : shift z w = u ↔ (z + w : ℂ) = u + u * conj ↑z * w :=
+  shiftFun_eq_iff
+
+theorem symm_shift (z : 𝔻) : (shift z).symm = shift (-z) := by
+  ext1
+  rfl
+
+@[simp]
+theorem star_shift (z w : 𝔻) : star (shift z w) = shift (star z) (star w) :=
+  coe_injective <| by simp [coe_shift]
+
+theorem norm_shift_swap (z w : 𝔻) : ‖(shift z w : ℂ)‖ = ‖(shift w z : ℂ)‖ := by
+  rw [coe_shift, norm_div, ← norm_conj (1 + _)]
+  simp [coe_shift, add_comm, mul_comm]
+
+theorem neg_shift (z w : 𝔻) : -shift z w = shift (-z) (-w) := by
+  ext1
+  simp [coe_shift, ← neg_add_rev, add_comm, neg_div]
+
+@[simp]
+theorem shift_zero : shift 0 = .refl 𝔻 := by
+  ext z
+  simp [coe_shift]
+
+@[simp]
+theorem shift_apply_zero (z : 𝔻) : shift z 0 = z := by simp [shift_eq_iff]
+
+@[simp]
+theorem shift_eq_zero_iff {z w : 𝔻} : shift z w = 0 ↔ w = -z := by
+  rw [← Equiv.eq_symm_apply, symm_shift, shift_apply_zero]
+
+@[simp]
+theorem shift_apply_neg_self (z : 𝔻) : shift z (-z) = 0 := by simp
+
+@[simp]
+theorem shift_neg_apply_self (z : 𝔻) : shift (-z) z = 0 := by simp
+
+@[simp]
+theorem shift_neg_apply_shift (z w : 𝔻) : shift (-z) (shift z w) = w := by
+  rw [← symm_shift, Equiv.symm_apply_apply]
+
+@[simp]
+theorem shift_apply_shift_neg (z w : 𝔻) : shift z (shift (-z) w) = w := by
+  simpa using shift_neg_apply_shift (-z) w
+
+/-- A shift by `0` is the identity map, and all other shifts have no fixed points. -/
+@[simp]
+theorem shift_eq_self_iff {z w : 𝔻} : shift z w = w ↔ z = 0 := by
+  rcases eq_or_ne z 0 with rfl | hz
+  · simp
+  suffices (z : ℂ) ≠ w * conj ↑z * w by
+    simpa [shift_eq_iff, hz, add_comm (z : ℂ)] using this
+  refine ne_of_apply_ne norm (ne_of_gt ?_)
+  calc
+    _ = ‖(z : ℂ)‖ * ‖(w : ℂ)‖ ^ 2 := by simp; ring
+    _ < ‖(z : ℂ)‖ := mul_lt_of_lt_one_right (by simpa) <| by
+      rw [← Complex.normSq_eq_norm_sq]; exact w.normSq_lt_one
+
+lemma shift_apply_circle_smul (c : Circle) (z w : 𝔻) :
+    shift z (c • w) = c • shift (c⁻¹ • z) w := by
+  ext1
+  simp only [coe_shift, coe_circle_smul, ← mul_div_assoc, mul_add,
+    map_mul, Circle.coe_inv_eq_conj, Complex.conj_conj, ← mul_assoc]
+  rw [← Circle.coe_inv_eq_conj, ← Circle.coe_mul]
+  simp [mul_comm (c : ℂ)]
+
+/-- The composition of two shifts is a rotation by `shiftCompCoeff z w` composed with a shift. -/
+@[simps! coe]
+def shiftCompCoeff (z w : 𝔻) : Circle :=
+  .ofConjDivSelf (1 + conj ↑z * w) (shift_den_ne_zero _ _)
+
+theorem shift_apply_shift (z w u : 𝔻) :
+    shift z (shift w u) = shiftCompCoeff z w • shift (shift w z) u := by
+  ext1
+  have H₁ (z w u : 𝔻) : 1 + u * conj (w : ℂ) + (w + u) * conj (z : ℂ) ≠ 0 := by
+    have := shift_den_ne_zero' (shift w u) z
+    rw [coe_shift, div_mul_eq_mul_div₀, add_div_eq_mul_add_div, div_ne_zero_iff] at this
+    · simpa [mul_comm] using this.left
+    · apply shift_den_ne_zero
+  have H₂ : 1 + w * conj (z : ℂ) + u * (conj ↑w + conj ↑z) ≠ 0 := by
+    simpa [mul_comm] using H₁ (star u) (star w) (star z)
+  simp [coe_shift]
+  field_simp
+    (disch := first | apply shift_den_ne_zero | apply shift_den_ne_zero' | apply H₁ | exact H₂)
+  ring
+
+theorem shift_trans_shift (z w : 𝔻) :
+    (shift z).trans (shift w) =
+      (shift (shift z w)).trans (MulAction.toPerm (shiftCompCoeff w z)) := by
+  ext1 u
+  simp [shift_apply_shift]
+
+end
+
+end UnitDisc
+
+end Complex

From 7be690b82c92bae85e34aa0a30e86445ae96a747 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 28 Dec 2025 22:42:09 -0600
Subject: [PATCH 3/8] Update

---
 Mathlib/Analysis/Complex/UnitDisc/Basic.lean  |   3 +
 .../Analysis/Complex/UnitDisc/Schwarz.lean    | 136 ++++++++++++++++++
 2 files changed, 139 insertions(+)
 create mode 100644 Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean

diff --git a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean
index 7eeeaa12d68fdd..cfba6a46fdc56e 100644
--- a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean
+++ b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean
@@ -42,6 +42,9 @@ instance instIsCancelMulZero : IsCancelMulZero UnitDisc := by unfold UnitDisc; i
 instance instHasDistribNeg : HasDistribNeg UnitDisc := by unfold UnitDisc; infer_instance
 instance instCoe : Coe UnitDisc ℂ := ⟨UnitDisc.coe⟩
 
+instance instCanLift : CanLift ℂ 𝔻 (↑) (‖·‖ < 1) where
+  prf x hx := ⟨⟨x, mem_ball_zero_iff.mpr hx⟩, rfl⟩
+
 @[ext]
 theorem coe_injective : Injective ((↑) : 𝔻 → ℂ) :=
   Subtype.coe_injective
diff --git a/Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean b/Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean
new file mode 100644
index 00000000000000..2df349ee0bb417
--- /dev/null
+++ b/Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean
@@ -0,0 +1,136 @@
+module
+
+public import Mathlib.Analysis.Complex.Basic
+public import Mathlib.Analysis.Calculus.FDeriv.Defs
+import Mathlib.Analysis.Complex.Schwarz
+import Mathlib.Analysis.Complex.UnitDisc.Shift
+
+open Function Set Metric
+open scoped BigOperators ComplexConjugate Complex.UnitDisc Topology
+
+public section
+
+namespace Complex
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {r R : ℝ}
+
+/-- **Schwarz-Pick lemma** for a map from a disc in `ℂ` to a disc in a normed space,
+estimating the distance between the images of two points in the disc. -/
+theorem dist_le_of_mapsTo_ball_of_mem {z w : ℂ} (hd : DifferentiableOn ℂ f (ball c r))
+    (h_maps : MapsTo f (ball c r) (closedBall (f z) R))
+    (hz : z ∈ ball c r) (hw : w ∈ ball c r) :
+    dist (f z) (f w) ≤ R * r * dist z w / ‖r ^ 2 - conj (z - c) * (w - c)‖ := by
+  wlog H : c = 0 ∧ r = 1
+  · set g : ℂ → ℂ := fun x ↦ c + r • x
+    have hr₀ : 0 < r := nonempty_ball.mp ⟨z, hz⟩
+    have hg_img : g '' ball 0 1 = ball c r := by
+      simpa only [g, ← image_smul, ← image_vadd, image_image] using affinity_unitBall hr₀ c
+    rw [← hg_img, mem_image] at hz hw
+    rcases hz with ⟨z, hz, rfl⟩
+    rcases hw with ⟨w, hw, rfl⟩
+    replace hd : DifferentiableOn ℂ (f ∘ g) (ball 0 1) :=
+      hd.comp (by fun_prop) (hg_img ▸ mapsTo_image _ _)
+    replace h_maps : MapsTo (f ∘ g) (ball 0 1) (closedBall (f (g z)) R) :=
+      h_maps.comp (hg_img ▸ mapsTo_image _ _)
+    convert this hd h_maps hz hw ⟨rfl, rfl⟩ using 1
+    simp [g, dist_eq_norm, ← mul_sub, abs_of_pos hr₀, mul_mul_mul_comm (r : ℂ) _ (r : ℂ), ← sq,
+      ← mul_one_sub]
+    field_simp
+  rcases H with ⟨rfl, rfl⟩
+  rw [mem_ball_zero_iff] at hz hw
+  lift z to 𝔻 using hz
+  lift w to 𝔻 using hw
+  set g : ℂ → ℂ := fun x ↦ (z + x) / (1 + conj ↑z * x)
+  have hg_coe : ∀ x : 𝔻, g x = z.shift x := by simp [g, UnitDisc.coe_shift]
+  have hg_maps : MapsTo g (ball 0 1) (ball 0 1) := by
+    intro x hx
+    rw [mem_ball_zero_iff] at hx ⊢
+    lift x to 𝔻 using hx
+    simpa only [hg_coe] using (z.shift x).norm_lt_one
+  have hg_img : g '' ball 0 1 = ball 0 1 := by
+    refine hg_maps.image_subset.antisymm fun x hx ↦ ?_
+    rw [mem_ball_zero_iff] at hx
+    use (-z).shift (.mk x hx), Subtype.prop _
+    simpa only [UnitDisc.coe_shift, g, ← UnitDisc.coe_inj]
+      using UnitDisc.shift_apply_shift_neg z (.mk x hx)
+  have hg₀ : g 0 = z := by simp [g]
+  replace hd : DifferentiableOn ℂ (f ∘ g) (ball 0 1) := by
+    refine hd.comp (fun x hx ↦ ?_) hg_maps
+    have : 1 + conj (z : ℂ) * x ≠ 0 := z.shift_den_ne_zero ⟨x, hx⟩
+    fun_prop (disch := assumption)
+  convert dist_le_div_mul_dist_of_mapsTo_ball hd
+    (by simpa only [Function.comp_apply, hg₀] using h_maps.comp hg_maps)
+    (z := (-z).shift w) (Subtype.prop _) using 1
+  · simp [hg_coe, hg₀, dist_comm]
+  · simp [UnitDisc.coe_shift, dist_eq_norm_sub', ← sub_eq_neg_add, ← sub_eq_add_neg, mul_div_assoc]
+
+theorem dist_le_of_differentiableOn_update_of_norm_le {ι : Type*} [Fintype ι] [DecidableEq ι]
+    {f : (ι → ℂ) → E} {c : ι → ℂ} {r : ι → ℝ} {M : ℝ}
+    (hfd : ∀ z ∈ univ.pi fun i ↦ ball (c i) (r i), ∀ i,
+      DifferentiableOn ℂ (f ∘ update z i) (ball (c i) (r i)))
+    (hM : ∀ z ∈ univ.pi fun i ↦ ball (c i) (r i), ‖f z‖ ≤ M)
+    {z w : ι → ℂ} (hz : z ∈ univ.pi fun i ↦ ball (c i) (r i))
+    (hw : w ∈ univ.pi fun i ↦ ball (c i) (r i)) :
+    dist (f z) (f w) ≤ 2 * M * ∑ i,
+      r i * dist (z i) (w i) / ‖r i ^ 2 - conj (z i - c i) * (w i - c i)‖ := by
+  rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
+  set z' : Fin (n + 1) → ι → ℂ := fun k i ↦ if (e i).castSucc < k then w i else z i
+  have hz'_dist (i : ι) :
+      dist (f (z' (e i).castSucc)) (f (z' (e i).succ)) ≤
+        2 * M * r i * dist (z i) (w i) / ‖r i ^ 2 - conj (z i - c i) * (w i - c i)‖ := by
+    simp only [mem_univ_pi, mem_ball] at *
+    set g : ℂ → E := f ∘ update (z' (e i).castSucc) i
+    have hgd : DifferentiableOn ℂ g (ball (c i) (r i)) := by
+      refine hfd (z' (e i).castSucc) (fun j ↦ ?_) i
+      by_cases H : e j < e i <;> simp [z', H, hz, hw]
+    have hmaps : MapsTo g (ball (c i) (r i)) (closedBall (g (z i)) (2 * M)) := by
+      intro x hx
+      rw [mem_ball] at hx
+      rw [mem_closedBall, two_mul]
+      refine (dist_le_norm_add_norm _ _).trans (add_le_add ?_ ?_) <;> apply hM <;>
+        · intro j
+          rcases eq_or_ne j i with rfl | hj <;> [skip; by_cases H : e j < e i] <;> simp [z', *]
+    convert dist_le_of_mapsTo_ball_of_mem (w := w i) hgd hmaps (by simp [hz]) (by simp [hw])
+      using 1
+    simp only [g, Function.comp_apply]
+    congr 2 with j <;>
+      rcases eq_or_ne j i with rfl | hj <;> simp [z', *, le_iff_eq_or_lt]
+  calc
+    dist (f z) (f w) ≤ ∑ k : Fin n, dist (f (z' k.castSucc)) (f (z' k.succ)) := by
+      rw [Finset.sum_fin_eq_sum_range]
+      convert dist_le_range_sum_dist (fun i ↦ if h : i < n + 1 then f (z' ⟨i, h⟩) else 0) n
+        with i hi
+      · simp [z', Fin.lt_def]
+      · rw [Finset.mem_range] at hi
+        simp [hi, hi.trans n.lt_add_one]
+    _ ≤ _ := by
+      rw [← e.sum_comp, Finset.mul_sum]
+      gcongr with i hi
+      simpa [mul_assoc, mul_div_assoc] using hz'_dist i
+
+theorem continuousOn_of_differentiableOn_update_of_bddAbove {ι : Type*} [Finite ι] [DecidableEq ι]
+    {f : (ι → ℂ) → E} {c : ι → ℂ} {r : ι → ℝ}
+    (hfd : ∀ z ∈ univ.pi fun i ↦ ball (c i) (r i), ∀ i,
+      DifferentiableOn ℂ (f ∘ update z i) (ball (c i) (r i)))
+    (hbdd : BddAbove ((‖f ·‖) '' univ.pi fun i ↦ ball (c i) (r i))) :
+    ContinuousOn f (univ.pi fun i ↦ ball (c i) (r i)) := by
+  rcases nonempty_fintype ι
+  rcases hbdd with ⟨M, hM⟩
+  rw [mem_upperBounds, forall_mem_image] at hM
+  intro z hz
+  rw [ContinuousWithinAt, tendsto_iff_dist_tendsto_zero]
+  refine squeeze_zero' (.of_forall fun _ ↦ dist_nonneg)
+    (eventually_mem_nhdsWithin.mono fun _ h ↦
+      dist_le_of_differentiableOn_update_of_norm_le hfd hM h hz) ?_
+  convert ContinuousWithinAt.tendsto _
+  · simp
+  · refine .const_mul _ <| tendsto_finset_sum _ fun i hi ↦ .div ?_ ?_ ?_
+    · exact Continuous.continuousWithinAt (by fun_prop)
+    · exact Continuous.continuousWithinAt (by fun_prop)
+    · rw [norm_ne_zero_iff, sub_ne_zero, conj_mul']
+      norm_cast
+      refine ne_of_gt ?_
+      gcongr
+      simpa using hz i
+
+end Complex

From 24ce7fb6a9707322dfb7504024946a8ffbf17c4d Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 29 Dec 2025 01:33:45 -0600
Subject: [PATCH 4/8] Add an aux lemma

---
 Mathlib/Analysis/Complex/UnitDisc/Basic.lean |  8 +++--
 Mathlib/Analysis/Complex/UnitDisc/Shift.lean | 34 ++++++++++++++------
 2 files changed, 30 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean
index 7eeeaa12d68fdd..cbcb5526fdfbc4 100644
--- a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean
+++ b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean
@@ -55,9 +55,13 @@ theorem norm_lt_one (z : 𝔻) : ‖(z : ℂ)‖ < 1 :=
 theorem norm_ne_one (z : 𝔻) : ‖(z : ℂ)‖ ≠ 1 :=
   z.norm_lt_one.ne
 
+theorem sq_norm_lt_one (z : 𝔻) : ‖(z : ℂ)‖ ^ 2 < 1 := by
+  rw [sq_lt_one_iff_abs_lt_one, abs_norm]
+  exact z.norm_lt_one
+
 theorem normSq_lt_one (z : 𝔻) : normSq z < 1 := by
-  convert (Real.sqrt_lt' one_pos).1 z.norm_lt_one
-  exact (one_pow 2).symm
+  rw [← Complex.norm_mul_self_eq_normSq, ← sq]
+  exact z.sq_norm_lt_one
 
 theorem coe_ne_one (z : 𝔻) : (z : ℂ) ≠ 1 :=
   ne_of_apply_ne (‖·‖) <| by simp [z.norm_ne_one]
diff --git a/Mathlib/Analysis/Complex/UnitDisc/Shift.lean b/Mathlib/Analysis/Complex/UnitDisc/Shift.lean
index adabfdd0ed575c..556d6d521fa59e 100644
--- a/Mathlib/Analysis/Complex/UnitDisc/Shift.lean
+++ b/Mathlib/Analysis/Complex/UnitDisc/Shift.lean
@@ -33,19 +33,29 @@ lemma shift_den_ne_zero' (z w : 𝔻) : 1 + z * conj (w : ℂ) ≠ 0 :=
 
 end
 
+theorem norm_shiftFun_le (z w : 𝔻) :
+    ‖(z + w : ℂ) / (1 + conj ↑z * w)‖ ≤ (‖(z : ℂ)‖ + ‖(w : ℂ)‖) / (1 + ‖(z : ℂ)‖ * ‖(w : ℂ)‖) := by
+  have hz := z.sq_norm_lt_one
+  have hw := w.sq_norm_lt_one
+  have hzw : z.re * w.re + z.im * w.im ≤ ‖(z : ℂ)‖ * ‖(w : ℂ)‖ := by
+    rw [norm_def, norm_def, ← Real.sqrt_mul, normSq_apply, normSq_apply]
+    · apply Real.le_sqrt_of_sq_le
+      linear_combination (norm := {apply le_of_eq; simp; ring})
+        sq_nonneg (z.re * w.im - z.im * w.re)
+    · apply normSq_nonneg
+  rw [norm_div, div_le_div_iff₀, ← sq_le_sq₀]
+  · rw [← sub_nonneg] at hzw
+    simp [mul_pow, RCLike.norm_sq_eq_def, add_sq] at hz hw ⊢
+    linear_combination 2 * mul_nonneg hzw (mul_nonneg (sub_nonneg.2 hz.le) (sub_nonneg.2 hw.le))
+  any_goals positivity
+  simpa using shift_den_ne_zero z w
+
 /-- Auxiliary definition for `shift` below. This function is not a part of the public API. -/
 def shiftFun (z w : 𝔻) : 𝔻 :=
   mk ((z + w : ℂ) / (1 + conj ↑z * w)) <| by
-    suffices ‖(z + w : ℂ)‖ < ‖1 + conj (z : ℂ) * w‖ by
-      rwa [norm_div, div_lt_one]
-      exact (norm_nonneg _).trans_lt this
-    dsimp only [Complex.norm_def]
-    gcongr
-    · apply normSq_nonneg -- TODO: add a `positivity` extension
-    · rw [← sub_pos]
-      convert mul_pos (sub_pos.2 z.normSq_lt_one) (sub_pos.2 w.normSq_lt_one) using 1
-      simp [normSq]
-      ring
+    refine (norm_shiftFun_le _ _).trans_lt ?_
+    rw [div_lt_one (by positivity)]
+    nlinarith only [z.norm_lt_one, w.norm_lt_one]
 
 theorem coe_shiftFun (z w : 𝔻) : (shiftFun z w : ℂ) = (z + w) / (1 + conj ↑z * w) := rfl
 
@@ -118,6 +128,10 @@ theorem shift_neg_apply_shift (z w : 𝔻) : shift (-z) (shift z w) = w := by
 theorem shift_apply_shift_neg (z w : 𝔻) : shift z (shift (-z) w) = w := by
   simpa using shift_neg_apply_shift (-z) w
 
+theorem norm_shift_le (z w : 𝔻) :
+    ‖(z.shift w : ℂ)‖ ≤ (‖(z : ℂ)‖ + ‖(w : ℂ)‖) / (1 + ‖(z : ℂ)‖ * ‖(w : ℂ)‖) :=
+  norm_shiftFun_le z w
+
 /-- A shift by `0` is the identity map, and all other shifts have no fixed points. -/
 @[simp]
 theorem shift_eq_self_iff {z w : 𝔻} : shift z w = w ↔ z = 0 := by

From 213150118e037c3246dd09e202860f4ed3ebba91 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 29 Dec 2025 01:38:57 -0600
Subject: [PATCH 5/8] Run mk_all

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index ae3a5cc2936ad4..dcb5faef342a61 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1697,6 +1697,7 @@ public import Mathlib.Analysis.Complex.TaylorSeries
 public import Mathlib.Analysis.Complex.Tietze
 public import Mathlib.Analysis.Complex.Trigonometric
 public import Mathlib.Analysis.Complex.UnitDisc.Basic
+public import Mathlib.Analysis.Complex.UnitDisc.Shift
 public import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
 public import Mathlib.Analysis.Complex.UpperHalfPlane.Exp
 public import Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

From 1babb19cbe938926e11a2d14fd5b3ae4d449c638 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 29 Dec 2025 07:35:51 -0600
Subject: [PATCH 6/8] Add a missing docstring

---
 Mathlib/Analysis/Complex/UnitDisc/Basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean
index cbcb5526fdfbc4..7f6414f5276b4b 100644
--- a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean
+++ b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean
@@ -200,6 +200,7 @@ theorem im_neg (z : 𝔻) : (-z).im = -z.im :=
 instance : Star 𝔻 where
   star z := mk (conj z) <| (norm_conj z).symm ▸ z.norm_lt_one
 
+/-- Conjugate point of the unit disc. Deprecated, use `star` instead. -/
 @[deprecated star (since := "2025-12-28")]
 protected def «conj» (z : 𝔻) := star z
 

From 8f51ae82e5d2f42fd555242166cc56691add3e09 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 29 Dec 2025 08:01:47 -0600
Subject: [PATCH 7/8] Add docs

---
 Mathlib.lean                                  |  1 +
 .../Analysis/Complex/UnitDisc/Schwarz.lean    | 32 ++++++++++++++++++-
 2 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index dcb5faef342a61..60c2dd362eb23e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1697,6 +1697,7 @@ public import Mathlib.Analysis.Complex.TaylorSeries
 public import Mathlib.Analysis.Complex.Tietze
 public import Mathlib.Analysis.Complex.Trigonometric
 public import Mathlib.Analysis.Complex.UnitDisc.Basic
+public import Mathlib.Analysis.Complex.UnitDisc.Schwarz
 public import Mathlib.Analysis.Complex.UnitDisc.Shift
 public import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
 public import Mathlib.Analysis.Complex.UpperHalfPlane.Exp
diff --git a/Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean b/Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean
index 2df349ee0bb417..f16f10162e8f80 100644
--- a/Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean
+++ b/Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2025 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
 module
 
 public import Mathlib.Analysis.Complex.Basic
@@ -5,6 +10,20 @@ public import Mathlib.Analysis.Calculus.FDeriv.Defs
 import Mathlib.Analysis.Complex.Schwarz
 import Mathlib.Analysis.Complex.UnitDisc.Shift
 
+/-!
+# Schwarz-Pick lemma for maps from a ball
+
+In this file we prove a version of the Schwarz lemma that estimates `dist (f z) (f w)`
+for two points of a disc where `f` is complex differentiable and is bounded.
+
+As a corollary, we prove a similar estimate for a function bounded on a polydisc,
+then use it to show that a function that is separately holomorphic on a polydisc `U`
+and is bounded on `U` is continuous on `U`.
+
+The latter lemma is a step towards Hartogs's theorem
+saying that a function that is separately holomorphic must be holomorphic.
+-/
+
 open Function Set Metric
 open scoped BigOperators ComplexConjugate Complex.UnitDisc Topology
 
@@ -15,7 +34,10 @@ namespace Complex
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {r R : ℝ}
 
 /-- **Schwarz-Pick lemma** for a map from a disc in `ℂ` to a disc in a normed space,
-estimating the distance between the images of two points in the disc. -/
+estimating the distance between the images of two points in the disc.
+
+This version assumes that the disc in the codomain
+is centered around the image of one o fthe points. -/
 theorem dist_le_of_mapsTo_ball_of_mem {z w : ℂ} (hd : DifferentiableOn ℂ f (ball c r))
     (h_maps : MapsTo f (ball c r) (closedBall (f z) R))
     (hz : z ∈ ball c r) (hw : w ∈ ball c r) :
@@ -64,6 +86,8 @@ theorem dist_le_of_mapsTo_ball_of_mem {z w : ℂ} (hd : DifferentiableOn ℂ f (
   · simp [hg_coe, hg₀, dist_comm]
   · simp [UnitDisc.coe_shift, dist_eq_norm_sub', ← sub_eq_neg_add, ← sub_eq_add_neg, mul_div_assoc]
 
+/-- Give a function that is separately holomorphic on an open polydisc and is bounded on it,
+this lemma provides an explicit estimate on the distance between the images of any two points. -/
 theorem dist_le_of_differentiableOn_update_of_norm_le {ι : Type*} [Fintype ι] [DecidableEq ι]
     {f : (ι → ℂ) → E} {c : ι → ℂ} {r : ι → ℝ} {M : ℝ}
     (hfd : ∀ z ∈ univ.pi fun i ↦ ball (c i) (r i), ∀ i,
@@ -108,6 +132,12 @@ theorem dist_le_of_differentiableOn_update_of_norm_le {ι : Type*} [Fintype ι]
       gcongr with i hi
       simpa [mul_assoc, mul_div_assoc] using hz'_dist i
 
+/-- A function that is separately holomorphic and is bounded on a polydisc
+must be continuous on the same polydisc.
+
+This is a preliminary lemma that is needed to prove Hartogs's theorem
+saying that the first assumption is enough to conclude that the function is in fact analytic
+on the polydisc. -/
 theorem continuousOn_of_differentiableOn_update_of_bddAbove {ι : Type*} [Finite ι] [DecidableEq ι]
     {f : (ι → ℂ) → E} {c : ι → ℂ} {r : ι → ℝ}
     (hfd : ∀ z ∈ univ.pi fun i ↦ ball (c i) (r i), ∀ i,

From 0cc44dd3d7b596d35e8554af3d9b82eaa97bec71 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 30 Dec 2025 07:56:53 -0600
Subject: [PATCH 8/8] Update Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean

---
 Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean b/Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean
index f16f10162e8f80..5240fb742c7e48 100644
--- a/Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean
+++ b/Mathlib/Analysis/Complex/UnitDisc/Schwarz.lean
@@ -37,7 +37,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E}
 estimating the distance between the images of two points in the disc.
 
 This version assumes that the disc in the codomain
-is centered around the image of one o fthe points. -/
+is centered around the image of one of the points. -/
 theorem dist_le_of_mapsTo_ball_of_mem {z w : ℂ} (hd : DifferentiableOn ℂ f (ball c r))
     (h_maps : MapsTo f (ball c r) (closedBall (f z) R))
     (hz : z ∈ ball c r) (hw : w ∈ ball c r) :