awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
⊢ z.im < HDiv.hDiv (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)

Tactic:
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
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
this : z.im < HDiv.hDiv (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
⊢ z.im <
    HDiv.hDiv (β := ℝ) z.im
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S))
            (↑z : ℂ)) :
        ℝ)

Tactic:
simpa [denom, coe_S, SpecialLinearGroup.toGL]

Premises used: UpperHalfPlane.denom, ModularGroup.coe_S, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ 𝒟ᵒ ⊆ 𝒟

Tactic:
fun _ ⟨hx, hx'⟩ ↦ ⟨hx.le, hx'.le⟩

Premises used: _private.0.ModularGroup.fdo_subset_fd.match_1, Membership.mem, LT.lt.le, Set.Subset, And.intro, ModularGroup.fd
-- Module: Mathlib.NumberTheory.Modular
Goal:
left : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑ρ : ℂ) : ℝ)
right : |ρ.re| ≤ 1 / 2
⊢ ρ ∈ 𝒟

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑ρ : ℂ) : ℝ)

Tactic:
norm_num [ρ, ← pow_two, div_pow]

Premises used: pow_two, UpperHalfPlane.ρ, div_pow
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ |ρ.re| ≤ 1 / 2

Tactic:
norm_num [ρ, ← pow_two, div_pow]

Premises used: pow_two, UpperHalfPlane.ρ, div_pow
-- Module: Mathlib.NumberTheory.Modular
Goal:
left : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑I : ℂ) : ℝ)
right : |I.re| ≤ 1 / 2
⊢ I ∈ 𝒟

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑I : ℂ) : ℝ)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ |I.re| ≤ 1 / 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
rw : |z.re| < 1 / 2
⊢ |2 * z.re| < 1

Tactic:
rw [abs_mul, abs_two, ← lt_div_iff₀' (zero_lt_two' ℝ)]

Premises used: Real, lt_div_iff₀', abs_mul, zero_lt_two', abs_two
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ |z.re| < 1 / 2

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ |z.re| < 1 / 2

Tactic:
exact h.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ 1 < z.re * z.re + z.im * z.im

Tactic:
simpa [Complex.normSq_apply] using h.1

Premises used: And.left, Complex.normSq_apply
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ 1 < z.re * z.re + z.im * z.im

Tactic:
have : 1 < z.re * z.re + z.im * z.im := by simpa [Complex.normSq_apply] using h.1
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
this : 1 < z.re * z.re + z.im * z.im
⊢ |z.re| < 1 / 2

Tactic:
have := h.2
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
this_1 : 1 < z.re * z.re + z.im * z.im
this : |z.re| < 1 / 2
inl : |z.re| = z.re ∧ 0 ≤ z.re → 3 < 4 * HPow.hPow (β := ℕ) z.im 2
inr : |z.re| = -z.re ∧ z.re < 0 → 3 < 4 * HPow.hPow (β := ℕ) z.im 2
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2

Tactic:
cases abs_cases z.re

Premises used: abs_cases, UpperHalfPlane.re
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
this_1 : 1 < z.re * z.re + z.im * z.im
this : |z.re| < 1 / 2
h_1 : |z.re| = z.re ∧ 0 ≤ z.re
nlinarith : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → 2 / 2 = 1
nlinarith₁ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → GT.gt (α := ℝ) 2 0
nlinarith₃ :
  4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 →
    4 * (1 - (z.re * z.re + z.im * z.im)) + (2 * |z.re| - HMul.hMul (α := ℝ) 1 1) + 4 * -(|z.re| - z.re) +
              (4 * HPow.hPow (β := ℕ) z.im 2 - 3) +
            2 * -((2 * |z.re| - HMul.hMul (α := ℝ) 1 1) * (|z.re| - z.re) - 0) +
          2 * (0 - (2 * |z.re| - HMul.hMul (α := ℝ) 1 1) * (0 - z.re)) +
        4 * ((|z.re| - z.re) * (|z.re| - z.re) - 0) =
      0
nlinarith₄ nlinarith₅ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → GT.gt (α := ℝ) 4 0
nlinarith₆ nlinarith₇ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → GT.gt (α := ℝ) 2 0
nlinarith₈ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → GT.gt (α := ℝ) 4 0
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2

