awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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
⊢ dist z z = 0
have rw₃ : HMul.hMul (α := ℝ) 2 0 = 0
Tactic: rw [dist_eq, dist_self, zero_div, arsinh_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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
⊢ dist z z = 0
have rw₄ : Eq (α := ℝ) 0 0
Tactic: rw [dist_eq, dist_self, zero_div, arsinh_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ 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)
have 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
Tactic: simp [field, cosh_dist, Complex.dist_eq, Complex.sq_norm, normSq_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z : ℍ
⊢ z.center 0 = z
have hre : (z.center 0).re = z.re
Tactic: apply ext_re_im
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z : ℍ
hre : (z.center 0).re = z.re
⊢ z.center 0 = z
have him : (z.center 0).im = z.im
Tactic: apply ext_re_im
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (hypothesis)
Goal:
z w : ℍ
r : ℝ
⊢ 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
have H : 2 * z.im * w.im ≠ 0
Tactic: have H : 2 * z.im * w.im ≠ 0 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
H : 2 * z.im * w.im ≠ 0
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
⊢ 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)
have 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)
Tactic: rw [← sqrt_sq dist_nonneg, dist_coe_center_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← sqrt_sq dist_nonneg, dist_coe_center_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
⊢ cmp (dist z w) r = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)
have inl : ∀ (hr₀ : r < 0), 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₀
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)
⊢ cmp (dist z w) r = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)
have inr : ∀ (hr₀ : 0 ≤ 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₀
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : r < 0
⊢ cmp (dist z w) r = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)
have trans : cmp (dist z w) r = Ordering.gt
Tactic: trans Ordering.gt
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : r < 0
trans : cmp (dist z w) r = Ordering.gt
⊢ cmp (dist z w) r = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)
have trans₁ : Ordering.gt = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)
Tactic: trans Ordering.gt
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (hypothesis)
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
⊢ cmp (dist z w) r = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)
have hr₀' : 0 ≤ w.im * Real.sinh r
Tactic: have hr₀' : 0 ≤ w.im * Real.sinh r := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (hypothesis)
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
⊢ cmp (dist z w) r = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)
have hzw₀ : 0 < 2 * z.im * w.im
Tactic: have hzw₀ : 0 < 2 * z.im * w.im := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
⊢ cmp (dist z w) r = cmp (dist (↑z : ℂ) (↑(w.center r) : ℂ)) (w.im * Real.sinh r)
have 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: 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
⊢ 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)
have 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)
Tactic: rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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₄ : ℝ
⊢ 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)
have 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)
Tactic: rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z : ℍ
r : ℝ
⊢ dist (↑z : ℂ) (↑(z.center r) : ℂ) = z.im * (Real.cosh r - 1)
have rw : |(↑(z.center r) : ℂ).im - (↑z : ℂ).im| = z.im * Real.cosh r - z.im
Tactic: rw [dist_of_re_eq (z.center_re r).symm, dist_comm, Real.dist_eq, mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (hypothesis)
Goal:
z w : ℍ
h : z.re = w.re
⊢ dist z w = dist (log z.im) (log w.im)
have h₀ : 0 < z.im / w.im
Tactic: have h₀ : 0 < z.im / w.im := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z w = dist (log z.im) (log w.im)
have 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|
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)
have rw₁ : (↑z : ℂ).re = (↑(w.center |log (z.im / w.im)|) : ℂ).re
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z w = dist (log z.im) (log w.im)
have 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|
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ 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|
have 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|
Tactic: nth_rw 4 [← abs_of_pos w.im_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ 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|
have 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)|
Tactic: simp only [← _root_.abs_mul, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)|
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ 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)))
have 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)))
Tactic: dsimp only [coe_mk, mk_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
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)))
have hbc : dist { re := 0, im := z.im : ℂ } { re := 0, im := w.im : ℂ } ≤ dist (↑z : ℂ) (↑w : ℂ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ z.im ≤ w.im * rexp (dist z w)
have rw : log z.im - log w.im ≤ 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ dist (↑z : ℂ) (↑(w.center (dist z w)) : ℂ) + dist (↑w : ℂ) (↑(w.center (dist z w)) : ℂ) = w.im * (rexp (dist z w) - 1)
have rw : w.im * Real.sinh (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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)
⊢ dist (↑z : ℂ) (↑(w.center (dist z w)) : ℂ) + dist (↑w : ℂ) (↑(w.center (dist z w)) : ℂ) = w.im * (rexp (dist z w) - 1)
have rw₁ : w.im * Real.sinh (dist z w) + w.im * (Real.cosh (dist z w) - 1) = w.im * (rexp (dist z w) - 1)
Tactic: rw [dist_center_dist, dist_self_center, ← mul_add, ← add_sub_assoc, Real.sinh_add_cosh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)
⊢ dist (↑z : ℂ) (↑(w.center (dist z w)) : ℂ) + dist (↑w : ℂ) (↑(w.center (dist z w)) : ℂ) = w.im * (rexp (dist z w) - 1)
have rw₂ : w.im * (Real.sinh (dist z w) + (Real.cosh (dist z w) - 1)) = w.im * (rexp (dist z w) - 1)
Tactic: rw [dist_center_dist, dist_self_center, ← mul_add, ← add_sub_assoc, Real.sinh_add_cosh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)
⊢ dist (↑z : ℂ) (↑(w.center (dist z w)) : ℂ) + dist (↑w : ℂ) (↑(w.center (dist z w)) : ℂ) = w.im * (rexp (dist z w) - 1)
have rw₃ : w.im * (Real.sinh (dist z w) + Real.cosh (dist z w) - 1) = w.im * (rexp (dist z w) - 1)
Tactic: rw [dist_center_dist, dist_self_center, ← mul_add, ← add_sub_assoc, Real.sinh_add_cosh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)
⊢ dist (↑z : ℂ) (↑(w.center (dist z w)) : ℂ) + dist (↑w : ℂ) (↑(w.center (dist z w)) : ℂ) = w.im * (rexp (dist z w) - 1)
have rw₄ : w.im * (rexp (dist z w) - 1) = w.im * (rexp (dist z w) - 1)
Tactic: rw [dist_center_dist, dist_self_center, ← mul_add, ← add_sub_assoc, Real.sinh_add_cosh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ w.im * (1 - rexp (-dist z w)) =
    dist (↑z : ℂ) (↑(w.center (dist z w)) : ℂ) - dist (↑w : ℂ) (↑(w.center (dist z w)) : ℂ)
have 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)
Tactic: rw [dist_center_dist, dist_self_center, ← Real.cosh_sub_sinh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
⊢ instTopologicalSpace = UniformSpace.toTopologicalSpace
have refine_1 : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] id
Tactic: refine le_antisymm (continuous_id_iff_le.1 ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
refine_1 : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] id
⊢ instTopologicalSpace = UniformSpace.toTopologicalSpace
have refine_2 : UniformSpace.toTopologicalSpace ≤ instTopologicalSpace
Tactic: refine le_antisymm (continuous_id_iff_le.1 ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] id
have refine_1 : Continuous (Y := ℝ) fun (x : ℍ × ℍ) ↦ dist (id x.1) (id x.2)
Tactic: refine (@continuous_iff_continuous_dist ℍ ℍ metricSpaceAux.toPseudoMetricSpace _ _).2 ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (hypothesis)
Goal:
z w : ℍ
r : ℝ
⊢ Continuous (Y := ℝ) fun (x : ℍ × ℍ) ↦ dist (id x.1) (id x.2)
have this : ∀ (x : ℍ × ℍ), 2 * √(x.1.im * x.2.im) ≠ 0
Tactic: have : ∀ x : ℍ × ℍ, 2 * √(x.1.im * x.2.im) ≠ 0 := fun x => by positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
⊢ UniformSpace.toTopologicalSpace ≤ instTopologicalSpace
have refine_2 : ∀ (z : ℍ), 𝓝 z ≤ 𝓝 z
Tactic: refine le_of_nhds_le_nhds fun z => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
⊢ 𝓝 z ≤ 𝓝 z
have refine_2 : 𝓝 z ≤ comap UpperHalfPlane.coe (𝓝 (↑z : ℂ))
Tactic: rw [nhds_induced]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
⊢ 𝓝 z ≤ comap UpperHalfPlane.coe (𝓝 (↑z : ℂ))
have refine_2 : ∀ (R : ℝ) (hR : 0 < R), ∃ (i : ℝ), 0 < i ∧ ball z i ⊆ UpperHalfPlane.coe ⁻¹' ball (↑z : ℂ) R
Tactic: refine (nhds_basis_ball.le_basis_iff (nhds_basis_ball.comap _)).2 fun R hR => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (hypothesis)
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
⊢ ∃ (i : ℝ), 0 < i ∧ ball z i ⊆ UpperHalfPlane.coe ⁻¹' ball (↑z : ℂ) R
have h₁ : 1 < R / z.im + 1
Tactic: have h₁ : 1 < R / im z + 1 := lt_add_of_pos_left _ (div_pos hR z.im_pos)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (hypothesis)
Goal:
z_1 w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / z.im + 1
⊢ ∃ (i : ℝ), 0 < i ∧ ball z i ⊆ UpperHalfPlane.coe ⁻¹' ball (↑z : ℂ) R
have h₀ : 0 < R / z.im + 1
Tactic: have h₀ : 0 < R / im z + 1 := one_pos.trans h₁