noncomputable def SchwarzPick.mobiusMap (a w : ℂ) : ℂ

noncomputable def SchwarzPick.mobiusInv (a w : ℂ) : ℂ

theorem SchwarzPick.mobiusMap_self (a : ℂ) : mobiusMap a a = 0

theorem SchwarzPick.mobiusInv_zero (a : ℂ) : mobiusInv a 0 = a

theorem SchwarzPick.norm_conj_mul_lt_one {a w : ℂ} (ha : ‖a‖ < 1) (hw : ‖w‖ < 1) : ‖(starRingEnd ℂ) a * w‖ < 1

theorem SchwarzPick.one_sub_conj_mul_ne_zero {a w : ℂ} (ha : ‖a‖ < 1) (hw : ‖w‖ < 1) : 1 - (starRingEnd ℂ) a * w ≠ 0

theorem SchwarzPick.norm_sq_lt_one_of_norm_lt_one {z : ℂ} (hz : ‖z‖ < 1) : ‖z‖ ^ 2 < 1

theorem SchwarzPick.one_sub_norm_sq_pos {z : ℂ} (hz : ‖z‖ < 1) : 0 < 1 - ‖z‖ ^ 2

theorem SchwarzPick.mobiusMap_mem_ball {a w : ℂ} (ha : ‖a‖ < 1) (hw : ‖w‖ < 1) : mobiusMap a w ∈ Metric.ball 0 1

theorem SchwarzPick.mobiusInv_mem_ball {a w : ℂ} (ha : ‖a‖ < 1) (hw : ‖w‖ < 1) : mobiusInv a w ∈ Metric.ball 0 1

theorem SchwarzPick.differentiableOn_mobiusMap {a : ℂ} (ha : ‖a‖ < 1) : DifferentiableOn ℂ (mobiusMap a) (Metric.ball 0 1)

theorem SchwarzPick.differentiableOn_mobiusInv {a : ℂ} (ha : ‖a‖ < 1) : DifferentiableOn ℂ (mobiusInv a) (Metric.ball 0 1)

theorem SchwarzPick.schwarz_pick (h : ℂ → ℂ) (hd : DifferentiableOn ℂ h (Metric.ball 0 1)) (h_maps : Set.MapsTo h (Metric.ball 0 1) (Metric.ball 0 1)) (z : ℂ) (hz : z ∈ Metric.ball 0 1) : ‖deriv h z‖ ≤ (1 - ‖h z‖ ^ 2) / (1 - ‖z‖ ^ 2)

noncomputable def SchwarzPick.hyperbolicDist (z w : ℂ) (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : ℝ

theorem SchwarzPick.hyperbolic_dist_formula (z w : ℂ) (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : hyperbolicDist z w hz hw = 2 * Real.artanh (‖z - w‖ / ‖(starRingEnd ℂ) w * z - 1‖)

noncomputable def SchwarzPick.poincareConformalFactor (z : ℂ) : ℝ