awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ ≠ 0
f : ℝ ≃ₜ ℝ :=
  Homeomorph.mulRight₀ (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ this
ff : ℝ ≃ₜ ℝ :=
  Homeomorph.addRight
    (((↑(p 1) : ℂ) * (↑z : ℂ) - (↑(p 0) : ℂ)) /
        ((HPow.hPow (α := ℂ) (β := ℕ) (↑(p 0) : ℂ) 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑(p 1) : ℂ) 2) *
          ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))).re
⊢ Tendsto
    (fun (g : (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type)) ↦
      ((↑g : SL(2, ℤ)) • z).re)
    cofinite (cocompact ℝ)
have h : (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type) =
    { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p } →
  ∀ (g : (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type)),
    ((↑g : SL(2, ℤ)) • z).re =
      Function.comp (β := ℝ) (⇑(f.trans ff) : (a : ℝ) → ℝ)
        (fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p }) ↦
          (lcRow0 p : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
            (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (↑g : SL(2, ℤ))) :
              Matrix (Fin 2) (Fin 2) ℝ))
        g
Tactic: convert! (f.trans ff).isClosedEmbedding.tendsto_cocompact.comp (tendsto_lcRow0 hp) with _ _ g
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ ≠ 0
f : ℝ ≃ₜ ℝ :=
  Homeomorph.mulRight₀ (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ this
ff : ℝ ≃ₜ ℝ :=
  Homeomorph.addRight
    (((↑(p 1) : ℂ) * (↑z : ℂ) - (↑(p 0) : ℂ)) /
        ((HPow.hPow (α := ℂ) (β := ℕ) (↑(p 0) : ℂ) 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑(p 1) : ℂ) 2) *
          ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))).re
e_1 :
  (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type) =
    { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p }
g : (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type)
⊢ ((↑g : SL(2, ℤ)) • z).re =
    Function.comp (β := ℝ) (⇑(f.trans ff) : (a : ℝ) → ℝ)
      (fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p }) ↦
        (lcRow0 p : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
          (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (↑g : SL(2, ℤ))) :
            Matrix (Fin 2) (Fin 2) ℝ))
      g
have h : ((↑g : SL(2, ℤ)) • z).re =
  HDiv.hDiv (α := ℝ)
      ((lcRow0 p : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
          (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (↑g : SL(2, ℤ))) :
            Matrix (Fin 2) (Fin 2) ℝ) :
        ℝ)
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2) +
    (((↑(p 1) : ℂ) * (↑z : ℂ) - (↑(p 0) : ℂ)) /
        ((HPow.hPow (α := ℂ) (β := ℕ) (↑(p 0) : ℂ) 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑(p 1) : ℂ) 2) *
          ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))).re
Tactic: 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)))
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)}
⊢ ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
have hs : s.Nonempty
Tactic: have hs : s.Nonempty := ⟨![1, 1], isCoprime_one_left⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
⊢ ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
have obtain : ∀ (p : Fin 2 → ℤ) (hp_coprime : p ∈ s)
  (hp :
    ∀ a ∈ s,
      LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
        ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ)),
  ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
Tactic: obtain ⟨p, hp_coprime, hp⟩ :=
    Filter.Tendsto.exists_within_forall_le hs (tendsto_normSq_coprime_pair z)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp :
  ∀ a ∈ s,
    LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
      ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ)
⊢ ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
have obtain : ∀ (g : SL(2, ℤ)) (hg : (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) g = p),
  ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
Tactic: obtain ⟨g, -, hg⟩ := bottom_row_surj hp_coprime
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp :
  ∀ a ∈ s,
    LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
      ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ)
g : SL(2, ℤ)
hg : (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) g = p
⊢ ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
have refine : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
Tactic: refine ⟨g, fun g' => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp :
  ∀ a ∈ s,
    LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
      ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ)