Tactic:
nlinarith
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
this_1 : 1 < z.re * z.re + z.im * z.im
this : |z.re| < 1 / 2
h_1 : |z.re| = -z.re ∧ z.re < 0
nlinarith : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → 2 / 2 = 1
nlinarith₁ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → GT.gt (α := ℝ) 2 0
nlinarith₃ :
  4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 →
    4 * (1 - (z.re * z.re + z.im * z.im)) + 4 * -(|z.re| - -z.re) + (4 * HPow.hPow (β := ℕ) z.im 2 - 3) +
            (0 - (2 * |z.re| - HMul.hMul (α := ℝ) 1 1) * (2 * |z.re| - HMul.hMul (α := ℝ) 1 1)) +
          4 * (0 - (2 * |z.re| - HMul.hMul (α := ℝ) 1 1) * (z.re - 0)) +
        4 * ((|z.re| - -z.re) * (|z.re| - -z.re) - 0) =
      0
nlinarith₄ nlinarith₅ nlinarith₆ nlinarith₇ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → GT.gt (α := ℝ) 4 0
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2

Tactic:
nlinarith
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
h : τ ∈ 𝒟
⊢ 1 ≤ τ.re * τ.re + τ.im * τ.im

Tactic:
simpa [Complex.normSq_apply] using h.1

Premises used: And.left, Complex.normSq_apply
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
h : τ ∈ 𝒟
⊢ 1 ≤ τ.re * τ.re + τ.im * τ.im

Tactic:
have : 1 ≤ τ.re * τ.re + τ.im * τ.im := by simpa [Complex.normSq_apply] using h.1
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
inl : |τ.re| = τ.re ∧ 0 ≤ τ.re → 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
inr : |τ.re| = -τ.re ∧ τ.re < 0 → 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2

Tactic:
cases abs_cases τ.re

Premises used: abs_cases, UpperHalfPlane.re
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
h_1 : |τ.re| = τ.re ∧ 0 ≤ τ.re
nlinarith : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → 2 / 2 = 1
nlinarith₁ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 2 0
nlinarith₃ :
  4 * HPow.hPow (β := ℕ) τ.im 2 < 3 →
    4 * (1 - (τ.re * τ.re + τ.im * τ.im)) + 2 * -(|τ.re| - τ.re) + (4 * HPow.hPow (β := ℕ) τ.im 2 - 3) +
            (2 * |τ.re| - HMul.hMul (α := ℝ) 1 1) +
          4 * ((|τ.re| - τ.re) * (0 - τ.re) - 0) +
        2 * (0 - (0 - τ.re) * (2 * |τ.re| - HMul.hMul (α := ℝ) 1 1)) =
      0
nlinarith₄ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 4 0
nlinarith₅ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 2 0
nlinarith₆ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 4 0
nlinarith₇ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 2 0
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2

Tactic:
nlinarith [h.2]

Premises used: And.right
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
h_1 : |τ.re| = -τ.re ∧ τ.re < 0
nlinarith : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → 2 / 2 = 1
nlinarith₁ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 2 0
nlinarith₃ :
  4 * HPow.hPow (β := ℕ) τ.im 2 < 3 →
    4 * (1 - (τ.re * τ.re + τ.im * τ.im)) + 2 * -(|τ.re| - -τ.re) + (4 * HPow.hPow (β := ℕ) τ.im 2 - 3) +
            (2 * |τ.re| - HMul.hMul (α := ℝ) 1 1) +
          4 * ((|τ.re| - -τ.re) * (τ.re - 0) - 0) +
        2 * (0 - (τ.re - 0) * (2 * |τ.re| - HMul.hMul (α := ℝ) 1 1)) =
      0
nlinarith₄ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 4 0
nlinarith₅ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 2 0
nlinarith₆ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 4 0
nlinarith₇ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 2 0
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2

Tactic:
nlinarith [h.2]

Premises used: And.right
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
rw : LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) + (↑n : ℂ)) : ℝ)
⊢ LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑(T ^ n • z) : ℂ) : ℝ)

Tactic:
rw [coe_T_zpow_smul_eq]

Premises used: ModularGroup.coe_T_zpow_smul_eq
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
⊢ 1 < z.re * z.re + z.im * z.im

Tactic:
have hz₁ : 1 < z.re * z.re + z.im * z.im := hz.1
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
⊢ 0 ≤ (↑n : ℝ) * (2 * z.re) + HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)

