awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im), (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
inr : (g⁻¹ • g • z).im = z.im
⊢ (g • z).im = z.im

Tactic:
rw [← this (g := g⁻¹) hg (by simpa using hz) (by simpa using le_of_not_ge hden)]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im), (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
⊢ (g⁻¹ • g • z).im = z.im

Tactic:
simp
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
inr :
  ∀
    (this :
      ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im)
        (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0), (g • z).im = z.im)
    (hc : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0), (g • z).im = z.im
wlog :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im)
    (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0), (g • z).im = z.im
⊢ (g • z).im = z.im

Tactic:
wlog hc : 0 ≤ g 1 0

Premises used: OfNat.ofNat, Subtype.val
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im)
    (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0), (g • z).im = z.im
hc : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ -g • z ∈ 𝒟

Tactic:
simpa using hg
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im)
    (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0), (g • z).im = z.im
hc : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ z.im ≤ (-g • z).im

Tactic:
simpa using hden
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im)
    (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0), (g • z).im = z.im
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_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im)
    (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0), (g • z).im = z.im
hc : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ (g • z).im = z.im

Tactic:
simpa using @this (-g) z (-g) z hz (by simpa using hg)
      (by simpa using hden) (by simpa using (not_le.mp hc).le)
-- 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 : z.im ≤ (g • 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, le_div_iff₀ (normSq_denom_pos _ z.im_ne_zero),
    mul_le_iff_le_one_right z.im_pos, normSq_eq_norm_sq, sq_le_one_iff₀ (norm_nonneg _)] at hden

Premises used: UpperHalfPlane.im_pos, UpperHalfPlane.im_ne_zero, sq_le_one_iff₀, Complex.normSq_eq_norm_sq, UpperHalfPlane.normSq_denom_pos, ModularGroup.im_smul_eq_div_normSq, le_div_iff₀, norm_nonneg, mul_le_iff_le_one_right
-- 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 : z.im ≤ (g • z).im
hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hden₁ :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
⊢ 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0

Tactic:
rw [im_smul_eq_div_normSq, le_div_iff₀ (normSq_denom_pos _ z.im_ne_zero),
    mul_le_iff_le_one_right z.im_pos, normSq_eq_norm_sq, sq_le_one_iff₀ (norm_nonneg _)] at hden

Premises used: UpperHalfPlane.im_pos, UpperHalfPlane.im_ne_zero, sq_le_one_iff₀, Complex.normSq_eq_norm_sq, UpperHalfPlane.normSq_denom_pos, ModularGroup.im_smul_eq_div_normSq, le_div_iff₀, norm_nonneg, mul_le_iff_le_one_right
-- 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 : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1

Tactic:
grind [abs_c_le_one hz hg]

Premises used: ModularGroup.abs_c_le_one
-- 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 : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1

Tactic:
have hc : g 1 0 = 0 ∨ g 1 0 = 1 := by grind [abs_c_le_one hz hg]
-- 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 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
inl : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0), (g • z).im = z.im
inr : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1), (g • z).im = z.im
⊢ (g • z).im = z.im

Tactic:
rcases hc with hc | hc
-- 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 = 0
inl : ∀ (h : (g = T ∨ g = -T) ∧ z.re = -1 / 2), (g • z).im = z.im
inl₁ : ∀ (h : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2), (g • z).im = z.im
inl₂ : ∀ (h : g = 1), (g • z).im = z.im
inl₃ : ∀ (h : g = -1), (g • z).im = z.im
⊢ (g • z).im = z.im

Tactic:
rcases cases_c_zero hz hg hc with h | h | h | h

