awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
⊢ dist z w < r ↔ dist (↑z : ℂ) (↑(w.center r) : ℂ) < w.im * Real.sinh r

Tactic:
lt_iff_lt_of_cmp_eq_cmp (cmp_dist_eq_cmp_dist_coe_center z w r)

Premises used: lt_iff_lt_of_cmp_eq_cmp, UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
⊢ r < dist z w ↔ w.im * Real.sinh r < dist (↑z : ℂ) (↑(w.center r) : ℂ)

Tactic:
lt_iff_lt_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 <| cmp_dist_eq_cmp_dist_coe_center z w r)

Premises used: cmp_eq_cmp_symm, lt_iff_lt_of_cmp_eq_cmp, UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center, Iff.mp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
⊢ dist z w ≤ r ↔ dist (↑z : ℂ) (↑(w.center r) : ℂ) ≤ w.im * Real.sinh r

Tactic:
le_iff_le_of_cmp_eq_cmp (cmp_dist_eq_cmp_dist_coe_center z w r)

Premises used: le_iff_le_of_cmp_eq_cmp, UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
h : z.re = w.re
⊢ 0 < z.im / w.im

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
h : z.re = w.re
⊢ 0 < z.im / w.im

Tactic:
have h₀ : 0 < z.im / w.im := by positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
rw : dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = w.im * |(z.im / w.im - w.im / z.im) / 2|
rw₁ : (↑z : ℂ).re = (↑(w.center |log (z.im / w.im)|) : ℂ).re
⊢ dist z w = dist (log z.im) (log w.im)

Tactic:
rw [dist_eq_iff_dist_coe_center_eq, Real.dist_eq, ← abs_sinh, ← log_div z.im_ne_zero w.im_ne_zero,
    sinh_log h₀, dist_of_re_eq, coe_im, coe_im, center_im, cosh_abs, cosh_log h₀, inv_div]

Premises used: Real.sinh_log, Real.cosh_abs, UpperHalfPlane.im_ne_zero, Real.abs_sinh, UpperHalfPlane.dist_of_re_eq, UpperHalfPlane.center_im, Real.log_div, UpperHalfPlane.dist_eq_iff_dist_coe_center_eq, Real.dist_eq, Real.cosh_log, inv_div, UpperHalfPlane.coe_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ (↑z : ℂ).re = (↑(w.center |log (z.im / w.im)|) : ℂ).re

Tactic:
h

Premises used: UpperHalfPlane.re
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ (↑z : ℂ).re = (↑(w.center |log (z.im / w.im)|) : ℂ).re

Tactic:
exact h
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
rw : dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = w.im * |(z.im / w.im - w.im / z.im) / 2|
⊢ dist z w = dist (log z.im) (log w.im)

Tactic:
rw [dist_eq_iff_dist_coe_center_eq, Real.dist_eq, ← abs_sinh, ← log_div z.im_ne_zero w.im_ne_zero,
    sinh_log h₀, dist_of_re_eq, coe_im, coe_im, center_im, cosh_abs, cosh_log h₀, inv_div] <;>
  [skip; exact h]

Premises used: Real.sinh_log, Real.cosh_abs, UpperHalfPlane.im_ne_zero, Real.abs_sinh, UpperHalfPlane.dist_of_re_eq, UpperHalfPlane.center_im, Real.log_div, UpperHalfPlane.dist_eq_iff_dist_coe_center_eq, Real.dist_eq, Real.cosh_log, inv_div, UpperHalfPlane.coe_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
nth_rw : dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = |w.im| * |(z.im / w.im - w.im / z.im) / 2|
⊢ dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = w.im * |(z.im / w.im - w.im / z.im) / 2|

Tactic:
nth_rw 4 [← abs_of_pos w.im_pos]

Premises used: UpperHalfPlane.im_pos, abs_of_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
simp : |z.im - w.im * ((z.im / w.im + w.im / z.im) / 2)| = |w.im * ((z.im / w.im - w.im / z.im) / 2)|
⊢ dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = |w.im| * |(z.im / w.im - w.im / z.im) / 2|

Tactic:
simp only [← _root_.abs_mul, Real.dist_eq]

Premises used: abs_mul, Real.dist_eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
e_a : z.im - w.im * ((z.im / w.im + w.im / z.im) / 2) = w.im * ((z.im / w.im - w.im / z.im) / 2)
⊢ |z.im - w.im * ((z.im / w.im + w.im / z.im) / 2)| = |w.im * ((z.im / w.im - w.im / z.im) / 2)|

