[GOAL]
g✝ : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
g : SL(2, R)
⊢ IsCoprime (↑g 1 0) (↑g 1 1)
[PROOFSTEP]
use-(↑g : Matrix (Fin 2) (Fin 2) R) 0 1, (↑g : Matrix (Fin 2) (Fin 2) R) 0 0
[GOAL]
case h
g✝ : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
g : SL(2, R)
⊢ -↑g 0 1 * ↑g 1 0 + ↑g 0 0 * ↑g 1 1 = 1
[PROOFSTEP]
rw [add_comm, neg_mul, ← sub_eq_add_neg, ← det_fin_two]
[GOAL]
case h
g✝ : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
g : SL(2, R)
⊢ det ↑g = 1
[PROOFSTEP]
exact g.det_coe
[GOAL]
g : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
⊢ Set.SurjOn (fun g => ↑g 1) Set.univ {cd | IsCoprime (cd 0) (cd 1)}
[PROOFSTEP]
rintro cd ⟨b₀, a, gcd_eqn⟩
[GOAL]
case intro.intro
g : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
⊢ cd ∈ (fun g => ↑g 1) '' Set.univ
[PROOFSTEP]
let A := of ![![a, -b₀], cd]
[GOAL]
case intro.intro
g : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : (fun x => Matrix (Fin (Nat.succ (Nat.succ 0))) (Fin (Nat.succ (Nat.succ 0))) R) ![![a, -b₀], cd] :=
  ↑of ![![a, -b₀], cd]
⊢ cd ∈ (fun g => ↑g 1) '' Set.univ
[PROOFSTEP]
have det_A_1 : det A = 1 := by
  convert gcd_eqn
  rw [det_fin_two]
  simp [(by ring : a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1)]
[GOAL]
g : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : (fun x => Matrix (Fin (Nat.succ (Nat.succ 0))) (Fin (Nat.succ (Nat.succ 0))) R) ![![a, -b₀], cd] :=
  ↑of ![![a, -b₀], cd]
⊢ det A = 1
[PROOFSTEP]
convert gcd_eqn
[GOAL]
case h.e'_2
g : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : (fun x => Matrix (Fin (Nat.succ (Nat.succ 0))) (Fin (Nat.succ (Nat.succ 0))) R) ![![a, -b₀], cd] :=
  ↑of ![![a, -b₀], cd]
⊢ det A = b₀ * cd 0 + a * cd 1
[PROOFSTEP]
rw [det_fin_two]
[GOAL]
case h.e'_2
g : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : (fun x => Matrix (Fin (Nat.succ (Nat.succ 0))) (Fin (Nat.succ (Nat.succ 0))) R) ![![a, -b₀], cd] :=
  ↑of ![![a, -b₀], cd]
⊢ A 0 0 * A 1 1 - A 0 1 * A 1 0 = b₀ * cd 0 + a * cd 1
[PROOFSTEP]
simp [(by ring : a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1)]
[GOAL]
g : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : (fun x => Matrix (Fin (Nat.succ (Nat.succ 0))) (Fin (Nat.succ (Nat.succ 0))) R) ![![a, -b₀], cd] :=
  ↑of ![![a, -b₀], cd]
⊢ a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1
[PROOFSTEP]
ring
[GOAL]
case intro.intro
g : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : (fun x => Matrix (Fin (Nat.succ (Nat.succ 0))) (Fin (Nat.succ (Nat.succ 0))) R) ![![a, -b₀], cd] :=
  ↑of ![![a, -b₀], cd]
det_A_1 : det A = 1
⊢ cd ∈ (fun g => ↑g 1) '' Set.univ
[PROOFSTEP]
refine' ⟨⟨A, det_A_1⟩, Set.mem_univ _, _⟩
[GOAL]
case intro.intro
g : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : (fun x => Matrix (Fin (Nat.succ (Nat.succ 0))) (Fin (Nat.succ (Nat.succ 0))) R) ![![a, -b₀], cd] :=
  ↑of ![![a, -b₀], cd]
det_A_1 : det A = 1
⊢ (fun g => ↑g 1) { val := A, property := det_A_1 } = cd
[PROOFSTEP]
ext
[GOAL]
case intro.intro.h
g : SL(2, ℤ)
z : ℍ
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : (fun x => Matrix (Fin (Nat.succ (Nat.succ 0))) (Fin (Nat.succ (Nat.succ 0))) R) ![![a, -b₀], cd] :=
  ↑of ![![a, -b₀], cd]
