awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T 1
hre : (g • z).re = 1 + z.re
hb : b = 1
linarith : z.re < -1 / 2 → 2 / 2 = 1
linarith₁ : z.re < -1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : z.re < -1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : z.re < -1 / 2 → 2 / 2 = 1
linarith₄ : z.re < -1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : z.re < -1 / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : z.re < -1 / 2 → 2 / 2 = 1
linarith₇ : z.re < -1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : z.re < -1 / 2 → GT.gt (α := ℝ) 2 0
linarith₉ : z.re < -1 / 2 → 2 * z.re - -HMul.hMul (α := ℝ) 1 1 + (-(2 * z.re) - HMul.hMul (α := ℝ) 1 1) = 0
linarith₁₀ : -1 / 2 < z.re → 2 / 2 = 1
linarith₁₁ : -1 / 2 < z.re → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ : -1 / 2 < z.re → GT.gt (α := ℝ) 2 0
linarith₁₃ : -1 / 2 < z.re → 2 / 2 = 1
linarith₁₄ : -1 / 2 < z.re → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₅ : -1 / 2 < z.re → GT.gt (α := ℝ) 2 0
linarith₁₆ : -1 / 2 < z.re → 2 / 2 = 1
linarith₁₇ : -1 / 2 < z.re → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₈ : -1 / 2 < z.re → GT.gt (α := ℝ) 2 0
⊢ z.re = -1 / 2
have linarith₁₉ : -1 / 2 < z.re →
  2 * -((g • z).re - (1 + z.re)) + (-HMul.hMul (α := ℝ) 1 1 - 2 * z.re) + (2 * (g • z).re - HMul.hMul (α := ℝ) 1 1) = 0
