awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(T * S) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(T * S) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(T * S) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
hz : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg : (T * S) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T * S)))
        (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖ ≤
    1
⊢ Eq (α := ℤ) (det (n := Fin 2) !![1, -1; 1, 0]) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(T * S) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(T * S) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(T * S) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
hz : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg : (T * S) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T * S)))
        (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖ ≤
    1
⊢ T * S = Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![1, -1; 1, 0] ⋯

Tactic:
decide
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(T * S) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(T * S) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(T * S) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
hz : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg : (T * S) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T * S)))
        (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖ ≤
    1
⊢ Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ))
              (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![1, -1; 1, 0] ⋯)))
          (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)) :
      ℝ)
    (1 : ℝ)

Tactic:
norm_num [ρ, denom, normSq, ← pow_two, div_pow]

Premises used: pow_two, UpperHalfPlane.ρ, Complex.normSq, UpperHalfPlane.denom, div_pow
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g_2 : SL(2, ℤ)
z_2 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc_1 : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
inr :
  ∀ (hc : 0 ≤ (↑(S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑(S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1)
    (hd : (↑(S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1) (hz : ρ ∈ 𝒟) (hg : (S * T) • ρ ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (S * T)))
            (↑ρ : ℂ)‖ ≤
        1),
    Eq (α := ℝ)
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (S * T)))
            (↑ρ : ℂ)) :
        ℝ)
      (1 : ℝ)
inr₁ :
  ∀ (hc : 0 ≤ (↑(T * S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑(T * S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1)
    (hd : (↑(T * S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1) (hz : ρ ∈ 𝒟) (hg : (T * S * T) • ρ ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T * S * T)))
            (↑ρ : ℂ)‖ ≤
        1),
    Eq (α := ℝ)
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T * S * T)))
            (↑ρ : ℂ)) :
        ℝ)
      (1 : ℝ)
⊢ Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    (1 : ℝ)

Tactic:
rcases case_c_one_d_one hz hg hden hc hd with ⟨(rfl | rfl), rfl⟩

Premises used: _private.0.ModularGroup.case_c_one_d_one, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
hz : ρ ∈ 𝒟
hg : (S * T) • ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (S * T)))
        (↑ρ : ℂ)‖ ≤
    1
⊢ Eq (α := ℤ) (det (n := Fin 2) !![0, -1; 1, 1]) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
hz : ρ ∈ 𝒟
hg : (S * T) • ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (S * T)))
        (↑ρ : ℂ)‖ ≤
    1
⊢ S * T = Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![0, -1; 1, 1] ⋯

Tactic:
decide
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
hz : ρ ∈ 𝒟
hg : (S * T) • ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (S * T)))
        (↑ρ : ℂ)‖ ≤
    1
⊢ Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ))
              (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![0, -1; 1, 1] ⋯)))
          (↑ρ : ℂ)) :
      ℝ)
    (1 : ℝ)

Tactic:
norm_num [ρ, denom, normSq, ← pow_two, div_pow]

Premises used: pow_two, UpperHalfPlane.ρ, Complex.normSq, UpperHalfPlane.denom, div_pow
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(T * S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(T * S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(T * S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
hz : ρ ∈ 𝒟
hg : (T * S * T) • ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T * S * T)))
        (↑ρ : ℂ)‖ ≤
    1
⊢ Eq (α := ℤ) (det (n := Fin 2) !![1, 0; 1, 1]) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(T * S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(T * S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(T * S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
hz : ρ ∈ 𝒟
hg : (T * S * T) • ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T * S * T)))
        (↑ρ : ℂ)‖ ≤
    1
⊢ T * S * T = Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![1, 0; 1, 1] ⋯

Tactic:
decide
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(T * S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(T * S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(T * S * T) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
hz : ρ ∈ 𝒟
hg : (T * S * T) • ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T * S * T)))
        (↑ρ : ℂ)‖ ≤
    1
⊢ Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ))
              (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![1, 0; 1, 1] ⋯)))
          (↑ρ : ℂ)) :
      ℝ)
    (1 : ℝ)

Tactic:
norm_num [ρ, denom, normSq, ← pow_two, div_pow]

Premises used: pow_two, UpperHalfPlane.ρ, Complex.normSq, UpperHalfPlane.denom, div_pow
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g_2 : SL(2, ℤ)
z_2 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc_1 : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
inr :
  ∀ (hc : 0 ≤ (↑(S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑(S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1)
    (hd : (↑(S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1) (hz : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟)
    (hg : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (S * T⁻¹)))
            (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖ ≤
        1),
    Eq (α := ℝ)
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (S * T⁻¹)))
            (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)) :
        ℝ)
      (1 : ℝ)
inr₁ :
  ∀ (hc : 0 ≤ (↑(T⁻¹ * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0)
    (hc : (↑(T⁻¹ * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1)
    (hd : (↑(T⁻¹ * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1) (hz : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟)
    (hg : (T⁻¹ * S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T⁻¹ * S * T⁻¹)))
            (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖ ≤
        1),
    Eq (α := ℝ)
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T⁻¹ * S * T⁻¹)))
            (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)) :
        ℝ)
      (1 : ℝ)
⊢ Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    (1 : ℝ)

Tactic:
rcases case_c_one_d_neg_one hz hg hden hc hd with ⟨(rfl | rfl), rfl⟩

Premises used: _private.0.ModularGroup.case_c_one_d_neg_one, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hz : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (S * T⁻¹)))
        (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖ ≤
    1
⊢ Eq (α := ℤ) (det (n := Fin 2) !![0, -1; 1, -1]) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hz : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (S * T⁻¹)))
        (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖ ≤
    1
⊢ S * T⁻¹ = Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![0, -1; 1, -1] ⋯

Tactic:
decide
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hz : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (S * T⁻¹)))
        (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖ ≤
    1
⊢ Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ))
              (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![0, -1; 1, -1] ⋯)))
          (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)) :
      ℝ)
    (1 : ℝ)

