awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
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 =
    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:
mod_cast congr_arg Complex.re (smul_eq_lcRow0_add z hp g.2)

Premises used: Int.cast, Real, HMul.hMul, UpperHalfPlane.coe, congrArg, Complex.ofReal_div._simp_1, Int.cast_pow, HSub.hSub, cast, Int.cast_add, Complex.ofReal_add, HDiv.hDiv, Complex.ofReal, Complex.re, congr_arg, HPow.hPow, HAdd.hAdd, Matrix.SpecialLinearGroup.map, Int.castRingHom, congr, Int.cast_pow._simp_1, HSMul.hSMul, Int.cast_add._simp_1, congrFun', OfNat.ofNat, Eq.symm, Subtype.val, Complex.ofReal_pow, Eq, DFunLike.coe, UpperHalfPlane.re, Eq.trans, Subtype.property, ModularGroup.lcRow0, ModularGroup.smul_eq_lcRow0_add
-- Module: Mathlib.NumberTheory.Modular
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 =
    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:
exact mod_cast congr_arg Complex.re (smul_eq_lcRow0_add z hp g.2)

Premises used: Complex.re, congr_arg, Subtype.property, ModularGroup.smul_eq_lcRow0_add
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)}
⊢ s.Nonempty

Tactic:
have hs : s.Nonempty := ⟨![1, 1], isCoprime_one_left⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd : Fin 2 → ℤ | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
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
⊢ ∃ (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)

Premises used: Filter.Tendsto.exists_within_forall_le, ModularGroup.tendsto_normSq_coprime_pair
-- Module: Mathlib.NumberTheory.Modular
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) : ℂ)) : ℝ)
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
⊢ ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

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

Premises used: ModularGroup.bottom_row_surj
-- Module: Mathlib.NumberTheory.Modular
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

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

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.Modular
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
refine : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
⊢ ∃ (g : SL(2, ℤ)), ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

Tactic:
refine ⟨g, fun g' => ?_⟩
-- Module: Mathlib.NumberTheory.Modular
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 : ℂ)) :
      ℝ)
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 : ℂ)) :
      ℝ)
⊢ (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]

Premises used: div_le_div_iff_of_pos_left, ModularGroup.im_smul_eq_div_normSq
-- Module: Mathlib.NumberTheory.Modular
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, ℤ)
⊢ 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:
simpa [← hg] using hp (g' 1) (bottom_row_coprime g')

Premises used: ModularGroup.bottom_row_coprime, OfNat.ofNat, Subtype.val
-- Module: Mathlib.NumberTheory.Modular
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, ℤ)
⊢ 0 < z.im

Tactic:
z.im_pos

Premises used: UpperHalfPlane.im_pos
-- Module: Mathlib.NumberTheory.Modular
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, ℤ)
⊢ 0 < z.im

Tactic:
exact z.im_pos

Premises used: UpperHalfPlane.im_pos
-- Module: Mathlib.NumberTheory.Modular
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, ℤ)
⊢ 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:
normSq_denom_pos g' z.im_ne_zero

Premises used: Real, UpperHalfPlane.im_ne_zero, UpperHalfPlane.normSq_denom_pos, Matrix.SpecialLinearGroup.map, Int.castRingHom, DFunLike.coe, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.Modular
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, ℤ)
⊢ 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:
exact normSq_denom_pos g' z.im_ne_zero

Premises used: Real, UpperHalfPlane.im_ne_zero, UpperHalfPlane.normSq_denom_pos, Matrix.SpecialLinearGroup.map, Int.castRingHom, DFunLike.coe, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.Modular
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, ℤ)
⊢ 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:
normSq_denom_pos g z.im_ne_zero

Premises used: Real, UpperHalfPlane.im_ne_zero, UpperHalfPlane.normSq_denom_pos, Matrix.SpecialLinearGroup.map, Int.castRingHom, DFunLike.coe, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.Modular
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, ℤ)
⊢ 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:
exact normSq_denom_pos g z.im_ne_zero

Premises used: Real, UpperHalfPlane.im_ne_zero, UpperHalfPlane.normSq_denom_pos, Matrix.SpecialLinearGroup.map, Int.castRingHom, DFunLike.coe, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ 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⟩⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }
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|
⊢ ∃ (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)

