awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re + 1| < |(g • z).re|
have linarith₂ : |(g • z).re| ≤ |(g • z).re + 1| → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re + 1| < |(g • z).re|
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (g • z).re ≤ 1 / 2
have 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|
Tactic: contrapose! hg'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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|
have right : |((T⁻¹ * g) • z).re| < |(g • z).re|
Tactic: refine ⟨T⁻¹ * g, (T_inv_mul_apply_one _).symm, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |((T⁻¹ * g) • z).re| < |(g • z).re|
have right : |(g • z).re - 1| < |(g • z).re|
Tactic: rw [mul_smul, re_T_inv_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 • z).re - 1| < |(g • z).re|
have right : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1 → |(g • z).re - 1| < |(g • z).re|
Tactic: cases abs_cases ((g • z).re - 1)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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|
⊢ |(g • z).re - 1| < |(g • z).re|
have right₁ : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0 → |(g • z).re - 1| < |(g • z).re|
Tactic: cases abs_cases ((g • z).re - 1)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have right : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re → |(g • z).re - 1| < |(g • z).re|
Tactic: cases abs_cases (g • z).re
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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|
⊢ |(g • z).re - 1| < |(g • z).re|
have right₁ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0 → |(g • z).re - 1| < |(g • z).re|
Tactic: cases abs_cases (g • z).re
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have right : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re → |(g • z).re - 1| < |(g • z).re|
Tactic: cases abs_cases (g • z).re
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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|
⊢ |(g • z).re - 1| < |(g • z).re|
have right₁ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0 → |(g • z).re - 1| < |(g • z).re|
Tactic: cases abs_cases (g • z).re
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith : |(g • z).re| ≤ |(g • z).re - 1| → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith₁ : |(g • z).re| ≤ |(g • z).re - 1| → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith₂ : |(g • z).re| ≤ |(g • z).re - 1| → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith : |(g • z).re| ≤ |(g • z).re - 1| → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith₁ : |(g • z).re| ≤ |(g • z).re - 1| → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith₂ : |(g • z).re| ≤ |(g • z).re - 1| → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith₃ : |(g • z).re| ≤ |(g • z).re - 1| → -1 + (HMul.hMul (α := ℝ) 1 1 - 2 * (g • z).re) + 2 * ((g • z).re - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith : |(g • z).re| ≤ |(g • z).re - 1| → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith₁ : |(g • z).re| ≤ |(g • z).re - 1| → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith₂ : |(g • z).re| ≤ |(g • z).re - 1| → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith : |(g • z).re| ≤ |(g • z).re - 1| → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith₁ : |(g • z).re| ≤ |(g • z).re - 1| → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have linarith₂ : |(g • z).re| ≤ |(g • z).re - 1| → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(g • z).re - 1| < |(g • z).re|
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0| ≤ 1
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0| ≤ 1
have this₁ : HPow.hPow (β := ℕ) c' 2 ≤ HPow.hPow (α := ℤ) (β := ℕ) 1 2
Tactic: replace this : c' ^ 2 ≤ 1 ^ 2 := by lia
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0| ≤ 1
have rwa : ∀ (this : |c'| ≤ |1|), |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0| ≤ 1
Tactic: rwa [sq_le_sq, abs_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0| ≤ 1
have rwa₁ : ∀ (this : |c'| ≤ 1), |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0| ≤ 1
Tactic: rwa [sq_le_sq, abs_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0| ≤ 1
have suffices : 3 * HPow.hPow (β := ℕ) c 2 ≤ 4
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
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 * HPow.hPow (β := ℕ) c 2 ≤ 4
have inl : ∀ (hc : c = 0), 3 * HPow.hPow (β := ℕ) c 2 ≤ 4
Tactic: rcases eq_or_ne c 0 with (hc | hc)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 * HPow.hPow (β := ℕ) c 2 ≤ 4
have inr : ∀ (hc : c ≠ 0), 3 * HPow.hPow (β := ℕ) c 2 ≤ 4
Tactic: rcases eq_or_ne c 0 with (hc | hc)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
have inr : HPow.hPow (β := ℕ) (3 * HPow.hPow (β := ℕ) c 2) 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 4 2
Tactic: apply le_of_sq_le_sq
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 * HPow.hPow (β := ℕ) c 2 ≤ 4
have inr₁ : LE.le (α := ℝ) 0 4
Tactic: apply le_of_sq_le_sq
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
⊢ 3 * HPow.hPow (β := ℕ) c 2 ≤ 4
have suffices : c ≠ 0 → 9 * HPow.hPow (β := ℕ) c 4 ≤ 16
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
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
have hbc : 3 ≤ 4 * HPow.hPow (β := ℕ) (g • z).im 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 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
have hbc₁ : 3 ≤ 4 * HPow.hPow (β := ℕ) z.im 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
⊢ 9 * HPow.hPow (β := ℕ) c 4 ≤ 16
have 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
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)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
⊢ 9 * HPow.hPow (β := ℕ) c 4 ≤ 16
have 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
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 _)