awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
him₁ :
  ‖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, 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
-- Module: Mathlib.NumberTheory.Modular
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 : 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 : 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 : 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 : 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 = ρ
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 = ρ
⊢ (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
-- Module: Mathlib.NumberTheory.Modular
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 = 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:
grind [cases_c_zero hz hg hc]

Premises used: _private.0.ModularGroup.cases_c_zero
-- Module: Mathlib.NumberTheory.Modular
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 = ρ
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 = ρ

Tactic:
rcases Int.abs_le_one_iff.mp (cases_d_of_c_eq_one hz him.le hc) with hd | hd | hd

Premises used: _private.0.ModularGroup.cases_d_of_c_eq_one, Eq.le, Int.abs_le_one_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Modular
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
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:
grind [cases_c_one_d_zero hz hg him.le hc hd]

Premises used: _private.0.ModularGroup.cases_c_one_d_zero, Eq.le
-- Module: Mathlib.NumberTheory.Modular
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
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:
grind [case_c_one_d_one hz hg him.le hc hd]

Premises used: Eq.le, _private.0.ModularGroup.case_c_one_d_one
-- Module: Mathlib.NumberTheory.Modular
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
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:
grind [case_c_one_d_neg_one hz hg him.le hc hd]

Premises used: Eq.le, _private.0.ModularGroup.case_c_one_d_neg_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
apply_fun : (T • z).re ≠ z.re
⊢ T • z ≠ z

Tactic:
apply_fun UpperHalfPlane.re

Premises used: UpperHalfPlane.re
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (T • z).re ≠ z.re

Tactic:
simp [-sl_moeb, re_T_smul]

Premises used: ModularGroup.sl_moeb, ModularGroup.re_T_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ T • z ≠ z

Tactic:
have : T • z ≠ z := by
    apply_fun UpperHalfPlane.re
    simp [-sl_moeb, re_T_smul]
-- Module: Mathlib.NumberTheory.Modular
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
rwa₂ rwa₃ rwa₄ rwa₅ : ¬T • z = z
⊢ T⁻¹ • z ≠ z

Tactic:
rwa [ne_eq, inv_smul_eq_iff, eq_comm]

Premises used: inv_smul_eq_iff, eq_comm, ne_eq
-- Module: Mathlib.NumberTheory.Modular
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

Tactic:
have : T⁻¹ • z ≠ z := by rwa [ne_eq, inv_smul_eq_iff, eq_comm]
-- Module: Mathlib.NumberTheory.Modular
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
⊢ (↑z : ℂ) ≠ -(↑I : ℂ)

Tactic:
grind [neg_im, coe_I, Complex.I_im, z.coe_im_pos]

Premises used: Complex.I_im, UpperHalfPlane.coe_I, UpperHalfPlane.coe_im_pos, Complex.neg_im
-- Module: Mathlib.NumberTheory.Modular
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
⊢ (↑z : ℂ) ≠ -(↑I : ℂ)

Tactic:
have : (z : ℂ) ≠ -I := by grind [neg_im, coe_I, Complex.I_im, z.coe_im_pos]
-- Module: Mathlib.NumberTheory.Modular
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 : ℂ)
contrapose : ∀ (hzI : S • z = z), z = I
⊢ S • z ≠ z

Tactic:
contrapose hzI
-- Module: Mathlib.NumberTheory.Modular
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
⊢ 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

Premises used: Iff.mpr, UpperHalfPlane.ext_iff, inv_mul_eq_iff_eq_mul₀, neg_eq_iff_eq_neg, UpperHalfPlane.modular_S_smul, UpperHalfPlane.ne_zero, sq, Inv.inv, UpperHalfPlane.coe_I, UpperHalfPlane.coe_mk, Complex.I_sq, sq_eq_sq_iff_eq_or_eq_neg, neg_ne_zero, neg_mul, mul_one
-- Module: Mathlib.NumberTheory.Modular
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 : I = z ∨ (↑I : ℂ) = -(↑z : ℂ)
⊢ z = I

Tactic:
grind
-- Module: Mathlib.NumberTheory.Modular
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

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
-- Module: Mathlib.NumberTheory.Modular
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_3 : (↑z : ℂ) ≠ -(↑I : ℂ)
this : S • z ≠ z
⊢ g = 1 ∨ g = -1

Tactic:
grind [cases_of_mem_fd_smul_mem_fd hz (hg ▸ hz), SL_neg_smul]

Premises used: ModularGroup.cases_of_mem_fd_smul_mem_fd, ModularGroup.SL_neg_smul
-- Module: Mathlib.NumberTheory.Modular
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_3 : (↑z : ℂ) ≠ -(↑I : ℂ)
this : S • z ≠ z
⊢ g = 1 ∨ g = -1

Tactic:
all_goals grind [cases_of_mem_fd_smul_mem_fd hz (hg ▸ hz), SL_neg_smul]

Premises used: ModularGroup.cases_of_mem_fd_smul_mem_fd, ModularGroup.SL_neg_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
mp : g • I = I → Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g
mpr : Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g → g • I = I
⊢ g • I = I ↔ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • I = I
⊢ (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)
-- Module: Mathlib.NumberTheory.Modular
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 = ρ
⊢ (g = 1 ∨ g = -1) ∨ g = S ∨ g = -S

Tactic:
norm_num [UpperHalfPlane.ext_iff, Complex.ext_iff, ρ] at this