Tactic:
norm_num [ρ, denom, normSq, ← pow_two, div_pow]

Premises used: pow_two, UpperHalfPlane.ρ, Complex.normSq, UpperHalfPlane.denom, div_pow
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(T⁻¹ * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(T⁻¹ * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(T⁻¹ * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hz : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg : (T⁻¹ * S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T⁻¹ * S * T⁻¹)))
        (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖ ≤
    1
⊢ Eq (α := ℤ) (det (n := Fin 2) !![-1, 0; 1, -1]) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(T⁻¹ * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(T⁻¹ * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(T⁻¹ * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hz : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg : (T⁻¹ * S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T⁻¹ * S * T⁻¹)))
        (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖ ≤
    1
⊢ T⁻¹ * S * T⁻¹ = Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![-1, 0; 1, -1] ⋯

Tactic:
decide
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hc_1 : 0 ≤ (↑(T⁻¹ * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(T⁻¹ * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑(T⁻¹ * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hz : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg : (T⁻¹ * S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T⁻¹ * S * T⁻¹)))
        (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖ ≤
    1
⊢ Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ))
              (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![-1, 0; 1, -1] ⋯)))
          (↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)) :
      ℝ)
    (1 : ℝ)

Tactic:
norm_num [ρ, denom, normSq, ← pow_two, div_pow]

Premises used: pow_two, UpperHalfPlane.ρ, Complex.normSq, UpperHalfPlane.denom, div_pow
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
⊢ (g • z).im = z.im

Tactic:
have him : (g • z).im = z.im := serreTheorem_im_eq hz hg
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
inr :
  ∀
    (this :
      ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (him : (g • z).im = z.im)
        (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0),
        (g = 1 ∨ g = -1) ∨
          (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
            (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
              (g = S ∨ g = -S) ∧ ‖(↑z : ℂ)‖ = 1 ∨
                (g = T * S ∨ g = -(T * S)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                  (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                    (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                      (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                        (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ)
    (hc : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0),
    (g = 1 ∨ g = -1) ∨
      (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
        (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
          (g = S ∨ g = -S) ∧ ‖(↑z : ℂ)‖ = 1 ∨
            (g = T * S ∨ g = -(T * S)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                  (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                    (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
wlog :
  ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (him : (g • z).im = z.im)
    (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0),
    (g = 1 ∨ g = -1) ∨
      (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
        (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
          (g = S ∨ g = -S) ∧ ‖(↑z : ℂ)‖ = 1 ∨
            (g = T * S ∨ g = -(T * S)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                  (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                    (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖(↑z : ℂ)‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ

Tactic:
wlog hc : 0 ≤ g 1 0

Premises used: OfNat.ofNat, Subtype.val
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (him : (g • z).im = z.im)
    (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0),
    (g = 1 ∨ g = -1) ∨
      (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
        (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
          (g = S ∨ g = -S) ∧ ‖(↑z : ℂ)‖ = 1 ∨
            (g = T * S ∨ g = -(T * S)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                  (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                    (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
hc : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ -g • z ∈ 𝒟

Tactic:
simpa using hg
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (him : (g • z).im = z.im)
    (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0),
    (g = 1 ∨ g = -1) ∨
      (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
        (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
          (g = S ∨ g = -S) ∧ ‖(↑z : ℂ)‖ = 1 ∨
            (g = T * S ∨ g = -(T * S)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                  (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                    (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
hc : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ (-g • z).im = z.im

Tactic:
simpa using him
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (him : (g • z).im = z.im)
    (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0),
    (g = 1 ∨ g = -1) ∨
      (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
        (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
          (g = S ∨ g = -S) ∧ ‖(↑z : ℂ)‖ = 1 ∨
            (g = T * S ∨ g = -(T * S)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                  (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                    (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
hc : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ 0 ≤ (↑(-g) : Matrix (Fin 2) (Fin 2) ℤ) 1 0

Tactic:
simpa using (not_le.mp hc).le

Premises used: not_le, LT.lt.le, Iff.mp
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (him : (g • z).im = z.im)
    (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0),
    (g = 1 ∨ g = -1) ∨
      (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
        (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
          (g = S ∨ g = -S) ∧ ‖(↑z : ℂ)‖ = 1 ∨
            (g = T * S ∨ g = -(T * S)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                  (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                    (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
hc : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖(↑z : ℂ)‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ

Tactic:
simpa [neg_eq_iff_eq_neg, or_comm] using @this (-g) z hz (by simpa using hg)
      (by simpa using him) (by simpa using (not_le.mp hc).le)

Premises used: neg_eq_iff_eq_neg, or_comm
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ =
    1

Tactic:
rw [im_smul_eq_div_normSq, div_eq_iff (normSq_denom_pos _ z.im_ne_zero).ne',
    eq_comm, mul_eq_left₀ z.im_ne_zero, normSq_eq_norm_sq,
    pow_eq_one_iff_of_nonneg (norm_nonneg _) two_ne_zero] at him

Premises used: UpperHalfPlane.im_ne_zero, mul_eq_left₀, Complex.normSq_eq_norm_sq, UpperHalfPlane.normSq_denom_pos, eq_comm, LT.lt.ne', two_ne_zero, div_eq_iff, ModularGroup.im_smul_eq_div_normSq, pow_eq_one_iff_of_nonneg, norm_nonneg