awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₁ :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑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

Tactic:
fin_cases 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
⊢ (↑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, ⋯⟩)

Tactic:
tauto
-- 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
⊢ (↑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, ⋯⟩)

Tactic:
tauto
-- 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
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
tauto
-- 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
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
tauto
-- 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
⊢ g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S

Tactic:
have hg' : g = T ^ g 0 0 * S := by
    ext i j
    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]
    fin_cases i <;> fin_cases j <;> tauto
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • 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
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟

Tactic:
rw [hg', mul_smul] at hg

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • 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
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
⊢ ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1

Tactic:
rw [hg', mul_smul] at hg

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • 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
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'₁ :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1

Tactic:
rw [hg', mul_smul] at hg

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • 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
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • 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 = 0

Tactic:
rw [hg', mul_smul] at hg

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • 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
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • 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:
rw [hg', mul_smul] at hg

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • 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
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • 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:
rw [hg', mul_smul] at hg

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • 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
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • 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

Tactic:
rw [hg', mul_smul] at hg

Premises used: SemigroupAction.mul_smul
-- 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
rw : { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }.re = -z.re
rw₁ : (↑{ coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } : ℂ).re = -z.re
rw₂ : (-(↑z : ℂ))⁻¹.re = -z.re
rw₃ : HDiv.hDiv (β := ℝ) (-(↑z : ℂ)).re ((normSq : (a : ℂ) → ℝ) (-(↑z : ℂ)) : ℝ) = -z.re
rw₄ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖-(↑z : ℂ)‖ 2 = -z.re
rw₅ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 = -z.re
rw₆ : (-(↑z : ℂ)).re / HPow.hPow (α := ℝ) (β := ℕ) 1 2 = -z.re
rw₇ : (-(↑z : ℂ)).re / 1 = -z.re
rw₈ : (-(↑z : ℂ)).re = -z.re
rw₉ : -(↑z : ℂ).re = -z.re
rw₁₀ rw₁₁ : -z.re = -z.re
⊢ (S • z).re = -z.re

Tactic:
rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]

Premises used: one_pow, Complex.normSq_eq_norm_sq, Complex.inv_re, UpperHalfPlane.modular_S_smul, Complex.neg_re, UpperHalfPlane.coe_mk, norm_neg, UpperHalfPlane.coe_re, div_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
⊢ (S • z).re = -z.re

Tactic:
have hSre : re (S • z) = -z.re := by
    rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
⊢ |(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z).re| ≤ 1 / 2

Tactic:
have := hg.2
-- 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 : |(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z).re| ≤ 1 / 2
⊢ |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2

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

Premises used: ModularGroup.coe_T_zpow_smul_eq, Complex.add_re, Complex.intCast_re, add_comm, UpperHalfPlane.coe_re
-- 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
⊢ |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| - |(-z.re)| ≤ 1 / 2

Tactic:
have := (abs_sub_abs_le_abs_add _ _).trans 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
this_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| - |(-z.re)| ≤ 1 / 2
⊢ |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| ≤ 1 / 2 + |z.re|

Tactic:
rw [abs_neg, sub_le_iff_le_add] at this

Premises used: abs_neg, sub_le_iff_le_add
-- 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_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| ≤ 1 / 2 + |z.re|
inl : ∀ (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 lt_or_eq_of_le hz.2 with hzre | hzre

Premises used: lt_or_eq_of_le, And.right
-- 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_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| ≤ 1 / 2 + |z.re|
hzre : |z.re| < 1 / 2
⊢ |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| < 1 / 2 + 1 / 2

Tactic:
have := this.trans_lt ((add_lt_add_iff_left _).mpr 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
this_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this_2 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| ≤ 1 / 2 + |z.re|
hzre : |z.re| < 1 / 2
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| < 1 / 2 + 1 / 2
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0| < 1

Tactic:
rw [add_halves, ← Int.cast_abs, ← Int.cast_one (R := ℝ), Int.cast_lt] at this

Premises used: Int.cast_abs, add_halves, Int.cast_lt, 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_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this_2 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| ≤ 1 / 2 + |z.re|
hzre : |z.re| < 1 / 2
this : |(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0| < 1
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ

Tactic:
grind [Int.abs_lt_one_iff, zpow_zero]

Premises used: zpow_zero, Int.abs_lt_one_iff
-- 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_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| ≤ 1 / 2 + |z.re|
hzre : |z.re| = 1 / 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1

Tactic:
rw [hzre, add_halves, ← Int.cast_abs, ← Int.cast_one (R := ℝ), Int.cast_le,
      Int.abs_le_one_iff] at this

Premises used: Int.cast_abs, Int.cast_le, add_halves, Int.abs_le_one_iff, 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_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| ≤ 1 / 2 + |z.re|
hzre : |z.re| = 1 / 2
this₁ :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
⊢ |z.re| = 1 / 2

Tactic:
rw [hzre, add_halves, ← Int.cast_abs, ← Int.cast_one (R := ℝ), Int.cast_le,
      Int.abs_le_one_iff] at this

Premises used: Int.cast_abs, Int.cast_le, add_halves, Int.abs_le_one_iff, 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_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hzre : |z.re| = 1 / 2
inr :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0),
    g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
inr₁ :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1),
    g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
inr₂ :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1),
    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 this with h | h | h
-- 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 = 0
⊢ |(-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