awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
simp :
  dist (↑a : ℂ) (↑b : ℂ) * dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑c : ℂ)) /
        (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) +
      dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) * dist (↑b : ℂ) (↑c : ℂ) /
        (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) =
    (dist (↑a : ℂ) (↑b : ℂ) * dist (↑c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) +
        dist (↑b : ℂ) (↑c : ℂ) * dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ))) /
      (2 * √(a.im * c.im) * dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)))
⊢ sinh ((dist a b + dist b c) / 2) =
    (dist (↑a : ℂ) (↑b : ℂ) * dist (↑c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) +
        dist (↑b : ℂ) (↑c : ℂ) * dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ))) /
      (2 * √(a.im * c.im) * dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)))

Tactic:
simp only [add_div _ _ (2 : ℝ), sinh_add, sinh_half_dist, cosh_half_dist, div_mul_div_comm]

Premises used: Real.sinh_add, div_mul_div_comm, UpperHalfPlane.cosh_half_dist, UpperHalfPlane.sinh_half_dist, OfNat.ofNat, add_div
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
rw :
  (dist (↑a : ℂ) (↑b : ℂ) * dist (↑c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) +
        dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) * dist (↑b : ℂ) (↑c : ℂ)) /
      (HMul.hMul (α := ℝ) 2 2 * (√(a.im * b.im) * √(b.im * c.im))) =
    (dist (↑a : ℂ) (↑b : ℂ) * dist (↑c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) +
        dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) * dist (↑b : ℂ) (↑c : ℂ)) /
      (HMul.hMul (α := ℝ) 2 2 * (√(a.im * c.im) * b.im))
⊢ dist (↑a : ℂ) (↑b : ℂ) * dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑c : ℂ)) /
        (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) +
      dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) * dist (↑b : ℂ) (↑c : ℂ) /
        (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) =
    (dist (↑a : ℂ) (↑b : ℂ) * dist (↑c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) +
        dist (↑b : ℂ) (↑c : ℂ) * dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ))) /
      (2 * √(a.im * c.im) * dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)))

Tactic:
rw [← add_div, Complex.dist_self_conj, coe_im, abs_of_pos b.im_pos, mul_comm (dist (b : ℂ) _),
    dist_comm (b : ℂ), Complex.dist_conj_comm, mul_mul_mul_comm, mul_mul_mul_comm _ _ _ b.im]

Premises used: UpperHalfPlane.im_pos, mul_mul_mul_comm, UpperHalfPlane.coe, Complex.dist_self_conj, dist_comm, UpperHalfPlane.im, mul_comm, Complex.dist_conj_comm, Dist.dist, abs_of_pos, UpperHalfPlane.coe_im, add_div
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
e_a : √(a.im * b.im) * √(b.im * c.im) = √(a.im * c.im) * b.im
⊢ (dist (↑a : ℂ) (↑b : ℂ) * dist (↑c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) +
        dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) * dist (↑b : ℂ) (↑c : ℂ)) /
      (HMul.hMul (α := ℝ) 2 2 * (√(a.im * b.im) * √(b.im * c.im))) =
    (dist (↑a : ℂ) (↑b : ℂ) * dist (↑c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) +
        dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) * dist (↑b : ℂ) (↑c : ℂ)) /
      (HMul.hMul (α := ℝ) 2 2 * (√(a.im * c.im) * b.im))

Tactic:
congr 2
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
e_a : 0 ≤ b.im
e_a₁ : 0 ≤ a.im
e_a₂ : 0 ≤ b.im
e_a₃ : 0 ≤ a.im
⊢ √(a.im * b.im) * √(b.im * c.im) = √(a.im * c.im) * b.im

Tactic:
rw [sqrt_mul, sqrt_mul, sqrt_mul, mul_comm (√a.im), mul_mul_mul_comm, mul_self_sqrt,
      mul_comm]

Premises used: mul_mul_mul_comm, Real.mul_self_sqrt, Real.sqrt_mul, UpperHalfPlane.im, mul_comm, Real.sqrt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
⊢ 0 ≤ b.im

Tactic:
(im_pos _).le

Premises used: UpperHalfPlane.im_pos, LT.lt.le
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
⊢ 0 ≤ b.im

Tactic:
exact (im_pos _).le

Premises used: UpperHalfPlane.im_pos, LT.lt.le
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
⊢ 0 ≤ a.im

Tactic:
(im_pos _).le

Premises used: UpperHalfPlane.im_pos, LT.lt.le
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
⊢ 0 ≤ a.im

