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 : 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 : ℂ)) :
        ℝ)
⊢ (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 : ℂ) → ℝ)
        ((↑((↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
      ℝ)
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 : ℂ)) :
        ℝ)
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) : ℂ)) :
        ℝ)
⊢ (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 : ℂ) → ℝ)
        ((↑((↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g₀ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
      ℝ)
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 (hypothesis)
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
have hg'' : (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]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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 ∈ 𝒟
have hg₀' : ∀ (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₀
-- 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 ∈ 𝒟
have left : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ)
Tactic: constructor
-- 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
left : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ)
⊢ g • z ∈ 𝒟
have right : |(g • z).re| ≤ 1 / 2
Tactic: constructor
-- 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
⊢ LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ)
have left : ∀ (hg₀' : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ) (1 : ℝ)),
  ∃ (g' : SL(2, ℤ)), (g • z).im < (g' • z).im
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 : 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
have left : (g • z).im < ((S * g) • z).im
Tactic: refine ⟨S * 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|
hg₀' : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑(g • z) : ℂ) : ℝ) (1 : ℝ)
⊢ (g • z).im < ((S * g) • z).im
have left : (g • z).im < (S • g • z).im
Tactic: rw [mul_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 : 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 : -(1 / 2) ≤ (g • z).re ∧ (g • z).re ≤ 1 / 2
Tactic: rw [abs_le]
-- 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
⊢ -(1 / 2) ≤ (g • z).re ∧ (g • z).re ≤ 1 / 2
have right : -(1 / 2) ≤ (g • z).re
Tactic: constructor
-- 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
right : -(1 / 2) ≤ (g • z).re
⊢ -(1 / 2) ≤ (g • z).re ∧ (g • z).re ≤ 1 / 2
have right₁ : (g • z).re ≤ 1 / 2
Tactic: constructor
-- 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
⊢ -(1 / 2) ≤ (g • z).re
have 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|
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' : (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|
have right : |((T * g) • z).re| < |(g • z).re|
Tactic: refine ⟨T * g, (T_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' : (g • z).re < -(1 / 2)
⊢ |((T * g) • z).re| < |(g • z).re|
have right : |(g • z).re + 1| < |(g • z).re|
Tactic: rw [mul_smul, re_T_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' : (g • z).re < -(1 / 2)
⊢ |(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' : (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|
⊢ |(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' : (g • z).re < -(1 / 2)
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' : (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|
⊢ |(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' : (g • z).re < -(1 / 2)
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' : (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|
⊢ |(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' : (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
⊢ |(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' : (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
⊢ |(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' : (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
⊢ |(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 ∧ 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 + (2 * (g • z).re - -HMul.hMul (α := ℝ) 1 1) + 2 * (0 - (g • z).re) = 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 ∧ 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' : (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
⊢ |(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' : (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
⊢ |(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 ∧ 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| →
  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
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 ∧ 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' : (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
⊢ |(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' : (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
⊢ |(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 ∧ 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 - 0) + (0 - (g • z).re) = 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
⊢ |(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' : (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
⊢ |(g • z).re + 1| < |(g • z).re|
have linarith₁ : |(g • z).re| ≤ |(g • z).re + 1| → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith