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

Tactic:
apply isCompact_closedBall

Premises used: ProperSpace.isCompact_closedBall
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a : ℝ
⊢ Isometry (β := ℍ) fun (y : ℝ) ↦ { coe := { re := a, im := rexp y }, coe_im_pos := ⋯ }

Tactic:
Isometry.of_dist_eq fun y₁ y₂ => ?_

Premises used: Isometry.of_dist_eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a : ℝ
refine :
  ∀ (y₁ y₂ : ℝ),
    dist { coe := { re := a, im := rexp y₁ : ℂ }, coe_im_pos := ⋯ : ℍ }
        { coe := { re := a, im := rexp y₂ : ℂ }, coe_im_pos := ⋯ : ℍ } =
      dist y₁ y₂
⊢ Isometry (β := ℍ) fun (y : ℝ) ↦ { coe := { re := a, im := rexp y }, coe_im_pos := ⋯ }

Tactic:
refine Isometry.of_dist_eq fun y₁ y₂ => ?_

Premises used: Isometry.of_dist_eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a y₁ y₂ : ℝ
rw :
  dist (log { coe := { re := a, im := rexp y₁ : ℂ }, coe_im_pos := ⋯ : ℍ }.im)
      (log { coe := { re := a, im := rexp y₂ : ℂ }, coe_im_pos := ⋯ : ℍ }.im) =
    dist y₁ y₂
rw₁ :
  { coe := { re := a, im := rexp y₁ : ℂ }, coe_im_pos := ⋯ : ℍ }.re =
    { coe := { re := a, im := rexp y₂ }, coe_im_pos := ⋯ }.re
⊢ dist { coe := { re := a, im := rexp y₁ : ℂ }, coe_im_pos := ⋯ : ℍ }
      { coe := { re := a, im := rexp y₂ : ℂ }, coe_im_pos := ⋯ : ℍ } =
    dist y₁ y₂

Tactic:
rw [dist_of_re_eq]

Premises used: UpperHalfPlane.dist_of_re_eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a y₁ y₂ : ℝ
⊢ dist (log { coe := { re := a, im := rexp y₁ : ℂ }, coe_im_pos := ⋯ : ℍ }.im)
      (log { coe := { re := a, im := rexp y₂ : ℂ }, coe_im_pos := ⋯ : ℍ }.im) =
    dist y₁ y₂

Tactic:
congr_arg₂ _ (log_exp _) (log_exp _)

Premises used: Real.log_exp, congr_arg₂
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a y₁ y₂ : ℝ
⊢ { coe := { re := a, im := rexp y₁ : ℂ }, coe_im_pos := ⋯ : ℍ }.re =
    { coe := { re := a, im := rexp y₂ }, coe_im_pos := ⋯ }.re

Tactic:
rfl

Premises used: Real.exp, UpperHalfPlane.re, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a y₁ y₂ : ℝ
⊢ dist (log { coe := { re := a, im := rexp y₁ : ℂ }, coe_im_pos := ⋯ : ℍ }.im)
      (log { coe := { re := a, im := rexp y₂ : ℂ }, coe_im_pos := ⋯ : ℍ }.im) =
    dist y₁ y₂

Tactic:
exacts [congr_arg₂ _ (log_exp _) (log_exp _), rfl]

Premises used: Real.log_exp, rfl, congr_arg₂
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a : ℝ
y₁ y₂ : ℍ
⊢ dist (a +ᵥ y₁) (a +ᵥ y₂) = dist y₁ y₂

Tactic:
simp only [dist_eq, coe_vadd, vadd_im, dist_add_left]

