awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ) (hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
hg : LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
e_4 : Complex.addCommGroup = NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module ℝ ℂ) NormedSpace.toModule (β := Module ℝ ℂ) NormedSpace.toModule
⊢ smulFDeriv g (↑τ : ℂ) = (-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ)) ∘SL smulFDeriv (J * g) (↑τ : ℂ)
have h : ∀ (x : ℂ),
  Eq (α := ℂ) ((smulFDeriv g (↑τ : ℂ) : (a : ℂ) → ℂ) x : ℂ)
    (((-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ)) ∘SL smulFDeriv (J * g) (↑τ : ℂ) : (a : ℂ) → ℂ) x : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (hypothesis)
Goal:
τ : ℍ
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
have this : HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ))
  (ContinuousLinearMap.restrictScalars ℝ
    (ContinuousLinearMap.toSpanSingleton ℂ
      ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2)))
  (↑τ : ℂ)
Tactic: have := (hasStrictDerivAt_smul hg τ).hasStrictFDerivAt.restrictScalars ℝ
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ sinh (dist z w / 2) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
have rw : sinh (2 * arsinh (dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))) / 2) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
Tactic: rw [dist_eq, mul_div_cancel_left₀ (arsinh _) two_ne_zero, sinh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
rw :
  sinh (2 * arsinh (dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))) / 2) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
⊢ sinh (dist z w / 2) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
have rw₁ : sinh (arsinh (dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)))) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
Tactic: rw [dist_eq, mul_div_cancel_left₀ (arsinh _) two_ne_zero, sinh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
rw :
  sinh (2 * arsinh (dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))) / 2) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
rw₁ : sinh (arsinh (dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)))) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
⊢ sinh (dist z w / 2) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
have rw₂ : dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
Tactic: rw [dist_eq, mul_div_cancel_left₀ (arsinh _) two_ne_zero, sinh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ cosh (dist z w / 2) = dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im))
have rw : (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2) /
    (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im)) =
  HPow.hPow (β := ℕ) (dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) 2 /
    (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im))
Tactic: rw [← sq_eq_sq₀, cosh_sq', sinh_half_dist, div_pow, div_pow, one_add_div, mul_pow, sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
rw :
  (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2) /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im)) =
    HPow.hPow (β := ℕ) (dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) 2 /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im))
⊢ cosh (dist z w / 2) = dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im))
have rw₁ : 0 ≤ z.im * w.im
Tactic: rw [← sq_eq_sq₀, cosh_sq', sinh_half_dist, div_pow, div_pow, one_add_div, mul_pow, sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
rw :
  (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2) /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im)) =
    HPow.hPow (β := ℕ) (dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) 2 /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im))
rw₁ : 0 ≤ z.im * w.im
⊢ cosh (dist z w / 2) = dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im))
have rw₂ : HPow.hPow (β := ℕ) (2 * √(z.im * w.im)) 2 ≠ 0
Tactic: rw [← sq_eq_sq₀, cosh_sq', sinh_half_dist, div_pow, div_pow, one_add_div, mul_pow, sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
rw :
  (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2) /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im)) =
    HPow.hPow (β := ℕ) (dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) 2 /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im))
rw₁ : 0 ≤ z.im * w.im
rw₂ : HPow.hPow (β := ℕ) (2 * √(z.im * w.im)) 2 ≠ 0
⊢ cosh (dist z w / 2) = dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im))
have ha : 0 ≤ cosh (dist z w / 2)
Tactic: rw [← sq_eq_sq₀, cosh_sq', sinh_half_dist, div_pow, div_pow, one_add_div, mul_pow, sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
rw :
  (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2) /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im)) =
    HPow.hPow (β := ℕ) (dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) 2 /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im))
rw₁ : 0 ≤ z.im * w.im
rw₂ : HPow.hPow (β := ℕ) (2 * √(z.im * w.im)) 2 ≠ 0
ha : 0 ≤ cosh (dist z w / 2)
⊢ cosh (dist z w / 2) = dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im))
have hb : 0 ≤ dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im))
Tactic: rw [← sq_eq_sq₀, cosh_sq', sinh_half_dist, div_pow, div_pow, one_add_div, mul_pow, sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2) /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im)) =
    HPow.hPow (β := ℕ) (dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) 2 /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im))