Tactic:
exact (im_pos _).le

Premises used: UpperHalfPlane.im_pos, LT.lt.le
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ dist z w = dist w z

Tactic:
simp only [dist_eq, dist_comm (z : ℂ), mul_comm]

Premises used: UpperHalfPlane.coe, dist_comm, UpperHalfPlane.dist_eq, mul_comm
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
rw : dist z w / 2 ≤ r / 2 ↔ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) ≤ sinh (r / 2)
rw₁ : sinh (dist z w / 2) ≤ sinh (r / 2) ↔ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) ≤ sinh (r / 2)
rw₂ rw₃ :
  dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) ≤ sinh (r / 2) ↔
    dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) ≤ sinh (r / 2)
⊢ dist z w ≤ r ↔ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) ≤ sinh (r / 2)

Tactic:
rw [← div_le_div_iff_of_pos_right (zero_lt_two' ℝ), ← sinh_le_sinh, sinh_half_dist]

Premises used: Real, div_le_div_iff_of_pos_right, zero_lt_two', UpperHalfPlane.sinh_half_dist, Real.sinh_le_sinh
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
rw : dist z w / 2 = r / 2 ↔ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = sinh (r / 2)
rw₁ : sinh (dist z w / 2) = sinh (r / 2) ↔ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = sinh (r / 2)
rw₂ rw₃ :
  dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = sinh (r / 2) ↔
    dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = sinh (r / 2)
⊢ dist z w = r ↔ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = sinh (r / 2)

Tactic:
rw [← div_left_inj' (two_ne_zero' ℝ), ← sinh_inj, sinh_half_dist]

Premises used: Real, Real.sinh_inj, two_ne_zero', UpperHalfPlane.sinh_half_dist, div_left_inj'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
hr : 0 ≤ r
rw :
  HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 / (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im)) =
      HPow.hPow (β := ℕ) (sinh (r / 2)) 2 ↔
    HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 / (4 * (z.im * w.im)) = HPow.hPow (β := ℕ) (sinh (r / 2)) 2
rw₁ : 0 ≤ z.im * w.im
ha : 0 ≤ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
hb : 0 ≤ sinh (r / 2)
⊢ dist z w = r ↔ HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 / (4 * z.im * w.im) = HPow.hPow (β := ℕ) (sinh (r / 2)) 2

Tactic:
rw [dist_eq_iff_eq_sinh, ← sq_eq_sq₀, div_pow, mul_pow, sq_sqrt, mul_assoc]

Premises used: UpperHalfPlane.dist_eq_iff_eq_sinh, mul_assoc, Real.sq_sqrt, div_pow, sq_eq_sq₀, mul_pow
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 / (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im)) =
      HPow.hPow (β := ℕ) (sinh (r / 2)) 2 ↔
    HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 / (4 * (z.im * w.im)) = HPow.hPow (β := ℕ) (sinh (r / 2)) 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ z.im * w.im

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ sinh (r / 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
rw :
  dist (↑a : ℂ) (↑c : ℂ) * dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) / (2 * √(a.im * c.im)) ≤
    (dist (↑a : ℂ) (↑b : ℂ) * dist (↑c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) +
        dist (↑b : ℂ) (↑c : ℂ) * dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ))) /
      (2 * √(a.im * c.im))
rw₁ : 0 < dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ))
⊢ dist a c ≤ dist a b + dist b c

Tactic:
rw [dist_le_iff_le_sinh, sinh_half_dist_add_dist, div_mul_eq_div_div _ _ (dist _ _), le_div_iff₀,
    div_mul_eq_mul_div]

Premises used: div_mul_eq_mul_div, UpperHalfPlane.sinh_half_dist_add_dist, Dist.dist, UpperHalfPlane.dist_le_iff_le_sinh, div_mul_eq_div_div, le_div_iff₀
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
hab :
  dist (↑a : ℂ) (↑c : ℂ) * dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) ≤
    dist (↑a : ℂ) (↑b : ℂ) * dist (↑c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) +
      dist (↑b : ℂ) (↑c : ℂ) * dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ))
⊢ dist (↑a : ℂ) (↑c : ℂ) * dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) / (2 * √(a.im * c.im)) ≤
    (dist (↑a : ℂ) (↑b : ℂ) * dist (↑c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) +
        dist (↑b : ℂ) (↑c : ℂ) * dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ))) /
      (2 * √(a.im * c.im))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
