awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 = z.im
have inr : (g⁻¹ • g • z).im = z.im
Tactic: rw [← this (g := g⁻¹) hg (by simpa using hz) (by simpa using le_of_not_ge hden)]
-- 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 ∈ 𝒟
hden : z.im ≤ (g • z).im
⊢ (g • z).im = z.im
have inr : ∀
  (this :
    ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im)
      (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0), (g • z).im = z.im)
  (hc : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0), (g • z).im = z.im
Tactic: wlog hc : 0 ≤ g 1 0
-- 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 ∈ 𝒟
hden : z.im ≤ (g • z).im
inr :
  ∀
    (this :
      ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im)
        (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0), (g • z).im = z.im)
    (hc : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0), (g • z).im = z.im
⊢ (g • z).im = z.im
have wlog : ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im)
  (hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0), (g • z).im = z.im
Tactic: wlog hc : 0 ≤ g 1 0
Cleared hypotheses: g, z, hz, hg, hden
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g_2 : SL(2, ℤ)
z_2 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
hc : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ (g • z).im = z.im
have hden₁ : ‖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, le_div_iff₀ (normSq_denom_pos _ z.im_ne_zero),
    mul_le_iff_le_one_right z.im_pos, normSq_eq_norm_sq, sq_le_one_iff₀ (norm_nonneg _)] at hden
Cleared hypotheses: hden, hc
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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 : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ (g • z).im = z.im
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_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 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
⊢ (g • z).im = z.im
have inl : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0), (g • z).im = z.im
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_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 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
inl : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0), (g • z).im = z.im
⊢ (g • z).im = z.im
have inr : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1), (g • z).im = z.im
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_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 = 0
⊢ (g • z).im = z.im
have inl : ∀ (h : (g = T ∨ g = -T) ∧ z.re = -1 / 2), (g • z).im = z.im
Tactic: rcases cases_c_zero hz hg hc with h | h | h | h
-- 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 = 0
inl : ∀ (h : (g = T ∨ g = -T) ∧ z.re = -1 / 2), (g • z).im = z.im
⊢ (g • z).im = z.im
have inl₁ : ∀ (h : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2), (g • z).im = z.im
Tactic: rcases cases_c_zero hz hg hc with h | h | h | h
-- 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 = 0
inl : ∀ (h : (g = T ∨ g = -T) ∧ z.re = -1 / 2), (g • z).im = z.im
inl₁ : ∀ (h : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2), (g • z).im = z.im
⊢ (g • z).im = z.im
have inl₂ : ∀ (h : g = 1), (g • z).im = z.im
Tactic: rcases cases_c_zero hz hg hc with h | h | h | h
-- 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 = 0
inl : ∀ (h : (g = T ∨ g = -T) ∧ z.re = -1 / 2), (g • z).im = z.im
inl₁ : ∀ (h : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2), (g • z).im = z.im
inl₂ : ∀ (h : g = 1), (g • z).im = z.im
⊢ (g • z).im = z.im
have inl₃ : ∀ (h : g = -1), (g • z).im = z.im
Tactic: rcases cases_c_zero hz hg hc with h | h | h | h
-- 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 = 0
h : (g = T ∨ g = -T) ∧ z.re = -1 / 2
⊢ (g • z).im = z.im
have inl : ∀ (hg : T • z ∈ 𝒟)
  (hden :
    ‖denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T))
          (↑z : ℂ)‖ ≤
      1)
  (hc : 0 ≤ (↑T : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑T : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0), (T • z).im = z.im
Tactic: rcases h with ⟨(rfl | rfl), -⟩
Cleared hypotheses: g, hg, hden, hc_1, hc, h
-- 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 = 0
h : (g = T ∨ g = -T) ∧ z.re = -1 / 2
inl :
  ∀ (hg : T • z ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T))
            (↑z : ℂ)‖ ≤
        1)
    (hc : 0 ≤ (↑T : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑T : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0), (T • z).im = z.im
⊢ (g • z).im = z.im
have inl₁ : ∀ (hg : -T • z ∈ 𝒟)
  (hden :
    ‖denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-T)))
          (↑z : ℂ)‖ ≤
      1)
  (hc : 0 ≤ (↑(-T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑(-T) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0),
  (-T • z).im = z.im
Tactic: rcases h with ⟨(rfl | rfl), -⟩
Cleared hypotheses: g, hg, hden, hc_1, hc, h
-- 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 = 0
h : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2
⊢ (g • z).im = z.im
have inl : ∀ (hg : T⁻¹ • z ∈ 𝒟)
  (hden :
    ‖denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T⁻¹))
          (↑z : ℂ)‖ ≤
      1)
  (hc : 0 ≤ (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0), (T⁻¹ • z).im = z.im
Tactic: rcases h with ⟨(rfl | rfl), -⟩
Cleared hypotheses: g, hg, hden, hc_1, hc, h
-- 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 = 0
h : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2
inl :
  ∀ (hg : T⁻¹ • z ∈ 𝒟)
    (hden :
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T⁻¹))
            (↑z : ℂ)‖ ≤
        1)
    (hc : 0 ≤ (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0),
    (T⁻¹ • z).im = z.im
⊢ (g • z).im = z.im
have inl₁ : ∀ (hg : -T⁻¹ • z ∈ 𝒟)
  (hden :
    ‖denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-T⁻¹)))
          (↑z : ℂ)‖ ≤
      1)
  (hc : 0 ≤ (↑(-T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) (hc : (↑(-T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0),
  (-T⁻¹ • z).im = z.im
Tactic: rcases h with ⟨(rfl | rfl), -⟩
Cleared hypotheses: g, hg, hden, hc_1, hc, h
-- 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 = 0
h : g = 1
⊢ (g • z).im = z.im
have inl : ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) 1 z ∈ 𝒟)
  (hden :
    ‖denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) 1))
          (↑z : ℂ)‖ ≤
      1)
  (hc : LE.le (α := ℤ) 0 ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0))
  (hc : Eq (α := ℤ) ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0), (HSMul.hSMul (α := SL(2, ℤ)) 1 z).im = z.im