Tactic:
congr 1
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ z.im - w.im * ((z.im / w.im + w.im / z.im) / 2) = w.im * ((z.im / w.im - w.im / z.im) / 2)

Tactic:
field
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
dsimp :
  2 * arsinh (dist { re := 0, im := z.im : ℂ } { re := 0, im := w.im : ℂ } / (2 * √(z.im * w.im))) ≤
    2 * arsinh (dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)))
⊢ 2 *
      arsinh
        (dist { re := 0, im := z.im : ℂ } { re := 0, im := w.im : ℂ } /
          (2 *
            √({ coe := { re := 0, im := z.im : ℂ }, coe_im_pos := ⋯ : ℍ }.im *
                { coe := { re := 0, im := w.im : ℂ }, coe_im_pos := ⋯ : ℍ }.im))) ≤
    2 * arsinh (dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)))

Tactic:
dsimp only [coe_mk, mk_im]

Premises used: UpperHalfPlane.coe_mk, UpperHalfPlane.mk_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
hbc : dist { re := 0, im := z.im : ℂ } { re := 0, im := w.im : ℂ } ≤ dist (↑z : ℂ) (↑w : ℂ)
⊢ 2 * arsinh (dist { re := 0, im := z.im : ℂ } { re := 0, im := w.im : ℂ } / (2 * √(z.im * w.im))) ≤
    2 * arsinh (dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ dist { re := 0, im := z.im : ℂ } { re := 0, im := w.im : ℂ } ≤ dist (↑z : ℂ) (↑w : ℂ)

Tactic:
simpa [sqrt_sq_eq_abs, ← dist_eq_norm] using Complex.abs_im_le_norm (z - w)

Premises used: dist_eq_norm, UpperHalfPlane.coe, Real.sqrt_sq_eq_abs, HSub.hSub, Complex.abs_im_le_norm
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
rw : log z.im - log w.im ≤ dist z w
⊢ z.im ≤ w.im * rexp (dist z w)

Tactic:
rw [← div_le_iff₀' w.im_pos, ← exp_log z.im_pos, ← exp_log w.im_pos, ← Real.exp_sub, exp_le_exp]

Premises used: UpperHalfPlane.im_pos, Real.exp_log, Real.exp_le_exp, Real.exp_sub, div_le_iff₀'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ log z.im - log w.im ≤ dist z w

Tactic:
(le_abs_self _).trans (dist_log_im_le z w)

Premises used: le_abs_self, UpperHalfPlane.dist_log_im_le, LE.le.trans
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ log z.im - log w.im ≤ dist z w

Tactic:
exact (le_abs_self _).trans (dist_log_im_le z w)

Premises used: le_abs_self, UpperHalfPlane.dist_log_im_le, LE.le.trans
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ z.im / rexp (dist z w) ≤ w.im

Tactic:
(div_le_iff₀ (exp_pos _)).2 (im_le_im_mul_exp_dist z w)

Premises used: Iff.mpr, div_le_iff₀, UpperHalfPlane.im_le_im_mul_exp_dist, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
rw : w.im * Real.sinh (dist z w) + dist (↑w : ℂ) (↑(w.center (dist z w)) : ℂ) = w.im * (rexp (dist z w) - 1)
rw₁ : w.im * Real.sinh (dist z w) + w.im * (Real.cosh (dist z w) - 1) = w.im * (rexp (dist z w) - 1)
rw₂ : w.im * (Real.sinh (dist z w) + (Real.cosh (dist z w) - 1)) = w.im * (rexp (dist z w) - 1)
rw₃ : w.im * (Real.sinh (dist z w) + Real.cosh (dist z w) - 1) = w.im * (rexp (dist z w) - 1)
rw₄ rw₅ : w.im * (rexp (dist z w) - 1) = w.im * (rexp (dist z w) - 1)
⊢ dist (↑z : ℂ) (↑(w.center (dist z w)) : ℂ) + dist (↑w : ℂ) (↑(w.center (dist z w)) : ℂ) = w.im * (rexp (dist z w) - 1)

Tactic:
rw [dist_center_dist, dist_self_center, ← mul_add, ← add_sub_assoc, Real.sinh_add_cosh]

Premises used: add_sub_assoc, UpperHalfPlane.dist_self_center, UpperHalfPlane.dist_center_dist, mul_add, Real.sinh_add_cosh
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
rw :
  w.im * (1 - (Real.cosh (dist z w) - Real.sinh (dist z w))) =
    w.im * Real.sinh (dist z w) - w.im * (Real.cosh (dist z w) - 1)
⊢ w.im * (1 - rexp (-dist z w)) =
    dist (↑z : ℂ) (↑(w.center (dist z w)) : ℂ) - dist (↑w : ℂ) (↑(w.center (dist z w)) : ℂ)

Tactic:
rw [dist_center_dist, dist_self_center, ← Real.cosh_sub_sinh]

Premises used: UpperHalfPlane.dist_self_center, UpperHalfPlane.dist_center_dist, Real.cosh_sub_sinh
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ w.im * (1 - (Real.cosh (dist z w) - Real.sinh (dist z w))) =
    w.im * Real.sinh (dist z w) - w.im * (Real.cosh (dist z w) - 1)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
⊢ instTopologicalSpace = UniformSpace.toTopologicalSpace

Tactic:
le_antisymm (continuous_id_iff_le.1 ?_) ?_

Premises used: le_antisymm, continuous_id_iff_le, Iff.mp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
refine_1 : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] id
refine_2 : UniformSpace.toTopologicalSpace ≤ instTopologicalSpace
⊢ instTopologicalSpace = UniformSpace.toTopologicalSpace

Tactic:
refine le_antisymm (continuous_id_iff_le.1 ?_) ?_

Premises used: le_antisymm, continuous_id_iff_le, Iff.mp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] id