⊢ dist (↑a : ℂ) (↑c : ℂ) * dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) ≤
    dist (↑a : ℂ) (↑b : ℂ) * dist (↑c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) +
      dist (↑b : ℂ) (↑c : ℂ) * dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ))

Tactic:
EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist (a : ℂ) b c (conj (b : ℂ))

Premises used: UpperHalfPlane.coe, EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
⊢ dist (↑a : ℂ) (↑c : ℂ) * dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) ≤
    dist (↑a : ℂ) (↑b : ℂ) * dist (↑c : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ)) +
      dist (↑b : ℂ) (↑c : ℂ) * dist (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ))

Tactic:
exact EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist (a : ℂ) b c (conj (b : ℂ))

Premises used: UpperHalfPlane.coe, EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
rw : ¬(↑b : ℂ).im = 0
⊢ 0 < dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ))

Tactic:
rw [dist_comm, dist_pos, Ne, Complex.conj_eq_iff_im]

Premises used: Ne, dist_comm, dist_pos, Complex.conj_eq_iff_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
⊢ ¬(↑b : ℂ).im = 0

Tactic:
b.im_ne_zero

Premises used: UpperHalfPlane.im_ne_zero, UpperHalfPlane.im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a b c : ℍ
⊢ ¬(↑b : ℂ).im = 0

Tactic:
exact b.im_ne_zero

Premises used: UpperHalfPlane.im_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
rw : 0 ≤ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
⊢ dist z w ≤ dist (↑z : ℂ) (↑w : ℂ) / √(z.im * w.im)

Tactic:
rw [dist_le_iff_le_sinh, ← div_mul_eq_div_div_swap, self_le_sinh_iff]

Premises used: div_mul_eq_div_div_swap, Real.self_le_sinh_iff, UpperHalfPlane.dist_le_iff_le_sinh
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ 0 ≤ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w : ℍ
r : ℝ
z : ℍ
rw : 2 * arsinh (dist (↑z : ℂ) (↑z : ℂ) / (2 * √(z.im * z.im))) = 0
rw₁ : 2 * arsinh (0 / (2 * √(z.im * z.im))) = 0
rw₂ : 2 * arsinh 0 = 0
rw₃ : HMul.hMul (α := ℝ) 2 0 = 0
rw₄ rw₅ : Eq (α := ℝ) 0 0
⊢ dist z z = 0

Tactic:
rw [dist_eq, dist_self, zero_div, arsinh_zero, mul_zero]

Premises used: Real.arsinh_zero, zero_div, UpperHalfPlane.dist_eq, MulZeroClass.mul_zero, dist_self
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w_1 : ℍ
r : ℝ
z w : ℍ
h : dist z w = 0
⊢ z = w

Tactic:
simpa [dist_eq, Real.sqrt_eq_zero', (mul_pos z.im_pos w.im_pos).not_ge, Set.ext_iff] using h

Premises used: UpperHalfPlane.im_pos, UpperHalfPlane.dist_eq, mul_pos, Set.ext_iff, LT.lt.not_ge, Real.sqrt_eq_zero'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
simp :
  z.im * w.im * 2 + (HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) =
    HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) z.im 2 + HPow.hPow (β := ℕ) w.im 2
⊢ Real.cosh (dist z w) =
    (HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) z.im 2 + HPow.hPow (β := ℕ) w.im 2) / (2 * z.im * w.im)

Tactic:
simp [field, cosh_dist, Complex.dist_eq, Complex.sq_norm, normSq_apply]

Premises used: Complex.sq_norm, UpperHalfPlane.cosh_dist, Complex.dist_eq, Complex.normSq_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ z.im * w.im * 2 + (HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) (z.im - w.im) 2) =
    HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) z.im 2 + HPow.hPow (β := ℕ) w.im 2

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z_1 w : ℍ
r_1 : ℝ
z : ℍ
r : ℝ
⊢ 0 < { re := z.re, im := z.im * Real.cosh r : ℂ }.im

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
⊢ (z.center r).re = z.re

Tactic:
rfl

Premises used: UpperHalfPlane.center, UpperHalfPlane.re, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
⊢ (z.center r).im = z.im * Real.cosh r

Tactic:
rfl

Premises used: UpperHalfPlane.im, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
hre : (z.center 0).re = z.re
him : (z.center 0).im = z.im
⊢ z.center 0 = z

Tactic:
apply ext_re_im