det_A_1 : det A = 1
x✝ : Fin 2
⊢ (fun g => ↑g 1) { val := A, property := det_A_1 } x✝ = cd x✝
[PROOFSTEP]
simp
[GOAL]
g : SL(2, ℤ)
z : ℍ
⊢ Tendsto (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop
[PROOFSTEP]
letI : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
[GOAL]
g : SL(2, ℤ)
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
⊢ Tendsto (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop
[PROOFSTEP]
let π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
[GOAL]
g : SL(2, ℤ)
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
⊢ Tendsto (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop
[PROOFSTEP]
let π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
[GOAL]
g : SL(2, ℤ)
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
⊢ Tendsto (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop
[PROOFSTEP]
let f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight (z : ℂ) + π₁.smulRight 1
[GOAL]
g : SL(2, ℤ)
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
⊢ Tendsto (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop
[PROOFSTEP]
have f_def : ⇑f = fun p : Fin 2 → ℝ => (p 0 : ℂ) * ↑z + p 1 :=
  by
  ext1
  dsimp only [LinearMap.coe_proj, real_smul, LinearMap.coe_smulRight, LinearMap.add_apply]
  rw [mul_one]
[GOAL]
g : SL(2, ℤ)
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
⊢ ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
[PROOFSTEP]
ext1
[GOAL]
case h
g : SL(2, ℤ)
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
x✝ : Fin 2 → ℝ
⊢ ↑f x✝ = ↑(x✝ 0) * ↑z + ↑(x✝ 1)
[PROOFSTEP]
dsimp only [LinearMap.coe_proj, real_smul, LinearMap.coe_smulRight, LinearMap.add_apply]
[GOAL]
case h
g : SL(2, ℤ)
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
x✝ : Fin 2 → ℝ
⊢ ↑(Function.eval 0 x✝) * ↑z + ↑(Function.eval 1 x✝) * 1 = ↑(x✝ 0) * ↑z + ↑(x✝ 1)
[PROOFSTEP]
rw [mul_one]
[GOAL]
g : SL(2, ℤ)
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
⊢ Tendsto (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop
[PROOFSTEP]
have : (fun p : Fin 2 → ℤ => normSq ((p 0 : ℂ) * ↑z + ↑(p 1))) = normSq ∘ f ∘ fun p : Fin 2 → ℤ => ((↑) : ℤ → ℝ) ∘ p :=
  by
  ext1
  rw [f_def]
  dsimp only [Function.comp]
  rw [ofReal_int_cast, ofReal_int_cast]
[GOAL]
g : SL(2, ℤ)
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
⊢ (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
[PROOFSTEP]
ext1
[GOAL]
case h
g : SL(2, ℤ)
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
x✝ : Fin 2 → ℤ
⊢ ↑normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1)) = (↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p) x✝
[PROOFSTEP]
rw [f_def]
[GOAL]
case h
g : SL(2, ℤ)
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
x✝ : Fin 2 → ℤ
⊢ ↑normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1)) = (↑normSq ∘ (fun p => ↑(p 0) * ↑z + ↑(p 1)) ∘ fun p => Int.cast ∘ p) x✝
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
case h
g : SL(2, ℤ)
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
x✝ : Fin 2 → ℤ
⊢ ↑normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1)) = ↑normSq (↑↑(x✝ 0) * ↑z + ↑↑(x✝ 1))
[PROOFSTEP]
rw [ofReal_int_cast, ofReal_int_cast]
[GOAL]
g : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
⊢ Tendsto (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop
[PROOFSTEP]
rw [this]
[GOAL]
g : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
⊢ Tendsto (↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p) cofinite atTop
[PROOFSTEP]
have hf : LinearMap.ker f = ⊥ :=
  by
  let g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm.comp ((z : ℂ) • ((conjAe : ℂ →ₐ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ))]
  suffices ((z : ℂ).im⁻¹ • g).comp f = LinearMap.id by exact LinearMap.ker_eq_bot_of_inverse this
  apply LinearMap.ext
  intro c
  have hz : (z : ℂ).im ≠ 0 := z.2.ne'
  rw [LinearMap.comp_apply, LinearMap.smul_apply, LinearMap.id_apply]
  ext i
  dsimp only [Pi.smul_apply, LinearMap.pi_apply, smul_eq_mul]
  fin_cases i
  · show (z : ℂ).im⁻¹ * (f c).im = c 0
    rw [f_def, add_im, ofReal_mul_im, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel hz, mul_one]
  · show (z : ℂ).im⁻¹ * ((z : ℂ) * conj (f c)).im = c 1
    rw [f_def, RingHom.map_add, RingHom.map_mul, mul_add, mul_left_comm, mul_conj, conj_ofReal, conj_ofReal, ←
      ofReal_mul, add_im, ofReal_im, zero_add, inv_mul_eq_iff_eq_mul₀ hz]
    simp only [ofReal_im, ofReal_re, mul_im, zero_add, mul_zero]
[GOAL]
g : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
⊢ LinearMap.ker f = ⊥
[PROOFSTEP]
let g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm.comp ((z : ℂ) • ((conjAe : ℂ →ₐ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ))]
[GOAL]
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
⊢ LinearMap.ker f = ⊥
[PROOFSTEP]
suffices ((z : ℂ).im⁻¹ • g).comp f = LinearMap.id by exact LinearMap.ker_eq_bot_of_inverse this
[GOAL]
g✝ : SL(2, ℤ)
z : ℍ
this✝¹ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this✝ : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
this : LinearMap.comp ((↑z).im⁻¹ • g) f = LinearMap.id
⊢ LinearMap.ker f = ⊥
[PROOFSTEP]
exact LinearMap.ker_eq_bot_of_inverse this
[GOAL]
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
⊢ LinearMap.comp ((↑z).im⁻¹ • g) f = LinearMap.id
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
⊢ ∀ (x : Fin 2 → ℝ), ↑(LinearMap.comp ((↑z).im⁻¹ • g) f) x = ↑LinearMap.id x
[PROOFSTEP]
intro c
[GOAL]
case h
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
c : Fin 2 → ℝ
⊢ ↑(LinearMap.comp ((↑z).im⁻¹ • g) f) c = ↑LinearMap.id c
[PROOFSTEP]
have hz : (z : ℂ).im ≠ 0 := z.2.ne'
[GOAL]
case h
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ ↑(LinearMap.comp ((↑z).im⁻¹ • g) f) c = ↑LinearMap.id c
[PROOFSTEP]
rw [LinearMap.comp_apply, LinearMap.smul_apply, LinearMap.id_apply]
[GOAL]
case h
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ • ↑g (↑f c) = c
[PROOFSTEP]
ext i
[GOAL]
case h.h
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
i : Fin 2
⊢ ((↑z).im⁻¹ • ↑g (↑f c)) i = c i
[PROOFSTEP]
dsimp only [Pi.smul_apply, LinearMap.pi_apply, smul_eq_mul]
[GOAL]
case h.h
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
i : Fin 2
⊢ (↑z).im⁻¹ *
      ↑(vecCons imLm ![LinearMap.comp imLm (↑z • ↑↑↑conjAe)] i)
        (↑(LinearMap.smulRight (LinearMap.proj 0) ↑z + LinearMap.smulRight (LinearMap.proj 1) 1) c) =
    c i
[PROOFSTEP]
fin_cases i
[GOAL]
case h.h.head
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ *
      ↑(vecCons imLm ![LinearMap.comp imLm (↑z • ↑↑↑conjAe)] { val := 0, isLt := (_ : 0 < 2) })
        (↑(LinearMap.smulRight (LinearMap.proj 0) ↑z + LinearMap.smulRight (LinearMap.proj 1) 1) c) =
    c { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
show (z : ℂ).im⁻¹ * (f c).im = c 0
[GOAL]
case h.h.head
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ * (↑f c).im = c 0
[PROOFSTEP]
rw [f_def, add_im, ofReal_mul_im, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel hz, mul_one]
[GOAL]
case h.h.tail.head
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ *
      ↑(vecCons imLm ![LinearMap.comp imLm (↑z • ↑↑↑conjAe)] { val := 1, isLt := (_ : (fun a => a < 2) 1) })
        (↑(LinearMap.smulRight (LinearMap.proj 0) ↑z + LinearMap.smulRight (LinearMap.proj 1) 1) c) =
    c { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
show (z : ℂ).im⁻¹ * ((z : ℂ) * conj (f c)).im = c 1
[GOAL]
case h.h.tail.head
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ * (↑z * ↑(starRingEnd ((fun x => ℂ) c)) (↑f c)).im = c 1
[PROOFSTEP]
rw [f_def, RingHom.map_add, RingHom.map_mul, mul_add, mul_left_comm, mul_conj, conj_ofReal, conj_ofReal, ← ofReal_mul,
  add_im, ofReal_im, zero_add, inv_mul_eq_iff_eq_mul₀ hz]
[GOAL]
case h.h.tail.head
g✝ : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, LinearMap.comp imLm (↑z • ↑↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z * ↑(c 1)).im = (↑z).im * c 1
[PROOFSTEP]
simp only [ofReal_im, ofReal_re, mul_im, zero_add, mul_zero]
[GOAL]
g : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
hf : LinearMap.ker f = ⊥
⊢ Tendsto (↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p) cofinite atTop
[PROOFSTEP]
have hf' : ClosedEmbedding f :=
  by
  have := @LinearEquiv.closedEmbedding_of_injective ℝ _ (Fin 2 → ℝ) _ _ ℂ _ _ _ f
  exact this hf
[GOAL]
g : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
hf : LinearMap.ker f = ⊥
⊢ ClosedEmbedding ↑f
[PROOFSTEP]
have := @LinearEquiv.closedEmbedding_of_injective ℝ _ (Fin 2 → ℝ) _ _ ℂ _ _ _ f
[GOAL]
g : SL(2, ℤ)
z : ℍ
this✝¹ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this✝ : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
hf : LinearMap.ker f = ⊥
this : LinearMap.ker f = ⊥ → ∀ [inst : FiniteDimensional ℝ (Fin 2 → ℝ)], ClosedEmbedding ↑f
⊢ ClosedEmbedding ↑f
[PROOFSTEP]
exact this hf
[GOAL]
g : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
hf : LinearMap.ker f = ⊥
hf' : ClosedEmbedding ↑f
⊢ Tendsto (↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p) cofinite atTop
[PROOFSTEP]
have h₂ : Tendsto (fun p : Fin 2 → ℤ => ((↑) : ℤ → ℝ) ∘ p) cofinite (cocompact _) :=
  by
  convert Tendsto.pi_map_coprodᵢ fun _ => Int.tendsto_coe_cofinite
  · rw [coprodᵢ_cofinite]
  · rw [coprodᵢ_cocompact]
[GOAL]
g : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
hf : LinearMap.ker f = ⊥
hf' : ClosedEmbedding ↑f
⊢ Tendsto (fun p => Int.cast ∘ p) cofinite (cocompact (Fin 2 → ℝ))
[PROOFSTEP]
convert Tendsto.pi_map_coprodᵢ fun _ => Int.tendsto_coe_cofinite
[GOAL]
case h.e'_4
g : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
hf : LinearMap.ker f = ⊥
hf' : ClosedEmbedding ↑f
⊢ cofinite = Filter.coprodᵢ fun x => cofinite
[PROOFSTEP]
rw [coprodᵢ_cofinite]
[GOAL]
case h.e'_5
g : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
hf : LinearMap.ker f = ⊥
hf' : ClosedEmbedding ↑f
⊢ cocompact (Fin 2 → ℝ) = Filter.coprodᵢ fun x => cocompact ℝ
[PROOFSTEP]
rw [coprodᵢ_cocompact]
[GOAL]
g : SL(2, ℤ)
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := LinearMap.smulRight π₀ ↑z + LinearMap.smulRight π₁ 1
f_def : ↑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => ↑normSq (↑(p 0) * ↑z + ↑(p 1))) = ↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p
hf : LinearMap.ker f = ⊥
hf' : ClosedEmbedding ↑f
h₂ : Tendsto (fun p => Int.cast ∘ p) cofinite (cocompact (Fin 2 → ℝ))
⊢ Tendsto (↑normSq ∘ ↑f ∘ fun p => Int.cast ∘ p) cofinite atTop
[PROOFSTEP]
exact tendsto_normSq_cocompact_atTop.comp (hf'.tendsto_cocompact.comp h₂)
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ (Fin 2 → ℝ) ≃ₗ[ℝ] Fin 2 → ℝ
[PROOFSTEP]
refine'
  LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 → ℝ)
    (GeneralLinearGroup.toLinear (planeConformalMatrix (cd 0 : ℝ) (-(cd 1 : ℝ)) _))
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ↑(cd 0) ^ 2 + (-↑(cd 1)) ^ 2 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ¬cd 0 ^ 2 + (-cd 1) ^ 2 = 0
[PROOFSTEP]
rw [neg_sq]
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ¬cd 0 ^ 2 + cd 1 ^ 2 = 0
[PROOFSTEP]
exact hcd.sq_add_sq_ne_zero
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ Tendsto (fun g => ↑(lcRow0 cd) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)
[PROOFSTEP]
let mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, (-(1 : ℤ) : ℝ)], (↑) ∘ cd]
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ cd]
⊢ Tendsto (fun g => ↑(lcRow0 cd) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)
[PROOFSTEP]
have hmB : Continuous mB := by
  refine' continuous_matrix _
  simp only [Fin.forall_fin_two, continuous_const, continuous_id', of_apply, cons_val_zero, cons_val_one, and_self_iff]
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ cd]
⊢ Continuous mB
[PROOFSTEP]
refine' continuous_matrix _
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ cd]
⊢ ∀ (i j : Fin 2), Continuous fun a => mB a i j
[PROOFSTEP]
simp only [Fin.forall_fin_two, continuous_const, continuous_id', of_apply, cons_val_zero, cons_val_one, and_self_iff]
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
⊢ Tendsto (fun g => ↑(lcRow0 cd) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)
[PROOFSTEP]
refine' Filter.Tendsto.of_tendsto_comp _ (comap_cocompact_le hmB)
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
⊢ Tendsto (mB ∘ fun g => ↑(lcRow0 cd) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
[PROOFSTEP]
let f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g : Matrix _ _ ℤ) ((↑) : ℤ → ℝ)
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
⊢ Tendsto (mB ∘ fun g => ↑(lcRow0 cd) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
[PROOFSTEP]
have cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m : Matrix (Fin 2) (Fin 2) ℤ => Matrix.map m ((↑) : ℤ → ℝ)) cofinite (cocompact _) := by
  simpa only [coprodᵢ_cofinite, coprodᵢ_cocompact] using
    Tendsto.pi_map_coprodᵢ fun _ : Fin 2 => Tendsto.pi_map_coprodᵢ fun _ : Fin 2 => Int.tendsto_coe_cofinite
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
⊢ Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
[PROOFSTEP]
simpa only [coprodᵢ_cofinite, coprodᵢ_cocompact] using
  Tendsto.pi_map_coprodᵢ fun _ : Fin 2 => Tendsto.pi_map_coprodᵢ fun _ : Fin 2 => Int.tendsto_coe_cofinite
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
⊢ Tendsto (mB ∘ fun g => ↑(lcRow0 cd) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
[PROOFSTEP]
have hf₁ : Tendsto f₁ cofinite (cocompact _) :=
  cocompact_ℝ_to_cofinite_ℤ_matrix.comp Subtype.coe_injective.tendsto_cofinite
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
⊢ Tendsto (mB ∘ fun g => ↑(lcRow0 cd) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
[PROOFSTEP]
have hf₂ : ClosedEmbedding (lcRow0Extend hcd) := (lcRow0Extend hcd).toContinuousLinearEquiv.toHomeomorph.closedEmbedding
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₂ : ClosedEmbedding ↑(lcRow0Extend hcd)
⊢ Tendsto (mB ∘ fun g => ↑(lcRow0 cd) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
[PROOFSTEP]
convert hf₂.tendsto_cocompact.comp (hf₁.comp Subtype.coe_injective.tendsto_cofinite) using 1
[GOAL]
case h.e'_3.h
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₂ : ClosedEmbedding ↑(lcRow0Extend hcd)
⊢ (mB ∘ fun g => ↑(lcRow0 cd) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) =
    ↑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a
[PROOFSTEP]
ext ⟨g, rfl⟩ i j : 3
[GOAL]
case h.e'_3.h.h.mk.a.h
g✝ : SL(2, ℤ)
z : ℍ
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : ClosedEmbedding ↑(lcRow0Extend hcd)
i j : Fin 2
⊢ (mB ∘ fun g_1 => ↑(lcRow0 (↑g 1)) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1))
      { val := g, property := (_ : ↑g 1 = ↑g 1) } i j =
    (↑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) { val := g, property := (_ : ↑g 1 = ↑g 1) } i j
[PROOFSTEP]
fin_cases i <;> [fin_cases j; skip]
  -- the following are proved by `simp`, but it is replaced by `simp only` to avoid timeouts.
[GOAL]
case h.e'_3.h.h.mk.a.h
g✝ : SL(2, ℤ)
z : ℍ
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : ClosedEmbedding ↑(lcRow0Extend hcd)
i j : Fin 2
⊢ (mB ∘ fun g_1 => ↑(lcRow0 (↑g 1)) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1))
      { val := g, property := (_ : ↑g 1 = ↑g 1) } i j =
    (↑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) { val := g, property := (_ : ↑g 1 = ↑g 1) } i j
[PROOFSTEP]
fin_cases i
[GOAL]
case h.e'_3.h.h.mk.a.h.head
g✝ : SL(2, ℤ)
z : ℍ
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : ClosedEmbedding ↑(lcRow0Extend hcd)
j : Fin 2
⊢ (mB ∘ fun g_1 => ↑(lcRow0 (↑g 1)) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1))
      { val := g, property := (_ : ↑g 1 = ↑g 1) } { val := 0, isLt := (_ : 0 < 2) } j =
    (↑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) { val := g, property := (_ : ↑g 1 = ↑g 1) }
      { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.e'_3.h.h.mk.a.h.tail.head
g✝ : SL(2, ℤ)
z : ℍ
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : ClosedEmbedding ↑(lcRow0Extend hcd)
j : Fin 2
⊢ (mB ∘ fun g_1 => ↑(lcRow0 (↑g 1)) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1))
      { val := g, property := (_ : ↑g 1 = ↑g 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } j =
    (↑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) { val := g, property := (_ : ↑g 1 = ↑g 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
skip
[GOAL]
case h.e'_3.h.h.mk.a.h.head.head
g✝ : SL(2, ℤ)
z : ℍ
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : ClosedEmbedding ↑(lcRow0Extend hcd)
⊢ (mB ∘ fun g_1 => ↑(lcRow0 (↑g 1)) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1))
      { val := g, property := (_ : ↑g 1 = ↑g 1) } { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    (↑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) { val := g, property := (_ : ↑g 1 = ↑g 1) }
      { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp only [mulVec, dotProduct, Fin.sum_univ_two, coe_matrix_coe, Int.coe_castRingHom, lcRow0_apply, Function.comp_apply,
  cons_val_zero, lcRow0Extend_apply, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv,
  GeneralLinearGroup.coe_toLinear, planeConformalMatrix_val, neg_neg, mulVecLin_apply, cons_val_one, head_cons,
  of_apply, Fin.mk_zero, Fin.mk_one]
[GOAL]
case h.e'_3.h.h.mk.a.h.head.tail.head
g✝ : SL(2, ℤ)
z : ℍ
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : ClosedEmbedding ↑(lcRow0Extend hcd)
⊢ (mB ∘ fun g_1 => ↑(lcRow0 (↑g 1)) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1))
      { val := g, property := (_ : ↑g 1 = ↑g 1) } { val := 0, isLt := (_ : 0 < 2) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    (↑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) { val := g, property := (_ : ↑g 1 = ↑g 1) }
      { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
convert congr_arg (fun n : ℤ => (-n : ℝ)) g.det_coe.symm using 1
[GOAL]
case h.e'_3
g✝ : SL(2, ℤ)
z : ℍ
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : ClosedEmbedding ↑(lcRow0Extend hcd)
⊢ (↑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) { val := g, property := (_ : ↑g 1 = ↑g 1) } { val := 0, isLt := (_ : 0 < 2) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    -↑(Matrix.det ↑g)
[PROOFSTEP]
simp only [mulVec, dotProduct, Fin.sum_univ_two, Matrix.det_fin_two, Function.comp_apply, Subtype.coe_mk,
  lcRow0Extend_apply, cons_val_zero, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv,
  GeneralLinearGroup.coe_toLinear, planeConformalMatrix_val, mulVecLin_apply, cons_val_one, head_cons, map_apply,
  neg_mul, Int.cast_sub, Int.cast_mul, neg_sub, of_apply, Fin.mk_zero, Fin.mk_one]
[GOAL]
case h.e'_3
g✝ : SL(2, ℤ)
z : ℍ
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : ClosedEmbedding ↑(lcRow0Extend hcd)
⊢ -(↑(↑g 1 1) * ↑(↑g 0 0)) + ↑(↑g 1 0) * ↑(↑g 0 1) = ↑(↑g 0 1) * ↑(↑g 1 0) - ↑(↑g 0 0) * ↑(↑g 1 1)
[PROOFSTEP]
ring
[GOAL]
case h.e'_3.h.h.mk.a.h.tail.head
g✝ : SL(2, ℤ)
z : ℍ
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g) Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m => Matrix.map m Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => ↑of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : ClosedEmbedding ↑(lcRow0Extend hcd)
j : Fin 2
⊢ (mB ∘ fun g_1 => ↑(lcRow0 (↑g 1)) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1))
      { val := g, property := (_ : ↑g 1 = ↑g 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } j =
    (↑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) { val := g, property := (_ : ↑g 1 = ↑g 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
rfl
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
⊢ ↑(g • z) =
    ↑(↑(lcRow0 p) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) +
      (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))
[PROOFSTEP]
have nonZ1 : (p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2 ≠ 0 := by exact_mod_cast hp.sq_add_sq_ne_zero
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
⊢ ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
[PROOFSTEP]
exact_mod_cast hp.sq_add_sq_ne_zero
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
⊢ ↑(g • z) =
    ↑(↑(lcRow0 p) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) +
      (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))
[PROOFSTEP]
have : ((↑) : ℤ → ℝ) ∘ p ≠ 0 := fun h => hp.ne_zero (by ext i; simpa using congr_fun h i)
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
h : Int.cast ∘ p = 0
⊢ p = 0
[PROOFSTEP]
ext i
[GOAL]
case h
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
h : Int.cast ∘ p = 0
i : Fin 2
⊢ p i = OfNat.ofNat 0 i
[PROOFSTEP]
simpa using congr_fun h i
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
⊢ ↑(g • z) =
    ↑(↑(lcRow0 p) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) +
      (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))
[PROOFSTEP]
have nonZ2 : (p 0 : ℂ) * z + p 1 ≠ 0 := by simpa using linear_ne_zero _ z this
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
⊢ ↑(p 0) * ↑z + ↑(p 1) ≠ 0
[PROOFSTEP]
simpa using linear_ne_zero _ z this
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0
⊢ ↑(g • z) =
    ↑(↑(lcRow0 p) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) +
      (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))
[PROOFSTEP]
field_simp [nonZ1, nonZ2, denom_ne_zero, num]
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0
⊢ (↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))) =
    ((↑(p 0) * ↑(↑g 0 0) + ↑(p 1) * ↑(↑g 0 1)) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1))) +
        (↑(p 1) * ↑z - ↑(p 0)) * (↑(p 0) ^ 2 + ↑(p 1) ^ 2)) *
      denom (↑g) z