Tactic:
(@continuous_iff_continuous_dist ℍ ℍ metricSpaceAux.toPseudoMetricSpace _ _).2 ?_

Premises used: Iff.mpr, continuous_iff_continuous_dist
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
refine_1 : Continuous (Y := ℝ) fun (x : ℍ × ℍ) ↦ dist (id x.1) (id x.2)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] id

Tactic:
refine (@continuous_iff_continuous_dist ℍ ℍ metricSpaceAux.toPseudoMetricSpace _ _).2 ?_

Premises used: Iff.mpr, continuous_iff_continuous_dist
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
x : ℍ × ℍ
⊢ 2 * √(x.1.im * x.2.im) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
⊢ ∀ (x : ℍ × ℍ), 2 * √(x.1.im * x.2.im) ≠ 0

Tactic:
have : ∀ x : ℍ × ℍ, 2 * √(x.1.im * x.2.im) ≠ 0 := fun x => by positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : ∀ (x : ℍ × ℍ), 2 * √(x.1.im * x.2.im) ≠ 0
⊢ Continuous (Y := ℝ) fun (x : ℍ × ℍ) ↦ dist (id x.1) (id x.2)

Tactic:
apply_rules [Continuous.div, Continuous.mul, continuous_const, Continuous.arsinh,
        Continuous.dist, continuous_coe.comp, continuous_fst, continuous_snd,
        Real.continuous_sqrt.comp, continuous_im.comp]

Premises used: Continuous.comp, continuous_const, Real.continuous_sqrt, Continuous.dist, continuous_snd, continuous_fst, Continuous.div, Continuous.mul, UpperHalfPlane.continuous_im, Continuous.arsinh, UpperHalfPlane.continuous_coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
⊢ UniformSpace.toTopologicalSpace ≤ instTopologicalSpace

Tactic:
le_of_nhds_le_nhds fun z => ?_

Premises used: le_of_nhds_le_nhds
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
refine_2 : ∀ (z : ℍ), 𝓝 z ≤ 𝓝 z
⊢ UniformSpace.toTopologicalSpace ≤ instTopologicalSpace

Tactic:
refine le_of_nhds_le_nhds fun z => ?_

Premises used: le_of_nhds_le_nhds
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
refine_2 : 𝓝 z ≤ comap UpperHalfPlane.coe (𝓝 (↑z : ℂ))
⊢ 𝓝 z ≤ 𝓝 z

Tactic:
rw [nhds_induced]

Premises used: nhds_induced
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
⊢ 𝓝 z ≤ comap UpperHalfPlane.coe (𝓝 (↑z : ℂ))

Tactic:
(nhds_basis_ball.le_basis_iff (nhds_basis_ball.comap _)).2 fun R hR => ?_

Premises used: Iff.mpr, Set.Mem, setOf, Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap, Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
refine_2 : ∀ (R : ℝ) (hR : 0 < R), ∃ (i : ℝ), 0 < i ∧ ball z i ⊆ UpperHalfPlane.coe ⁻¹' ball (↑z : ℂ) R
⊢ 𝓝 z ≤ comap UpperHalfPlane.coe (𝓝 (↑z : ℂ))