Premises used: UpperHalfPlane.dist_eq, UpperHalfPlane.coe_vadd, dist_add_left, UpperHalfPlane.vadd_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a : { x : ℝ // 0 < x }
⊢ Isometry (β := ℍ) fun (x : ℍ) ↦ a • x

Tactic:
Isometry.of_dist_eq fun y₁ y₂ => ?_

Premises used: Isometry.of_dist_eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a : { x : ℝ // 0 < x }
refine : ∀ (y₁ y₂ : ℍ), dist (a • y₁) (a • y₂) = dist y₁ y₂
⊢ Isometry (β := ℍ) fun (x : ℍ) ↦ a • x

Tactic:
refine Isometry.of_dist_eq fun y₁ y₂ => ?_

Premises used: Isometry.of_dist_eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a : { x : ℝ // 0 < x }
y₁ y₂ : ℍ
simp :
  2 * arsinh (dist ((↑a : ℝ) • (↑y₁ : ℂ)) ((↑a : ℝ) • (↑y₂ : ℂ)) / (2 * √((↑a : ℝ) * y₁.im * ((↑a : ℝ) * y₂.im)))) =
    2 * arsinh (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im)))
⊢ dist (a • y₁) (a • y₂) = dist y₁ y₂

Tactic:
simp only [dist_eq, coe_pos_real_smul, pos_real_im]

Premises used: UpperHalfPlane.coe_pos_real_smul, UpperHalfPlane.dist_eq, UpperHalfPlane.pos_real_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a : { x : ℝ // 0 < x }
y₁ y₂ : ℍ
e_a :
  dist ((↑a : ℝ) • (↑y₁ : ℂ)) ((↑a : ℝ) • (↑y₂ : ℂ)) / (2 * √((↑a : ℝ) * y₁.im * ((↑a : ℝ) * y₂.im))) =
    dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im))
⊢ 2 * arsinh (dist ((↑a : ℝ) • (↑y₁ : ℂ)) ((↑a : ℝ) • (↑y₂ : ℂ)) / (2 * √((↑a : ℝ) * y₁.im * ((↑a : ℝ) * y₂.im)))) =
    2 * arsinh (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im)))

Tactic:
congr 2
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a : { x : ℝ // 0 < x }
y₁ y₂ : ℍ
e_a :
  |(↑a : ℝ)| * dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (|(↑a : ℝ)| * (2 * √(y₁.im * y₂.im))) =
    dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im))
⊢ dist ((↑a : ℝ) • (↑y₁ : ℂ)) ((↑a : ℝ) • (↑y₂ : ℂ)) / (2 * √((↑a : ℝ) * y₁.im * ((↑a : ℝ) * y₂.im))) =
    dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im))

Tactic:
rw [dist_smul₀, mul_mul_mul_comm, Real.sqrt_mul (mul_self_nonneg _), Real.sqrt_mul_self_eq_abs,
    Real.norm_eq_abs, mul_left_comm]

Premises used: mul_self_nonneg, mul_mul_mul_comm, Real.sqrt_mul, mul_left_comm, Real.sqrt_mul_self_eq_abs, dist_smul₀, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a : { x : ℝ // 0 < x }
y₁ y₂ : ℍ
⊢ |(↑a : ℝ)| * dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (|(↑a : ℝ)| * (2 * √(y₁.im * y₂.im))) =
    dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im))

Tactic:
mul_div_mul_left _ _ (mt _root_.abs_eq_zero.1 a.2.ne')

Premises used: mt, LT.lt.ne', abs_eq_zero, Iff.mp, mul_div_mul_left, Subtype.property
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
a : { x : ℝ // 0 < x }
y₁ y₂ : ℍ
⊢ |(↑a : ℝ)| * dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (|(↑a : ℝ)| * (2 * √(y₁.im * y₂.im))) =
    dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im))

Tactic:
exact mul_div_mul_left _ _ (mt _root_.abs_eq_zero.1 a.2.ne')

Premises used: mt, LT.lt.ne', mul_div_mul_left, Subtype.property
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
⊢ 0 ≤ y₁.im * y₂.im

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
⊢ 0 ≤ y₁.im * y₂.im

Tactic:
have h₁ : 0 ≤ im y₁ * im y₂ := by positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
⊢ ‖(↑y₁ : ℂ) * (↑y₂ : ℂ)‖ ≠ 0

Tactic:
simp [y₁.ne_zero, y₂.ne_zero]

Premises used: UpperHalfPlane.ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
⊢ ‖(↑y₁ : ℂ) * (↑y₂ : ℂ)‖ ≠ 0

Tactic:
have h₂ : ‖(y₁ * y₂ : ℂ)‖ ≠ 0 := by simp [y₁.ne_zero, y₂.ne_zero]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖(↑y₁ : ℂ) * (↑y₂ : ℂ)‖ ≠ 0
simp_rw :
  2 *
      arsinh
        (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (‖(↑y₁ : ℂ)‖ * ‖(↑y₂ : ℂ)‖) / (2 * √(y₁.im * y₂.im) / ‖(↑y₁ : ℂ) * (↑y₂ : ℂ)‖)) =
    2 * arsinh (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im)))
