awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
⊢ |1 + -z.re| ≤ 1 / 2

Tactic:
simp only [h, Int.cast_zero, zero_add, Int.cast_one] at this

Premises used: Int.cast_zero, zero_add, Int.cast_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
⊢ |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2

Tactic:
simp only [h, Int.cast_zero, zero_add, Int.cast_one] at this

Premises used: Int.cast_zero, zero_add, Int.cast_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0
this : |(-z.re)| ≤ 1 / 2
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ

Tactic:
grind [zpow_zero]

Premises used: zpow_zero
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
inr : ∀ (hzre : z.re = 1 / 2), g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
inr₁ :
  ∀ (hzre : z.re = -(1 / 2)), g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ

Tactic:
rcases (abs_eq one_half_pos.le).mp hzre with hzre | hzre

Premises used: abs_eq, Iff.mp
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = -(1 / 2)
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ

Tactic:
norm_num [hzre] at this
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
⊢ z.re = 1 / 2

Tactic:
rcases (abs_eq one_half_pos.le).mp hzre with hzre | hzre <;> [skip; norm_num [hzre] at this]

Premises used: abs_eq, Iff.mp
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ g = T * S

Tactic:
rw [h, zpow_one] at hg'

Premises used: zpow_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
hg'₁ : g = T * S
⊢ (S • z).re = -z.re

Tactic:
rw [h, zpow_one] at hg'

Premises used: zpow_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
hg'₁ : g = T * S
hSre₁ : (S • z).re = -z.re
⊢ |z.re| = 1 / 2

Tactic:
rw [h, zpow_one] at hg'

Premises used: zpow_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
hg'₁ : g = T * S
hSre₁ : (S • z).re = -z.re
hzre₁ : |z.re| = 1 / 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1

Tactic:
rw [h, zpow_one] at hg'

Premises used: zpow_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
hg'₁ : g = T * S
hSre₁ : (S • z).re = -z.re
hzre₁ : |z.re| = 1 / 2
h₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
⊢ |1 + -z.re| ≤ 1 / 2

Tactic:
rw [h, zpow_one] at hg'

Premises used: zpow_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
hg'₁ : g = T * S
hSre₁ : (S • z).re = -z.re
hzre₁ : |z.re| = 1 / 2
h₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this₁ : |1 + -z.re| ≤ 1 / 2
⊢ z.re = 1 / 2

Tactic:
rw [h, zpow_one] at hg'

Premises used: zpow_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ z.re = (HVAdd.hVAdd (α := ℝ) 1 ρ).re

Tactic:
norm_num [hzre, ρ]

Premises used: UpperHalfPlane.ρ
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
inr : ‖(↑z : ℂ)‖ = ‖(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ

Tactic:
refine .inr <| .inr ⟨hg', eq_of_re_of_norm (by norm_num [hzre, ρ]) ?_⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ 1 + (↑ρ : ℂ) = -HPow.hPow (β := ℕ) (↑ρ : ℂ) 2

Tactic:
grind [ρ_sq]

Premises used: UpperHalfPlane.ρ_sq
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ ‖(↑z : ℂ)‖ = ‖(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖

Tactic:
simp [hz', show 1 + (ρ : ℂ) = -ρ ^ 2 by grind [ρ_sq], norm_ρ]

Premises used: UpperHalfPlane.norm_ρ
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
⊢ 0 ≤ 1 / 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
⊢ z.re = 1 / 2 ∨ z.re = -(1 / 2)

Tactic:
rw [abs_eq (by norm_num)] at hzre

Premises used: abs_eq
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
hzre₁ : z.re = 1 / 2 ∨ z.re = -(1 / 2)
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1

Tactic:
rw [abs_eq (by norm_num)] at hzre

Premises used: abs_eq
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
hzre₁ : z.re = 1 / 2 ∨ z.re = -(1 / 2)
h₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
⊢ |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2

Tactic:
rw [abs_eq (by norm_num)] at hzre

Premises used: abs_eq
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : z.re = 1 / 2 ∨ z.re = -(1 / 2)
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
inr : ∀ (hzre : z.re = 1 / 2), g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
inr₁ :
  ∀ (hzre : z.re = -(1 / 2)), g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ

Tactic:
rcases hzre with hzre | hzre
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ

Tactic:
norm_num [hzre] at this
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : z.re = 1 / 2 ∨ z.re = -(1 / 2)
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
⊢ z.re = -(1 / 2)

Tactic:
rcases hzre with hzre | hzre <;> [norm_num [hzre] at this; skip]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T⁻¹ * S
hSre : (S • z).re = -z.re
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
hzre : z.re = -(1 / 2)
⊢ z.re = ρ.re

Tactic:
norm_num [hzre, ρ]

Premises used: UpperHalfPlane.ρ
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T⁻¹ * S
hSre : (S • z).re = -z.re
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
hzre : z.re = -(1 / 2)
rw : 1 = ‖(↑ρ : ℂ)‖
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ ‖(↑z : ℂ)‖ = ‖(↑ρ : ℂ)‖

Tactic:
rw [hz', norm_ρ]

Premises used: UpperHalfPlane.norm_ρ
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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
hg' : g = T⁻¹ * S
hSre : (S • z).re = -z.re
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
hzre : z.re = -(1 / 2)
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ

Tactic:
exact .inr <| .inl ⟨hg', eq_of_re_of_norm (by norm_num [hzre, ρ]) (by rw [hz', norm_ρ])⟩
-- 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 = 1
⊢ g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T

Tactic:
Subtype.ext ?_

Premises used: Matrix.SpecialLinearGroup, Subtype.ext
-- 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 = 1
refine :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) = (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T) : Matrix (Fin 2) (Fin 2) ℤ)
⊢ g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T

Tactic:
refine Subtype.ext ?_

Premises used: Subtype.ext
-- 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 = 1
rw :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) =
    !![(HMul.hMul (α := ℤ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 1) * 1 +
          (HMul.hMul (α := ℤ) 1 (-1) + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 0) * 0,
        (HMul.hMul (α := ℤ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 1) * 1 +
          (HMul.hMul (α := ℤ) 1 (-1) + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 0) * 1;
      (HMul.hMul (α := ℤ) 0 0 + HMul.hMul (α := ℤ) 1 1) * 1 + (HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 0) * 0,
        (HMul.hMul (α := ℤ) 0 0 + HMul.hMul (α := ℤ) 1 1) * 1 +
          (HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 0) * 1]
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) = (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T) : Matrix (Fin 2) (Fin 2) ℤ)

Tactic:
rw [coe_mul, coe_mul, coe_T_zpow, coe_S, coe_T, mul_fin_two, mul_fin_two]

Premises used: Matrix.mul_fin_two, ModularGroup.coe_T, ModularGroup.coe_T_zpow, ModularGroup.coe_S, Matrix.SpecialLinearGroup.coe_mul