awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg'₁ :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq₁ : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm₁ : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this₂ : (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)

Tactic:
rw [this] at hg
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg'₁ :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq₁ : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm₁ : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this₂ : (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
⊢ z.re = 1 / 2

Tactic:
rw [this] at hg
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg'₁ :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq₁ : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm₁ : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this₂ : (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h'₁ : z.re = 1 / 2
⊢ z = HVAdd.hVAdd (α := ℝ) 1 ρ

Tactic:
rw [this] at hg
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg'₁ :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq₁ : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm₁ : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this₂ : (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h'₁ : z.re = 1 / 2
hρ₁ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ S • ρ = T • ρ

Tactic:
rw [this] at hg
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg'₁ :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq₁ : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm₁ : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this₂ : (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h'₁ : z.re = 1 / 2
hρ₁ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this₃ : S • ρ = T • ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ

Tactic:
rw [this] at hg
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw :
  T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹
⊢ g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹

Tactic:
rw [hgeq]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this_4 : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
inl :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0),
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
      T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹
inr :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1),
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
      T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹

Tactic:
rcases this with h | h
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h_1 : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h_1 : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
suffices : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹

Tactic:
suffices g 0 0 = 0 ∨ g 0 0 = -1 by rcases this with h | h <;> simp [h]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ HAdd.hAdd (α := ℝ) 1 (-2⁻¹) = 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ HSub.hSub (α := ℝ) (-2⁻¹) 2⁻¹ = -1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ LE.le (α := ℝ) (-1) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) ∧ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 0

Tactic:
simpa only [ρ, neg_div, one_div, ← coe_re, coe_T_zpow_smul_eq, coe_vadd, add_re, ofReal_re,
      show 1 + (-2⁻¹ : ℝ) = 2⁻¹ by norm_num, intCast_re, abs_le, ← sub_le_iff_le_add',
      show (-2⁻¹ : ℝ) - (2⁻¹ : ℝ) = -1 by norm_num, add_le_iff_nonpos_right, Int.cast_nonpos] using
      hg.2

Premises used: neg_div, UpperHalfPlane.ρ, ModularGroup.coe_T_zpow_smul_eq, add_le_iff_nonpos_right, abs_le, Complex.add_re, Complex.intCast_re, Int.cast_nonpos, sub_le_iff_le_add', And.right, one_div, Complex.ofReal_re, UpperHalfPlane.coe_vadd, UpperHalfPlane.coe_re
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ LE.le (α := ℝ) (-1) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) ∧ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 0

Tactic:
have : (-1 : ℝ) ≤ g 0 0 ∧ g 0 0 ≤ 0 := by
    simpa only [ρ, neg_div, one_div, ← coe_re, coe_T_zpow_smul_eq, coe_vadd, add_re, ofReal_re,
      show 1 + (-2⁻¹ : ℝ) = 2⁻¹ by norm_num, intCast_re, abs_le, ← sub_le_iff_le_add',
      show (-2⁻¹ : ℝ) - (2⁻¹ : ℝ) = -1 by norm_num, add_le_iff_nonpos_right, Int.cast_nonpos] using
      hg.2
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this_4 : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
this : LE.le (α := ℝ) (-1) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) ∧ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 0
⊢ -1 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 0

Tactic:
rw [← Int.cast_one, ← Int.cast_neg, Int.cast_le] at this

Premises used: Int.cast_neg, Int.cast_le, Int.cast_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this_4 : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
this : -1 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1

Tactic:
grind
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
inr :
  ∀ (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 • z).im = z.im
wlog : ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im), (g • z).im = z.im
⊢ (g • z).im = z.im

Tactic:
wlog hden : z.im ≤ (g • z).im

Premises used: UpperHalfPlane.im, HSMul.hSMul
-- 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 ∈ 𝒟

Tactic:
simpa using hz
-- 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 • z).im ≤ (g⁻¹ • g • z).im

Tactic:
simpa using le_of_not_ge hden

Premises used: le_of_not_ge