Premises used: ModularGroup.tendsto_abs_re_smul, Filter.Tendsto.exists_forall_le
-- Module: Mathlib.NumberTheory.Modular
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|

Tactic:
⟨g, g.2, ?_⟩

Premises used: And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.NumberTheory.Modular
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|
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|
⊢ ∃ (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:
refine ⟨g, g.2, ?_⟩
-- Module: Mathlib.NumberTheory.Modular
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
⊢ (↑g1 : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd

Tactic:
Eq.trans hg1.symm (Set.mem_singleton_iff.mp (Set.mem_preimage.mp g.2))

Premises used: Set.mem_singleton_iff, Iff.mp, Eq.symm, Set.mem_preimage, Eq.trans, Subtype.property
-- Module: Mathlib.NumberTheory.Modular
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
⊢ (↑g1 : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd

Tactic:
exact Eq.trans hg1.symm (Set.mem_singleton_iff.mp (Set.mem_preimage.mp g.2))

Premises used: Set.mem_singleton_iff, Iff.mp, Eq.symm, Set.mem_preimage, Eq.trans, Subtype.property
-- Module: Mathlib.NumberTheory.Modular
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
⊢ 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))
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this_1 : 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
this :
  Membership.mem (γ := Set SL(2, ℤ))
    (Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {cd}) g1
⊢ |((↑g : SL(2, ℤ)) • z).re| ≤ |(g1 • z).re|

Tactic:
hg ⟨g1, this⟩

Premises used: Subtype.mk
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this_1 : 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
this :
  Membership.mem (γ := Set SL(2, ℤ))
    (Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {cd}) g1
⊢ |((↑g : SL(2, ℤ)) • z).re| ≤ |(g1 • z).re|

Tactic:
exact hg ⟨g1, this⟩

Premises used: Subtype.mk
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
n : ℤ
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 : ℂ)
⊢ (↑(T ^ n • z) : ℂ) = (↑z : ℂ) + (↑n : ℂ)

Tactic:
rw [UpperHalfPlane.coe_specialLinearGroup_apply]

Premises used: UpperHalfPlane.coe_specialLinearGroup_apply
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
n : ℤ
⊢ ((↑((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:
simp [coe_T_zpow, -map_zpow]

Premises used: map_zpow, ModularGroup.coe_T_zpow
-- Module: Mathlib.NumberTheory.Modular
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 : ℝ)
rw₄ rw₅ : z.re + (↑n : ℝ) = z.re + (↑n : ℝ)
⊢ (T ^ n • z).re = z.re + (↑n : ℝ)

Tactic:
rw [← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re, coe_re]

Premises used: ModularGroup.coe_T_zpow_smul_eq, Complex.add_re, Complex.intCast_re, UpperHalfPlane.coe_re
-- Module: Mathlib.NumberTheory.Modular
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
rw₄ : (↑z : ℂ).im = z.im
rw₅ rw₆ : z.im = z.im
⊢ (T ^ n • z).im = z.im

Tactic:
rw [← coe_im, coe_T_zpow_smul_eq, add_im, intCast_im, add_zero, coe_im]

Premises used: Complex.add_im, ModularGroup.coe_T_zpow_smul_eq, add_zero, Complex.intCast_im, UpperHalfPlane.coe_im
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
⊢ (T • z).re = z.re + 1

Tactic:
simpa using re_T_zpow_smul z 1

Premises used: ModularGroup.re_T_zpow_smul, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
⊢ (T • z).im = z.im

Tactic:
simpa using im_T_zpow_smul z 1

Premises used: ModularGroup.im_T_zpow_smul, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
⊢ (T⁻¹ • z).re = z.re - 1

Tactic:
simpa using re_T_zpow_smul z (-1)

Premises used: ModularGroup.re_T_zpow_smul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
⊢ (T⁻¹ • z).im = z.im

Tactic:
simpa using im_T_zpow_smul z (-1)

Premises used: ModularGroup.im_T_zpow_smul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ).det = 1

Tactic:
have had := g.det_coe
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ).det = 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * 0 =
    1

Tactic:
rw [det_fin_two, hc] at had

Premises used: Matrix.det_fin_two
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * 0 =
    1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ).det = 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1

Tactic:
replace had : g 0 0 * g 1 1 = 1 := by rw [det_fin_two, hc] at had; lia