Tactic: linarith [(le_abs_self _).trans (abs_neg z.re ▸ hz.2), (le_abs_self _).trans hg.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T (-1)
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
have inr : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
Tactic: right
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T (-1)
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = -1
⊢ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
have inr : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T (-1)
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = -1
⊢ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2
have inr : z.re = 1 / 2
Tactic: rw [hgz, zpow_neg_one, eq_self_iff_true, true_or, true_and]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T (-1)
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = -1
⊢ z.re = 1 / 2
have hre₁ : (g • z).re = -1 + z.re
Tactic: rw [hb, Int.cast_neg, Int.cast_one] at hre
Cleared hypotheses: hre, hb
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T (-1)
hre : (g • z).re = -1 + z.re
hb : b = -1
⊢ z.re = 1 / 2
have linarith : z.re < 1 / 2 → 2 / 2 = 1
Tactic: linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T (-1)
hre : (g • z).re = -1 + z.re
hb : b = -1
linarith : z.re < 1 / 2 → 2 / 2 = 1
⊢ z.re = 1 / 2
have linarith₁ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T (-1)
hre : (g • z).re = -1 + z.re
hb : b = -1
linarith : z.re < 1 / 2 → 2 / 2 = 1
linarith₁ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ z.re = 1 / 2
have linarith₂ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T (-1)
hre : (g • z).re = -1 + z.re
hb : b = -1
linarith : z.re < 1 / 2 → 2 / 2 = 1
linarith₁ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : z.re < 1 / 2 → 2 / 2 = 1
linarith₄ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : z.re < 1 / 2 → 2 / 2 = 1
linarith₇ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
⊢ z.re = 1 / 2
have linarith₉ : z.re < 1 / 2 →
  2 * ((g • z).re - (-1 + z.re)) + (2 * z.re - HMul.hMul (α := ℝ) 1 1) + (-(2 * (g • z).re) - HMul.hMul (α := ℝ) 1 1) =
    0
Tactic: linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T (-1)
hre : (g • z).re = -1 + z.re
hb : b = -1
linarith : z.re < 1 / 2 → 2 / 2 = 1
linarith₁ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : z.re < 1 / 2 → 2 / 2 = 1
linarith₄ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : z.re < 1 / 2 → 2 / 2 = 1
linarith₇ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₉ :
  z.re < 1 / 2 →
    2 * ((g • z).re - (-1 + z.re)) + (2 * z.re - HMul.hMul (α := ℝ) 1 1) +
        (-(2 * (g • z).re) - HMul.hMul (α := ℝ) 1 1) =
      0
linarith₁₀ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
⊢ z.re = 1 / 2
have linarith₁₁ : 1 / 2 < z.re → 2 / 2 = 1
Tactic: linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T (-1)
hre : (g • z).re = -1 + z.re
hb : b = -1
linarith : z.re < 1 / 2 → 2 / 2 = 1
linarith₁ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : z.re < 1 / 2 → 2 / 2 = 1
linarith₄ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : z.re < 1 / 2 → 2 / 2 = 1
linarith₇ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₉ :
  z.re < 1 / 2 →
    2 * ((g • z).re - (-1 + z.re)) + (2 * z.re - HMul.hMul (α := ℝ) 1 1) +
        (-(2 * (g • z).re) - HMul.hMul (α := ℝ) 1 1) =
      0
linarith₁₀ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₁₁ : 1 / 2 < z.re → 2 / 2 = 1
⊢ z.re = 1 / 2
have linarith₁₂ : 1 / 2 < z.re → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T (-1)
hre : (g • z).re = -1 + z.re
hb : b = -1
linarith : z.re < 1 / 2 → 2 / 2 = 1
linarith₁ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : z.re < 1 / 2 → 2 / 2 = 1
linarith₄ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : z.re < 1 / 2 → 2 / 2 = 1
linarith₇ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₉ :
  z.re < 1 / 2 →
    2 * ((g • z).re - (-1 + z.re)) + (2 * z.re - HMul.hMul (α := ℝ) 1 1) +
        (-(2 * (g • z).re) - HMul.hMul (α := ℝ) 1 1) =
      0
linarith₁₀ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₁₁ : 1 / 2 < z.re → 2 / 2 = 1
linarith₁₂ : 1 / 2 < z.re → HMul.hMul (α := ℝ) 1 2 = 2
⊢ z.re = 1 / 2
have linarith₁₃ : 1 / 2 < z.re → GT.gt (α := ℝ) 2 0
Tactic: linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
hgz : g = HPow.hPow (β := ℤ) T (-1)
hre : (g • z).re = -1 + z.re
hb : b = -1
linarith : z.re < 1 / 2 → 2 / 2 = 1
linarith₁ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : z.re < 1 / 2 → 2 / 2 = 1
linarith₄ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : z.re < 1 / 2 → 2 / 2 = 1
linarith₇ : z.re < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₉ :
  z.re < 1 / 2 →
    2 * ((g • z).re - (-1 + z.re)) + (2 * z.re - HMul.hMul (α := ℝ) 1 1) +
        (-(2 * (g • z).re) - HMul.hMul (α := ℝ) 1 1) =
      0
linarith₁₀ : z.re < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₁₁ : 1 / 2 < z.re → 2 / 2 = 1
linarith₁₂ : 1 / 2 < z.re → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : 1 / 2 < z.re → GT.gt (α := ℝ) 2 0
linarith₁₄ : 1 / 2 < z.re → 2 / 2 = 1
linarith₁₅ : 1 / 2 < z.re → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₆ : 1 / 2 < z.re → GT.gt (α := ℝ) 2 0
linarith₁₇ : 1 / 2 < z.re → 2 / 2 = 1
linarith₁₈ : 1 / 2 < z.re → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₉ : 1 / 2 < z.re → GT.gt (α := ℝ) 2 0
⊢ z.re = 1 / 2
have linarith₂₀ : 1 / 2 < z.re → HMul.hMul (α := ℝ) 1 1 - 2 * z.re + (2 * z.re - HMul.hMul (α := ℝ) 1 1) = 0
Tactic: linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1| ≤ 1
have this : ‖(↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)‖ ≤ 1
Tactic: have : ‖(z : ℂ) + g 1 1‖ ≤ 1 := by simpa [denom, hc] using hg'
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
this : ‖(↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)‖ ≤ 1
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1| ≤ 1
have this₁ : |((↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)).re| ≤ 1
Tactic: have := (abs_re_le_norm _).trans this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
this_1 : ‖(↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)‖ ≤ 1
this : |((↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)).re| ≤ 1
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1| ≤ 1
have this₁ : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) + z.re| ≤ 1
Tactic: rw [add_re, intCast_re, add_comm, coe_re] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
this_1 : ‖(↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)‖ ≤ 1
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) + z.re| ≤ 1
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1| ≤ 1
have this₁ : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)| - |z.re| ≤ 1
Tactic: have := (abs_sub_abs_le_abs_add ..).trans this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
this_1 : ‖(↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)‖ ≤ 1
this_2 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) + z.re| ≤ 1
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)| - |z.re| ≤ 1
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1| ≤ 1
have this₁ : |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1| ≤ ⌊1 + 1 / 2⌋
Tactic: grw [sub_le_iff_le_add, hz.2, ← Int.cast_abs, ← Int.le_floor] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
this_1 : ‖(↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)‖ ≤ 1
this_2 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) + z.re| ≤ 1
this : |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1| ≤ ⌊1 + 1 / 2⌋
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1| ≤ 1
have h : 1 = ⌊1 + 1 / 2⌋
Tactic: convert! this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
this_1 : ‖(↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)‖ ≤ 1
this_2 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) + z.re| ≤ 1
this : |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1| ≤ ⌊1 + 1 / 2⌋
⊢ 1 = ⌊1 + 1 / 2⌋
have h : (↑1 : ℝ) ≤ 1 + 1 / 2 ∧ 1 + 1 / 2 < HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1
Tactic: rw [eq_comm, Int.floor_eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
Tactic: have hb : g 0 1 = -1 := by
    simpa [-SpecialLinearGroup.det_coe, det_fin_two, hd, hc, neg_eq_iff_eq_neg] using g.property
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hz' : ‖(↑z : ℂ)‖ = 1
Tactic: have hz' : ‖(z : ℂ)‖ = 1 :=
    le_antisymm (by simpa [denom, hc, hd] using hg') (one_le_normSq_iff.mp hz.1)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
⊢ g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
have a : ∀ (i j : Fin 2),
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S) : Matrix (Fin 2) (Fin 2) ℤ) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
i j : Fin 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S) : Matrix (Fin 2) (Fin 2) ℤ) i j
have a : (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] i j
Tactic: simp only [coe_mul, coe_S, coe_T_zpow, Matrix.mul_fin_two, mul_zero, mul_one, zero_add,
      one_mul, add_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
i j : Fin 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] i j
have a : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) j =
  !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
i j : Fin 2
a :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] i j
have a₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j =
  !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
j : Fin 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have a : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
j : Fin 2
a :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have a₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j