Tactic:
refine (nhds_basis_ball.le_basis_iff (nhds_basis_ball.comap _)).2 fun R hR => ?_

Premises used: Iff.mpr, Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap, Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
⊢ 1 < R / z.im + 1

Tactic:
have h₁ : 1 < R / im z + 1 := lt_add_of_pos_left _ (div_pos hR z.im_pos)
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / z.im + 1
⊢ 0 < R / z.im + 1

Tactic:
have h₀ : 0 < R / im z + 1 := one_pos.trans h₁
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / z.im + 1
h₀ : 0 < R / z.im + 1
⊢ ∃ (i : ℝ), 0 < i ∧ ball z i ⊆ UpperHalfPlane.coe ⁻¹' ball (↑z : ℂ) R

Tactic:
⟨log (R / im z + 1), Real.log_pos h₁, ?_⟩

Premises used: HDiv.hDiv, Real.log_pos, Real.log, UpperHalfPlane.im, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / z.im + 1
h₀ : 0 < R / z.im + 1
refine_2 : ball z (log (R / z.im + 1)) ⊆ UpperHalfPlane.coe ⁻¹' ball (↑z : ℂ) R
⊢ ∃ (i : ℝ), 0 < i ∧ ball z i ⊆ UpperHalfPlane.coe ⁻¹' ball (↑z : ℂ) R

Tactic:
refine ⟨log (R / im z + 1), Real.log_pos h₁, ?_⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / z.im + 1
h₀ : 0 < R / z.im + 1
⊢ ball z (log (R / z.im + 1)) ⊆ UpperHalfPlane.coe ⁻¹' ball (↑z : ℂ) R

Tactic:
fun w hw => (dist_coe_le w z).trans_lt ?_

Premises used: Set.Mem, setOf, Metric.ball, Set.Subset, Set.preimage, UpperHalfPlane.dist_coe_le, LE.le.trans_lt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / z.im + 1
h₀ : 0 < R / z.im + 1
refine_2 : ∀ (w : ℍ) (hw : w ∈ ball z (log (R / z.im + 1))), z.im * (rexp (dist w z) - 1) < R
⊢ ball z (log (R / z.im + 1)) ⊆ UpperHalfPlane.coe ⁻¹' ball (↑z : ℂ) R

Tactic:
refine fun w hw => (dist_coe_le w z).trans_lt ?_

Premises used: UpperHalfPlane.dist_coe_le, LE.le.trans_lt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w_1 : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / z.im + 1
h₀ : 0 < R / z.im + 1
w : ℍ
hw : w ∈ ball z (log (R / z.im + 1))
refine_2 : rexp (dist w z) - 1 < R / z.im
refine_2₁ : rexp (dist w z) < R / z.im + 1
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : dist w z < log (R / z.im + 1)
⊢ z.im * (rexp (dist w z) - 1) < R

Tactic:
rwa [← lt_div_iff₀' z.im_pos, sub_lt_iff_lt_add, ← Real.lt_log_iff_exp_lt h₀]

Premises used: UpperHalfPlane.im_pos, lt_div_iff₀', Real.lt_log_iff_exp_lt, sub_lt_iff_lt_add
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℂ
h rwa rwa₁ rwa₂ rwa₃ : dist w (↑(z.center r) : ℂ) ≤ z.im * Real.sinh r
⊢ dist (↑(z.center r) : ℂ) w ≤ z.im * Real.sinh r

Tactic:
rwa [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
h : ∀ (w : ℂ), w ∈ UpperHalfPlane.coe '' closedBall z r ↔ w ∈ closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r)
⊢ UpperHalfPlane.coe '' closedBall z r = closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r)

Tactic:
ext w
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℂ
h : w ∈ UpperHalfPlane.coe '' closedBall z r → w ∈ closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r)
h₁ : w ∈ closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' closedBall z r
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r ↔ w ∈ closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r)

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ closedBall z r
⊢ (↑w : ℂ) ∈ closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r)

Tactic:
dist_le_iff_dist_coe_center_le.1 hw

Premises used: UpperHalfPlane.dist_le_iff_dist_coe_center_le, Set.Mem, setOf, Iff.mp, Metric.closedBall
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ closedBall z r
⊢ (↑w : ℂ) ∈ closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r)

Tactic:
exact dist_le_iff_dist_coe_center_le.1 hw