Premises used: UpperHalfPlane.ext_re_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
⊢ (z.center 0).re = z.re

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
⊢ (z.center 0).im = z.im

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
⊢ 2 * z.im * w.im ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
⊢ 2 * z.im * w.im ≠ 0

Tactic:
have H : 2 * z.im * w.im ≠ 0 := by positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
H : 2 * z.im * w.im ≠ 0
simp :
  HPow.hPow (β := ℕ) (z.re - w.re) 2 +
      (HPow.hPow (β := ℕ) z.im 2 - 2 * z.im * (w.im * Real.cosh r) +
        HPow.hPow (β := ℕ) w.im 2 * (HPow.hPow (β := ℕ) (Real.sinh r) 2 + 1)) =
    HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) z.im 2 + HPow.hPow (β := ℕ) w.im 2 -
        2 * z.im * w.im * Real.cosh r +
      HPow.hPow (β := ℕ) w.im 2 * HPow.hPow (β := ℕ) (Real.sinh r) 2
⊢ HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑(w.center r) : ℂ)) 2 =
    2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2

Tactic:
simp only [Complex.dist_eq, Complex.sq_norm, normSq_apply, coe_re, coe_im, center_re, center_im,
    cosh_dist', mul_div_cancel₀ _ H, sub_sq z.im, mul_pow, Real.cosh_sq, sub_re, sub_im, mul_sub, ←
    sq]

Premises used: sub_sq, mul_sub, UpperHalfPlane.center_re, Complex.sub_im, Complex.sub_re, Complex.sq_norm, UpperHalfPlane.center_im, Real.cosh_sq, sq, mul_div_cancel₀, Complex.dist_eq, UpperHalfPlane.im, UpperHalfPlane.coe_re, Complex.normSq_apply, UpperHalfPlane.cosh_dist', mul_pow, UpperHalfPlane.coe_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
H : 2 * z.im * w.im ≠ 0
⊢ HPow.hPow (β := ℕ) (z.re - w.re) 2 +
      (HPow.hPow (β := ℕ) z.im 2 - 2 * z.im * (w.im * Real.cosh r) +
        HPow.hPow (β := ℕ) w.im 2 * (HPow.hPow (β := ℕ) (Real.sinh r) 2 + 1)) =
    HPow.hPow (β := ℕ) (z.re - w.re) 2 + HPow.hPow (β := ℕ) z.im 2 + HPow.hPow (β := ℕ) w.im 2 -
        2 * z.im * w.im * Real.cosh r +
      HPow.hPow (β := ℕ) w.im 2 * HPow.hPow (β := ℕ) (Real.sinh r) 2

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
rw :
  √(HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑(w.center r) : ℂ)) 2) =
    √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
rw₁ rw₂ :
  √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2) =
    √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
⊢ dist (↑z : ℂ) (↑(w.center r) : ℂ) =
    √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)

Tactic:
rw [← sqrt_sq dist_nonneg, dist_coe_center_sq]

Premises used: dist_nonneg, Real.sqrt_sq, UpperHalfPlane.dist_coe_center_sq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
inl : ∀ (hr₀ : r < 0), cmp (dist z w) r = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)
inr : ∀ (hr₀ : 0 ≤ r), cmp (dist z w) r = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)
⊢ cmp (dist z w) r = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)

Tactic:
rcases lt_or_ge r 0 with hr₀ | hr₀

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : r < 0
trans : cmp (dist z w) r = Ordering.gt
trans₁ : Ordering.gt = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)
⊢ cmp (dist z w) r = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)

Tactic:
trans Ordering.gt

Premises used: Ordering.gt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : r < 0
⊢ cmp (dist z w) r = Ordering.gt

Tactic:
(hr₀.trans_le dist_nonneg).cmp_eq_gt

Premises used: dist_nonneg, LT.lt.cmp_eq_gt, LT.lt.trans_le
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : r < 0
⊢ Ordering.gt = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)

Tactic:
((mul_neg_of_pos_of_neg w.im_pos (sinh_neg_iff.2 hr₀)).trans_le dist_nonneg).cmp_eq_gt.symm

Premises used: Iff.mpr, UpperHalfPlane.im_pos, dist_nonneg, LT.lt.cmp_eq_gt, LT.lt.trans_le, Real.sinh_neg_iff, Eq.symm, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : r < 0
⊢ cmp (dist z w) r = Ordering.gt

Tactic:
exacts [(hr₀.trans_le dist_nonneg).cmp_eq_gt,
      ((mul_neg_of_pos_of_neg w.im_pos (sinh_neg_iff.2 hr₀)).trans_le dist_nonneg).cmp_eq_gt.symm]