Premises used: UpperHalfPlane.ρ, UpperHalfPlane.ext_iff, Complex.ext_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • I = I
this : (g = 1 ∨ g = -1) ∨ g = S ∨ g = -S
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g

Tactic:
grind
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
this : S • I = I
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g → g • I = I

Tactic:
simp +contextual [-sl_moeb, or_imp, this]

Premises used: ModularGroup.sl_moeb, or_imp
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
mpr : S • I = I
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S, -S} g → g • I = I

Tactic:
suffices S • I = I by simp +contextual [-sl_moeb, or_imp, this]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
mpr : (↑{ coe := (-(↑I : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } : ℂ) = (↑I : ℂ)
⊢ S • I = I

Tactic:
rw [modular_S_smul, UpperHalfPlane.ext_iff]

Premises used: UpperHalfPlane.ext_iff, UpperHalfPlane.modular_S_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
⊢ (↑{ coe := (-(↑I : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } : ℂ) = (↑I : ℂ)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
mp : g • ρ = ρ → Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g
mpr : Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g → g • ρ = ρ
⊢ g • ρ = ρ ↔ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
rw : ¬((-(↑ρ : ℂ))⁻¹.re = (↑ρ : ℂ).re ∧ (-(↑ρ : ℂ))⁻¹.im = (↑ρ : ℂ).im)
⊢ S • ρ ≠ ρ

Tactic:
rw [ne_eq, UpperHalfPlane.ext_iff, modular_S_smul, coe_mk, Complex.ext_iff]

Premises used: UpperHalfPlane.ext_iff, UpperHalfPlane.modular_S_smul, Complex.ext_iff, ne_eq, UpperHalfPlane.coe_mk
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
⊢ ¬((-(↑ρ : ℂ))⁻¹.re = (↑ρ : ℂ).re ∧ (-(↑ρ : ℂ))⁻¹.im = (↑ρ : ℂ).im)

Tactic:
norm_num [ρ, ← pow_two, div_pow]

Premises used: pow_two, UpperHalfPlane.ρ, div_pow
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
⊢ 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]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
this : S • ρ ≠ ρ
⊢ g ≠ S ∧ g ≠ -S

Tactic:
grind [SL_neg_smul]

Premises used: ModularGroup.SL_neg_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
⊢ 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]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
rw : ¬(↑1 : ℂ) + (↑ρ : ℂ) = (↑ρ : ℂ)
⊢ T • ρ ≠ ρ

Tactic:
rw [ne_eq, UpperHalfPlane.ext_iff, modular_T_smul, coe_vadd]

Premises used: UpperHalfPlane.ext_iff, ne_eq, UpperHalfPlane.coe_vadd, UpperHalfPlane.modular_T_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ ¬(↑1 : ℂ) + (↑ρ : ℂ) = (↑ρ : ℂ)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ T • ρ ≠ ρ

Tactic:
have : T • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_T_smul, coe_vadd]
        norm_num
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
this : T • ρ ≠ ρ
rwa : ¬T⁻¹ • ρ = ρ
rwa₁ : ¬ρ = T • ρ
rwa₂ rwa₃ rwa₄ rwa₅ : ¬T • ρ = ρ
⊢ T⁻¹ • ρ ≠ ρ

Tactic:
rwa [ne_eq, inv_smul_eq_iff, eq_comm]

Premises used: inv_smul_eq_iff, eq_comm, ne_eq
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
this : T • ρ ≠ ρ
⊢ T⁻¹ • ρ ≠ ρ

Tactic:
have : T⁻¹ • ρ ≠ ρ := by rwa [ne_eq, inv_smul_eq_iff, eq_comm]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
this_1 : T • ρ ≠ ρ
this : T⁻¹ • ρ ≠ ρ
⊢ g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹

Tactic:
grind [SL_neg_smul]

Premises used: ModularGroup.SL_neg_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ 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]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
simp :
  ¬((↑(HVAdd.hVAdd (α := ℝ) 1 { coe := (-(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }) : ℂ).re =
        (↑ρ : ℂ).re ∧
      (↑(HVAdd.hVAdd (α := ℝ) 1 { coe := (-(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }) : ℂ).im =
        (↑ρ : ℂ).im)
⊢ (T * S * T) • ρ ≠ ρ

Tactic:
simp only [mul_smul, modular_T_smul, modular_S_smul,
          ne_eq, UpperHalfPlane.ext_iff, Complex.ext_iff]

Premises used: UpperHalfPlane.ext_iff, UpperHalfPlane.modular_S_smul, Complex.ext_iff, ne_eq, SemigroupAction.mul_smul, UpperHalfPlane.modular_T_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
⊢ ¬((↑(HVAdd.hVAdd (α := ℝ) 1 { coe := (-(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }) : ℂ).re =
        (↑ρ : ℂ).re ∧
      (↑(HVAdd.hVAdd (α := ℝ) 1 { coe := (-(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }) : ℂ).im =
        (↑ρ : ℂ).im)

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

Premises used: pow_two, UpperHalfPlane.ρ, Complex.normSq, div_pow
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
⊢ (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]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
this : (T * S * T) • ρ ≠ ρ
⊢ g ≠ T * S * T ∧ g ≠ -(T * S * T)

Tactic:
grind [SL_neg_smul]

Premises used: ModularGroup.SL_neg_smul