g : SL(2, ℤ)
hg : (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) g = p
g' : SL(2, ℤ)
⊢ (g' • z).im ≤ (g • z).im
have rw : LE.le (α := ℝ)
  ((normSq : (a : ℂ) → ℝ)
      (denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)) :
    ℝ)
  ((normSq : (a : ℂ) → ℝ)
      (denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g'))
        (↑z : ℂ)) :
    ℝ)
Tactic: rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
    div_le_div_iff_of_pos_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp :
  ∀ a ∈ s,
    LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
      ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ)
g : SL(2, ℤ)
hg : (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) g = p
g' : SL(2, ℤ)
rw :
  LE.le (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g'))
          (↑z : ℂ)) :
      ℝ)
⊢ (g' • z).im ≤ (g • z).im
have ha : 0 < z.im
Tactic: rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
    div_le_div_iff_of_pos_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp :
  ∀ a ∈ s,
    LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
      ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ)
g : SL(2, ℤ)
hg : (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) g = p
g' : SL(2, ℤ)
rw :
  LE.le (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g'))
          (↑z : ℂ)) :
      ℝ)
ha : 0 < z.im
⊢ (g' • z).im ≤ (g • z).im
have hb : LT.lt (α := ℝ) (0 : ℝ)
  ((normSq : (a : ℂ) → ℝ)
      (denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g'))
        (↑z : ℂ)) :
    ℝ)
Tactic: rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
    div_le_div_iff_of_pos_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp :
  ∀ a ∈ s,
    LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
      ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ)
g : SL(2, ℤ)
hg : (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) g = p
g' : SL(2, ℤ)
rw :
  LE.le (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g'))
          (↑z : ℂ)) :
      ℝ)
ha : 0 < z.im
hb :
  LT.lt (α := ℝ) (0 : ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g'))
          (↑z : ℂ)) :
      ℝ)
⊢ (g' • z).im ≤ (g • z).im
have hc : LT.lt (α := ℝ) (0 : ℝ)
  ((normSq : (a : ℂ) → ℝ)
      (denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)) :
    ℝ)
Tactic: rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
    div_le_div_iff_of_pos_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
let let₁ let₂ : ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
⊢ ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
have let₃ : let s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)};
∀ (hs : s.Nonempty), ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
Tactic: 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 [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
    div_le_div_iff_of_pos_left]
  · simpa [← hg] using hp (g' 1) (bottom_row_coprime g')
  · exact z.im_pos
  · exact normSq_denom_pos g' z.im_ne_zero
  · exact normSq_denom_pos g z.im_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
let let₁ let₂ : ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
let₃ :
  let s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)};
  ∀ (hs : s.Nonempty), ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
⊢ ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
have let₄ : let s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)};
∀ (hs : s.Nonempty) (p : Fin 2 → ℤ) (hp_coprime : p ∈ s)
  (hp :
    ∀ a ∈ s,
      LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
        ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ)),
  ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
Tactic: 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 [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
    div_le_div_iff_of_pos_left]
  · simpa [← hg] using hp (g' 1) (bottom_row_coprime g')
  · exact z.im_pos
  · exact normSq_denom_pos g' z.im_ne_zero
  · exact normSq_denom_pos g z.im_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
let let₁ let₂ : ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
let₃ :
  let s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)};
  ∀ (hs : s.Nonempty), ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
let₄ :
  let s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)};
  ∀ (hs : s.Nonempty) (p : Fin 2 → ℤ) (hp_coprime : p ∈ s)
    (hp :
      ∀ a ∈ s,
        LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
          ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ)),
    ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
⊢ ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
have let₅ : let s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)};
∀ (hs : s.Nonempty) (p : Fin 2 → ℤ) (hp_coprime : p ∈ s)
  (hp :
    ∀ a ∈ s,
      LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
        ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ))
  (g : SL(2, ℤ)) (hg : (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) g = p),
  ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
Tactic: 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 [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
    div_le_div_iff_of_pos_left]
  · simpa [← hg] using hp (g' 1) (bottom_row_coprime g')
  · exact z.im_pos
  · exact normSq_denom_pos g' z.im_ne_zero
  · exact normSq_denom_pos g z.im_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