have e_a : HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 =
  HPow.hPow (β := ℕ) (dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) 2
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 =
    HPow.hPow (β := ℕ) (dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) 2
have e_a : HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) +
    (HAdd.hAdd (α := ℝ) (β := ℝ) ((Complex.normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
        ((Complex.normSq : (a : ℂ) → ℝ) (↑w : ℂ) : ℝ) -
      2 * ((↑z : ℂ).re * (↑w : ℂ).re - z.im * -w.im)) =
  HAdd.hAdd (α := ℝ) (β := ℝ) ((Complex.normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
      ((Complex.normSq : (a : ℂ) → ℝ) (↑w : ℂ) : ℝ) -
    2 * ((↑z : ℂ).re * (↑w : ℂ).re - z.im * w.im)
Tactic: simp only [Complex.dist_eq, Complex.sq_norm, Complex.normSq_sub, Complex.normSq_conj,
      Complex.conj_conj, Complex.mul_re, Complex.conj_re, Complex.conj_im, coe_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ tanh (dist z w / 2) = dist (↑z : ℂ) (↑w : ℂ) / dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))
have rw : 2 * √(z.im * w.im) ≠ 0
Tactic: rw [tanh_eq_sinh_div_cosh, sinh_half_dist, cosh_half_dist, div_div_div_comm, div_self, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ rexp (dist z w / 2) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
have rw : sinh (dist z w / 2) + cosh (dist z w / 2) =
  (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
Tactic: rw [← sinh_add_cosh, sinh_half_dist, cosh_half_dist, add_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
rw :
  sinh (dist z w / 2) + cosh (dist z w / 2) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
⊢ rexp (dist z w / 2) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
have rw₁ : dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) + cosh (dist z w / 2) =
  (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
Tactic: rw [← sinh_add_cosh, sinh_half_dist, cosh_half_dist, add_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
rw :
  sinh (dist z w / 2) + cosh (dist z w / 2) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
rw₁ :
  dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) + cosh (dist z w / 2) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
⊢ rexp (dist z w / 2) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
have rw₂ : dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) +
    dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im)) =
  (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
Tactic: rw [← sinh_add_cosh, sinh_half_dist, cosh_half_dist, add_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
rw :
  sinh (dist z w / 2) + cosh (dist z w / 2) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
rw₁ :
  dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) + cosh (dist z w / 2) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
rw₂ :
  dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) +
      dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im)) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
⊢ rexp (dist z w / 2) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
have rw₃ : dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) +
    dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im)) =
  dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) +
    dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im))
Tactic: rw [← sinh_add_cosh, sinh_half_dist, cosh_half_dist, add_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ cosh (dist z w) = 1 + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 / (2 * z.im * w.im)
have hc : Ne (α := ℝ) 2 0
Tactic: rw [dist_eq, cosh_two_mul, cosh_sq', add_assoc, ← two_mul, sinh_arsinh, div_pow, mul_pow,
    sq_sqrt, sq (2 : ℝ), mul_assoc, ← mul_div_assoc, mul_assoc, mul_div_mul_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
hc : Ne (α := ℝ) 2 0
⊢ cosh (dist z w) = 1 + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 / (2 * z.im * w.im)
have rw : 0 ≤ z.im * w.im
Tactic: rw [dist_eq, cosh_two_mul, cosh_sq', add_assoc, ← two_mul, sinh_arsinh, div_pow, mul_pow,
    sq_sqrt, sq (2 : ℝ), mul_assoc, ← mul_div_assoc, mul_assoc, mul_div_mul_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
a b c : ℍ
⊢ 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 : ℂ)))
have 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 : ℂ)))
Tactic: simp only [add_div _ _ (2 : ℝ), sinh_add, sinh_half_dist, cosh_half_dist, div_mul_div_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
a b c : ℍ
⊢ 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 : ℂ)))
have 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))
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
a b c : ℍ
⊢ (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))
have e_a : √(a.im * b.im) * √(b.im * c.im) = √(a.im * c.im) * b.im
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
a b c : ℍ
⊢ √(a.im * b.im) * √(b.im * c.im) = √(a.im * c.im) * b.im
have e_a : 0 ≤ b.im
Tactic: rw [sqrt_mul, sqrt_mul, sqrt_mul, mul_comm (√a.im), mul_mul_mul_comm, mul_self_sqrt,
      mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
a b c : ℍ
e_a : 0 ≤ b.im
⊢ √(a.im * b.im) * √(b.im * c.im) = √(a.im * c.im) * b.im
have e_a₁ : 0 ≤ a.im
Tactic: rw [sqrt_mul, sqrt_mul, sqrt_mul, mul_comm (√a.im), mul_mul_mul_comm, mul_self_sqrt,
      mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
⊢ dist z w ≤ r ↔ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) ≤ sinh (r / 2)
have rw : dist z w / 2 ≤ r / 2 ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
rw : dist z w / 2 ≤ 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)
have rw₁ : sinh (dist z w / 2) ≤ sinh (r / 2) ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)
⊢ dist z w ≤ r ↔ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) ≤ sinh (r / 2)
have rw₂ : dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) ≤ sinh (r / 2) ↔
  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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
