awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
h : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
imz : 0 < z.im
⊢ HMul.hMul (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) < z.im
have nlinarith : z.im ≤ HMul.hMul (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) →
  z.im - HMul.hMul (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) +
      (0 - HSub.hSub (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) * (0 - z.im)) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
h : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
⊢ 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 : ℂ)) :
        ℝ)
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
⊢ ρ ∈ 𝒟
have left : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑ρ : ℂ) : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
left : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑ρ : ℂ) : ℝ)
⊢ ρ ∈ 𝒟
have right : |ρ.re| ≤ 1 / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
⊢ I ∈ 𝒟
have left : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑I : ℂ) : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
left : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑I : ℂ) : ℝ)
⊢ I ∈ 𝒟
have right : |I.re| ≤ 1 / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ |2 * z.re| < 1
have rw : |z.re| < 1 / 2
Tactic: rw [abs_mul, abs_two, ← lt_div_iff₀' (zero_lt_two' ℝ)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
this : 1 < z.re * z.re + z.im * z.im
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have this₁ : |z.re| < 1 / 2
Tactic: have := h.2
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
h : z ∈ 𝒟ᵒ
this_1 : 1 < z.re * z.re + z.im * z.im
this : |z.re| < 1 / 2
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have inl : |z.re| = z.re ∧ 0 ≤ z.re → 3 < 4 * HPow.hPow (β := ℕ) z.im 2
Tactic: cases abs_cases z.re
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have inr : |z.re| = -z.re ∧ z.re < 0 → 3 < 4 * HPow.hPow (β := ℕ) z.im 2
Tactic: cases abs_cases z.re
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have nlinarith : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → 2 / 2 = 1
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have nlinarith₁ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have nlinarith₂ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have nlinarith₄ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → GT.gt (α := ℝ) 4 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have nlinarith : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → 2 / 2 = 1
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have nlinarith₁ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have nlinarith₂ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 < 4 * HPow.hPow (β := ℕ) z.im 2
have nlinarith₄ : 4 * HPow.hPow (β := ℕ) z.im 2 ≤ 3 → GT.gt (α := ℝ) 4 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
τ : ℍ
h : τ ∈ 𝒟
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have this : 1 ≤ τ.re * τ.re + τ.im * τ.im
Tactic: have : 1 ≤ τ.re * τ.re + τ.im * τ.im := by simpa [Complex.normSq_apply] using h.1
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have inl : |τ.re| = τ.re ∧ 0 ≤ τ.re → 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
Tactic: cases abs_cases τ.re
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
inl : |τ.re| = τ.re ∧ 0 ≤ τ.re → 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have inr : |τ.re| = -τ.re ∧ τ.re < 0 → 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
Tactic: cases abs_cases τ.re
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
h_1 : |τ.re| = τ.re ∧ 0 ≤ τ.re
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have nlinarith : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → 2 / 2 = 1
Tactic: nlinarith [h.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
h_1 : |τ.re| = τ.re ∧ 0 ≤ τ.re
nlinarith : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → 2 / 2 = 1
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have nlinarith₁ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: nlinarith [h.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have nlinarith₂ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith [h.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have 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
Tactic: nlinarith [h.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have nlinarith₄ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 4 0
Tactic: nlinarith [h.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
h_1 : |τ.re| = -τ.re ∧ τ.re < 0
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have nlinarith : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → 2 / 2 = 1
Tactic: nlinarith [h.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
h_1 : |τ.re| = -τ.re ∧ τ.re < 0
nlinarith : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → 2 / 2 = 1
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have nlinarith₁ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: nlinarith [h.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have nlinarith₂ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith [h.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have 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
Tactic: nlinarith [h.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 3 ≤ 4 * HPow.hPow (β := ℕ) τ.im 2
have nlinarith₄ : 4 * HPow.hPow (β := ℕ) τ.im 2 < 3 → GT.gt (α := ℝ) 4 0
Tactic: nlinarith [h.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
⊢ LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑(T ^ n • z) : ℂ) : ℝ)
have rw : LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) + (↑n : ℂ)) : ℝ)
Tactic: rw [coe_T_zpow_smul_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
⊢ LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) + (↑n : ℂ)) : ℝ)
have hz₁ : 1 < z.re * z.re + z.im * z.im
Tactic: have hz₁ : 1 < z.re * z.re + z.im * z.im := hz.1
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
⊢ LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) + (↑n : ℂ)) : ℝ)
have hzn : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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 : ℝ)
⊢ LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) + (↑n : ℂ)) : ℝ)
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
this : LT.lt (α := ℝ) |(↑n : ℝ)| 1
⊢ n = 0
have rwa : ∀ (this : LT.lt (α := ℝ) (↑|n| : ℝ) 1), n = 0
Tactic: rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
this : LT.lt (α := ℝ) |(↑n : ℝ)| 1
rwa : ∀ (this : LT.lt (α := ℝ) (↑|n| : ℝ) 1), n = 0
⊢ n = 0
have rwa₁ : ∀ (this : LT.lt (α := ℝ) (↑|n| : ℝ) (↑1 : ℝ)), n = 0
Tactic: rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ n = 0
have rwa₂ : ∀ (this : |n| < 1), n = 0
Tactic: rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ n = 0
have rwa₃ : ∀ (this : n = 0), n = 0
Tactic: rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
⊢ n = 0
have suffices : LT.lt (α := ℝ) |(↑n : ℝ)| 1
Tactic: suffices |(n : ℝ)| < 1 by
    rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
⊢ LT.lt (α := ℝ) |(↑n : ℝ)| 1
have h₁ : |z.re| < 1 / 2
Tactic: have h₁ := hz.2
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
⊢ LT.lt (α := ℝ) |(↑n : ℝ)| 1
have h₂ : |(T ^ n • z).re| < 1 / 2
Tactic: have h₂ := hg.2
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
h₂ : |(T ^ n • z).re| < 1 / 2
⊢ LT.lt (α := ℝ) |(↑n : ℝ)| 1
have h₃ : |z.re + (↑n : ℝ)| < 1 / 2
Tactic: rw [re_T_zpow_smul] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
⊢ ∃ (g : SL(2, ℤ)), g • z ∈ 𝒟
have obtain : ∀ (g₀ : SL(2, ℤ)) (hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im), ∃ (g : SL(2, ℤ)), g • z ∈ 𝒟
Tactic: obtain ⟨g₀, hg₀⟩ := exists_max_im z
-- 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, ℤ)), g • z ∈ 𝒟
have 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 ∈ 𝒟
Tactic: obtain ⟨g, hg, hg'⟩ := exists_row_one_eq_and_min_re z (bottom_row_coprime g₀)
-- 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|
⊢ ∃ (g : SL(2, ℤ)), g • z ∈ 𝒟
have refine : g • z ∈ 𝒟
Tactic: refine ⟨g, ?_⟩
-- 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|
⊢ (g • z).im = (g₀ • z).im
have 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
Tactic: rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
        denom_apply, denom_apply, 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 : 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
⊢ (g • z).im = (g₀ • z).im
have 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 : ℂ)) :
      ℝ)
Tactic: rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
        denom_apply, denom_apply, 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 : 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 : ℂ)) :
        ℝ)
⊢ (g • z).im = (g₀ • z).im
have 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 : ℂ)) :
      ℝ)
Tactic: rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
        denom_apply, denom_apply, hg]