awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 : ℝ)
⊢ Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    (1 : ℝ)
have 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 : ℝ)
Tactic: rcases cases_c_one_d_zero hz hg hden hc hd with
        ⟨rfl, hnm⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
Cleared hypotheses: g, z, hz, hg, hden, hc_1, hc, hd
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    (1 : ℝ)
have 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 : ℝ)
Tactic: rcases case_c_one_d_one hz hg hden hc hd with ⟨(rfl | rfl), rfl⟩
Cleared hypotheses: g, z, hz, hg, hden, hc_1, hc, hd
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 : ℝ)
⊢ Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    (1 : ℝ)
have 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 : ℝ)
Tactic: rcases case_c_one_d_one hz hg hden hc hd with ⟨(rfl | rfl), rfl⟩
Cleared hypotheses: g, z, hz, hg, hden, hc_1, hc, hd
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    (1 : ℝ)
have 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 : ℝ)
Tactic: rcases case_c_one_d_neg_one hz hg hden hc hd with ⟨(rfl | rfl), rfl⟩
Cleared hypotheses: g, z, hz, hg, hden, hc_1, hc, hd
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 : ℝ)
⊢ Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    (1 : ℝ)
have 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 : ℝ)
Tactic: rcases case_c_one_d_neg_one hz hg hden hc hd with ⟨(rfl | rfl), rfl⟩
Cleared hypotheses: g, z, hz, hg, hden, hc_1, hc, hd
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • 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 = ρ
have him : (g • z).im = z.im
Tactic: have him : (g • z).im = z.im := serreTheorem_im_eq hz hg
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
⊢ (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 = ρ
have 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 = ρ
Tactic: wlog hc : 0 ≤ g 1 0
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 = ρ
⊢ (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 = ρ
have 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 = ρ
Tactic: wlog hc : 0 ≤ g 1 0
Cleared hypotheses: hz, hg, him
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
⊢ (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 = ρ
have him₁ : ‖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
Cleared hypotheses: him, hc
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him :
  ‖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 = 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 = ρ
have hc₁ : (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him :
  ‖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
⊢ (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 = ρ
have inl : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 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: rcases hc with hc | hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him :
  ‖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 = 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 = ρ
have inr : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1),
  (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: rcases hc with hc | hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him :
  ‖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
⊢ (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 = ρ
have inr : ∀ (hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 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: rcases Int.abs_le_one_iff.mp (cases_d_of_c_eq_one hz him.le hc) with hd | hd | hd