⊢ dist z w = r ↔ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = sinh (r / 2)
have rw : dist z w / 2 = r / 2 ↔ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = sinh (r / 2)
Tactic: rw [← div_left_inj' (two_ne_zero' ℝ), ← sinh_inj, sinh_half_dist]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
rw : dist z w / 2 = 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)
have rw₁ : sinh (dist z w / 2) = sinh (r / 2) ↔ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = sinh (r / 2)
Tactic: rw [← div_left_inj' (two_ne_zero' ℝ), ← sinh_inj, sinh_half_dist]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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)
⊢ dist z w = r ↔ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = sinh (r / 2)
have rw₂ : dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = sinh (r / 2) ↔
  dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = sinh (r / 2)
Tactic: rw [← div_left_inj' (two_ne_zero' ℝ), ← sinh_inj, sinh_half_dist]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ dist z w = r ↔ HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 / (4 * z.im * w.im) = HPow.hPow (β := ℕ) (sinh (r / 2)) 2
have 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
Tactic: rw [dist_eq_iff_eq_sinh, ← sq_eq_sq₀, div_pow, mul_pow, sq_sqrt, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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
⊢ dist z w = r ↔ HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 / (4 * z.im * w.im) = HPow.hPow (β := ℕ) (sinh (r / 2)) 2
have rw₁ : 0 ≤ z.im * w.im
Tactic: rw [dist_eq_iff_eq_sinh, ← sq_eq_sq₀, div_pow, mul_pow, sq_sqrt, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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
⊢ dist z w = r ↔ HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 / (4 * z.im * w.im) = HPow.hPow (β := ℕ) (sinh (r / 2)) 2
have ha : 0 ≤ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
Tactic: rw [dist_eq_iff_eq_sinh, ← sq_eq_sq₀, div_pow, mul_pow, sq_sqrt, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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))
⊢ dist z w = r ↔ HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 / (4 * z.im * w.im) = HPow.hPow (β := ℕ) (sinh (r / 2)) 2
have hb : 0 ≤ sinh (r / 2)
Tactic: rw [dist_eq_iff_eq_sinh, ← sq_eq_sq₀, div_pow, mul_pow, sq_sqrt, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
a b c : ℍ
⊢ dist a c ≤ dist a b + dist b c
have 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))
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
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))
⊢ dist a c ≤ dist a b + dist b c
have rw₁ : 0 < dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ))
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
a b c : ℍ
⊢ 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))
have 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 : ℂ))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
a b c : ℍ
⊢ 0 < dist (↑b : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑b : ℂ))
have rw : ¬(↑b : ℂ).im = 0
Tactic: rw [dist_comm, dist_pos, Ne, Complex.conj_eq_iff_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z w : ℍ
⊢ dist z w ≤ dist (↑z : ℂ) (↑w : ℂ) / √(z.im * w.im)
have rw : 0 ≤ dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
Tactic: rw [dist_le_iff_le_sinh, ← div_mul_eq_div_div_swap, self_le_sinh_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Metric (goal)
Goal:
z_1 w : ℍ
r : ℝ
z : ℍ
⊢ dist z z = 0
have rw : 2 * arsinh (dist (↑z : ℂ) (↑z : ℂ) / (2 * √(z.im * z.im))) = 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
⊢ dist z z = 0
have rw₁ : 2 * arsinh (0 / (2 * √(z.im * z.im))) = 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
⊢ dist z z = 0
have rw₂ : 2 * arsinh 0 = 0
Tactic: rw [dist_eq, dist_self, zero_div, arsinh_zero, mul_zero]