[PROOFSTEP]
rw [(by simp : (p 1 : ℂ) * z - p 0 = (p 1 * z - p 0) * ↑(Matrix.det (↑g : Matrix (Fin 2) (Fin 2) ℤ)))]
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0
⊢ ↑(p 1) * ↑z - ↑(p 0) = (↑(p 1) * ↑z - ↑(p 0)) * ↑(Matrix.det ↑g)
[PROOFSTEP]
simp
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0
⊢ (↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))) =
    ((↑(p 0) * ↑(↑g 0 0) + ↑(p 1) * ↑(↑g 0 1)) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1))) +
        (↑(p 1) * ↑z - ↑(p 0)) * ↑(Matrix.det ↑g) * (↑(p 0) ^ 2 + ↑(p 1) ^ 2)) *
      denom (↑g) z
[PROOFSTEP]
rw [← hg, det_fin_two]
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0
⊢ (↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) *
      ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * (↑(↑g 1 0) * ↑z + ↑(↑g 1 1)))) =
    ((↑(↑g 1 0) * ↑(↑g 0 0) + ↑(↑g 1 1) * ↑(↑g 0 1)) *
          ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * (↑(↑g 1 0) * ↑z + ↑(↑g 1 1))) +
        (↑(↑g 1 1) * ↑z - ↑(↑g 1 0)) * ↑(↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) * (↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2)) *
      denom (↑g) z
[PROOFSTEP]
simp only [Int.coe_castRingHom, coe_matrix_coe, Int.cast_mul, ofReal_int_cast, map_apply, denom, Int.cast_sub,
  coe_GLPos_coe_GL_coe_matrix, coe'_apply_complex]
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0
⊢ (↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) *
      ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * (↑(↑g 1 0) * ↑z + ↑(↑g 1 1)))) =
    ((↑(↑g 1 0) * ↑(↑g 0 0) + ↑(↑g 1 1) * ↑(↑g 0 1)) *
          ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * (↑(↑g 1 0) * ↑z + ↑(↑g 1 1))) +
        (↑(↑g 1 1) * ↑z - ↑(↑g 1 0)) * (↑(↑g 0 0) * ↑(↑g 1 1) - ↑(↑g 0 1) * ↑(↑g 1 0)) *
          (↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2)) *
      (↑(↑g 1 0) * ↑z + ↑(↑g 1 1))