⊢ dist (ModularGroup.S • y₁) (ModularGroup.S • y₂) = dist y₁ y₂

Tactic:
simp_rw [modular_S_smul, inv_neg, dist_eq, dist_neg_neg,
          dist_inv_inv₀ y₁.ne_zero y₂.ne_zero, mk_im, neg_im, inv_im, coe_im, neg_div, neg_neg,
          div_mul_div_comm, ← normSq_mul, Real.sqrt_div h₁, ← norm_def, mul_div (2 : ℝ)]

Premises used: mul_div, neg_div, dist_inv_inv₀, Complex.normSq_mul, div_mul_div_comm, inv_neg, neg_neg, UpperHalfPlane.modular_S_smul, UpperHalfPlane.ne_zero, UpperHalfPlane.dist_eq, Complex.norm_def, UpperHalfPlane.mk_im, dist_neg_neg, Complex.inv_im, Real.sqrt_div, OfNat.ofNat, UpperHalfPlane.coe_im, Complex.neg_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖(↑y₁ : ℂ) * (↑y₂ : ℂ)‖ ≠ 0
rw :
  2 *
      arsinh
        (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im)) / (‖(↑y₁ : ℂ)‖ * ‖(↑y₂ : ℂ)‖ / ‖(↑y₁ : ℂ) * (↑y₂ : ℂ)‖)) =
    2 * arsinh (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im)))
rw₁ :
  2 * arsinh (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im)) / (‖(↑y₁ : ℂ) * (↑y₂ : ℂ)‖ / ‖(↑y₁ : ℂ) * (↑y₂ : ℂ)‖)) =
    2 * arsinh (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im)))
rw₂ :
  2 * arsinh (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im)) / 1) =
    2 * arsinh (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im)))
rw₃ rw₄ :
  2 * arsinh (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im))) =
    2 * arsinh (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im)))
⊢ 2 *
      arsinh
        (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (‖(↑y₁ : ℂ)‖ * ‖(↑y₂ : ℂ)‖) / (2 * √(y₁.im * y₂.im) / ‖(↑y₁ : ℂ) * (↑y₂ : ℂ)‖)) =
    2 * arsinh (dist (↑y₁ : ℂ) (↑y₂ : ℂ) / (2 * √(y₁.im * y₂.im)))

Tactic:
rw [div_div_div_comm, ← norm_mul, div_self h₂, div_one]

Premises used: norm_mul, div_div_div_comm, div_one, div_self
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
⊢ Isometry (β := ℍ) fun (z : ℍ) ↦ ModularGroup.S • z

Tactic:
have h₀ : Isometry (fun z => ModularGroup.S • z : ℍ → ℍ) :=
      Isometry.of_dist_eq fun y₁ y₂ => by
        have h₁ : 0 ≤ im y₁ * im y₂ := by positivity
        have h₂ : ‖(y₁ * y₂ : ℂ)‖ ≠ 0 := by simp [y₁.ne_zero, y₂.ne_zero]
        simp_rw [modular_S_smul, inv_neg, dist_eq, dist_neg_neg,
          dist_inv_inv₀ y₁.ne_zero y₂.ne_zero, mk_im, neg_im, inv_im, coe_im, neg_div, neg_neg,
          div_mul_div_comm, ← normSq_mul, Real.sqrt_div h₁, ← norm_def, mul_div (2 : ℝ)]
        rw [div_div_div_comm, ← norm_mul, div_self h₂, div_one]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry (β := ℍ) fun (z : ℍ) ↦ ModularGroup.S • z
