-- 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
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
⊢ ∃ (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, ℤ)),
  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: 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