-- Mathlib/NumberTheory/Modular.lean
theorem exists_max_im : ∃ g : SL(2, ℤ), ∀ g' : SL(2, ℤ), (g' • z).im ≤ (g • z).im

Proof state:
case intro.intro.intro.intro
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ 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)

Tactic:
simpa [← hg] using hp (g' 1) (bottom_row_coprime g')

Result:
no goals

Proof state:
case intro.intro.intro.intro
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ 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, ℤ)
⊢ (g' • z).im ≤ (g • z).im

Tactic:
rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
  div_le_div_iff_of_pos_left]

Result:
case intro.intro.intro.intro
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ 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)

case intro.intro.intro.intro.ha
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ 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 < z.im

case intro.intro.intro.intro.hb
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ 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)

case intro.intro.intro.intro.hc
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ 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)

Proof state:
z : ℍ
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

Tactic:
let s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}

Result:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

Proof state:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

Tactic:
have hs : s.Nonempty := ⟨![1, 1], isCoprime_one_left⟩

Result:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

Proof state:
case intro.intro.intro.intro.hc
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ 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)

Tactic:
exact normSq_denom_pos g z

Result:
no goals

Proof state:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
⊢ ∃ g, ∀ (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)

Result:
case intro.intro
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

Proof state:
case intro.intro.intro.intro.ha
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ 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 < z.im

Tactic:
exact z.im_pos

Result:
no goals

Proof state:
case intro.intro
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

Tactic:
obtain ⟨g, -, hg⟩ := bottom_row_surj hp_coprime

Result:
case intro.intro.intro.intro
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ 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, ℤ)), (g' • z).im ≤ (g • z).im

Proof state:
case intro.intro.intro.intro.hb
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ 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)

Tactic:
exact normSq_denom_pos g' z

Result:
no goals

Proof state:
case intro.intro.intro.intro
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ 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, ℤ)), (g' • z).im ≤ (g • z).im

Tactic:
refine ⟨g, fun g' => ?_⟩

Result:
case intro.intro.intro.intro
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ 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, ℤ)
⊢ (g' • z).im ≤ (g • z).im