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 = 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
⊢ (T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = S * T ∨
      T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = T * S * T) ∧
    z = ρ

Tactic:
⟨?_, hρ⟩

Premises used: And.intro
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
refine :
  T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = S * T ∨ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = T * S * T
⊢ (T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = S * T ∨
      T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = T * S * T) ∧
    z = ρ

Tactic:
refine ⟨?_, hρ⟩
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
rw : 1 = -(↑ρ : ℂ) * ((↑1 : ℂ) + (↑ρ : ℂ))
⊢ (S * T) • ρ = ρ

Tactic:
rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, eq_comm, UpperHalfPlane.ext_iff,
      modular_S_smul, modular_T_smul, UpperHalfPlane.coe_mk, coe_vadd,
      ← mul_one (_ : ℂ)⁻¹, inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr ρ.ne_zero)]

Premises used: Iff.mpr, inv_smul_eq_iff, UpperHalfPlane.ρ, UpperHalfPlane.ext_iff, ModularGroup.S_inv, inv_mul_eq_iff_eq_mul₀, UpperHalfPlane.modular_S_smul, UpperHalfPlane.ne_zero, eq_comm, ModularGroup.S, Inv.inv, UpperHalfPlane.coe_mk, UpperHalfPlane.coe_vadd, neg_ne_zero, mul_one, ModularGroup.SL_neg_smul, SemigroupAction.mul_smul, UpperHalfPlane.modular_T_smul
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
⊢ 1 = -(↑ρ : ℂ) * ((↑1 : ℂ) + (↑ρ : ℂ))

Tactic:
grind [ρ_sq, ofReal_one]

Premises used: Complex.ofReal_one, UpperHalfPlane.ρ_sq
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
⊢ (S * T) • ρ = ρ

Tactic:
have hSTρ : (S * T) • ρ = ρ := by
    rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, eq_comm, UpperHalfPlane.ext_iff,
      modular_S_smul, modular_T_smul, UpperHalfPlane.coe_mk, coe_vadd,
      ← mul_one (_ : ℂ)⁻¹, inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr ρ.ne_zero)]
    grind [ρ_sq, ofReal_one]
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟

Tactic:
rw [hgeq, hρ, mul_assoc, mul_smul, hSTρ] at hg

Premises used: mul_assoc, SemigroupAction.mul_smul
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
⊢ ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1

Tactic:
rw [hgeq, hρ, mul_assoc, mul_smul, hSTρ] at hg

Premises used: mul_assoc, SemigroupAction.mul_smul
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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 [hgeq, hρ, mul_assoc, mul_smul, hSTρ] at hg

Premises used: mul_assoc, SemigroupAction.mul_smul
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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

Tactic:
rw [hgeq, hρ, mul_assoc, mul_smul, hSTρ] at hg

Premises used: mul_assoc, SemigroupAction.mul_smul
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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:
rw [hgeq, hρ, mul_assoc, mul_smul, hSTρ] at hg

Premises used: mul_assoc, SemigroupAction.mul_smul
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq₁ : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)

Tactic:
rw [hgeq, hρ, mul_assoc, mul_smul, hSTρ] at hg

Premises used: mul_assoc, SemigroupAction.mul_smul
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq₁ : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
⊢ z.re = -1 / 2

Tactic:
rw [hgeq, hρ, mul_assoc, mul_smul, hSTρ] at hg

Premises used: mul_assoc, SemigroupAction.mul_smul
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq₁ : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre₁ : z.re = -1 / 2
⊢ z = ρ

Tactic:
rw [hgeq, hρ, mul_assoc, mul_smul, hSTρ] at hg

Premises used: mul_assoc, SemigroupAction.mul_smul
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq₁ : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre₁ : z.re = -1 / 2
hρ₁ : z = ρ
⊢ (S * T) • ρ = ρ

Tactic:
rw [hgeq, hρ, mul_assoc, mul_smul, hSTρ] at hg

Premises used: mul_assoc, SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
inl :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0),
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = S * T ∨
      T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = T * S * T
inr :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1),
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = S * T ∨
      T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = T * S * T
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = S * T ∨ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = T * S * T

Tactic:
rcases this with h | h
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = S * T ∨ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = T * S * T

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = S * T ∨ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = T * S * T

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
suffices : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = S * T ∨ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T = T * S * T

Tactic:
suffices g 0 0 = 0 ∨ g 0 0 = 1 by rcases this with h | h <;> simp [h]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
⊢ |(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ).re| ≤ 1 / 2

Tactic:
have hgzre := hg.2
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hgzre : |(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ).re| ≤ 1 / 2
⊢ HAdd.hAdd (α := ℝ) 2⁻¹ 2⁻¹ = 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hgzre : |(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ).re| ≤ 1 / 2
⊢ 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧ LE.le (α := ℝ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) 1

Tactic:
simp only [Fin.isValue, ρ, neg_div, one_div, ← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re,
    abs_le, le_add_iff_nonneg_right, Int.cast_nonneg_iff, neg_add_le_iff_le_add,
    show (2⁻¹ : ℝ) + 2⁻¹ = 1 by norm_num] at hgzre

Premises used: le_add_iff_nonneg_right, neg_div, UpperHalfPlane.ρ, ModularGroup.coe_T_zpow_smul_eq, Int.cast_nonneg_iff, abs_le, Complex.add_re, Complex.intCast_re, neg_add_le_iff_le_add, Fin.isValue, one_div, UpperHalfPlane.coe_re
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hgzre : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧ LE.le (α := ℝ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) 1
⊢ 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 1

Tactic:
rw [← Int.cast_one (R := ℝ), Int.cast_le] at hgzre

Premises used: Int.cast_le, Int.cast_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hgzre : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1

Tactic:
grind
-- 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 : Matrix (Fin 2) (Fin 2) ℤ).det = 1

Tactic:
have := 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 = -1
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ).det = 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 -
      (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 =
    1

Tactic:
simp_rw [det_fin_two] at this

Premises used: Matrix.det_fin_two
-- 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
this :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 -
      (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 =
    1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1

Tactic:
grind
-- 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 : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1

Tactic:
have : g 0 1 = -g 0 0 - 1 := by
    have := g.property
    simp_rw [det_fin_two] at this
    grind
-- 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
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 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
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 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