[PROOFSTEP]
ring
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ Tendsto (fun g => |UpperHalfPlane.re (↑g • z)|) cofinite atTop
[PROOFSTEP]
suffices Tendsto (fun g : (fun g : SL(2, ℤ) => (↑ₘg) 1) ⁻¹' { p } => ((g : SL(2, ℤ)) • z).re) cofinite (cocompact ℝ) by
  exact tendsto_norm_cocompact_atTop.comp this
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : Tendsto (fun g => UpperHalfPlane.re (↑g • z)) cofinite (cocompact ℝ)
⊢ Tendsto (fun g => |UpperHalfPlane.re (↑g • z)|) cofinite atTop
[PROOFSTEP]
exact tendsto_norm_cocompact_atTop.comp this
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ Tendsto (fun g => UpperHalfPlane.re (↑g • z)) cofinite (cocompact ℝ)
[PROOFSTEP]
have : ((p 0 : ℝ) ^ 2 + (p 1 : ℝ) ^ 2)⁻¹ ≠ 0 := by
  apply inv_ne_zero
  exact_mod_cast hp.sq_add_sq_ne_zero
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0
[PROOFSTEP]
apply inv_ne_zero
[GOAL]
case h
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
[PROOFSTEP]
exact_mod_cast hp.sq_add_sq_ne_zero
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0
⊢ Tendsto (fun g => UpperHalfPlane.re (↑g • z)) cofinite (cocompact ℝ)
[PROOFSTEP]
let f := Homeomorph.mulRight₀ _ this
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0
f : ℝ ≃ₜ ℝ := Homeomorph.mulRight₀ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ this
⊢ Tendsto (fun g => UpperHalfPlane.re (↑g • z)) cofinite (cocompact ℝ)
[PROOFSTEP]
let ff := Homeomorph.addRight (((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1))).re
[GOAL]
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0
f : ℝ ≃ₜ ℝ := Homeomorph.mulRight₀ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ this
ff : ℝ ≃ₜ ℝ := Homeomorph.addRight ((↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))).re
⊢ Tendsto (fun g => UpperHalfPlane.re (↑g • z)) cofinite (cocompact ℝ)
[PROOFSTEP]
convert (f.trans ff).closedEmbedding.tendsto_cocompact.comp (tendsto_lcRow0 hp) with _ _ g
[GOAL]
case h.e'_3.h.h
g✝ : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0
f : ℝ ≃ₜ ℝ := Homeomorph.mulRight₀ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ this
ff : ℝ ≃ₜ ℝ := Homeomorph.addRight ((↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))).re
e_1✝ : ↑((fun g => ↑g 1) ⁻¹' {p}) = { g // ↑g 1 = p }
g : ↑((fun g => ↑g 1) ⁻¹' {p})
⊢ UpperHalfPlane.re (↑g • z) =
    (↑(Homeomorph.trans f ff) ∘ fun g => ↑(lcRow0 p) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) g
[PROOFSTEP]
change
  ((g : SL(2, ℤ)) • z).re =
    lcRow0 p ↑(↑g : SL(2, ℝ)) / ((p 0 : ℝ) ^ 2 + (p 1 : ℝ) ^ 2) +
      Complex.re (((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1)))
[GOAL]
case h.e'_3.h.h
g✝ : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0
f : ℝ ≃ₜ ℝ := Homeomorph.mulRight₀ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ this
ff : ℝ ≃ₜ ℝ := Homeomorph.addRight ((↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))).re
e_1✝ : ↑((fun g => ↑g 1) ⁻¹' {p}) = { g // ↑g 1 = p }
g : ↑((fun g => ↑g 1) ⁻¹' {p})
⊢ UpperHalfPlane.re (↑g • z) =
    ↑(lcRow0 p) ↑(↑(SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) +
      ((↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))).re
[PROOFSTEP]
exact_mod_cast congr_arg Complex.re (smul_eq_lcRow0_add z hp g.2)
[GOAL]
g : SL(2, ℤ)
z : ℍ
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
[PROOFSTEP]
classical
let s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
have hs : s.Nonempty := ⟨![1, 1], isCoprime_one_left⟩
obtain ⟨p, hp_coprime, hp⟩ := Filter.Tendsto.exists_within_forall_le hs (tendsto_normSq_coprime_pair z)
obtain ⟨g, -, hg⟩ := bottom_row_surj hp_coprime
refine' ⟨g, fun g' => _⟩
rw [SpecialLinearGroup.im_smul_eq_div_normSq, SpecialLinearGroup.im_smul_eq_div_normSq, div_le_div_left]
· simpa [← hg] using hp ((↑ₘg') 1) (bottom_row_coprime g')
· exact z.im_pos
· exact normSq_denom_pos g' z
· exact normSq_denom_pos g z
[GOAL]
g : SL(2, ℤ)
z : ℍ
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
[PROOFSTEP]
let s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
[GOAL]
g : SL(2, ℤ)
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
[PROOFSTEP]
have hs : s.Nonempty := ⟨![1, 1], isCoprime_one_left⟩
[GOAL]
g : SL(2, ℤ)
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : Set.Nonempty s
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
[PROOFSTEP]
obtain ⟨p, hp_coprime, hp⟩ := Filter.Tendsto.exists_within_forall_le hs (tendsto_normSq_coprime_pair z)
[GOAL]
case intro.intro
g : SL(2, ℤ)
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : Set.Nonempty s
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ (a : Fin 2 → ℤ), a ∈ s → ↑normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ ↑normSq (↑(a 0) * ↑z + ↑(a 1))
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
[PROOFSTEP]
obtain ⟨g, -, hg⟩ := bottom_row_surj hp_coprime
[GOAL]
case intro.intro.intro.intro
g✝ : SL(2, ℤ)
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : Set.Nonempty s
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ (a : Fin 2 → ℤ), a ∈ s → ↑normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ ↑normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g => ↑g 1) g = p
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
[PROOFSTEP]
refine' ⟨g, fun g' => _⟩
[GOAL]
case intro.intro.intro.intro
g✝ : SL(2, ℤ)
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : Set.Nonempty s
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ (a : Fin 2 → ℤ), a ∈ s → ↑normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ ↑normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g => ↑g 1) g = p
g' : SL(2, ℤ)
⊢ UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
[PROOFSTEP]
rw [SpecialLinearGroup.im_smul_eq_div_normSq, SpecialLinearGroup.im_smul_eq_div_normSq, div_le_div_left]
[GOAL]
case intro.intro.intro.intro
g✝ : SL(2, ℤ)
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : Set.Nonempty s
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ (a : Fin 2 → ℤ), a ∈ s → ↑normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ ↑normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g => ↑g 1) g = p
g' : SL(2, ℤ)
⊢ ↑normSq (denom (↑g) z) ≤ ↑normSq (denom (↑g') z)
[PROOFSTEP]
simpa [← hg] using hp ((↑ₘg') 1) (bottom_row_coprime g')
[GOAL]
case intro.intro.intro.intro.ha
g✝ : SL(2, ℤ)
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : Set.Nonempty s
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ (a : Fin 2 → ℤ), a ∈ s → ↑normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ ↑normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g => ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < UpperHalfPlane.im z
[PROOFSTEP]
exact z.im_pos
[GOAL]
case intro.intro.intro.intro.hb
g✝ : SL(2, ℤ)
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : Set.Nonempty s
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ (a : Fin 2 → ℤ), a ∈ s → ↑normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ ↑normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g => ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < ↑normSq (denom (↑g') z)
[PROOFSTEP]
exact normSq_denom_pos g' z
[GOAL]
case intro.intro.intro.intro.hc
g✝ : SL(2, ℤ)
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : Set.Nonempty s
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ (a : Fin 2 → ℤ), a ∈ s → ↑normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ ↑normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g => ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < ↑normSq (denom (↑g) z)
[PROOFSTEP]
exact normSq_denom_pos g z
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ∃ g, ↑g 1 = cd ∧ ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
[PROOFSTEP]
haveI : Nonempty { g : SL(2, ℤ) // (↑ₘg) 1 = cd } :=
  let ⟨x, hx⟩ := bottom_row_surj hcd
  ⟨⟨x, hx.2⟩⟩
[GOAL]
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
⊢ ∃ g, ↑g 1 = cd ∧ ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
[PROOFSTEP]
obtain ⟨g, hg⟩ := Filter.Tendsto.exists_forall_le (tendsto_abs_re_smul z hcd)
[GOAL]
case intro
g✝ : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
g : { g // ↑g 1 = cd }
hg : ∀ (a : { g // ↑g 1 = cd }), |UpperHalfPlane.re (↑g • z)| ≤ |UpperHalfPlane.re (↑a • z)|
⊢ ∃ g, ↑g 1 = cd ∧ ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
[PROOFSTEP]
refine' ⟨g, g.2, _⟩
[GOAL]
case intro
g✝ : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
g : { g // ↑g 1 = cd }
hg : ∀ (a : { g // ↑g 1 = cd }), |UpperHalfPlane.re (↑g • z)| ≤ |UpperHalfPlane.re (↑a • z)|
⊢ ∀ (g' : SL(2, ℤ)), ↑↑g 1 = ↑g' 1 → |UpperHalfPlane.re (↑g • z)| ≤ |UpperHalfPlane.re (g' • z)|
[PROOFSTEP]
intro g1 hg1
[GOAL]
case intro
g✝ : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
g : { g // ↑g 1 = cd }
hg : ∀ (a : { g // ↑g 1 = cd }), |UpperHalfPlane.re (↑g • z)| ≤ |UpperHalfPlane.re (↑a • z)|
g1 : SL(2, ℤ)
hg1 : ↑↑g 1 = ↑g1 1
⊢ |UpperHalfPlane.re (↑g • z)| ≤ |UpperHalfPlane.re (g1 • z)|
[PROOFSTEP]
have : g1 ∈ (fun g : SL(2, ℤ) => (↑ₘg) 1) ⁻¹' { cd } :=
  by
  rw [Set.mem_preimage, Set.mem_singleton_iff]
  exact Eq.trans hg1.symm (Set.mem_singleton_iff.mp (Set.mem_preimage.mp g.2))
[GOAL]
g✝ : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
g : { g // ↑g 1 = cd }
hg : ∀ (a : { g // ↑g 1 = cd }), |UpperHalfPlane.re (↑g • z)| ≤ |UpperHalfPlane.re (↑a • z)|
g1 : SL(2, ℤ)
hg1 : ↑↑g 1 = ↑g1 1
⊢ g1 ∈ (fun g => ↑g 1) ⁻¹' {cd}
[PROOFSTEP]
rw [Set.mem_preimage, Set.mem_singleton_iff]
[GOAL]
g✝ : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
g : { g // ↑g 1 = cd }
hg : ∀ (a : { g // ↑g 1 = cd }), |UpperHalfPlane.re (↑g • z)| ≤ |UpperHalfPlane.re (↑a • z)|
g1 : SL(2, ℤ)
hg1 : ↑↑g 1 = ↑g1 1
⊢ ↑g1 1 = cd
[PROOFSTEP]
exact Eq.trans hg1.symm (Set.mem_singleton_iff.mp (Set.mem_preimage.mp g.2))
[GOAL]
case intro
g✝ : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this✝ : Nonempty { g // ↑g 1 = cd }
g : { g // ↑g 1 = cd }
hg : ∀ (a : { g // ↑g 1 = cd }), |UpperHalfPlane.re (↑g • z)| ≤ |UpperHalfPlane.re (↑a • z)|
g1 : SL(2, ℤ)
hg1 : ↑↑g 1 = ↑g1 1
this : g1 ∈ (fun g => ↑g 1) ⁻¹' {cd}
⊢ |UpperHalfPlane.re (↑g • z)| ≤ |UpperHalfPlane.re (g1 • z)|
[PROOFSTEP]
exact hg ⟨g1, this⟩
[GOAL]
g : SL(2, ℤ)
z : ℍ
n : ℤ
⊢ ↑(T ^ n • z) = ↑z + ↑n
[PROOFSTEP]
rw [sl_moeb, UpperHalfPlane.coe_smul]
[GOAL]
g : SL(2, ℤ)
z : ℍ
n : ℤ
⊢ num (↑(T ^ n)) z / denom (↑(T ^ n)) z = ↑z + ↑n
[PROOFSTEP]
simp [coe_T_zpow, denom, num, -map_zpow]
[GOAL]
g : SL(2, ℤ)
z : ℍ
n : ℤ
⊢ UpperHalfPlane.re (T ^ n • z) = UpperHalfPlane.re z + ↑n
[PROOFSTEP]
rw [← coe_re, coe_T_zpow_smul_eq, add_re, int_cast_re, coe_re]
[GOAL]
g : SL(2, ℤ)
z : ℍ
n : ℤ
⊢ UpperHalfPlane.im (T ^ n • z) = UpperHalfPlane.im z
[PROOFSTEP]
rw [← coe_im, coe_T_zpow_smul_eq, add_im, int_cast_im, add_zero, coe_im]
[GOAL]
g : SL(2, ℤ)
z : ℍ
⊢ UpperHalfPlane.re (T • z) = UpperHalfPlane.re z + 1
[PROOFSTEP]
simpa using re_T_zpow_smul z 1
[GOAL]
g : SL(2, ℤ)
z : ℍ
⊢ UpperHalfPlane.im (T • z) = UpperHalfPlane.im z
[PROOFSTEP]
simpa using im_T_zpow_smul z 1
[GOAL]
g : SL(2, ℤ)
z : ℍ
⊢ UpperHalfPlane.re (T⁻¹ • z) = UpperHalfPlane.re z - 1
[PROOFSTEP]
simpa using re_T_zpow_smul z (-1)
[GOAL]
g : SL(2, ℤ)
z : ℍ
⊢ UpperHalfPlane.im (T⁻¹ • z) = UpperHalfPlane.im z
[PROOFSTEP]
simpa using im_T_zpow_smul z (-1)
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z
[PROOFSTEP]
have had := g.det_coe
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : det ↑g = 1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z
[PROOFSTEP]
replace had : (↑ₘg) 0 0 * (↑ₘg) 1 1 = 1
[GOAL]
case had
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : det ↑g = 1
⊢ ↑g 0 0 * ↑g 1 1 = 1
[PROOFSTEP]
rw [det_fin_two, hc] at had
[GOAL]
case had
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 0 = 1
⊢ ↑g 0 0 * ↑g 1 1 = 1
[PROOFSTEP]
linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z
[PROOFSTEP]
rcases Int.eq_one_or_neg_one_of_mul_eq_one' had with (⟨ha, hd⟩ | ⟨ha, hd⟩)
[GOAL]
case inl.intro
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z
[PROOFSTEP]
use(↑ₘg) 0 1
[GOAL]
case h
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ∀ (z : ℍ), g • z = T ^ ↑g 0 1 • z
[PROOFSTEP]
suffices g = T ^ (↑ₘg) 0 1 by intro z; conv_lhs => rw [this]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
this : g = T ^ ↑g 0 1
⊢ ∀ (z : ℍ), g • z = T ^ ↑g 0 1 • z
[PROOFSTEP]
intro z
[GOAL]
g : SL(2, ℤ)
z✝ : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
this : g = T ^ ↑g 0 1
z : ℍ
⊢ g • z = T ^ ↑g 0 1 • z
[PROOFSTEP]
conv_lhs => rw [this]
[GOAL]
g : SL(2, ℤ)
z✝ : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
this : g = T ^ ↑g 0 1
z : ℍ
| g • z
[PROOFSTEP]
rw [this]
[GOAL]
g : SL(2, ℤ)
z✝ : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
this : g = T ^ ↑g 0 1
z : ℍ
| g • z
[PROOFSTEP]
rw [this]
[GOAL]
g : SL(2, ℤ)
z✝ : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
this : g = T ^ ↑g 0 1
z : ℍ
| g • z
[PROOFSTEP]
rw [this]
[GOAL]
case h
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ g = T ^ ↑g 0 1
[PROOFSTEP]
ext i j
[GOAL]
case h.a
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
i j : Fin 2
⊢ ↑g i j = ↑(T ^ ↑g 0 1) i j
[PROOFSTEP]
fin_cases i
[GOAL]
case h.a.head
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
j : Fin 2
⊢ ↑g { val := 0, isLt := (_ : 0 < 2) } j = ↑(T ^ ↑g 0 1) { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.a.tail.head
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
j : Fin 2
⊢ ↑g { val := 1, isLt := (_ : (fun a => a < 2) 1) } j = ↑(T ^ ↑g 0 1) { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.a.head.head
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑(T ^ ↑g 0 1) { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]
[GOAL]
case h.a.head.tail.head
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑(T ^ ↑g 0 1) { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]
[GOAL]
case h.a.tail.head.head
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑(T ^ ↑g 0 1) { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]
[GOAL]
case h.a.tail.head.tail.head
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑(T ^ ↑g 0 1) { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]
[GOAL]
case inr.intro
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z
[PROOFSTEP]
use-((↑ₘg) 0 1)
[GOAL]
case h
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ∀ (z : ℍ), g • z = T ^ (-↑g 0 1) • z
[PROOFSTEP]
suffices g = -T ^ (-((↑ₘg) 0 1)) by intro z; conv_lhs => rw [this, SL_neg_smul]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
this : g = -T ^ (-↑g 0 1)
⊢ ∀ (z : ℍ), g • z = T ^ (-↑g 0 1) • z
[PROOFSTEP]
intro z
[GOAL]
g : SL(2, ℤ)
z✝ : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
this : g = -T ^ (-↑g 0 1)
z : ℍ
⊢ g • z = T ^ (-↑g 0 1) • z
[PROOFSTEP]
conv_lhs => rw [this, SL_neg_smul]
[GOAL]
g : SL(2, ℤ)
z✝ : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
this : g = -T ^ (-↑g 0 1)
z : ℍ
| g • z
[PROOFSTEP]
rw [this, SL_neg_smul]
[GOAL]
g : SL(2, ℤ)
z✝ : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
this : g = -T ^ (-↑g 0 1)
z : ℍ
| g • z
[PROOFSTEP]
rw [this, SL_neg_smul]
[GOAL]
g : SL(2, ℤ)
z✝ : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
this : g = -T ^ (-↑g 0 1)
z : ℍ
| g • z
[PROOFSTEP]
rw [this, SL_neg_smul]
[GOAL]
case h
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ g = -T ^ (-↑g 0 1)
[PROOFSTEP]
ext i j
[GOAL]
case h.a
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
i j : Fin 2
⊢ ↑g i j = ↑(-T ^ (-↑g 0 1)) i j
[PROOFSTEP]
fin_cases i
[GOAL]
case h.a.head
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
j : Fin 2
⊢ ↑g { val := 0, isLt := (_ : 0 < 2) } j = ↑(-T ^ (-↑g 0 1)) { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.a.tail.head
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
j : Fin 2
⊢ ↑g { val := 1, isLt := (_ : (fun a => a < 2) 1) } j =
    ↑(-T ^ (-↑g 0 1)) { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.a.head.head
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ↑g { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑(-T ^ (-↑g 0 1)) { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]
[GOAL]
case h.a.head.tail.head
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ↑g { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑(-T ^ (-↑g 0 1)) { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]
[GOAL]
case h.a.tail.head.head
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ↑g { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑(-T ^ (-↑g 0 1)) { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]
[GOAL]
case h.a.tail.head.tail.head
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ↑g { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑(-T ^ (-↑g 0 1)) { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
⊢ g = T ^ ↑g 0 0 * S * T ^ ↑g 1 1
[PROOFSTEP]
have hg := g.det_coe.symm
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : 1 = det ↑g
⊢ g = T ^ ↑g 0 0 * S * T ^ ↑g 1 1
[PROOFSTEP]
replace hg : (↑ₘg) 0 1 = (↑ₘg) 0 0 * (↑ₘg) 1 1 - 1
[GOAL]
case hg
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : 1 = det ↑g
⊢ ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
[PROOFSTEP]
rw [det_fin_two, hc] at hg
[GOAL]
case hg
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : 1 = ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 1
⊢ ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
[PROOFSTEP]
linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ g = T ^ ↑g 0 0 * S * T ^ ↑g 1 1
[PROOFSTEP]
refine' Subtype.ext _
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ↑g = ↑(T ^ ↑g 0 0 * S * T ^ ↑g 1 1)
[PROOFSTEP]
conv_lhs => rw [Matrix.eta_fin_two (↑ₘg)]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
| ↑g
[PROOFSTEP]
rw [Matrix.eta_fin_two (↑ₘg)]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
| ↑g
[PROOFSTEP]
rw [Matrix.eta_fin_two (↑ₘg)]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
| ↑g
[PROOFSTEP]
rw [Matrix.eta_fin_two (↑ₘg)]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ↑of ![![↑g 0 0, ↑g 0 1], ![↑g 1 0, ↑g 1 1]] = ↑(T ^ ↑g 0 0 * S * T ^ ↑g 1 1)
[PROOFSTEP]
rw [hc, hg]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ↑of ![![↑g 0 0, ↑g 0 0 * ↑g 1 1 - 1], ![1, ↑g 1 1]] = ↑(T ^ ↑g 0 0 * S * T ^ ↑g 1 1)
[PROOFSTEP]
simp only [coe_mul, coe_T_zpow, coe_S, mul_fin_two]
  -- Porting note: Was `congrm !![_, _; _, _] <;> ring`.
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ↑of ![![↑g 0 0, ↑g 0 0 * ↑g 1 1 - 1], ![1, ↑g 1 1]] =
    ↑of
      ![![(1 * 0 + ↑g 0 0 * 1) * 1 + (1 * -1 + ↑g 0 0 * 0) * 0,
          (1 * 0 + ↑g 0 0 * 1) * ↑g 1 1 + (1 * -1 + ↑g 0 0 * 0) * 1],
        ![(0 * 0 + 1 * 1) * 1 + (0 * -1 + 1 * 0) * 0, (0 * 0 + 1 * 1) * ↑g 1 1 + (0 * -1 + 1 * 0) * 1]]
[PROOFSTEP]
congr! 3 <;> [skip; congr! 1; congr! 2]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ↑of ![![↑g 0 0, ↑g 0 0 * ↑g 1 1 - 1], ![1, ↑g 1 1]] =
    ↑of
      ![![(1 * 0 + ↑g 0 0 * 1) * 1 + (1 * -1 + ↑g 0 0 * 0) * 0,
          (1 * 0 + ↑g 0 0 * 1) * ↑g 1 1 + (1 * -1 + ↑g 0 0 * 0) * 1],
        ![(0 * 0 + 1 * 1) * 1 + (0 * -1 + 1 * 0) * 0, (0 * 0 + 1 * 1) * ↑g 1 1 + (0 * -1 + 1 * 0) * 1]]
[PROOFSTEP]
congr! 3
[GOAL]
case h.e'_6.h.e'_3.h.e'_3
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ↑g 0 0 = (1 * 0 + ↑g 0 0 * 1) * 1 + (1 * -1 + ↑g 0 0 * 0) * 0
[PROOFSTEP]
skip
[GOAL]
case h.e'_6.h.e'_3.h.e'_4
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ![↑g 0 0 * ↑g 1 1 - 1] = ![(1 * 0 + ↑g 0 0 * 1) * ↑g 1 1 + (1 * -1 + ↑g 0 0 * 0) * 1]
[PROOFSTEP]
congr! 1
[GOAL]
case h.e'_6.h.e'_4.h.e'_3
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ![1, ↑g 1 1] = ![(0 * 0 + 1 * 1) * 1 + (0 * -1 + 1 * 0) * 0, (0 * 0 + 1 * 1) * ↑g 1 1 + (0 * -1 + 1 * 0) * 1]
[PROOFSTEP]
congr! 2
[GOAL]
case h.e'_6.h.e'_3.h.e'_3
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ↑g 0 0 = (1 * 0 + ↑g 0 0 * 1) * 1 + (1 * -1 + ↑g 0 0 * 0) * 0
[PROOFSTEP]
ring
[GOAL]
case h.e'_6.h.e'_3.h.e'_4.h.e'_3
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ↑g 0 0 * ↑g 1 1 - 1 = (1 * 0 + ↑g 0 0 * 1) * ↑g 1 1 + (1 * -1 + ↑g 0 0 * 0) * 1
[PROOFSTEP]
ring
[GOAL]
case h.e'_6.h.e'_4.h.e'_3.h.e'_4.h.e'_3
g : SL(2, ℤ)
z : ℍ
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ↑g 1 1 = (0 * 0 + 1 * 1) * ↑g 1 1 + (0 * -1 + 1 * 0) * 1
[PROOFSTEP]
ring
[GOAL]
g : SL(2, ℤ)
z : ℍ
h : 1 < ↑normSq ↑z
⊢ ↑normSq ↑(S • z) < 1
[PROOFSTEP]
simpa [coe_S, num, denom] using (inv_lt_inv z.normSq_pos zero_lt_one).mpr h
[GOAL]
g : SL(2, ℤ)
z : ℍ
h : ↑normSq ↑z < 1
⊢ UpperHalfPlane.im z < UpperHalfPlane.im (S • z)
[PROOFSTEP]
have : z.im < z.im / normSq (z : ℂ) := by
  have imz : 0 < z.im := im_pos z
  apply (lt_div_iff z.normSq_pos).mpr
  nlinarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
h : ↑normSq ↑z < 1
⊢ UpperHalfPlane.im z < UpperHalfPlane.im z / ↑normSq ↑z
[PROOFSTEP]
have imz : 0 < z.im := im_pos z
[GOAL]
g : SL(2, ℤ)
z : ℍ
h : ↑normSq ↑z < 1
imz : 0 < UpperHalfPlane.im z
⊢ UpperHalfPlane.im z < UpperHalfPlane.im z / ↑normSq ↑z
[PROOFSTEP]
apply (lt_div_iff z.normSq_pos).mpr
[GOAL]
g : SL(2, ℤ)
z : ℍ
h : ↑normSq ↑z < 1
imz : 0 < UpperHalfPlane.im z
⊢ UpperHalfPlane.im z * ↑normSq ↑z < UpperHalfPlane.im z
[PROOFSTEP]
nlinarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
h : ↑normSq ↑z < 1
this : UpperHalfPlane.im z < UpperHalfPlane.im z / ↑normSq ↑z
⊢ UpperHalfPlane.im z < UpperHalfPlane.im (S • z)
[PROOFSTEP]
convert this
[GOAL]
case h.e'_4
g : SL(2, ℤ)
z : ℍ
h : ↑normSq ↑z < 1
this : UpperHalfPlane.im z < UpperHalfPlane.im z / ↑normSq ↑z
⊢ UpperHalfPlane.im (S • z) = UpperHalfPlane.im z / ↑normSq ↑z
[PROOFSTEP]
simp only [SpecialLinearGroup.im_smul_eq_div_normSq]
[GOAL]
case h.e'_4
g : SL(2, ℤ)
z : ℍ
h : ↑normSq ↑z < 1
this : UpperHalfPlane.im z < UpperHalfPlane.im z / ↑normSq ↑z
⊢ UpperHalfPlane.im z / ↑normSq (denom (↑S) z) = UpperHalfPlane.im z / ↑normSq ↑z
[PROOFSTEP]
simp [denom, coe_S]
[GOAL]
g : SL(2, ℤ)
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ |2 * UpperHalfPlane.re z| < 1
[PROOFSTEP]
rw [abs_mul, abs_two, ← lt_div_iff' (zero_lt_two' ℝ)]
[GOAL]
g : SL(2, ℤ)
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ |UpperHalfPlane.re z| < 1 / 2
[PROOFSTEP]
exact h.2
[GOAL]
g : SL(2, ℤ)
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ 3 < 4 * UpperHalfPlane.im z ^ 2
[PROOFSTEP]
have : 1 < z.re * z.re + z.im * z.im := by simpa [Complex.normSq_apply] using h.1
[GOAL]
g : SL(2, ℤ)
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ 1 < UpperHalfPlane.re z * UpperHalfPlane.re z + UpperHalfPlane.im z * UpperHalfPlane.im z
[PROOFSTEP]
simpa [Complex.normSq_apply] using h.1
[GOAL]
g : SL(2, ℤ)
z : ℍ
h : z ∈ 𝒟ᵒ
this : 1 < UpperHalfPlane.re z * UpperHalfPlane.re z + UpperHalfPlane.im z * UpperHalfPlane.im z
⊢ 3 < 4 * UpperHalfPlane.im z ^ 2
[PROOFSTEP]
have := h.2
[GOAL]
g : SL(2, ℤ)
z : ℍ
h : z ∈ 𝒟ᵒ
this✝ : 1 < UpperHalfPlane.re z * UpperHalfPlane.re z + UpperHalfPlane.im z * UpperHalfPlane.im z
this : |UpperHalfPlane.re z| < 1 / 2
⊢ 3 < 4 * UpperHalfPlane.im z ^ 2
[PROOFSTEP]
cases abs_cases z.re
[GOAL]
case inl
g : SL(2, ℤ)
z : ℍ
h : z ∈ 𝒟ᵒ
this✝ : 1 < UpperHalfPlane.re z * UpperHalfPlane.re z + UpperHalfPlane.im z * UpperHalfPlane.im z
this : |UpperHalfPlane.re z| < 1 / 2
h✝ : |UpperHalfPlane.re z| = UpperHalfPlane.re z ∧ 0 ≤ UpperHalfPlane.re z
⊢ 3 < 4 * UpperHalfPlane.im z ^ 2
[PROOFSTEP]
nlinarith
[GOAL]
case inr
g : SL(2, ℤ)
z : ℍ
h : z ∈ 𝒟ᵒ
this✝ : 1 < UpperHalfPlane.re z * UpperHalfPlane.re z + UpperHalfPlane.im z * UpperHalfPlane.im z
this : |UpperHalfPlane.re z| < 1 / 2
h✝ : |UpperHalfPlane.re z| = -UpperHalfPlane.re z ∧ UpperHalfPlane.re z < 0
⊢ 3 < 4 * UpperHalfPlane.im z ^ 2
[PROOFSTEP]
nlinarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
⊢ 1 < ↑normSq ↑(T ^ n • z)
[PROOFSTEP]
have hz₁ : 1 < z.re * z.re + z.im * z.im := hz.1
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < UpperHalfPlane.re z * UpperHalfPlane.re z + UpperHalfPlane.im z * UpperHalfPlane.im z
⊢ 1 < ↑normSq ↑(T ^ n • z)
[PROOFSTEP]
have hzn := Int.nneg_mul_add_sq_of_abs_le_one n (abs_two_mul_re_lt_one_of_mem_fdo hz).le
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < UpperHalfPlane.re z * UpperHalfPlane.re z + UpperHalfPlane.im z * UpperHalfPlane.im z
hzn : 0 ≤ ↑n * (2 * UpperHalfPlane.re z) + ↑n * ↑n
⊢ 1 < ↑normSq ↑(T ^ n • z)
[PROOFSTEP]
have : 1 < (z.re + ↑n) * (z.re + ↑n) + z.im * z.im := by linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < UpperHalfPlane.re z * UpperHalfPlane.re z + UpperHalfPlane.im z * UpperHalfPlane.im z
hzn : 0 ≤ ↑n * (2 * UpperHalfPlane.re z) + ↑n * ↑n
⊢ 1 < (UpperHalfPlane.re z + ↑n) * (UpperHalfPlane.re z + ↑n) + UpperHalfPlane.im z * UpperHalfPlane.im z
[PROOFSTEP]
linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < UpperHalfPlane.re z * UpperHalfPlane.re z + UpperHalfPlane.im z * UpperHalfPlane.im z
hzn : 0 ≤ ↑n * (2 * UpperHalfPlane.re z) + ↑n * ↑n
this : 1 < (UpperHalfPlane.re z + ↑n) * (UpperHalfPlane.re z + ↑n) + UpperHalfPlane.im z * UpperHalfPlane.im z
⊢ 1 < ↑normSq ↑(T ^ n • z)
[PROOFSTEP]
simpa [coe_T_zpow, normSq, num, denom, -map_zpow]
[GOAL]
g : SL(2, ℤ)
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
⊢ n = 0
[PROOFSTEP]
suffices |(n : ℝ)| < 1 by rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this
[GOAL]
g : SL(2, ℤ)
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
this : |↑n| < 1
⊢ n = 0
[PROOFSTEP]
rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this
[GOAL]
g : SL(2, ℤ)
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
⊢ |↑n| < 1
[PROOFSTEP]
have h₁ := hz.2
[GOAL]
g : SL(2, ℤ)
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |UpperHalfPlane.re z| < 1 / 2
⊢ |↑n| < 1
[PROOFSTEP]
have h₂ := hg.2
[GOAL]
g : SL(2, ℤ)
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |UpperHalfPlane.re z| < 1 / 2
h₂ : |UpperHalfPlane.re (T ^ n • z)| < 1 / 2
⊢ |↑n| < 1
[PROOFSTEP]
rw [re_T_zpow_smul] at h₂
[GOAL]
g : SL(2, ℤ)
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |UpperHalfPlane.re z| < 1 / 2
h₂ : |UpperHalfPlane.re z + ↑n| < 1 / 2
⊢ |↑n| < 1
[PROOFSTEP]
calc
  |(n : ℝ)| ≤ |z.re| + |z.re + (n : ℝ)| := abs_add' (n : ℝ) z.re
  _ < 1 / 2 + 1 / 2 := (add_lt_add h₁ h₂)
  _ = 1 := add_halves 1
[GOAL]
g : SL(2, ℤ)
z✝ z : ℍ
⊢ ∃ g, g • z ∈ 𝒟
[PROOFSTEP]
obtain ⟨g₀, hg₀⟩ := exists_max_im z
[GOAL]
case intro
g : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
⊢ ∃ g, g • z ∈ 𝒟
[PROOFSTEP]
obtain ⟨g, hg, hg'⟩ := exists_row_one_eq_and_min_re z (bottom_row_coprime g₀)
[GOAL]
case intro.intro.intro
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
⊢ ∃ g, g • z ∈ 𝒟
[PROOFSTEP]
refine'
  ⟨g, _⟩
    -- `g` has same max im property as `g₀`
[GOAL]
case intro.intro.intro
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
⊢ g • z ∈ 𝒟
[PROOFSTEP]
have hg₀' : ∀ g' : SL(2, ℤ), (g' • z).im ≤ (g • z).im :=
  by
  have hg'' : (g • z).im = (g₀ • z).im := by
    rw [SpecialLinearGroup.im_smul_eq_div_normSq, SpecialLinearGroup.im_smul_eq_div_normSq, denom_apply, denom_apply,
      hg]
  simpa only [hg''] using hg₀
[GOAL]
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
⊢ ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
[PROOFSTEP]
have hg'' : (g • z).im = (g₀ • z).im := by
  rw [SpecialLinearGroup.im_smul_eq_div_normSq, SpecialLinearGroup.im_smul_eq_div_normSq, denom_apply, denom_apply, hg]
[GOAL]
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
⊢ UpperHalfPlane.im (g • z) = UpperHalfPlane.im (g₀ • z)
[PROOFSTEP]
rw [SpecialLinearGroup.im_smul_eq_div_normSq, SpecialLinearGroup.im_smul_eq_div_normSq, denom_apply, denom_apply, hg]
[GOAL]
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
hg'' : UpperHalfPlane.im (g • z) = UpperHalfPlane.im (g₀ • z)
⊢ ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
[PROOFSTEP]
simpa only [hg''] using hg₀
[GOAL]
case intro.intro.intro
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
⊢ g • z ∈ 𝒟
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.intro.left
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
⊢ 1 ≤ ↑normSq ↑(g • z)
[PROOFSTEP]
contrapose! hg₀'
[GOAL]
case intro.intro.intro.left
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
hg₀' : ↑normSq ↑(g • z) < 1
⊢ ∃ g', UpperHalfPlane.im (g • z) < UpperHalfPlane.im (g' • z)
[PROOFSTEP]
refine' ⟨S * g, _⟩
[GOAL]
case intro.intro.intro.left
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
hg₀' : ↑normSq ↑(g • z) < 1
⊢ UpperHalfPlane.im (g • z) < UpperHalfPlane.im ((S * g) • z)
[PROOFSTEP]
rw [mul_smul]
[GOAL]
case intro.intro.intro.left
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
hg₀' : ↑normSq ↑(g • z) < 1
⊢ UpperHalfPlane.im (g • z) < UpperHalfPlane.im (S • g • z)
[PROOFSTEP]
exact im_lt_im_S_smul hg₀'
[GOAL]
case intro.intro.intro.right
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
⊢ |UpperHalfPlane.re (g • z)| ≤ 1 / 2
[PROOFSTEP]
show
  |(g • z).re| ≤
    1 /
      2
        -- if not, then either `T` or `T'` decrease |Re|.
[GOAL]
case intro.intro.intro.right
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
⊢ |UpperHalfPlane.re (g • z)| ≤ 1 / 2
[PROOFSTEP]
rw [abs_le]
[GOAL]
case intro.intro.intro.right
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
⊢ -(1 / 2) ≤ UpperHalfPlane.re (g • z) ∧ UpperHalfPlane.re (g • z) ≤ 1 / 2
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.intro.right.left
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
⊢ -(1 / 2) ≤ UpperHalfPlane.re (g • z)
[PROOFSTEP]
contrapose! hg'
[GOAL]
case intro.intro.intro.right.left
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : UpperHalfPlane.re (g • z) < -(1 / 2)
⊢ ∃ g', ↑g 1 = ↑g' 1 ∧ |UpperHalfPlane.re (g' • z)| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
refine' ⟨T * g, (T_mul_apply_one _).symm, _⟩
[GOAL]
case intro.intro.intro.right.left
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : UpperHalfPlane.re (g • z) < -(1 / 2)
⊢ |UpperHalfPlane.re ((T * g) • z)| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
rw [mul_smul, re_T_smul]
[GOAL]
case intro.intro.intro.right.left
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : UpperHalfPlane.re (g • z) < -(1 / 2)
⊢ |UpperHalfPlane.re (g • z) + 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
cases abs_cases ((g • z).re + 1)
[GOAL]
case intro.intro.intro.right.left.inl
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : UpperHalfPlane.re (g • z) < -(1 / 2)
h✝ : |UpperHalfPlane.re (g • z) + 1| = UpperHalfPlane.re (g • z) + 1 ∧ 0 ≤ UpperHalfPlane.re (g • z) + 1
⊢ |UpperHalfPlane.re (g • z) + 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
cases abs_cases (g • z).re
[GOAL]
case intro.intro.intro.right.left.inr
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : UpperHalfPlane.re (g • z) < -(1 / 2)
h✝ : |UpperHalfPlane.re (g • z) + 1| = -(UpperHalfPlane.re (g • z) + 1) ∧ UpperHalfPlane.re (g • z) + 1 < 0
⊢ |UpperHalfPlane.re (g • z) + 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
cases abs_cases (g • z).re
[GOAL]
case intro.intro.intro.right.left.inl.inl
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : UpperHalfPlane.re (g • z) < -(1 / 2)
h✝¹ : |UpperHalfPlane.re (g • z) + 1| = UpperHalfPlane.re (g • z) + 1 ∧ 0 ≤ UpperHalfPlane.re (g • z) + 1
h✝ : |UpperHalfPlane.re (g • z)| = UpperHalfPlane.re (g • z) ∧ 0 ≤ UpperHalfPlane.re (g • z)
⊢ |UpperHalfPlane.re (g • z) + 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
linarith
[GOAL]
case intro.intro.intro.right.left.inl.inr
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : UpperHalfPlane.re (g • z) < -(1 / 2)
h✝¹ : |UpperHalfPlane.re (g • z) + 1| = UpperHalfPlane.re (g • z) + 1 ∧ 0 ≤ UpperHalfPlane.re (g • z) + 1
h✝ : |UpperHalfPlane.re (g • z)| = -UpperHalfPlane.re (g • z) ∧ UpperHalfPlane.re (g • z) < 0
⊢ |UpperHalfPlane.re (g • z) + 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
linarith
[GOAL]
case intro.intro.intro.right.left.inr.inl
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : UpperHalfPlane.re (g • z) < -(1 / 2)
h✝¹ : |UpperHalfPlane.re (g • z) + 1| = -(UpperHalfPlane.re (g • z) + 1) ∧ UpperHalfPlane.re (g • z) + 1 < 0
h✝ : |UpperHalfPlane.re (g • z)| = UpperHalfPlane.re (g • z) ∧ 0 ≤ UpperHalfPlane.re (g • z)
⊢ |UpperHalfPlane.re (g • z) + 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
linarith
[GOAL]
case intro.intro.intro.right.left.inr.inr
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : UpperHalfPlane.re (g • z) < -(1 / 2)
h✝¹ : |UpperHalfPlane.re (g • z) + 1| = -(UpperHalfPlane.re (g • z) + 1) ∧ UpperHalfPlane.re (g • z) + 1 < 0
h✝ : |UpperHalfPlane.re (g • z)| = -UpperHalfPlane.re (g • z) ∧ UpperHalfPlane.re (g • z) < 0
⊢ |UpperHalfPlane.re (g • z) + 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
linarith
[GOAL]
case intro.intro.intro.right.right
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |UpperHalfPlane.re (g • z)| ≤ |UpperHalfPlane.re (g' • z)|
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
⊢ UpperHalfPlane.re (g • z) ≤ 1 / 2
[PROOFSTEP]
contrapose! hg'
[GOAL]
case intro.intro.intro.right.right
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : 1 / 2 < UpperHalfPlane.re (g • z)
⊢ ∃ g', ↑g 1 = ↑g' 1 ∧ |UpperHalfPlane.re (g' • z)| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
refine' ⟨T⁻¹ * g, (T_inv_mul_apply_one _).symm, _⟩
[GOAL]
case intro.intro.intro.right.right
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : 1 / 2 < UpperHalfPlane.re (g • z)
⊢ |UpperHalfPlane.re ((T⁻¹ * g) • z)| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
rw [mul_smul, re_T_inv_smul]
[GOAL]
case intro.intro.intro.right.right
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : 1 / 2 < UpperHalfPlane.re (g • z)
⊢ |UpperHalfPlane.re (g • z) - 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
cases abs_cases ((g • z).re - 1)
[GOAL]
case intro.intro.intro.right.right.inl
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : 1 / 2 < UpperHalfPlane.re (g • z)
h✝ : |UpperHalfPlane.re (g • z) - 1| = UpperHalfPlane.re (g • z) - 1 ∧ 0 ≤ UpperHalfPlane.re (g • z) - 1
⊢ |UpperHalfPlane.re (g • z) - 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
cases abs_cases (g • z).re
[GOAL]
case intro.intro.intro.right.right.inr
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : 1 / 2 < UpperHalfPlane.re (g • z)
h✝ : |UpperHalfPlane.re (g • z) - 1| = -(UpperHalfPlane.re (g • z) - 1) ∧ UpperHalfPlane.re (g • z) - 1 < 0
⊢ |UpperHalfPlane.re (g • z) - 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
cases abs_cases (g • z).re
[GOAL]
case intro.intro.intro.right.right.inl.inl
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : 1 / 2 < UpperHalfPlane.re (g • z)
h✝¹ : |UpperHalfPlane.re (g • z) - 1| = UpperHalfPlane.re (g • z) - 1 ∧ 0 ≤ UpperHalfPlane.re (g • z) - 1
h✝ : |UpperHalfPlane.re (g • z)| = UpperHalfPlane.re (g • z) ∧ 0 ≤ UpperHalfPlane.re (g • z)
⊢ |UpperHalfPlane.re (g • z) - 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
linarith
[GOAL]
case intro.intro.intro.right.right.inl.inr
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : 1 / 2 < UpperHalfPlane.re (g • z)
h✝¹ : |UpperHalfPlane.re (g • z) - 1| = UpperHalfPlane.re (g • z) - 1 ∧ 0 ≤ UpperHalfPlane.re (g • z) - 1
h✝ : |UpperHalfPlane.re (g • z)| = -UpperHalfPlane.re (g • z) ∧ UpperHalfPlane.re (g • z) < 0
⊢ |UpperHalfPlane.re (g • z) - 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
linarith
[GOAL]
case intro.intro.intro.right.right.inr.inl
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : 1 / 2 < UpperHalfPlane.re (g • z)
h✝¹ : |UpperHalfPlane.re (g • z) - 1| = -(UpperHalfPlane.re (g • z) - 1) ∧ UpperHalfPlane.re (g • z) - 1 < 0
h✝ : |UpperHalfPlane.re (g • z)| = UpperHalfPlane.re (g • z) ∧ 0 ≤ UpperHalfPlane.re (g • z)
⊢ |UpperHalfPlane.re (g • z) - 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
linarith
[GOAL]
case intro.intro.intro.right.right.inr.inr
g✝ : SL(2, ℤ)
z✝ z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g₀ • z)
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), UpperHalfPlane.im (g' • z) ≤ UpperHalfPlane.im (g • z)
hg' : 1 / 2 < UpperHalfPlane.re (g • z)
h✝¹ : |UpperHalfPlane.re (g • z) - 1| = -(UpperHalfPlane.re (g • z) - 1) ∧ UpperHalfPlane.re (g • z) - 1 < 0
h✝ : |UpperHalfPlane.re (g • z)| = -UpperHalfPlane.re (g • z) ∧ UpperHalfPlane.re (g • z) < 0
⊢ |UpperHalfPlane.re (g • z) - 1| < |UpperHalfPlane.re (g • z)|
[PROOFSTEP]
linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ |↑g 1 0| ≤ 1
[PROOFSTEP]
let c' : ℤ := (↑ₘg) 1 0
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
⊢ |↑g 1 0| ≤ 1
[PROOFSTEP]
let c : ℝ := (c' : ℝ)
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
⊢ |↑g 1 0| ≤ 1
[PROOFSTEP]
suffices 3 * c ^ 2 < 4
  by
  rw [← Int.cast_pow, ← Int.cast_three, ← Int.cast_four, ← Int.cast_mul, Int.cast_lt] at this
  replace this : c' ^ 2 ≤ 1 ^ 2; · linarith
  rwa [sq_le_sq, abs_one] at this
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : 3 * c ^ 2 < 4
⊢ |↑g 1 0| ≤ 1
[PROOFSTEP]
rw [← Int.cast_pow, ← Int.cast_three, ← Int.cast_four, ← Int.cast_mul, Int.cast_lt] at this
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : 3 * c' ^ 2 < 4
⊢ |↑g 1 0| ≤ 1
[PROOFSTEP]
replace this : c' ^ 2 ≤ 1 ^ 2
[GOAL]
case this
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : 3 * c' ^ 2 < 4
⊢ c' ^ 2 ≤ 1 ^ 2
[PROOFSTEP]
linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c' ^ 2 ≤ 1 ^ 2
⊢ |↑g 1 0| ≤ 1
[PROOFSTEP]
rwa [sq_le_sq, abs_one] at this
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
⊢ 3 * c ^ 2 < 4
[PROOFSTEP]
suffices c ≠ 0 → 9 * c ^ 4 < 16 by
  rcases eq_or_ne c 0 with (hc | hc)
  · rw [hc]; norm_num
  · refine' (abs_lt_of_sq_lt_sq' _ (by norm_num)).2
    specialize this hc
    linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
⊢ 3 * c ^ 2 < 4
[PROOFSTEP]
rcases eq_or_ne c 0 with (hc | hc)
[GOAL]
case inl
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c = 0
⊢ 3 * c ^ 2 < 4
[PROOFSTEP]
rw [hc]
[GOAL]
case inl
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c = 0
⊢ 3 * 0 ^ 2 < 4
[PROOFSTEP]
norm_num
[GOAL]
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c ≠ 0
⊢ 3 * c ^ 2 < 4
[PROOFSTEP]
refine' (abs_lt_of_sq_lt_sq' _ (by norm_num)).2
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c ≠ 0
⊢ 0 ≤ 4
[PROOFSTEP]
norm_num
[GOAL]
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c ≠ 0
⊢ (3 * c ^ 2) ^ 2 < 4 ^ 2
[PROOFSTEP]
specialize this hc
[GOAL]
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
this : 9 * c ^ 4 < 16
⊢ (3 * c ^ 2) ^ 2 < 4 ^ 2
[PROOFSTEP]
linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
⊢ c ≠ 0 → 9 * c ^ 4 < 16
[PROOFSTEP]
intro hc
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
⊢ 9 * c ^ 4 < 16
[PROOFSTEP]
replace hc : 0 < c ^ 4
[GOAL]
case hc
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
⊢ 0 < c ^ 4
[PROOFSTEP]
change 0 < c ^ (2 * 2)
[GOAL]
case hc
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
⊢ 0 < c ^ (2 * 2)
[PROOFSTEP]
rw [pow_mul]
[GOAL]
case hc
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
⊢ 0 < (c ^ 2) ^ 2
[PROOFSTEP]
apply sq_pos_of_pos (sq_pos_of_ne_zero _ hc)
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : 0 < c ^ 4
⊢ 9 * c ^ 4 < 16
[PROOFSTEP]
have h₁ :=
  mul_lt_mul_of_pos_right
    (mul_lt_mul'' (three_lt_four_mul_im_sq_of_mem_fdo hg) (three_lt_four_mul_im_sq_of_mem_fdo hz) (by linarith)
      (by linarith))
    hc
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : 0 < c ^ 4
⊢ 0 ≤ 3
[PROOFSTEP]
linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : 0 < c ^ 4
⊢ 0 ≤ 3
[PROOFSTEP]
linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : 0 < c ^ 4
h₁ : 3 * 3 * c ^ 4 < 4 * UpperHalfPlane.im (g • z) ^ 2 * (4 * UpperHalfPlane.im z ^ 2) * c ^ 4
⊢ 9 * c ^ 4 < 16
[PROOFSTEP]
have h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1 :=
  div_le_one_of_le (pow_four_le_pow_two_of_pow_two_le (UpperHalfPlane.c_mul_im_sq_le_normSq_denom z g)) (sq_nonneg _)
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : 0 < c ^ 4
h₁ : 3 * 3 * c ^ 4 < 4 * UpperHalfPlane.im (g • z) ^ 2 * (4 * UpperHalfPlane.im z ^ 2) * c ^ 4
h₂ : (c * UpperHalfPlane.im z) ^ 4 / ↑normSq (denom (↑g) z) ^ 2 ≤ 1
⊢ 9 * c ^ 4 < 16
[PROOFSTEP]
let nsq := normSq (denom g z)
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : 0 < c ^ 4
h₁ : 3 * 3 * c ^ 4 < 4 * UpperHalfPlane.im (g • z) ^ 2 * (4 * UpperHalfPlane.im z ^ 2) * c ^ 4
h₂ : (c * UpperHalfPlane.im z) ^ 4 / ↑normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : (fun x => ℝ) (denom (↑g) z) := ↑normSq (denom (↑g) z)
⊢ 9 * c ^ 4 < 16
[PROOFSTEP]
calc
  9 * c ^ 4 < c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16 := by linarith
  _ = c ^ 4 * z.im ^ 4 / nsq ^ 2 * 16 :=
    by
    rw [SpecialLinearGroup.im_smul_eq_div_normSq, div_pow]
    ring
  _ ≤ 16 := by rw [← mul_pow]; linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : 0 < c ^ 4
h₁ : 3 * 3 * c ^ 4 < 4 * UpperHalfPlane.im (g • z) ^ 2 * (4 * UpperHalfPlane.im z ^ 2) * c ^ 4
h₂ : (c * UpperHalfPlane.im z) ^ 4 / ↑normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : (fun x => ℝ) (denom (↑g) z) := ↑normSq (denom (↑g) z)
⊢ 9 * c ^ 4 < c ^ 4 * UpperHalfPlane.im z ^ 2 * UpperHalfPlane.im (g • z) ^ 2 * 16
[PROOFSTEP]
linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : 0 < c ^ 4
h₁ : 3 * 3 * c ^ 4 < 4 * UpperHalfPlane.im (g • z) ^ 2 * (4 * UpperHalfPlane.im z ^ 2) * c ^ 4
h₂ : (c * UpperHalfPlane.im z) ^ 4 / ↑normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : (fun x => ℝ) (denom (↑g) z) := ↑normSq (denom (↑g) z)
⊢ c ^ 4 * UpperHalfPlane.im z ^ 2 * UpperHalfPlane.im (g • z) ^ 2 * 16 = c ^ 4 * UpperHalfPlane.im z ^ 4 / nsq ^ 2 * 16
[PROOFSTEP]
rw [SpecialLinearGroup.im_smul_eq_div_normSq, div_pow]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : 0 < c ^ 4
h₁ : 3 * 3 * c ^ 4 < 4 * UpperHalfPlane.im (g • z) ^ 2 * (4 * UpperHalfPlane.im z ^ 2) * c ^ 4
h₂ : (c * UpperHalfPlane.im z) ^ 4 / ↑normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : (fun x => ℝ) (denom (↑g) z) := ↑normSq (denom (↑g) z)
⊢ c ^ 4 * UpperHalfPlane.im z ^ 2 * (UpperHalfPlane.im z ^ 2 / ↑normSq (denom (↑g) z) ^ 2) * 16 =
    c ^ 4 * UpperHalfPlane.im z ^ 4 / nsq ^ 2 * 16
[PROOFSTEP]
ring
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : 0 < c ^ 4
h₁ : 3 * 3 * c ^ 4 < 4 * UpperHalfPlane.im (g • z) ^ 2 * (4 * UpperHalfPlane.im z ^ 2) * c ^ 4
h₂ : (c * UpperHalfPlane.im z) ^ 4 / ↑normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : (fun x => ℝ) (denom (↑g) z) := ↑normSq (denom (↑g) z)
⊢ c ^ 4 * UpperHalfPlane.im z ^ 4 / nsq ^ 2 * 16 ≤ 16
[PROOFSTEP]
rw [← mul_pow]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : 0 < c ^ 4
h₁ : 3 * 3 * c ^ 4 < 4 * UpperHalfPlane.im (g • z) ^ 2 * (4 * UpperHalfPlane.im z ^ 2) * c ^ 4
h₂ : (c * UpperHalfPlane.im z) ^ 4 / ↑normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : (fun x => ℝ) (denom (↑g) z) := ↑normSq (denom (↑g) z)
⊢ (c * UpperHalfPlane.im z) ^ 4 / nsq ^ 2 * 16 ≤ 16
[PROOFSTEP]
linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ ↑g 1 0 = 0
[PROOFSTEP]
have hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → (↑ₘg') 1 0 ≠ 1 :=
  by
  intro g' hg'
  by_contra hc
  let a := (↑ₘg') 0 0
  let d := (↑ₘg') 1 1
  have had : T ^ (-a) * g' = S * T ^ d := by rw [g_eq_of_c_eq_one hc]; group
  let w := T ^ (-a) • g' • z
  have h₁ : w = S • T ^ d • z := by simp only [← mul_smul, had]
  replace h₁ : normSq w < 1 := h₁.symm ▸ normSq_S_smul_lt_one (one_lt_normSq_T_zpow_smul hz d)
  have h₂ : 1 < normSq w := one_lt_normSq_T_zpow_smul hg' (-a)
  linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
[PROOFSTEP]
intro g' hg'
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
⊢ ↑g' 1 0 ≠ 1
[PROOFSTEP]
by_contra hc
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
⊢ False
[PROOFSTEP]
let a := (↑ₘg') 0 0
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
⊢ False
[PROOFSTEP]
let d := (↑ₘg') 1 1
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
⊢ False
[PROOFSTEP]
have had : T ^ (-a) * g' = S * T ^ d := by rw [g_eq_of_c_eq_one hc]; group
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
⊢ T ^ (-a) * g' = S * T ^ d
[PROOFSTEP]
rw [g_eq_of_c_eq_one hc]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
⊢ T ^ (-a) * (T ^ ↑g' 0 0 * S * T ^ ↑g' 1 1) = S * T ^ d
[PROOFSTEP]
group
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
⊢ False
[PROOFSTEP]
let w := T ^ (-a) • g' • z
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
⊢ False
[PROOFSTEP]
have h₁ : w = S • T ^ d • z := by simp only [← mul_smul, had]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
⊢ w = S • T ^ d • z
[PROOFSTEP]
simp only [← mul_smul, had]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
h₁ : w = S • T ^ d • z
⊢ False
[PROOFSTEP]
replace h₁ : normSq w < 1 := h₁.symm ▸ normSq_S_smul_lt_one (one_lt_normSq_T_zpow_smul hz d)
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
h₁ : ↑normSq ↑w < 1
⊢ False
[PROOFSTEP]
have h₂ : 1 < normSq w := one_lt_normSq_T_zpow_smul hg' (-a)
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
h₁ : ↑normSq ↑w < 1
h₂ : 1 < ↑normSq ↑w
⊢ False
[PROOFSTEP]
linarith
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
⊢ ↑g 1 0 = 0
[PROOFSTEP]
have hn : (↑ₘg) 1 0 ≠ -1 := by
  intro hc
  replace hc : (↑ₘ(-g)) 1 0 = 1; · simp [← neg_eq_iff_eq_neg.mpr hc]
  replace hg : -g • z ∈ 𝒟ᵒ := (SL_neg_smul g z).symm ▸ hg
  exact hp hg hc
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
⊢ ↑g 1 0 ≠ -1
[PROOFSTEP]
intro hc
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hc : ↑g 1 0 = -1
⊢ False
[PROOFSTEP]
replace hc : (↑ₘ(-g)) 1 0 = 1
[GOAL]
case hc
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hc : ↑g 1 0 = -1
⊢ (-↑g) 1 0 = 1
[PROOFSTEP]
simp [← neg_eq_iff_eq_neg.mpr hc]
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hc : (-↑g) 1 0 = 1
⊢ False
[PROOFSTEP]
replace hg : -g • z ∈ 𝒟ᵒ := (SL_neg_smul g z).symm ▸ hg
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hc : (-↑g) 1 0 = 1
hg : -g • z ∈ 𝒟ᵒ
⊢ False
[PROOFSTEP]
exact hp hg hc
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hn : ↑g 1 0 ≠ -1
⊢ ↑g 1 0 = 0
[PROOFSTEP]
specialize hp hg
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hn : ↑g 1 0 ≠ -1
hp : ↑g 1 0 ≠ 1
⊢ ↑g 1 0 = 0
[PROOFSTEP]
rcases Int.abs_le_one_iff.mp <| abs_c_le_one hz hg with ⟨⟩
[GOAL]
case inl
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hn : ↑g 1 0 ≠ -1
hp : ↑g 1 0 ≠ 1
h✝ : ↑g 1 0 = 0
⊢ ↑g 1 0 = 0
[PROOFSTEP]
tauto
[GOAL]
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hn : ↑g 1 0 ≠ -1
hp : ↑g 1 0 ≠ 1
h✝ : ↑g 1 0 = 1 ∨ ↑g 1 0 = -1
⊢ ↑g 1 0 = 0
[PROOFSTEP]
tauto
[GOAL]
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ z = g • z
[PROOFSTEP]
obtain ⟨n, hn⟩ := exists_eq_T_zpow_of_c_eq_zero (c_eq_zero hz hg)
[GOAL]
case intro
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
n : ℤ
hn : ∀ (z : ℍ), g • z = T ^ n • z
⊢ z = g • z
[PROOFSTEP]
rw [hn] at hg ⊢
[GOAL]
case intro
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hg : T ^ n • z ∈ 𝒟ᵒ
hn : ∀ (z : ℍ), g • z = T ^ n • z
⊢ z = T ^ n • z
[PROOFSTEP]
simp [eq_zero_of_mem_fdo_of_T_zpow_mem_fdo hz hg, one_smul]