awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
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 = T ^ b
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = -1
⊢ g = HPow.hPow (β := ℤ) T (-1)

Tactic:
rw [hb] at hgz
-- Module: Mathlib.NumberTheory.Modular
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 = T ^ b
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = -1
hgz₁ : g = HPow.hPow (β := ℤ) T (-1)
⊢ (g • z).re = (↑b : ℝ) + z.re

Tactic:
rw [hb] at hgz
-- Module: Mathlib.NumberTheory.Modular
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 = T ^ b
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = -1
hgz₁ : g = HPow.hPow (β := ℤ) T (-1)
hre₁ : (g • z).re = (↑b : ℝ) + z.re
⊢ b = -1

Tactic:
rw [hb] at hgz
-- Module: Mathlib.NumberTheory.Modular
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 0
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = 0
inl :
  (HPow.hPow (β := ℤ) T 0 = T ∨ HPow.hPow (β := ℤ) T 0 = -T) ∧ z.re = -1 / 2 ∨
    (HPow.hPow (β := ℤ) T 0 = T⁻¹ ∨ HPow.hPow (β := ℤ) T 0 = -T⁻¹) ∧ z.re = 1 / 2 ∨
      HPow.hPow (β := ℤ) T 0 = 1 ∨ HPow.hPow (β := ℤ) T 0 = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
rw [hgz]
-- Module: Mathlib.NumberTheory.Modular
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 0
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = 0
⊢ (HPow.hPow (β := ℤ) T 0 = T ∨ HPow.hPow (β := ℤ) T 0 = -T) ∧ z.re = -1 / 2 ∨
    (HPow.hPow (β := ℤ) T 0 = T⁻¹ ∨ HPow.hPow (β := ℤ) T 0 = -T⁻¹) ∧ z.re = 1 / 2 ∨
      HPow.hPow (β := ℤ) T 0 = 1 ∨ HPow.hPow (β := ℤ) T 0 = -1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Modular
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
inr : (g = T ∨ g = -T) ∧ z.re = -1 / 2
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
left
-- Module: Mathlib.NumberTheory.Modular
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
inr : z.re = -1 / 2
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2

Tactic:
rw [hgz, zpow_one, eq_self_iff_true, true_or, true_and]

Premises used: true_or, zpow_one, eq_self_iff_true, true_and
-- Module: Mathlib.NumberTheory.Modular
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 • z).re = 1 + z.re

Tactic:
rw [hb, Int.cast_one] at hre

Premises used: Int.cast_one
-- Module: Mathlib.NumberTheory.Modular
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
hre₁ : (g • z).re = 1 + z.re
⊢ b = 1

Tactic:
rw [hb, Int.cast_one] at hre

Premises used: Int.cast_one
-- Module: Mathlib.NumberTheory.Modular
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
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
linarith₂₀ : -1 / 2 < z.re → GT.gt (α := ℝ) 2 0
⊢ z.re = -1 / 2

Tactic:
linarith [(le_abs_self _).trans (abs_neg z.re ▸ hz.2), (le_abs_self _).trans hg.2]

Premises used: le_abs_self, And.right, LE.le.trans
-- Module: Mathlib.NumberTheory.Modular
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
inr : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
right
-- Module: Mathlib.NumberTheory.Modular
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
inr : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2
⊢ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
left
-- Module: Mathlib.NumberTheory.Modular
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
inr : z.re = 1 / 2
⊢ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2

Tactic:
rw [hgz, zpow_neg_one, eq_self_iff_true, true_or, true_and]

Premises used: zpow_neg_one, true_or, eq_self_iff_true, true_and
-- Module: Mathlib.NumberTheory.Modular
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 • z).re = -1 + z.re

Tactic:
rw [hb, Int.cast_neg, Int.cast_one] at hre

Premises used: Int.cast_neg, Int.cast_one
-- Module: Mathlib.NumberTheory.Modular
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
hre₁ : (g • z).re = -1 + z.re
⊢ b = -1

Tactic:
rw [hb, Int.cast_neg, Int.cast_one] at hre