pos : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0), Isometry (β := ℍ) fun (x : ℍ) ↦ g • x
neg : ∀ (hc : ¬(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0), Isometry (β := ℍ) fun (x : ℍ) ↦ g • x
⊢ Isometry (β := ℍ) fun (x : ℍ) ↦ g • x

Tactic:
by_cases hc : g 1 0 = 0

Premises used: OfNat.ofNat, Subtype.val
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry (β := ℍ) fun (z : ℍ) ↦ ModularGroup.S • z
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
pos :
  ∀ (u : { x : ℝ // 0 < x }) (v : ℝ)
    (h : Eq (α := ℍ → ℍ) (fun (x : ℍ) ↦ g • x) ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)),
    Isometry (β := ℍ) fun (x : ℍ) ↦ g • x
⊢ Isometry (β := ℍ) fun (x : ℍ) ↦ g • x

Tactic:
obtain ⟨u, v, h⟩ := exists_SL2_smul_eq_of_apply_zero_one_eq_zero g hc

Premises used: UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry (β := ℍ) fun (z : ℍ) ↦ ModularGroup.S • z
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
u : { x : ℝ // 0 < x }
v : ℝ
h : Eq (α := ℍ → ℍ) (fun (x : ℍ) ↦ g • x) ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)
pos : Isometry (α := ℍ) (β := ℍ) ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)
⊢ Isometry (β := ℍ) fun (x : ℍ) ↦ g • x

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry (β := ℍ) fun (z : ℍ) ↦ ModularGroup.S • z
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
u : { x : ℝ // 0 < x }
v : ℝ
h : Eq (α := ℍ → ℍ) (fun (x : ℍ) ↦ g • x) ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)
⊢ Isometry (α := ℍ) (β := ℍ) ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)

Tactic:
(isometry_real_vadd v).comp (isometry_pos_mul u)

Premises used: Isometry.comp, UpperHalfPlane.isometry_real_vadd, UpperHalfPlane.isometry_pos_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry (β := ℍ) fun (z : ℍ) ↦ ModularGroup.S • z
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
u : { x : ℝ // 0 < x }
v : ℝ
h : Eq (α := ℍ → ℍ) (fun (x : ℍ) ↦ g • x) ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)
⊢ Isometry (α := ℍ) (β := ℍ) ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)

Tactic:
exact (isometry_real_vadd v).comp (isometry_pos_mul u)

