awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
this_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| ≤ 1 / 2 + |z.re|
hzre : |z.re| = 1 / 2
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have this₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
Tactic: rw [hzre, add_halves, ← Int.cast_abs, ← Int.cast_one (R := ℝ), Int.cast_le,
      Int.abs_le_one_iff] at this
Cleared hypotheses: this, hzre
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
this_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hzre : |z.re| = 1 / 2
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have inr : ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0),
  g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rcases this with h | h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
this_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hzre : |z.re| = 1 / 2
inr :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0),
    g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have inr₁ : ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1),
  g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rcases this with h | h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
this_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hzre : |z.re| = 1 / 2
inr :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0),
    g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
inr₁ :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1),
    g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have inr₂ : ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1),
  g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rcases this with h | h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have this₁ : |(-z.re)| ≤ 1 / 2
Tactic: simp only [h, Int.cast_zero, zero_add, Int.cast_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have this₁ : |1 + -z.re| ≤ 1 / 2
Tactic: simp only [h, Int.cast_zero, zero_add, Int.cast_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have this₁ : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
Tactic: simp only [h, Int.cast_zero, zero_add, Int.cast_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have inr : ∀ (hzre : z.re = 1 / 2), g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rcases (abs_eq one_half_pos.le).mp hzre with hzre | hzre
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
inr : ∀ (hzre : z.re = 1 / 2), g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have inr₁ : ∀ (hzre : z.re = -(1 / 2)), g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rcases (abs_eq one_half_pos.le).mp hzre with hzre | hzre
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hzre₁ : z.re = 1 / 2
Tactic: rcases (abs_eq one_half_pos.le).mp hzre with hzre | hzre <;> [skip; norm_num [hzre] at this]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hg'₁ : g = T * S
Tactic: rw [h, zpow_one] at hg'
Cleared hypotheses: hg', hSre, hzre_1, h, this, hzre
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T * S
hSre : (S • z).re = -z.re
hzre_1 : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have inr : ‖(↑z : ℂ)‖ = ‖(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖
Tactic: refine .inr <| .inr ⟨hg', eq_of_re_of_norm (by norm_num [hzre, ρ]) ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : |z.re| = 1 / 2
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hzre₁ : z.re = 1 / 2 ∨ z.re = -(1 / 2)
Tactic: rw [abs_eq (by norm_num)] at hzre
Cleared hypotheses: hzre, h, this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : z.re = 1 / 2 ∨ z.re = -(1 / 2)
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have inr : ∀ (hzre : z.re = 1 / 2), g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rcases hzre with hzre | hzre
Cleared hypotheses: hzre
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : z.re = 1 / 2 ∨ z.re = -(1 / 2)
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
inr : ∀ (hzre : z.re = 1 / 2), g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have inr₁ : ∀ (hzre : z.re = -(1 / 2)), g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rcases hzre with hzre | hzre
Cleared hypotheses: hzre
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
hSre : (S • z).re = -z.re
hzre : z.re = 1 / 2 ∨ z.re = -(1 / 2)
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hzre₁ : z.re = -(1 / 2)
Tactic: rcases hzre with hzre | hzre <;> [norm_num [hzre] at this; skip]
Cleared hypotheses: hzre
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T⁻¹ * S
hSre : (S • z).re = -z.re
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
hzre : z.re = -(1 / 2)
⊢ ‖(↑z : ℂ)‖ = ‖(↑ρ : ℂ)‖
have rw : 1 = ‖(↑ρ : ℂ)‖
Tactic: rw [hz', norm_ρ]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
hg'_1 :
  ‖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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
hg' : g = T⁻¹ * S
hSre : (S • z).re = -z.re
h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
this : |(↑(-1) : ℝ) + -z.re| ≤ 1 / 2
hzre : z.re = -(1 / 2)
rw : 1 = ‖(↑ρ : ℂ)‖
⊢ ‖(↑z : ℂ)‖ = ‖(↑ρ : ℂ)‖
have rw₁ : Eq (α := ℝ) 1 1
Tactic: rw [hz', norm_ρ]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
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
⊢ g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
have refine : (↑g : Matrix (Fin 2) (Fin 2) ℤ) = (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T) : Matrix (Fin 2) (Fin 2) ℤ)
Tactic: refine Subtype.ext ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
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
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) = (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T) : Matrix (Fin 2) (Fin 2) ℤ)
have rw : (↑g : Matrix (Fin 2) (Fin 2) ℤ) =
  !![(HMul.hMul (α := ℤ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 1) * 1 +
        (HMul.hMul (α := ℤ) 1 (-1) + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 0) * 0,
      (HMul.hMul (α := ℤ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 1) * 1 +
        (HMul.hMul (α := ℤ) 1 (-1) + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 0) * 1;
    (HMul.hMul (α := ℤ) 0 0 + HMul.hMul (α := ℤ) 1 1) * 1 + (HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 0) * 0,
      (HMul.hMul (α := ℤ) 0 0 + HMul.hMul (α := ℤ) 1 1) * 1 + (HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 0) * 1]
Tactic: rw [coe_mul, coe_mul, coe_T_zpow, coe_S, coe_T, mul_fin_two, mul_fin_two]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
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
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) =
    !![(HMul.hMul (α := ℤ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 1) * 1 +
          (HMul.hMul (α := ℤ) 1 (-1) + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 0) * 0,
        (HMul.hMul (α := ℤ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 1) * 1 +
          (HMul.hMul (α := ℤ) 1 (-1) + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 0) * 1;
      (HMul.hMul (α := ℤ) 0 0 + HMul.hMul (α := ℤ) 1 1) * 1 + (HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 0) * 0,
        (HMul.hMul (α := ℤ) 0 0 + HMul.hMul (α := ℤ) 1 1) * 1 +
          (HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 0) * 1]
have ring_nf : (↑g : Matrix (Fin 2) (Fin 2) ℤ) =
  !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, 1]
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
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
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, 1]
have a : ∀ (i j : Fin 2),
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, 1] i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
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
i j : Fin 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, 1] i j
have a : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) j =
  !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, 1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
    j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
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
i j : Fin 2
a :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, 1]
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, 1] i j
have a₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j =
  !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, 1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
    j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
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
j : Fin 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, 1]
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have a : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, 1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j