Premises used: Int.cast_neg, Int.cast_one
-- Module: Mathlib.NumberTheory.Modular
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
linarith₂₀ : 1 / 2 < z.re → HMul.hMul (α := ℝ) 1 1 - 2 * z.re + (2 * z.re - HMul.hMul (α := ℝ) 1 1) = 0
⊢ z.re = 1 / 2

Tactic:
linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]

Premises used: le_abs_self, And.right, LE.le.trans
-- Module: Mathlib.NumberTheory.Modular
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
⊢ ‖(↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)‖ ≤ 1

Tactic:
simpa [denom, hc] using hg'

Premises used: UpperHalfPlane.denom
-- Module: Mathlib.NumberTheory.Modular
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
⊢ ‖(↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)‖ ≤ 1

Tactic:
have : ‖(z : ℂ) + g 1 1‖ ≤ 1 := by simpa [denom, hc] using hg'
-- Module: Mathlib.NumberTheory.Modular
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
⊢ |((↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)).re| ≤ 1

Tactic:
have := (abs_re_le_norm _).trans this
-- Module: Mathlib.NumberTheory.Modular
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) : ℝ) + z.re| ≤ 1

Tactic:
rw [add_re, intCast_re, add_comm, coe_re] at this

Premises used: Complex.add_re, Complex.intCast_re, add_comm, UpperHalfPlane.coe_re
-- Module: Mathlib.NumberTheory.Modular
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) : ℝ)| - |z.re| ≤ 1

Tactic:
have := (abs_sub_abs_le_abs_add ..).trans this
-- Module: Mathlib.NumberTheory.Modular
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 + 1 / 2⌋

Tactic:
grw [sub_le_iff_le_add, hz.2, ← Int.cast_abs, ← Int.le_floor] at this

Premises used: Int.cast_abs, sub_le_iff_le_add, And.right, Int.le_floor
-- Module: Mathlib.NumberTheory.Modular
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 + 1 / 2⌋

Tactic:
this
-- Module: Mathlib.NumberTheory.Modular
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⌋
h : 1 = ⌊1 + 1 / 2⌋
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1| ≤ 1

Tactic:
convert! this
-- Module: Mathlib.NumberTheory.Modular
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⌋
h : (↑1 : ℝ) ≤ 1 + 1 / 2 ∧ 1 + 1 / 2 < HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1
⊢ 1 = ⌊1 + 1 / 2⌋

Tactic:
rw [eq_comm, Int.floor_eq_iff]

Premises used: eq_comm, Int.floor_eq_iff
-- Module: Mathlib.NumberTheory.Modular
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 ∧ 1 + 1 / 2 < HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Modular
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 : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1

Tactic:
simpa [-SpecialLinearGroup.det_coe, det_fin_two, hd, hc, neg_eq_iff_eq_neg] using g.property

Premises used: Matrix.SpecialLinearGroup.det_coe, neg_eq_iff_eq_neg, Matrix.det_fin_two, Subtype.property
-- Module: Mathlib.NumberTheory.Modular
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 : 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
-- Module: Mathlib.NumberTheory.Modular
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
⊢ ‖(↑z : ℂ)‖ ≤ 1

Tactic:
simpa [denom, hc, hd] using hg'

Premises used: UpperHalfPlane.denom
-- Module: Mathlib.NumberTheory.Modular
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
⊢ ‖(↑z : ℂ)‖ = 1

Tactic:
have hz' : ‖(z : ℂ)‖ = 1 :=
    le_antisymm (by simpa [denom, hc, hd] using hg') (one_le_normSq_iff.mp hz.1)
-- Module: Mathlib.NumberTheory.Modular
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
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
⊢ g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S

Tactic:
ext i j
-- Module: Mathlib.NumberTheory.Modular
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) ℤ) i j = !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] i j
⊢ (↑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:
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]

Premises used: MulZeroClass.zero_mul, zero_add, MulZeroClass.mul_zero, Matrix.mul_fin_two, mul_one, add_zero, ModularGroup.coe_T_zpow, ModularGroup.coe_S, Matrix.SpecialLinearGroup.coe_mul, one_mul
-- Module: Mathlib.NumberTheory.Modular
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
a₁ :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] i j

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.Modular
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, ⋯⟩)
a₁ :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑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

Tactic:
fin_cases j