Premises used: _private.0.ModularGroup.cases_c_zero
-- 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 = 0
h : (g = T ∨ g = -T) ∧ z.re = -1 / 2
inl :
  ∀ (hg : T • z ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T))
            (↑z : ℂ)‖ ≤
        1)
    (hc : 0 ≤ (↑T : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑T : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0), (T • z).im = z.im
inl₁ :
  ∀ (hg : -T • z ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-T)))
            (↑z : ℂ)‖ ≤
        1)
    (hc : 0 ≤ (↑(-T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑(-T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0),
    (-T • z).im = z.im
⊢ (g • z).im = z.im

Tactic:
rcases h with ⟨(rfl | rfl), -⟩

Premises used: rfl
-- 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 = 0
h : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2
inl :
  ∀ (hg : T⁻¹ • z ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T⁻¹))
            (↑z : ℂ)‖ ≤
        1)
    (hc : 0 ≤ (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0),
    (T⁻¹ • z).im = z.im
inl₁ :
  ∀ (hg : -T⁻¹ • z ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-T⁻¹)))
            (↑z : ℂ)‖ ≤
        1)
    (hc : 0 ≤ (↑(-T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑(-T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0),
    (-T⁻¹ • z).im = z.im
⊢ (g • z).im = z.im

Tactic:
rcases h with ⟨(rfl | rfl), -⟩

Premises used: rfl
-- 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 = 0
h : g = 1
inl :
  ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) 1 z ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) 1))
            (↑z : ℂ)‖ ≤
        1)
    (hc : LE.le (α := ℤ) 0 ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0))
    (hc : Eq (α := ℤ) ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0), (HSMul.hSMul (α := SL(2, ℤ)) 1 z).im = z.im
⊢ (g • z).im = z.im

Tactic:
rcases h with ⟨(rfl | rfl), -⟩

Premises used: rfl
-- 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 = 0
h : g = -1
inl :
  ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) (-1) z ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-1)))
            (↑z : ℂ)‖ ≤
        1)
    (hc : LE.le (α := ℤ) 0 ((↑(-1) : Matrix (Fin 2) (Fin 2) ℤ) 1 0))
    (hc : Eq (α := ℤ) ((↑(-1) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0), (HSMul.hSMul (α := SL(2, ℤ)) (-1) z).im = z.im
⊢ (g • z).im = z.im

Tactic:
rcases h with ⟨(rfl | rfl), -⟩

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

Tactic:
simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Premises used: zpow_neg_one, ModularGroup.im_T_smul, ModularGroup.im_T_zpow_smul, one_smul, ModularGroup.SL_neg_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z_2 z : ℍ
hz : z ∈ 𝒟
hg : -T • z ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-T)))
        (↑z : ℂ)‖ ≤
    1
hc_1 : 0 ≤ (↑(-T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(-T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ (-T • z).im = z.im

Tactic:
simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Premises used: zpow_neg_one, ModularGroup.im_T_smul, ModularGroup.im_T_zpow_smul, one_smul, ModularGroup.SL_neg_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z_2 z : ℍ
hz : z ∈ 𝒟
hg : T⁻¹ • z ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T⁻¹))
        (↑z : ℂ)‖ ≤
    1
hc_1 : 0 ≤ (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ (T⁻¹ • z).im = z.im

Tactic:
simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Premises used: zpow_neg_one, ModularGroup.im_T_smul, ModularGroup.im_T_zpow_smul, one_smul, ModularGroup.SL_neg_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z_2 z : ℍ
hz : z ∈ 𝒟
hg : -T⁻¹ • z ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-T⁻¹)))
        (↑z : ℂ)‖ ≤
    1
hc_1 : 0 ≤ (↑(-T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0
hc : (↑(-T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ (-T⁻¹ • z).im = z.im

Tactic:
simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Premises used: zpow_neg_one, ModularGroup.im_T_smul, ModularGroup.im_T_zpow_smul, one_smul, ModularGroup.SL_neg_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z_2 z : ℍ
hz : z ∈ 𝒟
hg : HSMul.hSMul (α := SL(2, ℤ)) 1 z ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) 1))
        (↑z : ℂ)‖ ≤
    1
hc_1 : LE.le (α := ℤ) 0 ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0)
hc : Eq (α := ℤ) ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0
⊢ (HSMul.hSMul (α := SL(2, ℤ)) 1 z).im = z.im

