awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' • z).im ≤ (g • z).im
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|

Tactic:
⟨T * g, (T_mul_apply_one _).symm, ?_⟩

Premises used: HMul.hMul, ModularGroup.T_mul_apply_one, ModularGroup.T, And.intro, Exists.intro, Eq.symm
-- 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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
right : |((T * g) • z).re| < |(g • z).re|
⊢ ∃ (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 ⟨T * g, (T_mul_apply_one _).symm, ?_⟩
-- 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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
right : |(g • z).re + 1| < |(g • z).re|
⊢ |((T * g) • z).re| < |(g • z).re|

Tactic:
rw [mul_smul, re_T_smul]

Premises used: ModularGroup.re_T_smul, 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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
right : |(g • z).re + 1| = (g • z).re + 1 ∧ 0 ≤ (g • z).re + 1 → |(g • z).re + 1| < |(g • z).re|
right₁ : |(g • z).re + 1| = -((g • z).re + 1) ∧ (g • z).re + 1 < 0 → |(g • z).re + 1| < |(g • z).re|
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
cases abs_cases ((g • z).re + 1)

Premises used: abs_cases, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, UpperHalfPlane.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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h : |(g • z).re + 1| = (g • z).re + 1 ∧ 0 ≤ (g • z).re + 1
right : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re → |(g • z).re + 1| < |(g • z).re|
right₁ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0 → |(g • z).re + 1| < |(g • z).re|
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
cases abs_cases (g • z).re

Premises used: abs_cases, HSMul.hSMul, UpperHalfPlane.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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h : |(g • z).re + 1| = -((g • z).re + 1) ∧ (g • z).re + 1 < 0
right : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re → |(g • z).re + 1| < |(g • z).re|
right₁ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0 → |(g • z).re + 1| < |(g • z).re|
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
cases abs_cases (g • z).re

Premises used: abs_cases, HSMul.hSMul, UpperHalfPlane.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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h : |(g • z).re + 1| = (g • z).re + 1 ∧ 0 ≤ (g • z).re + 1
h_1 : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
linarith : |(g • z).re| ≤ |(g • z).re + 1| → 2 / 2 = 1
linarith₁ : |(g • z).re| ≤ |(g • z).re + 1| → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : |(g • z).re| ≤ |(g • z).re + 1| → GT.gt (α := ℝ) 2 0
linarith₃ : |(g • z).re| ≤ |(g • z).re + 1| → -1 + (2 * (g • z).re - -HMul.hMul (α := ℝ) 1 1) + 2 * (0 - (g • z).re) = 0
linarith₄ : |(g • z).re| ≤ |(g • z).re + 1| → GT.gt (α := ℝ) 2 0
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
linarith
-- 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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h : |(g • z).re + 1| = (g • z).re + 1 ∧ 0 ≤ (g • z).re + 1
h_1 : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
linarith : |(g • z).re| ≤ |(g • z).re + 1| → 2 / 2 = 1
linarith₁ : |(g • z).re| ≤ |(g • z).re + 1| → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : |(g • z).re| ≤ |(g • z).re + 1| → GT.gt (α := ℝ) 2 0
linarith₃ :
  |(g • z).re| ≤ |(g • z).re + 1| →
    2 * (g • z).re - -HMul.hMul (α := ℝ) 1 1 + (|(g • z).re + 1| - ((g • z).re + 1)) + -(|(g • z).re| - -(g • z).re) +
        (|(g • z).re| - |(g • z).re + 1|) =
      0
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
linarith
-- 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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h : |(g • z).re + 1| = -((g • z).re + 1) ∧ (g • z).re + 1 < 0
h_1 : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
linarith : |(g • z).re| ≤ |(g • z).re + 1| → 2 / 2 = 1
linarith₁ : |(g • z).re| ≤ |(g • z).re + 1| → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : |(g • z).re| ≤ |(g • z).re + 1| → GT.gt (α := ℝ) 2 0
linarith₃ : |(g • z).re| ≤ |(g • z).re + 1| → -1 + ((g • z).re + 1 - 0) + (0 - (g • z).re) = 0
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
linarith
-- 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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h : |(g • z).re + 1| = -((g • z).re + 1) ∧ (g • z).re + 1 < 0
h_1 : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
linarith : |(g • z).re| ≤ |(g • z).re + 1| → 2 / 2 = 1
linarith₁ : |(g • z).re| ≤ |(g • z).re + 1| → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : |(g • z).re| ≤ |(g • z).re + 1| → GT.gt (α := ℝ) 2 0
linarith₃ :
  |(g • z).re| ≤ |(g • z).re + 1| →
    -1 + (|(g • z).re + 1| - -((g • z).re + 1)) + -(|(g • z).re| - -(g • z).re) + (|(g • z).re| - |(g • z).re + 1|) = 0
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
linarith
-- 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' : 1 / 2 < (g • z).re),
    ∃ (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).re ≤ 1 / 2

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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
⊢ ∃ (g' : SL(2, ℤ)),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g' : Matrix (Fin 2) (Fin 2) ℤ) 1 ∧ |(g' • z).re| < |(g • z).re|

Tactic:
⟨T⁻¹ * g, (T_inv_mul_apply_one _).symm, ?_⟩

Premises used: HMul.hMul, ModularGroup.T, ModularGroup.T_inv_mul_apply_one, Inv.inv, And.intro, Exists.intro, Eq.symm
-- 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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
right : |((T⁻¹ * g) • z).re| < |(g • z).re|
⊢ ∃ (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 ⟨T⁻¹ * g, (T_inv_mul_apply_one _).symm, ?_⟩
-- 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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
right : |(g • z).re - 1| < |(g • z).re|
⊢ |((T⁻¹ * g) • z).re| < |(g • z).re|

Tactic:
rw [mul_smul, re_T_inv_smul]

Premises used: ModularGroup.re_T_inv_smul, 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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
right : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1 → |(g • z).re - 1| < |(g • z).re|
right₁ : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0 → |(g • z).re - 1| < |(g • z).re|
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
cases abs_cases ((g • z).re - 1)

Premises used: HSub.hSub, abs_cases, HSMul.hSMul, OfNat.ofNat, UpperHalfPlane.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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1
right : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re → |(g • z).re - 1| < |(g • z).re|
right₁ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0 → |(g • z).re - 1| < |(g • z).re|
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
cases abs_cases (g • z).re

Premises used: abs_cases, HSMul.hSMul, UpperHalfPlane.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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0
right : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re → |(g • z).re - 1| < |(g • z).re|
right₁ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0 → |(g • z).re - 1| < |(g • z).re|
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
cases abs_cases (g • z).re

Premises used: abs_cases, HSMul.hSMul, UpperHalfPlane.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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1
h_1 : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
linarith : |(g • z).re| ≤ |(g • z).re - 1| → 2 / 2 = 1
linarith₁ : |(g • z).re| ≤ |(g • z).re - 1| → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : |(g • z).re| ≤ |(g • z).re - 1| → GT.gt (α := ℝ) 2 0
linarith₃ :
  |(g • z).re| ≤ |(g • z).re - 1| →
    -1 + (|(g • z).re - 1| - ((g • z).re - 1)) + -(|(g • z).re| - (g • z).re) + (|(g • z).re| - |(g • z).re - 1|) = 0
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
linarith
-- 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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1
h_1 : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
linarith : |(g • z).re| ≤ |(g • z).re - 1| → 2 / 2 = 1
linarith₁ : |(g • z).re| ≤ |(g • z).re - 1| → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : |(g • z).re| ≤ |(g • z).re - 1| → GT.gt (α := ℝ) 2 0
linarith₃ : |(g • z).re| ≤ |(g • z).re - 1| → -1 + (HMul.hMul (α := ℝ) 1 1 - 2 * (g • z).re) + 2 * ((g • z).re - 0) = 0
linarith₄ : |(g • z).re| ≤ |(g • z).re - 1| → GT.gt (α := ℝ) 2 0
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
linarith
-- 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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0
h_1 : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
linarith : |(g • z).re| ≤ |(g • z).re - 1| → 2 / 2 = 1
linarith₁ : |(g • z).re| ≤ |(g • z).re - 1| → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : |(g • z).re| ≤ |(g • z).re - 1| → GT.gt (α := ℝ) 2 0
linarith₃ :
  |(g • z).re| ≤ |(g • z).re - 1| →
    HMul.hMul (α := ℝ) 1 1 - 2 * (g • z).re + (|(g • z).re - 1| - -((g • z).re - 1)) + -(|(g • z).re| - (g • z).re) +
        (|(g • z).re| - |(g • z).re - 1|) =
      0
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
linarith
-- 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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0
h_1 : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
linarith : |(g • z).re| ≤ |(g • z).re - 1| → 2 / 2 = 1
linarith₁ : |(g • z).re| ≤ |(g • z).re - 1| → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : |(g • z).re| ≤ |(g • z).re - 1| → GT.gt (α := ℝ) 2 0
linarith₃ :
  |(g • z).re| ≤ |(g • z).re - 1| →
    HMul.hMul (α := ℝ) 1 1 - 2 * (g • z).re + ((g • z).re - 1 - 0) + ((g • z).re - 0) = 0
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
this : 3 * HPow.hPow (β := ℕ) c 2 ≤ 4
⊢ 3 * HPow.hPow (β := ℕ) c' 2 ≤ 4

Tactic:
rw [← Int.cast_pow, ← Int.cast_three, ← Int.cast_four, ← Int.cast_mul, Int.cast_le] at this

Premises used: Int.cast_le, Int.cast_pow, Int.cast_four, Int.cast_mul, Int.cast_three
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
this : 3 * HPow.hPow (β := ℕ) c' 2 ≤ 4
⊢ HPow.hPow (β := ℕ) c' 2 ≤ HPow.hPow (α := ℤ) (β := ℕ) 1 2

Tactic:
lia
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
this : 3 * HPow.hPow (β := ℕ) c' 2 ≤ 4
⊢ HPow.hPow (β := ℕ) c' 2 ≤ HPow.hPow (α := ℤ) (β := ℕ) 1 2

Tactic:
replace this : c' ^ 2 ≤ 1 ^ 2 := by lia
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
this : HPow.hPow (β := ℕ) c' 2 ≤ HPow.hPow (α := ℤ) (β := ℕ) 1 2
rwa : ∀ (this : |c'| ≤ |1|), |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0| ≤ 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : |c'| ≤ 1), |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0| ≤ 1
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0| ≤ 1

Tactic:
rwa [sq_le_sq, abs_one] at this

Premises used: sq_le_sq, abs_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
suffices : 3 * HPow.hPow (β := ℕ) c 2 ≤ 4
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0| ≤ 1

Tactic:
suffices 3 * c ^ 2 ≤ 4 by
    rw [← Int.cast_pow, ← Int.cast_three, ← Int.cast_four, ← Int.cast_mul, Int.cast_le] at this
    replace this : c' ^ 2 ≤ 1 ^ 2 := by lia
    rwa [sq_le_sq, abs_one] at this
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
this : c ≠ 0 → 9 * HPow.hPow (β := ℕ) c 4 ≤ 16
inl : ∀ (hc : c = 0), 3 * HPow.hPow (β := ℕ) c 2 ≤ 4
inr : ∀ (hc : c ≠ 0), 3 * HPow.hPow (β := ℕ) c 2 ≤ 4
⊢ 3 * HPow.hPow (β := ℕ) c 2 ≤ 4

Tactic:
rcases eq_or_ne c 0 with (hc | hc)

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
this : c ≠ 0 → 9 * HPow.hPow (β := ℕ) c 4 ≤ 16
hc : c = 0
⊢ 3 * HPow.hPow (β := ℕ) c 2 ≤ 4

Tactic:
simp [hc]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
this : c ≠ 0 → 9 * HPow.hPow (β := ℕ) c 4 ≤ 16
hc : c ≠ 0
inr : HPow.hPow (β := ℕ) (3 * HPow.hPow (β := ℕ) c 2) 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 4 2
inr₁ : LE.le (α := ℝ) 0 4
⊢ 3 * HPow.hPow (β := ℕ) c 2 ≤ 4

Tactic:
apply le_of_sq_le_sq

Premises used: le_of_sq_le_sq
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
this : c ≠ 0 → 9 * HPow.hPow (β := ℕ) c 4 ≤ 16
hc : c ≠ 0
⊢ HPow.hPow (β := ℕ) (3 * HPow.hPow (β := ℕ) c 2) 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 4 2

Tactic:
grind
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
this : c ≠ 0 → 9 * HPow.hPow (β := ℕ) c 4 ≤ 16
hc : c ≠ 0
⊢ LE.le (α := ℝ) 0 4

Tactic:
grind
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
suffices : c ≠ 0 → 9 * HPow.hPow (β := ℕ) c 4 ≤ 16
⊢ 3 * HPow.hPow (β := ℕ) c 2 ≤ 4

Tactic:
suffices c ≠ 0 → 9 * c ^ 4 ≤ 16 by
    rcases eq_or_ne c 0 with (hc | hc)
    · simp [hc]
    · apply le_of_sq_le_sq <;> grind
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
hbc : 3 ≤ 4 * HPow.hPow (β := ℕ) (g • z).im 2
hbc₁ : 3 ≤ 4 * HPow.hPow (β := ℕ) z.im 2
⊢ HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
⊢ g • z ∈ 𝒟

Tactic:
assumption
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) (g • z).im 2

Tactic:
exact three_le_four_mul_im_sq_of_mem_fd (by assumption)

Premises used: ModularGroup.three_le_four_mul_im_sq_of_mem_fd
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
⊢ z ∈ 𝒟

Tactic:
assumption
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) z.im 2

Tactic:
exact three_le_four_mul_im_sq_of_mem_fd (by assumption)

Premises used: ModularGroup.three_le_four_mul_im_sq_of_mem_fd
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
⊢ HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4

Tactic:
have h₁ : 3 * 3 * c ^ 4 ≤ 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4 := by
    gcongr <;> exact three_le_four_mul_im_sq_of_mem_fd (by assumption)
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
h₁ :
  HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4
⊢ HPow.hPow (β := ℕ) (c * z.im) 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 ≤
    1

Tactic:
have h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1 :=
    div_le_one_of_le₀
      (pow_four_le_pow_two_of_pow_two_le (z.c_mul_im_sq_le_normSq_denom g)) (sq_nonneg _)
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
h₁ :
  HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4
h₂ :
  HPow.hPow (β := ℕ) (c * z.im) 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 ≤
    1
linarith :
  HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 2 * HPow.hPow (β := ℕ) (g • z).im 2 * 16 <
      9 * HPow.hPow (β := ℕ) c 4 →
    HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 -
          4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4 +
        (HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 2 * HPow.hPow (β := ℕ) (g • z).im 2 * 16 -
          9 * HPow.hPow (β := ℕ) c 4) =
      0
⊢ 9 * HPow.hPow (β := ℕ) c 4 ≤ HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 2 * HPow.hPow (β := ℕ) (g • z).im 2 * 16

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
h₁ :
  HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4
h₂ :
  HPow.hPow (β := ℕ) (c * z.im) 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 ≤
    1
⊢ HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 2 * HPow.hPow (β := ℕ) (g • z).im 2 * 16 =
    HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 4 /
        HPow.hPow (α := ℝ) (β := ℕ)
          ((normSq : (a : ℂ) → ℝ)
              (denom
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                  ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                (↑z : ℂ)) :
            ℝ)
          2 *
      16

Tactic:
grind [im_smul_eq_div_normSq]

Premises used: ModularGroup.im_smul_eq_div_normSq