awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 = ρ
⊢ (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 = 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 Int.abs_le_one_iff.mp (cases_d_of_c_eq_one hz him.le hc) with hd | hd | hd
-- 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
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 = ρ
inr₁ :
  ∀ (hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 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 = ρ
⊢ (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 = -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 Int.abs_le_one_iff.mp (cases_d_of_c_eq_one hz him.le hc) with hd | hd | hd
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ T • z ≠ z
have apply_fun : (T • z).re ≠ z.re
Tactic: apply_fun UpperHalfPlane.re
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ g = 1 ∨ g = -1
have this : T • z ≠ z
Tactic: have : T • z ≠ z := by
    apply_fun UpperHalfPlane.re
    simp [-sl_moeb, re_T_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
this : T • z ≠ z
⊢ T⁻¹ • z ≠ z
have rwa : ¬T⁻¹ • z = z
Tactic: rwa [ne_eq, inv_smul_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
this : T • z ≠ z
rwa : ¬T⁻¹ • z = z
⊢ T⁻¹ • z ≠ z
have rwa₁ : ¬z = T • z
Tactic: rwa [ne_eq, inv_smul_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
this : T • z ≠ z
rwa : ¬T⁻¹ • z = z
rwa₁ : ¬z = T • z
⊢ T⁻¹ • z ≠ z
have rwa₂ : ¬T • z = z
Tactic: rwa [ne_eq, inv_smul_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
this : T • z ≠ z
⊢ g = 1 ∨ g = -1
have this₁ : T⁻¹ • z ≠ z
Tactic: have : T⁻¹ • z ≠ z := by rwa [ne_eq, inv_smul_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
this_1 : T • z ≠ z
this : T⁻¹ • z ≠ z
⊢ g = 1 ∨ g = -1
have this₁ : (↑z : ℂ) ≠ -(↑I : ℂ)
Tactic: have : (z : ℂ) ≠ -I := by grind [neg_im, coe_I, Complex.I_im, z.coe_im_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
this_1 : T • z ≠ z
this_2 : T⁻¹ • z ≠ z
this : (↑z : ℂ) ≠ -(↑I : ℂ)
⊢ S • z ≠ z
have contrapose : ∀ (hzI : S • z = z), z = I
Tactic: contrapose hzI
Cleared hypotheses: hzI
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
this_1 : T • z ≠ z
this_2 : T⁻¹ • z ≠ z
this : (↑z : ℂ) ≠ -(↑I : ℂ)
hzI : S • z = z
⊢ z = I
have hzI₁ : I = z ∨ (↑I : ℂ) = -(↑z : ℂ)
Tactic: rw [UpperHalfPlane.ext_iff, modular_S_smul, coe_mk, ← mul_one (_ : ℂ)⁻¹,
      inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr z.ne_zero), neg_mul, ← neg_eq_iff_eq_neg, ← I_sq,
      ← sq, sq_eq_sq_iff_eq_or_eq_neg, ← coe_I, ← UpperHalfPlane.ext_iff] at hzI
Cleared hypotheses: hzI
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
this_1 : T • z ≠ z
this_2 : T⁻¹ • z ≠ z
this : (↑z : ℂ) ≠ -(↑I : ℂ)
⊢ g = 1 ∨ g = -1
have this₁ : S • z ≠ z
Tactic: have : S • z ≠ z := by
    contrapose hzI
    rw [UpperHalfPlane.ext_iff, modular_S_smul, coe_mk, ← mul_one (_ : ℂ)⁻¹,
      inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr z.ne_zero), neg_mul, ← neg_eq_iff_eq_neg, ← I_sq,
      ← sq, sq_eq_sq_iff_eq_or_eq_neg, ← coe_I, ← UpperHalfPlane.ext_iff] at hzI
    grind
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
⊢ g • I = I ↔ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g
have mp : g • I = I → Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
mp : g • I = I → Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g
⊢ g • I = I ↔ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g
have mpr : Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g → g • I = I
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hg : g • I = I
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g
have this : (g = 1 ∨ g = -1) ∨
  (g = T ∨ g = -T) ∧ I.re = -1 / 2 ∨
    (g = T⁻¹ ∨ g = -T⁻¹) ∧ I.re = 1 / 2 ∨
      (g = S ∨ g = -S) ∧ ‖(↑I : ℂ)‖ = 1 ∨
        (g = T * S ∨ g = -(T * S)) ∧ I = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
          (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ I = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
            (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ I = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = S * T ∨ g = -(S * T)) ∧ I = ρ ∨
                (g = T * S * T ∨ g = -(T * S * T)) ∧ I = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ I = ρ
Tactic: have := cases_of_mem_fd_smul_mem_fd I_mem_fd (hg.symm ▸ I_mem_fd)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hg : g • I = I
this :
  (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ I.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ I.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖(↑I : ℂ)‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ I = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ I = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ I = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ I = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ I = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ I = ρ
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g
have this₁ : (g = 1 ∨ g = -1) ∨ g = S ∨ g = -S
Tactic: norm_num [UpperHalfPlane.ext_iff, Complex.ext_iff, ρ] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g → g • I = I
have mpr : S • I = I
Tactic: suffices S • I = I by simp +contextual [-sl_moeb, or_imp, this]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
⊢ S • I = I
have mpr : (↑{ coe := (-(↑I : ℂ))⁻¹, coe_im_pos := sorry : ℍ } : ℂ) = (↑I : ℂ)
Tactic: rw [modular_S_smul, UpperHalfPlane.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
⊢ g • ρ = ρ ↔ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g
have mp : g • ρ = ρ → Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
mp : g • ρ = ρ → Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g
⊢ g • ρ = ρ ↔ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g
have mpr : Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g → g • ρ = ρ
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
⊢ S • ρ ≠ ρ
have rw : ¬((-(↑ρ : ℂ))⁻¹.re = (↑ρ : ℂ).re ∧ (-(↑ρ : ℂ))⁻¹.im = (↑ρ : ℂ).im)
Tactic: rw [ne_eq, UpperHalfPlane.ext_iff, modular_S_smul, coe_mk, Complex.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
⊢ g ≠ S ∧ g ≠ -S
have this : S • ρ ≠ ρ
Tactic: have : S • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_S_smul, coe_mk, Complex.ext_iff]
        norm_num [ρ, ← pow_two, div_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g
have neS : g ≠ S ∧ g ≠ -S
Tactic: have neS : g ≠ S ∧ g ≠ -S := by
      have : S • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_S_smul, coe_mk, Complex.ext_iff]
        norm_num [ρ, ← pow_two, div_pow]
      grind [SL_neg_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ T • ρ ≠ ρ
have rw : ¬(↑1 : ℂ) + (↑ρ : ℂ) = (↑ρ : ℂ)
Tactic: rw [ne_eq, UpperHalfPlane.ext_iff, modular_T_smul, coe_vadd]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
have this : T • ρ ≠ ρ
Tactic: have : T • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_T_smul, coe_vadd]
        norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
this : T • ρ ≠ ρ
⊢ T⁻¹ • ρ ≠ ρ
have rwa : ¬T⁻¹ • ρ = ρ
Tactic: rwa [ne_eq, inv_smul_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
this : T • ρ ≠ ρ
rwa : ¬T⁻¹ • ρ = ρ
⊢ T⁻¹ • ρ ≠ ρ
have rwa₁ : ¬ρ = T • ρ
Tactic: rwa [ne_eq, inv_smul_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
this : T • ρ ≠ ρ
rwa : ¬T⁻¹ • ρ = ρ
rwa₁ : ¬ρ = T • ρ
⊢ T⁻¹ • ρ ≠ ρ
have rwa₂ : ¬T • ρ = ρ
Tactic: rwa [ne_eq, inv_smul_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
this : T • ρ ≠ ρ
⊢ g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
have this₁ : T⁻¹ • ρ ≠ ρ
Tactic: have : T⁻¹ • ρ ≠ ρ := by rwa [ne_eq, inv_smul_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g
have neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
Tactic: have neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹ := by
      have : T • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_T_smul, coe_vadd]
        norm_num
      have : T⁻¹ • ρ ≠ ρ := by rwa [ne_eq, inv_smul_eq_iff, eq_comm]
      grind [SL_neg_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
⊢ (T * S * T) • ρ ≠ ρ
have simp : ¬((↑(HVAdd.hVAdd (α := ℝ) 1 { coe := (-(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ))⁻¹, coe_im_pos := sorry : ℍ }) : ℂ).re =
      (↑ρ : ℂ).re ∧
    (↑(HVAdd.hVAdd (α := ℝ) 1 { coe := (-(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ))⁻¹, coe_im_pos := sorry : ℍ }) : ℂ).im =
      (↑ρ : ℂ).im)
Tactic: simp only [mul_smul, modular_T_smul, modular_S_smul,
          ne_eq, UpperHalfPlane.ext_iff, Complex.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
⊢ g ≠ T * S * T ∧ g ≠ -(T * S * T)
have this : (T * S * T) • ρ ≠ ρ
Tactic: have : (T * S * T) • ρ ≠ ρ := by
        simp only [mul_smul, modular_T_smul, modular_S_smul,
          ne_eq, UpperHalfPlane.ext_iff, Complex.ext_iff]
        norm_num [ρ, ← pow_two, div_pow, normSq]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g
have neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T)
Tactic: have neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T) := by
      have : (T * S * T) • ρ ≠ ρ := by
        simp only [mul_smul, modular_T_smul, modular_S_smul,
          ne_eq, UpperHalfPlane.ext_iff, Complex.ext_iff]
        norm_num [ρ, ← pow_two, div_pow, normSq]
      grind [SL_neg_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T)
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g
have this : (g = 1 ∨ g = -1) ∨
  (g = T ∨ g = -T) ∧ ρ.re = -1 / 2 ∨
    (g = T⁻¹ ∨ g = -T⁻¹) ∧ ρ.re = 1 / 2 ∨
      (g = S ∨ g = -S) ∧ ‖(↑ρ : ℂ)‖ = 1 ∨
        (g = T * S ∨ g = -(T * S)) ∧ ρ = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
          (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ ρ = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
            (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ ρ = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = S * T ∨ g = -(S * T)) ∧ ρ = ρ ∨
                (g = T * S * T ∨ g = -(T * S * T)) ∧ ρ = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ ρ = ρ
Tactic: have := cases_of_mem_fd_smul_mem_fd ρ_mem_fd (hg ▸ ρ_mem_fd)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T)
this :
  (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ ρ.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ ρ.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖(↑ρ : ℂ)‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ ρ = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ ρ = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ ρ = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ ρ = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ ρ = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ ρ = ρ
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g
have this₁ : (g = 1 ∨ g = -1) ∨ (g = S * T ∨ g = -(S * T)) ∨ g = T⁻¹ * S ∨ g = -(T⁻¹ * S)
Tactic: norm_num [UpperHalfPlane.ext_iff, Complex.ext_iff, norm_ρ, ρ, neS, neT, neTST] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g → g • ρ = ρ
have mpr : (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ
Tactic: suffices (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ by simp +contextual [-sl_moeb, or_imp, this]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
⊢ (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ
have mpr : (↑ρ : ℂ) = (↑{ coe := (-(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ))⁻¹, coe_im_pos := sorry } : ℂ)
Tactic: rw [mul_smul T⁻¹, inv_smul_eq_iff, ← eq_inv_smul_iff (g := S), S_inv, SL_neg_smul,
      mul_smul, eq_comm, and_self, modular_T_smul, modular_S_smul, UpperHalfPlane.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
⊢ g = 1 ∨ g = -1
have this : ρ ∉ 𝒟ᵒ
Tactic: have : ρ ∉ 𝒟ᵒ := by
    intro h
    grind [norm_ρ, one_lt_normSq_iff.mp h.1]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
this : ρ ∉ 𝒟ᵒ
h : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟ᵒ
⊢ False
have this₁ : (HVAdd.hVAdd (α := ℝ) 1 ρ).re = 1 / 2
Tactic: have : ((1 : ℝ) +ᵥ ρ).re = 1 / 2 := by norm_num [← coe_re, coe_vadd, ρ]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
this : ρ ∉ 𝒟ᵒ
⊢ g = 1 ∨ g = -1
have this₁ : HVAdd.hVAdd (α := ℝ) 1 ρ ∉ 𝒟ᵒ
Tactic: have : (1 : ℝ) +ᵥ ρ ∉ 𝒟ᵒ := by
    intro h
    have : ((1 : ℝ) +ᵥ ρ).re = 1 / 2 := by norm_num [← coe_re, coe_vadd, ρ]
    grind [h.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
have inl : ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) 1 z ∈ 𝒟ᵒ), Eq (α := ℤ) ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0
Tactic: rcases eq_one_or_neg_one_of_mem_fdo_mem_fdo hz hg with rfl | rfl
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
inl : ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) 1 z ∈ 𝒟ᵒ), Eq (α := ℤ) ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
have inr : ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) (-1) z ∈ 𝒟ᵒ), Eq (α := ℤ) ((↑(-1) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0
Tactic: rcases eq_one_or_neg_one_of_mem_fdo_mem_fdo hz hg with rfl | rfl
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ z = g • z
have inl : ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) 1 z ∈ 𝒟ᵒ), z = HSMul.hSMul (α := SL(2, ℤ)) 1 z
Tactic: rcases eq_one_or_neg_one_of_mem_fdo_mem_fdo hz hg with rfl | rfl
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
inl : ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) 1 z ∈ 𝒟ᵒ), z = HSMul.hSMul (α := SL(2, ℤ)) 1 z
⊢ z = g • z
have inr : ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) (-1) z ∈ 𝒟ᵒ), z = HSMul.hSMul (α := SL(2, ℤ)) (-1) z
Tactic: rcases eq_one_or_neg_one_of_mem_fdo_mem_fdo hz hg with rfl | rfl
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
⊢ IsClosed 𝒟
have refine : IsClosed (X := ℍ) fun (z : ℍ) ↦ Real.le✝ |z.re| (1 / 2)
Tactic: refine .inter (.preimage (by fun_prop) isClosed_Ici) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
⊢ IsOpen 𝒟ᵒ
have refine : IsOpen (X := ℍ) fun (z : ℍ) ↦ Real.lt✝ |z.re| (1 / 2)
Tactic: refine .inter (.preimage (by fun_prop) isOpen_Ioi) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
⊢ UpperHalfPlane.coe '' 𝒟ᵒ = {z : ℂ | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2}
have h : ∀ (x : ℂ), x ∈ UpperHalfPlane.coe '' 𝒟ᵒ ↔ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
x : ℂ
⊢ x ∈ UpperHalfPlane.coe '' 𝒟ᵒ ↔ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2} x
have h : x ∈ UpperHalfPlane.coe '' 𝒟ᵒ → Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2} x
Tactic: refine ⟨?_, fun ⟨hxim, hxnorm, hxre⟩ ↦ ⟨⟨x, hxim⟩, ⟨one_lt_normSq_iff.mpr hxnorm, hxre⟩, rfl⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
⊢ UpperHalfPlane.coe '' 𝒟 = {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
have h : ∀ (x : ℂ), x ∈ UpperHalfPlane.coe '' 𝒟 ↔ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
x : ℂ
⊢ x ∈ UpperHalfPlane.coe '' 𝒟 ↔ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x
have h : x ∈ UpperHalfPlane.coe '' 𝒟 → Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x
Tactic: refine ⟨?_, fun ⟨hxim, hxnorm, hxre⟩ ↦ ⟨⟨x, hxim⟩, ⟨one_le_normSq_iff.mpr hxnorm, hxre⟩, rfl⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
⊢ IsClosed (UpperHalfPlane.coe '' 𝒟)
have rw : IsClosed (X := ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
Tactic: rw [coe_fd]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
⊢ IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
have refine_1 : IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 0 z.im
Tactic: refine .inter ?_ (.inter ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
refine_1 : IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 0 z.im
⊢ IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
have refine_2 : IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 1 ‖z‖
Tactic: refine .inter ?_ (.inter ?_ ?_)