Premises used: Isometry.comp, UpperHalfPlane.isometry_real_vadd, UpperHalfPlane.isometry_pos_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry (β := ℍ) fun (z : ℍ) ↦ ModularGroup.S • z
hc : ¬(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
neg :
  ∀ (u : { x : ℝ // 0 < x }) (v w : ℝ)
    (h :
      Eq (α := ℍ → ℍ) (fun (x : ℍ) ↦ g • x)
        ((fun (x : ℍ) ↦ w +ᵥ x) ∘ (fun (x : ℍ) ↦ ModularGroup.S • x) ∘ (fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)),
    Isometry (β := ℍ) fun (x : ℍ) ↦ g • x
⊢ Isometry (β := ℍ) fun (x : ℍ) ↦ g • x

Tactic:
obtain ⟨u, v, w, h⟩ := exists_SL2_smul_eq_of_apply_zero_one_ne_zero g hc

Premises used: UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w_1 : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry (β := ℍ) fun (z : ℍ) ↦ ModularGroup.S • z
hc : ¬(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
u : { x : ℝ // 0 < x }
v w : ℝ
h :
  Eq (α := ℍ → ℍ) (fun (x : ℍ) ↦ g • x)
    ((fun (x : ℍ) ↦ w +ᵥ x) ∘ (fun (x : ℍ) ↦ ModularGroup.S • x) ∘ (fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)
neg :
  Isometry (α := ℍ) (β := ℍ)
    ((fun (x : ℍ) ↦ w +ᵥ x) ∘ (fun (x : ℍ) ↦ ModularGroup.S • x) ∘ (fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)
⊢ Isometry (β := ℍ) fun (x : ℍ) ↦ g • x

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w_1 : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry (β := ℍ) fun (z : ℍ) ↦ ModularGroup.S • z
hc : ¬(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
u : { x : ℝ // 0 < x }
v w : ℝ
h :
  Eq (α := ℍ → ℍ) (fun (x : ℍ) ↦ g • x)
    ((fun (x : ℍ) ↦ w +ᵥ x) ∘ (fun (x : ℍ) ↦ ModularGroup.S • x) ∘ (fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)
⊢ Isometry (α := ℍ) (β := ℍ)
    ((fun (x : ℍ) ↦ w +ᵥ x) ∘ (fun (x : ℍ) ↦ ModularGroup.S • x) ∘ (fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)

Tactic:
(isometry_real_vadd w).comp (h₀.comp <| (isometry_real_vadd v).comp <| isometry_pos_mul u)

Premises used: Isometry.comp, UpperHalfPlane.isometry_real_vadd, UpperHalfPlane.isometry_pos_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w_1 : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry (β := ℍ) fun (z : ℍ) ↦ ModularGroup.S • z
hc : ¬(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
u : { x : ℝ // 0 < x }
v w : ℝ
h :
  Eq (α := ℍ → ℍ) (fun (x : ℍ) ↦ g • x)
    ((fun (x : ℍ) ↦ w +ᵥ x) ∘ (fun (x : ℍ) ↦ ModularGroup.S • x) ∘ (fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)
⊢ Isometry (α := ℍ) (β := ℍ)
    ((fun (x : ℍ) ↦ w +ᵥ x) ∘ (fun (x : ℍ) ↦ ModularGroup.S • x) ∘ (fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)

Tactic:
exact
        (isometry_real_vadd w).comp (h₀.comp <| (isometry_real_vadd v).comp <| isometry_pos_mul u)

Premises used: Isometry.comp, UpperHalfPlane.isometry_real_vadd, UpperHalfPlane.isometry_pos_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
simp :
  -((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * z) + -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) =
    -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) + -((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * z)
⊢ num (-g) z = -num g z

Tactic:
simp [num]

Premises used: UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
⊢ -((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * z) + -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) =
    -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) + -((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * z)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
simp :
  -((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * z) + -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) =
    -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) + -((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * z)
⊢ denom (-g) z = -denom g z

Tactic:
simp [denom]

Premises used: UpperHalfPlane.denom
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
⊢ -((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * z) + -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) =
    -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) + -((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * z)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
h : cd ≠ 0
contrapose : ∀ (h : (↑(cd 0) : ℂ) * z + (↑(cd 1) : ℂ) = 0), cd = 0
⊢ (↑(cd 0) : ℂ) * z + (↑(cd 1) : ℂ) ≠ 0

Tactic:
contrapose h
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
h : (↑(cd 0) : ℂ) * z + (↑(cd 1) : ℂ) = 0
⊢ ((↑(cd 0) : ℂ) * z + (↑(cd 1) : ℂ)).im = Complex.im 0

Tactic:
apply_fun Complex.im at h

Premises used: Complex.im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
h : ((↑(cd 0) : ℂ) * z + (↑(cd 1) : ℂ)).im = Complex.im 0
⊢ cd 0 = 0

Tactic:
simpa only [Complex.add_im, Complex.mul_im, Complex.ofReal_im, zero_mul, add_zero,
      Complex.zero_im, mul_eq_zero, hz, or_false] using h

Premises used: Complex.mul_im, Complex.add_im, MulZeroClass.zero_mul, Complex.zero_im, mul_eq_zero, or_false, Complex.ofReal_im, add_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
h : (↑(cd 0) : ℂ) * z + (↑(cd 1) : ℂ) = 0
⊢ cd 0 = 0

Tactic:
have : cd 0 = 0 := by
    -- we will need this twice
    apply_fun Complex.im at h
    simpa only [Complex.add_im, Complex.mul_im, Complex.ofReal_im, zero_mul, add_zero,
      Complex.zero_im, mul_eq_zero, hz, or_false] using h
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
h : (↑(cd 0) : ℂ) * z + (↑(cd 1) : ℂ) = 0
this : cd 0 = 0
⊢ cd 1 = 0

Tactic:
simp only [this, zero_mul, Complex.ofReal_zero, zero_add, Complex.ofReal_eq_zero] at h

Premises used: MulZeroClass.zero_mul, zero_add, Complex.ofReal_eq_zero, Complex.ofReal_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
this : cd 0 = 0
h : cd 1 = 0
h₁ : ∀ (i : Fin 2), cd i = 0 i
⊢ cd = 0

Tactic:
ext i
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
this : cd 0 = 0
h : cd 1 = 0
i : Fin 2
h₁ : cd ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h₂ : cd ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ cd i = 0 i

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
this : cd 0 = 0
h : cd 1 = 0
⊢ cd ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
assumption
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
this : cd 0 = 0
h : cd 1 = 0
⊢ cd ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
assumption
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
cd : Fin 2 → ℝ
τ : ℍ
h : cd ≠ 0
⊢ (↑(cd 0) : ℂ) * (↑τ : ℂ) + (↑(cd 1) : ℂ) ≠ 0

Tactic:
linear_ne_zero_of_im τ.im_ne_zero h

Premises used: UpperHalfPlane.im_ne_zero, UpperHalfPlane.linear_ne_zero_of_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
⊢ denom g z ≠ 0

Tactic:
linear_ne_zero_of_im hz fun H ↦ g.det.ne_zero ?_

Premises used: Units.ne_zero, UpperHalfPlane.denom, UpperHalfPlane.linear_ne_zero_of_im, Matrix.GeneralLinearGroup.det, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
refine :
  ∀ (H : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 = 0),
    Eq (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
⊢ denom g z ≠ 0

Tactic:
refine linear_ne_zero_of_im hz fun H ↦ g.det.ne_zero ?_

Premises used: Units.ne_zero, UpperHalfPlane.linear_ne_zero_of_im, Matrix.GeneralLinearGroup.det, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
H : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 = 0
⊢ Eq (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0

Tactic:
simp [Matrix.det_fin_two, H]

Premises used: Matrix.det_fin_two
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
⊢ denom g (↑z : ℂ) ≠ 0

Tactic:
denom_ne_zero_of_im g z.im_ne_zero

Premises used: UpperHalfPlane.im_ne_zero, UpperHalfPlane.denom_ne_zero_of_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((Complex.normSq : (a : ℂ) → ℝ) (denom g z) : ℝ)

Tactic:
Complex.normSq_pos.mpr (denom_ne_zero_of_im g hz)

Premises used: Iff.mpr, Complex.normSq_pos, UpperHalfPlane.denom_ne_zero_of_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
⊢ Ne (α := ℝ) ((Complex.normSq : (a : ℂ) → ℝ) (denom g z) : ℝ) (0 : ℝ)

Tactic:
ne_of_gt (normSq_denom_pos g hz)

Premises used: ne_of_gt, UpperHalfPlane.normSq_denom_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
field_simp :
  denom (g * h) z =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * num h z + denom h z * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)
⊢ denom (g * h) z =
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (num h z / denom h z) +
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) *
      denom h z

Tactic:
field_simp [denom_ne_zero_of_im h hz]

Premises used: UpperHalfPlane.denom_ne_zero_of_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
simp :
  ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) +
          (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) *
        z +
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) +
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) *
        ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * z + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) +
      ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * z + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) *
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)
⊢ denom (g * h) z =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * num h z + denom h z * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)

Tactic:
simp only [denom, Units.val_mul, mul_apply, Fin.sum_univ_succ, Finset.univ_unique,
    Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_zero_eq_one, Complex.ofReal_add,
    Complex.ofReal_mul, num]

Premises used: Complex.ofReal_add, Matrix.mul_apply, Finset.univ_unique, Fin.succ_zero_eq_one, Finset.sum_singleton, UpperHalfPlane.denom, Fin.default_eq_zero, UpperHalfPlane.num, Units.val_mul, Complex.ofReal_mul, Fin.sum_univ_succ
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
⊢ ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) +
          (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) *
        z +
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) +
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) *
        ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * z + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) +
      ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * z + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) *
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)

Tactic:
ring