Tactic:
have hzn := Int.nneg_mul_add_sq_of_abs_le_one n (abs_two_mul_re_lt_one_of_mem_fdo hz).le
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
hzn : 0 ≤ (↑n : ℝ) * (2 * z.re) + HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)
linarith :
  (z.re + (↑n : ℝ)) * (z.re + (↑n : ℝ)) + z.im * z.im ≤ 1 →
    1 - (z.re * z.re + z.im * z.im) + (0 - ((↑n : ℝ) * (2 * z.re) + HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ))) +
        ((z.re + (↑n : ℝ)) * (z.re + (↑n : ℝ)) + z.im * z.im - 1) =
      0
⊢ 1 < (z.re + (↑n : ℝ)) * (z.re + (↑n : ℝ)) + z.im * z.im

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
hzn : 0 ≤ (↑n : ℝ) * (2 * z.re) + HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)
⊢ 1 < (z.re + (↑n : ℝ)) * (z.re + (↑n : ℝ)) + z.im * z.im

Tactic:
have : 1 < (z.re + ↑n) * (z.re + ↑n) + z.im * z.im := by linarith
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
hzn : 0 ≤ (↑n : ℝ) * (2 * z.re) + HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)
this : 1 < (z.re + (↑n : ℝ)) * (z.re + (↑n : ℝ)) + z.im * z.im
⊢ LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) + (↑n : ℂ)) : ℝ)

Tactic:
simpa [normSq, num, denom]

Premises used: Complex.normSq, UpperHalfPlane.denom, UpperHalfPlane.num
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
this : LT.lt (α := ℝ) |(↑n : ℝ)| 1
rwa : ∀ (this : LT.lt (α := ℝ) (↑|n| : ℝ) 1), n = 0
rwa₁ : ∀ (this : LT.lt (α := ℝ) (↑|n| : ℝ) (↑1 : ℝ)), n = 0
rwa₂ : ∀ (this : |n| < 1), n = 0
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : n = 0), n = 0
⊢ n = 0

Tactic:
rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this

Premises used: Int.cast_abs, Int.cast_lt, Int.abs_lt_one_iff, Int.cast_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
suffices : LT.lt (α := ℝ) |(↑n : ℝ)| 1
⊢ n = 0

Tactic:
suffices |(n : ℝ)| < 1 by
    rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
⊢ |z.re| < 1 / 2

Tactic:
have h₁ := hz.2
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
⊢ |(T ^ n • z).re| < 1 / 2

Tactic:
have h₂ := hg.2
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
h₂ : |(T ^ n • z).re| < 1 / 2
⊢ |z.re + (↑n : ℝ)| < 1 / 2

Tactic:
rw [re_T_zpow_smul] at h₂

Premises used: ModularGroup.re_T_zpow_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
h₂ : |z.re + (↑n : ℝ)| < 1 / 2
⊢ |(↑n : ℝ)| ≤ |z.re| + |z.re + (↑n : ℝ)|

Tactic:
abs_add' (n : ℝ) z.re

Premises used: Int.cast, abs_add', UpperHalfPlane.re
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
h₂ : |z.re + (↑n : ℝ)| < 1 / 2
⊢ |z.re| + |z.re + (↑n : ℝ)| < 1 / 2 + 1 / 2

Tactic:
add_lt_add h₁ h₂

Premises used: add_lt_add
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
h₂ : |z.re + (↑n : ℝ)| < 1 / 2
⊢ 1 / 2 + 1 / 2 = 1

Tactic:
add_halves 1

Premises used: add_halves, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
h₂ : |z.re + (↑n : ℝ)| < 1 / 2
⊢ LT.lt (α := ℝ) |(↑n : ℝ)| 1

Tactic:
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

Premises used: Int.cast, add_halves, add_lt_add, abs_add', OfNat.ofNat, UpperHalfPlane.re
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
obtain : ∀ (g₀ : SL(2, ℤ)) (hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im), ∃ (g : SL(2, ℤ)), g • z ∈ 𝒟
⊢ ∃ (g : SL(2, ℤ)), g • z ∈ 𝒟

Tactic:
obtain ⟨g₀, hg₀⟩ := exists_max_im z