let let₁ let₂ : ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
let₃ :
  let s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)};
  ∀ (hs : s.Nonempty), ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
let₄ :
  let s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)};
  ∀ (hs : s.Nonempty) (p : Fin 2 → ℤ) (hp_coprime : p ∈ s)
    (hp :
      ∀ a ∈ s,
        LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
          ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ)),
    ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
let₅ :
  let s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)};
  ∀ (hs : s.Nonempty) (p : Fin 2 → ℤ) (hp_coprime : p ∈ s)
    (hp :
      ∀ a ∈ s,
        LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
          ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ))
    (g : SL(2, ℤ)) (hg : (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) g = p),
    ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
⊢ ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
have let₆ : let s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)};
∀ (hs : s.Nonempty) (p : Fin 2 → ℤ) (hp_coprime : p ∈ s)
  (hp :
    ∀ a ∈ s,
      LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) : ℝ)
        ((normSq : (a : ℂ) → ℝ) ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) : ℝ))
  (g : SL(2, ℤ)) (hg : (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) g = p) (g' : SL(2, ℤ)),
  (g' • z).im ≤ (g • z).im
Tactic: 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 [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
    div_le_div_iff_of_pos_left]
  · simpa [← hg] using hp (g' 1) (bottom_row_coprime g')
  · exact z.im_pos
  · exact normSq_denom_pos g' z.im_ne_zero
  · exact normSq_denom_pos g z.im_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ∃ (g : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd ∧
      ∀ (g' : SL(2, ℤ)),
        (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
have this : Nonempty { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }
Tactic: haveI : Nonempty { g : SL(2, ℤ) // g 1 = cd } :=
    let ⟨x, hx⟩ := bottom_row_surj hcd
    ⟨⟨x, hx.2⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }
⊢ ∃ (g : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd ∧
      ∀ (g' : SL(2, ℤ)),
        (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
have obtain : ∀ (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd })
  (hg :
    ∀ (a : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }),
      |((↑g : SL(2, ℤ)) • z).re| ≤ |((↑a : SL(2, ℤ)) • z).re|),
  ∃ (g : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd ∧
      ∀ (g' : SL(2, ℤ)),
        (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
Tactic: obtain ⟨g, hg⟩ := Filter.Tendsto.exists_forall_le (tendsto_abs_re_smul z hcd)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }
g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }
hg :
  ∀ (a : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }),
    |((↑g : SL(2, ℤ)) • z).re| ≤ |((↑a : SL(2, ℤ)) • z).re|
⊢ ∃ (g : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd ∧
      ∀ (g' : SL(2, ℤ)),
        (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
have refine : ∀ (g' : SL(2, ℤ)),
  (↑(↑g : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 →
    |((↑g : SL(2, ℤ)) • z).re| ≤ |(g' • z).re|
Tactic: refine ⟨g, g.2, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }
g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }
hg :
  ∀ (a : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }),
    |((↑g : SL(2, ℤ)) • z).re| ≤ |((↑a : SL(2, ℤ)) • z).re|
g1 : SL(2, ℤ)
hg1 : (↑(↑g : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g1 : Matrix (Fin 2) (Fin 2) ℤ) 1
⊢ |((↑g : SL(2, ℤ)) • z).re| ≤ |(g1 • z).re|
have this₁ : Membership.mem (γ := Set SL(2, ℤ))
  (Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {cd}) g1
Tactic: 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))
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
⊢ (↑(T ^ n • z) : ℂ) = (↑z : ℂ) + (↑n : ℂ)
have rw : ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
      (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
    ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
      (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ)) =
  (↑z : ℂ) + (↑n : ℂ)
Tactic: rw [UpperHalfPlane.coe_specialLinearGroup_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
⊢ (T ^ n • z).re = z.re + (↑n : ℝ)
have rw : (↑(T ^ n • z) : ℂ).re = z.re + (↑n : ℝ)
Tactic: rw [← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re, coe_re]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
rw : (↑(T ^ n • z) : ℂ).re = z.re + (↑n : ℝ)
⊢ (T ^ n • z).re = z.re + (↑n : ℝ)
have rw₁ : ((↑z : ℂ) + (↑n : ℂ)).re = z.re + (↑n : ℝ)
Tactic: rw [← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re, coe_re]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
rw : (↑(T ^ n • z) : ℂ).re = z.re + (↑n : ℝ)
rw₁ : ((↑z : ℂ) + (↑n : ℂ)).re = z.re + (↑n : ℝ)
⊢ (T ^ n • z).re = z.re + (↑n : ℝ)
have rw₂ : (↑z : ℂ).re + Complex.re (↑n : ℂ) = z.re + (↑n : ℝ)
Tactic: rw [← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re, coe_re]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
rw : (↑(T ^ n • z) : ℂ).re = z.re + (↑n : ℝ)
rw₁ : ((↑z : ℂ) + (↑n : ℂ)).re = z.re + (↑n : ℝ)
rw₂ : (↑z : ℂ).re + Complex.re (↑n : ℂ) = z.re + (↑n : ℝ)
⊢ (T ^ n • z).re = z.re + (↑n : ℝ)
have rw₃ : (↑z : ℂ).re + (↑n : ℝ) = z.re + (↑n : ℝ)
Tactic: rw [← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re, coe_re]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
rw : (↑(T ^ n • z) : ℂ).re = z.re + (↑n : ℝ)
rw₁ : ((↑z : ℂ) + (↑n : ℂ)).re = z.re + (↑n : ℝ)
rw₂ : (↑z : ℂ).re + Complex.re (↑n : ℂ) = z.re + (↑n : ℝ)
rw₃ : (↑z : ℂ).re + (↑n : ℝ) = z.re + (↑n : ℝ)
⊢ (T ^ n • z).re = z.re + (↑n : ℝ)
have rw₄ : z.re + (↑n : ℝ) = z.re + (↑n : ℝ)
Tactic: rw [← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re, coe_re]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
⊢ (T ^ n • z).im = z.im
have rw : (↑(T ^ n • z) : ℂ).im = z.im
Tactic: rw [← coe_im, coe_T_zpow_smul_eq, add_im, intCast_im, add_zero, coe_im]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
rw : (↑(T ^ n • z) : ℂ).im = z.im
⊢ (T ^ n • z).im = z.im
have rw₁ : ((↑z : ℂ) + (↑n : ℂ)).im = z.im
Tactic: rw [← coe_im, coe_T_zpow_smul_eq, add_im, intCast_im, add_zero, coe_im]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
rw : (↑(T ^ n • z) : ℂ).im = z.im
rw₁ : ((↑z : ℂ) + (↑n : ℂ)).im = z.im
⊢ (T ^ n • z).im = z.im
have rw₂ : (↑z : ℂ).im + Complex.im (↑n : ℂ) = z.im
Tactic: rw [← coe_im, coe_T_zpow_smul_eq, add_im, intCast_im, add_zero, coe_im]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
rw : (↑(T ^ n • z) : ℂ).im = z.im
rw₁ : ((↑z : ℂ) + (↑n : ℂ)).im = z.im
rw₂ : (↑z : ℂ).im + Complex.im (↑n : ℂ) = z.im
⊢ (T ^ n • z).im = z.im
have rw₃ : (↑z : ℂ).im + 0 = z.im
Tactic: rw [← coe_im, coe_T_zpow_smul_eq, add_im, intCast_im, add_zero, coe_im]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
rw : (↑(T ^ n • z) : ℂ).im = z.im
rw₁ : ((↑z : ℂ) + (↑n : ℂ)).im = z.im
rw₂ : (↑z : ℂ).im + Complex.im (↑n : ℂ) = z.im
rw₃ : (↑z : ℂ).im + 0 = z.im
⊢ (T ^ n • z).im = z.im
have rw₄ : (↑z : ℂ).im = z.im
Tactic: rw [← coe_im, coe_T_zpow_smul_eq, add_im, intCast_im, add_zero, coe_im]