Premises used: UpperHalfPlane.dist_le_iff_dist_coe_center_le, Iff.mp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r)
⊢ 0 < w.im

Tactic:
im_pos_of_dist_center_le hw

Premises used: UpperHalfPlane.im_pos_of_dist_center_le
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r)
h :
  ∀ (w : ℍ) (hw : (↑w : ℂ) ∈ closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r)),
    (↑w : ℂ) ∈ UpperHalfPlane.coe '' closedBall z r
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r

Tactic:
lift w to ℍ using im_pos_of_dist_center_le hw

Premises used: UpperHalfPlane.im_pos_of_dist_center_le
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℍ
hw : (↑w : ℂ) ∈ closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r)
⊢ (↑w : ℂ) ∈ UpperHalfPlane.coe '' closedBall z r

Tactic:
mem_image_of_mem _ (dist_le_iff_dist_coe_center_le.2 hw)

Premises used: Iff.mpr, UpperHalfPlane.dist_le_iff_dist_coe_center_le, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℍ
hw : (↑w : ℂ) ∈ closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r)
⊢ (↑w : ℂ) ∈ UpperHalfPlane.coe '' closedBall z r

Tactic:
exact mem_image_of_mem _ (dist_le_iff_dist_coe_center_le.2 hw)

Premises used: Iff.mpr, UpperHalfPlane.dist_le_iff_dist_coe_center_le, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
h : ∀ (w : ℂ), w ∈ UpperHalfPlane.coe '' ball z r ↔ w ∈ ball (↑(z.center r) : ℂ) (z.im * Real.sinh r)
⊢ UpperHalfPlane.coe '' ball z r = ball (↑(z.center r) : ℂ) (z.im * Real.sinh r)

Tactic:
ext w
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℂ
h : w ∈ UpperHalfPlane.coe '' ball z r → w ∈ ball (↑(z.center r) : ℂ) (z.im * Real.sinh r)
h₁ : w ∈ ball (↑(z.center r) : ℂ) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' ball z r
⊢ w ∈ UpperHalfPlane.coe '' ball z r ↔ w ∈ ball (↑(z.center r) : ℂ) (z.im * Real.sinh r)

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ ball z r
⊢ (↑w : ℂ) ∈ ball (↑(z.center r) : ℂ) (z.im * Real.sinh r)

Tactic:
dist_lt_iff_dist_coe_center_lt.1 hw

Premises used: Set.Mem, setOf, UpperHalfPlane.dist_lt_iff_dist_coe_center_lt, Metric.ball, Iff.mp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ ball z r
⊢ (↑w : ℂ) ∈ ball (↑(z.center r) : ℂ) (z.im * Real.sinh r)

Tactic:
exact dist_lt_iff_dist_coe_center_lt.1 hw

Premises used: UpperHalfPlane.dist_lt_iff_dist_coe_center_lt, Iff.mp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ ball (↑(z.center r) : ℂ) (z.im * Real.sinh r)
⊢ 0 < w.im

Tactic:
im_pos_of_dist_center_le (ball_subset_closedBall hw)

Premises used: Metric.ball_subset_closedBall, UpperHalfPlane.im_pos_of_dist_center_le
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ ball (↑(z.center r) : ℂ) (z.im * Real.sinh r)
h : ∀ (w : ℍ) (hw : (↑w : ℂ) ∈ ball (↑(z.center r) : ℂ) (z.im * Real.sinh r)), (↑w : ℂ) ∈ UpperHalfPlane.coe '' ball z r
⊢ w ∈ UpperHalfPlane.coe '' ball z r

Tactic:
lift w to ℍ using im_pos_of_dist_center_le (ball_subset_closedBall hw)

Premises used: Metric.ball_subset_closedBall, UpperHalfPlane.im_pos_of_dist_center_le
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℍ
hw : (↑w : ℂ) ∈ ball (↑(z.center r) : ℂ) (z.im * Real.sinh r)
⊢ (↑w : ℂ) ∈ UpperHalfPlane.coe '' ball z r

Tactic:
mem_image_of_mem _ (dist_lt_iff_dist_coe_center_lt.2 hw)

Premises used: Iff.mpr, UpperHalfPlane.dist_lt_iff_dist_coe_center_lt, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℍ
hw : (↑w : ℂ) ∈ ball (↑(z.center r) : ℂ) (z.im * Real.sinh r)
⊢ (↑w : ℂ) ∈ UpperHalfPlane.coe '' ball z r