Premises used: ModularGroup.exists_max_im
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
obtain :
  ∀ (g : SL(2, ℤ)) (hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1)
    (hg' :
      ∀ (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 • z ∈ 𝒟
⊢ ∃ (g : SL(2, ℤ)), g • z ∈ 𝒟

Tactic:
obtain ⟨g, hg, hg'⟩ := exists_row_one_eq_and_min_re z (bottom_row_coprime g₀)

Premises used: ModularGroup.bottom_row_coprime, ModularGroup.exists_row_one_eq_and_min_re
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (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 • z ∈ 𝒟

Tactic:
⟨g, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
refine : g • z ∈ 𝒟
⊢ ∃ (g : SL(2, ℤ)), g • z ∈ 𝒟

Tactic:
refine ⟨g, ?_⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
rw :
  HDiv.hDiv (β := ℝ) z.im
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
            (↑z : ℂ)) :
        ℝ) =
    (g₀ • z).im
rw₁ :
  HDiv.hDiv (β := ℝ) z.im
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
            (↑z : ℂ)) :
        ℝ) =
    HDiv.hDiv (β := ℝ) z.im
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g₀))
            (↑z : ℂ)) :
        ℝ)
rw₂ :
  HDiv.hDiv (β := ℝ) z.im
      ((normSq : (a : ℂ) → ℝ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ) =
    HDiv.hDiv (β := ℝ) z.im
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g₀))
            (↑z : ℂ)) :
        ℝ)
rw₃ :
  HDiv.hDiv (β := ℝ) z.im
      ((normSq : (a : ℂ) → ℝ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ) =
    HDiv.hDiv (β := ℝ) z.im
      ((normSq : (a : ℂ) → ℝ)
          ((↑((↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ)
rw₄ rw₅ :
  HDiv.hDiv (β := ℝ) z.im
      ((normSq : (a : ℂ) → ℝ)
          ((↑((↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ) =
    HDiv.hDiv (β := ℝ) z.im
      ((normSq : (a : ℂ) → ℝ)
          ((↑((↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ)
⊢ (g • z).im = (g₀ • z).im

Tactic:
rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
        denom_apply, denom_apply, hg]

Premises used: ModularGroup.denom_apply, ModularGroup.im_smul_eq_div_normSq
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
⊢ (g • z).im = (g₀ • z).im

Tactic:
have hg'' : (g • z).im = (g₀ • z).im := by
      rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
        denom_apply, denom_apply, hg]
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
hg'' : (g • z).im = (g₀ • z).im
⊢ ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

Tactic:
simpa only [hg''] using hg₀
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (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' • z).im ≤ (g • z).im

Tactic:
have hg₀' : ∀ g' : SL(2, ℤ), (g' • z).im ≤ (g • z).im := by
    have hg'' : (g • z).im = (g₀ • z).im := by
      rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
        denom_apply, denom_apply, hg]
    simpa only [hg''] using hg₀
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
left : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ)
right : |(g • z).re| ≤ 1 / 2
⊢ g • z ∈ 𝒟

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
left :
  ∀ (hg₀' : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ) (1 : ℝ)),
    ∃ (g' : SL(2, ℤ)), (g • z).im < (g' • z).im
⊢ LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ)

Tactic:
contrapose! hg₀'
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ) (1 : ℝ)
⊢ ∃ (g' : SL(2, ℤ)), (g • z).im < (g' • z).im

Tactic:
⟨S * g, ?_⟩

Premises used: HMul.hMul, ModularGroup.S, Exists.intro
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ) (1 : ℝ)
left : (g • z).im < ((S * g) • z).im
⊢ ∃ (g' : SL(2, ℤ)), (g • z).im < (g' • z).im

Tactic:
refine ⟨S * g, ?_⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ) (1 : ℝ)
left : (g • z).im < (S • g • z).im
⊢ (g • z).im < ((S * g) • z).im

Tactic:
rw [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ) (1 : ℝ)
⊢ (g • z).im < (S • g • z).im

Tactic:
im_lt_im_S_smul hg₀'

Premises used: ModularGroup.im_lt_im_S_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ) (1 : ℝ)
⊢ (g • z).im < (S • g • z).im

Tactic:
exact im_lt_im_S_smul hg₀'

Premises used: ModularGroup.im_lt_im_S_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
right : -(1 / 2) ≤ (g • z).re ∧ (g • z).re ≤ 1 / 2
⊢ |(g • z).re| ≤ 1 / 2

Tactic:
rw [abs_le]

Premises used: abs_le
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
right : -(1 / 2) ≤ (g • z).re
right₁ : (g • z).re ≤ 1 / 2
⊢ -(1 / 2) ≤ (g • z).re ∧ (g • z).re ≤ 1 / 2

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1
hg' :
  ∀ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
right :
  ∀ (hg' : (g • z).re < -(1 / 2)),
    ∃ (g' : SL(2, ℤ)),
      (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 ∧ |(g' • z).re| < |(g • z).re|
⊢ -(1 / 2) ≤ (g • z).re

Tactic:
contrapose! hg'