Premises used: Iff.mpr, UpperHalfPlane.im_pos, dist_nonneg, LT.lt.cmp_eq_gt, LT.lt.trans_le, Real.sinh_neg_iff, Eq.symm, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
⊢ 0 ≤ w.im * Real.sinh r

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
⊢ 0 ≤ w.im * Real.sinh r

Tactic:
have hr₀' : 0 ≤ w.im * Real.sinh r := by positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
⊢ 0 < 2 * z.im * w.im

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
⊢ 0 < 2 * z.im * w.im

Tactic:
have hzw₀ : 0 < 2 * z.im * w.im := by positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
inr :
  cmp (Real.cosh (dist z w)) (Real.cosh r) =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
      (HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
⊢ cmp (dist z w) r = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)

Tactic:
simp only [← cosh_strictMonoOn.cmp_map_eq dist_nonneg hr₀,
    ← (pow_left_strictMonoOn₀ (M₀ := ℝ) two_ne_zero).cmp_map_eq dist_nonneg hr₀',
    dist_coe_center_sq]

Premises used: dist_nonneg, two_ne_zero, StrictMonoOn.cmp_map_eq, Real.cosh_strictMonoOn, pow_left_strictMonoOn₀, UpperHalfPlane.dist_coe_center_sq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
inr :
  cmp (2 * z.im * w.im * Real.cosh (dist z w)) (2 * z.im * w.im * Real.cosh r) =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
      (HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
inr₁ :
  cmp (2 * z.im * w.im * Real.cosh (dist z w) - 2 * z.im * w.im * Real.cosh r) 0 =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
      (HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
inr₂ :
  cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r)) 0 =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
      (HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
inr₃ :
  cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
      (0 + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2) =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
      (HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
inr₄ : ℝ
inr₅ :
  cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
      (HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2) =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
      (HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
inr₆ : ℝ
inr₇ :
  cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
      (HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2) =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
      (HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
inr₈ : ℝ
⊢ cmp (Real.cosh (dist z w)) (Real.cosh r) =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)
      (HPow.hPow (β := ℕ) (w.im * Real.sinh r) 2)

Tactic:
rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add]

Premises used: mul_sub, cmp_mul_pos_left, zero_add, cmp_sub_zero, cmp_add_right
-- 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:
eq_iff_eq_of_cmp_eq_cmp (cmp_dist_eq_cmp_dist_coe_center z w r)

Premises used: eq_iff_eq_of_cmp_eq_cmp, UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
rw : |(↑(z.center r) : ℂ).im - (↑z : ℂ).im| = z.im * Real.cosh r - z.im
⊢ dist (↑z : ℂ) (↑(z.center r) : ℂ) = z.im * (Real.cosh r - 1)

Tactic:
rw [dist_of_re_eq (z.center_re r).symm, dist_comm, Real.dist_eq, mul_sub, mul_one]

Premises used: mul_sub, UpperHalfPlane.center_re, dist_comm, Real.dist_eq, mul_one, Eq.symm, Complex.dist_of_re_eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
⊢ |(↑(z.center r) : ℂ).im - (↑z : ℂ).im| = z.im * Real.cosh r - z.im

Tactic:
abs_of_nonneg (sub_nonneg.2 <| le_mul_of_one_le_right z.im_pos.le (one_le_cosh _))

Premises used: Iff.mpr, Real.one_le_cosh, UpperHalfPlane.im_pos, LT.lt.le, UpperHalfPlane.im, le_mul_of_one_le_right, abs_of_nonneg, sub_nonneg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z : ℍ
r : ℝ
⊢ |(↑(z.center r) : ℂ).im - (↑z : ℂ).im| = z.im * Real.cosh r - z.im

Tactic:
exact abs_of_nonneg (sub_nonneg.2 <| le_mul_of_one_le_right z.im_pos.le (one_le_cosh _))

Premises used: Iff.mpr, Real.one_le_cosh, UpperHalfPlane.im_pos, LT.lt.le, le_mul_of_one_le_right, abs_of_nonneg, sub_nonneg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ dist (↑z : ℂ) (↑(w.center (dist z w)) : ℂ) = w.im * Real.sinh (dist z w)

Tactic:
dist_eq_iff_dist_coe_center_eq.1 rfl

Premises used: UpperHalfPlane.dist_eq_iff_dist_coe_center_eq, Iff.mp, rfl