Tactic:
exact mem_image_of_mem _ (dist_lt_iff_dist_coe_center_lt.2 hw)

Premises used: Iff.mpr, UpperHalfPlane.dist_lt_iff_dist_coe_center_lt, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
h : ∀ (w : ℂ), w ∈ UpperHalfPlane.coe '' sphere z r ↔ w ∈ sphere (↑(z.center r) : ℂ) (z.im * Real.sinh r)
⊢ UpperHalfPlane.coe '' sphere z r = sphere (↑(z.center r) : ℂ) (z.im * Real.sinh r)

Tactic:
ext w
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℂ
h : w ∈ UpperHalfPlane.coe '' sphere z r → w ∈ sphere (↑(z.center r) : ℂ) (z.im * Real.sinh r)
h₁ : w ∈ sphere (↑(z.center r) : ℂ) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' sphere z r
⊢ w ∈ UpperHalfPlane.coe '' sphere z r ↔ w ∈ sphere (↑(z.center r) : ℂ) (z.im * Real.sinh r)

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ sphere z r
⊢ (↑w : ℂ) ∈ sphere (↑(z.center r) : ℂ) (z.im * Real.sinh r)

Tactic:
dist_eq_iff_dist_coe_center_eq.1 hw

Premises used: Set.Mem, setOf, UpperHalfPlane.dist_eq_iff_dist_coe_center_eq, Iff.mp, Metric.sphere
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ sphere z r
⊢ (↑w : ℂ) ∈ sphere (↑(z.center r) : ℂ) (z.im * Real.sinh r)

Tactic:
exact dist_eq_iff_dist_coe_center_eq.1 hw

Premises used: UpperHalfPlane.dist_eq_iff_dist_coe_center_eq, Iff.mp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ sphere (↑(z.center r) : ℂ) (z.im * Real.sinh r)
⊢ 0 < w.im

Tactic:
im_pos_of_dist_center_le (sphere_subset_closedBall hw)

Premises used: UpperHalfPlane.im_pos_of_dist_center_le, Metric.sphere_subset_closedBall
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ sphere (↑(z.center r) : ℂ) (z.im * Real.sinh r)
h :
  ∀ (w : ℍ) (hw : (↑w : ℂ) ∈ sphere (↑(z.center r) : ℂ) (z.im * Real.sinh r)),
    (↑w : ℂ) ∈ UpperHalfPlane.coe '' sphere z r
⊢ w ∈ UpperHalfPlane.coe '' sphere z r

Tactic:
lift w to ℍ using im_pos_of_dist_center_le (sphere_subset_closedBall hw)

Premises used: UpperHalfPlane.im_pos_of_dist_center_le, Metric.sphere_subset_closedBall
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℍ
hw : (↑w : ℂ) ∈ sphere (↑(z.center r) : ℂ) (z.im * Real.sinh r)
⊢ (↑w : ℂ) ∈ UpperHalfPlane.coe '' sphere z r

Tactic:
mem_image_of_mem _ (dist_eq_iff_dist_coe_center_eq.2 hw)

Premises used: Iff.mpr, UpperHalfPlane.dist_eq_iff_dist_coe_center_eq, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
w : ℍ
hw : (↑w : ℂ) ∈ sphere (↑(z.center r) : ℂ) (z.im * Real.sinh r)
⊢ (↑w : ℂ) ∈ UpperHalfPlane.coe '' sphere z r

Tactic:
exact mem_image_of_mem _ (dist_eq_iff_dist_coe_center_eq.2 hw)

Premises used: Iff.mpr, UpperHalfPlane.dist_eq_iff_dist_coe_center_eq, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
⊢ ProperSpace ℍ

Tactic:
⟨fun z r => ?_⟩

Premises used: ProperSpace.mk
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
refine : ∀ (z : ℍ) (r : ℝ), IsCompact (closedBall z r)
⊢ ProperSpace ℍ

Tactic:
refine ⟨fun z r => ?_⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w : ℍ
r_1 : ℝ
z : ℍ
r : ℝ
rw : IsCompact (closedBall (↑(z.center r) : ℂ) (z.im * Real.sinh r))
⊢ IsCompact (closedBall z r)

Tactic:
rw [isEmbedding_coe.isCompact_iff (f := ((↑) : ℍ → ℂ)), image_coe_closedBall]

Premises used: UpperHalfPlane.image_coe_closedBall, Topology.IsEmbedding.isCompact_iff, UpperHalfPlane.isEmbedding_coe