Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 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 = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ

pp: case inr.inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 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 = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ

pp: case inr.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 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 = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 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]

Goal state after:
case inr.inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 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 = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ

case inr.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 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 = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