Tactic:
simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Premises used: zpow_neg_one, ModularGroup.im_T_smul, ModularGroup.im_T_zpow_smul, one_smul, ModularGroup.SL_neg_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z_2 z : ℍ
hz : z ∈ 𝒟
hg : HSMul.hSMul (α := SL(2, ℤ)) (-1) z ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-1)))
        (↑z : ℂ)‖ ≤
    1
hc_1 : LE.le (α := ℤ) 0 ((↑(-1) : Matrix (Fin 2) (Fin 2) ℤ) 1 0)
hc : Eq (α := ℤ) ((↑(-1) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0
⊢ (HSMul.hSMul (α := SL(2, ℤ)) (-1) z).im = z.im

Tactic:
simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Premises used: zpow_neg_one, ModularGroup.im_T_smul, ModularGroup.im_T_zpow_smul, one_smul, ModularGroup.SL_neg_smul
-- 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
inr :
  Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    (1 : ℝ)
⊢ (g • z).im = z.im

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]

Premises used: UpperHalfPlane.im_ne_zero, mul_eq_left₀, UpperHalfPlane.normSq_denom_pos, eq_comm, LT.lt.ne', div_eq_iff, ModularGroup.im_smul_eq_div_normSq
-- 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
inr :
  ∀ (hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0),
    Eq (α := ℝ)
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
            (↑z : ℂ)) :
        ℝ)
      (1 : ℝ)
inr₁ :
  ∀ (hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 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 : ℝ)
inr₂ :
  ∀ (hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 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 : ℝ)
⊢ 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 Int.abs_le_one_iff.mp (cases_d_of_c_eq_one hz hden hc) with hd | hd | hd

Premises used: _private.0.ModularGroup.cases_d_of_c_eq_one, Int.abs_le_one_iff, Iff.mp
-- 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 = 0
inr :
  ∀ (hnm : ‖(↑z : ℂ)‖ = 1) (hg : S • z ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S))
            (↑z : ℂ)‖ ≤
        1)
    (hc : 0 ≤ (↑S : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑S : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1)
    (hd : (↑S : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0),
    Eq (α := ℝ)
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S))
            (↑z : ℂ)) :
        ℝ)
      (1 : ℝ)
inr₁ :
  ∀ (hc : 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 : ρ ∈ 𝒟) (hg : (T⁻¹ * S) • ρ ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T⁻¹ * S)))
            (↑ρ : ℂ)‖ ≤
        1),
    Eq (α := ℝ)
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T⁻¹ * S)))
            (↑ρ : ℂ)) :
        ℝ)
      (1 : ℝ)
inr₂ :
  ∀ (hc : 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, ℝ)) (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, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    (1 : ℝ)

Tactic:
rcases cases_c_one_d_zero hz hg hden hc hd with
        ⟨rfl, hnm⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩

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

Tactic:
simp [normSq_eq_norm_sq, denom, coe_S, hnm]

Premises used: Complex.normSq_eq_norm_sq, UpperHalfPlane.denom, ModularGroup.coe_S
-- 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 : ρ ∈ 𝒟
hg : (T⁻¹ * S) • ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T⁻¹ * S)))
        (↑ρ : ℂ)‖ ≤
    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 : ρ ∈ 𝒟
hg : (T⁻¹ * S) • ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T⁻¹ * S)))
        (↑ρ : ℂ)‖ ≤
    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 : ρ ∈ 𝒟
hg : (T⁻¹ * S) • ρ ∈ 𝒟
hden :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (T⁻¹ * S)))
        (↑ρ : ℂ)‖ ≤
    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] ⋯)))
          (↑ρ : ℂ)) :
      ℝ)
    (1 : ℝ)

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

Premises used: pow_two, UpperHalfPlane.ρ, UpperHalfPlane.denom, div_pow