Tactic: rcases h with ⟨(rfl | rfl), -⟩
Cleared hypotheses: g, hg, hden, hc_1, hc, h
-- 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 = 0
h : g = -1
⊢ (g • z).im = z.im
have inl : ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) (-1) z ∈ 𝒟)
  (hden :
    ‖denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-1)))
          (↑z : ℂ)‖ ≤
      1)
  (hc : LE.le (α := ℤ) 0 ((↑(-1) : Matrix (Fin 2) (Fin 2) ℤ) 1 0))
  (hc : Eq (α := ℤ) ((↑(-1) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0), (HSMul.hSMul (α := SL(2, ℤ)) (-1) z).im = z.im
Tactic: rcases h with ⟨(rfl | rfl), -⟩
Cleared hypotheses: g, hg, hden, hc_1, hc, h
-- 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
⊢ (g • z).im = z.im
have inr : Eq (α := ℝ)
  ((normSq : (a : ℂ) → ℝ)
      (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]
-- 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
⊢ 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 : ∀ (hd : (↑g : 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, ℝ)) g))
          (↑z : ℂ)) :
      ℝ)
    (1 : ℝ)
Tactic: rcases Int.abs_le_one_iff.mp (cases_d_of_c_eq_one hz hden hc) with hd | hd | 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
inr :
  ∀ (hd : (↑g : 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, ℝ)) g))
            (↑z : ℂ)) :
        ℝ)
      (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₁ : ∀ (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 : ℝ)
Tactic: rcases Int.abs_le_one_iff.mp (cases_d_of_c_eq_one hz hden hc) with hd | hd | 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
inr :
  ∀ (hd : (↑g : 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, ℝ)) g))
            (↑z : ℂ)) :
        ℝ)
      (1 : ℝ)
inr₁ :
  ∀ (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 : ℝ)
⊢ 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₂ : ∀ (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 : ℝ)
Tactic: rcases Int.abs_le_one_iff.mp (cases_d_of_c_eq_one hz hden hc) with hd | hd | 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 = 0
⊢ 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 : ∀ (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 : ℝ)
Tactic: rcases cases_c_one_d_zero hz hg hden hc hd with
        ⟨rfl, hnm⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
Cleared hypotheses: g, 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 = 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 : ℝ)
⊢ 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 : ρ ∈ 𝒟) (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 : ℝ)
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