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 ∈ 𝒟
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
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)
linarith : z.re < -1 / 2 → 2 / 2 = 1
linarith₁ : z.re < -1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : z.re < -1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : z.re < -1 / 2 → 2 * z.re - -HMul.hMul (α := ℝ) 1 1 + (0 - (2 * z.re + 1)) = 0
linarith₄ : -1 / 2 < z.re → 2 / 2 = 1
linarith₅ : -1 / 2 < z.re → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : -1 / 2 < z.re → GT.gt (α := ℝ) 2 0
⊢ z.re = -1 / 2
have linarith₇ : -1 / 2 < z.re →
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (2 * z.re + 1) - 1 + (-HMul.hMul (α := ℝ) 1 1 - 2 * z.re) +
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) =
    0
Tactic: linarith [hz.1, show 0 ≤ 2 * z.re + 1 by linarith [(neg_le_abs _).trans hz.2]]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 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) ∧
    z = ρ
have hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
Tactic: obtain ⟨hnorm, hre⟩ : normSq z = 1 ∧ z.re = -1 / 2 := by
    have hnorm : normSq ((z : ℂ) + 1) ≤ 1 := by simpa [denom, hc, hd, norm_def] using hg'
    have : normSq (z + 1) = normSq z + (2 * z.re + 1) := by simp [normSq]; ring
    rw [this] at hnorm
    constructor <;> linarith [hz.1, show 0 ≤ 2 * z.re + 1 by linarith [(neg_le_abs _).trans hz.2]]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (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) ∧
    z = ρ
have hre : z.re = -1 / 2
Tactic: obtain ⟨hnorm, hre⟩ : normSq z = 1 ∧ z.re = -1 / 2 := by
    have hnorm : normSq ((z : ℂ) + 1) ≤ 1 := by simpa [denom, hc, hd, norm_def] using hg'
    have : normSq (z + 1) = normSq z + (2 * z.re + 1) := by simp [normSq]; ring
    rw [this] at hnorm
    constructor <;> linarith [hz.1, show 0 ≤ 2 * z.re + 1 by linarith [(neg_le_abs _).trans hz.2]]
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
⊢ z = ρ
have hre₁ : z.re = ρ.re
Tactic: apply eq_of_re_of_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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hre₁ : z.re = ρ.re
⊢ z = ρ
have hnorm₁ : ‖(↑z : ℂ)‖ = ‖(↑ρ : ℂ)‖
Tactic: apply eq_of_re_of_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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
⊢ ‖(↑z : ℂ)‖ = ‖(↑ρ : ℂ)‖
have hnorm₁ : √((normSq : (a : ℂ) → ℝ) (↑z : ℂ)) = ‖(↑ρ : ℂ)‖
Tactic: rw [norm_def, hnorm, norm_ρ, Real.sqrt_one]
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hnorm₁ : √((normSq : (a : ℂ) → ℝ) (↑z : ℂ)) = ‖(↑ρ : ℂ)‖
⊢ ‖(↑z : ℂ)‖ = ‖(↑ρ : ℂ)‖
have hnorm₂ : √1 = ‖(↑ρ : ℂ)‖
Tactic: rw [norm_def, hnorm, norm_ρ, Real.sqrt_one]
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hnorm₁ : √((normSq : (a : ℂ) → ℝ) (↑z : ℂ)) = ‖(↑ρ : ℂ)‖
hnorm₂ : √1 = ‖(↑ρ : ℂ)‖
⊢ ‖(↑z : ℂ)‖ = ‖(↑ρ : ℂ)‖
have hnorm₃ : √1 = 1
Tactic: rw [norm_def, hnorm, norm_ρ, Real.sqrt_one]
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hnorm₁ : √((normSq : (a : ℂ) → ℝ) (↑z : ℂ)) = ‖(↑ρ : ℂ)‖
hnorm₂ : √1 = ‖(↑ρ : ℂ)‖
hnorm₃ : √1 = 1
⊢ ‖(↑z : ℂ)‖ = ‖(↑ρ : ℂ)‖
have hnorm₄ : Eq (α := ℝ) 1 1
Tactic: rw [norm_def, hnorm, norm_ρ, Real.sqrt_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
⊢ (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) ∧
    z = ρ
have hρ : z = ρ
Tactic: have hρ : z = ρ := by
    apply eq_of_re_of_norm
    · simp [hre, ρ]
    · rw [norm_def, hnorm, norm_ρ, Real.sqrt_one]
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
⊢ (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) ∧
    z = ρ
have refine : 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: refine ⟨?_, hρ⟩
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
⊢ (S * T) • ρ = ρ
have rw : 1 = -(↑ρ : ℂ) * ((↑1 : ℂ) + (↑ρ : ℂ))
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, eq_comm, UpperHalfPlane.ext_iff,
      modular_S_smul, modular_T_smul, UpperHalfPlane.coe_mk, coe_vadd,
      ← mul_one (_ : ℂ)⁻¹, inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr ρ.ne_zero)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
⊢ 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
have hSTρ : (S * T) • ρ = ρ
Tactic: have hSTρ : (S * T) • ρ = ρ := by
    rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, eq_comm, UpperHalfPlane.ext_iff,
      modular_S_smul, modular_T_smul, UpperHalfPlane.coe_mk, coe_vadd,
      ← mul_one (_ : ℂ)⁻¹, inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr ρ.ne_zero)]
    grind [ρ_sq, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (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
have hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ ∈ 𝒟
Tactic: rw [hgeq, hρ, mul_assoc, mul_smul, hSTρ] at hg
Cleared hypotheses: hg, hg', hc, hd, hgeq, hnorm, hre, hρ, hSTρ
-- 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 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
this : (↑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
have 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
Tactic: rcases this with 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 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
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
⊢ 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
have 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
Tactic: rcases this with 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 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (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
have suffices : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
Tactic: suffices g 0 0 = 0 ∨ g 0 0 = 1 by rcases this with h | h <;> simp [h]
-- 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 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
have hgzre : |(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ).re| ≤ 1 / 2
Tactic: have hgzre := hg.2
-- 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 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hgzre : |(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • ρ).re| ≤ 1 / 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
have hgzre₁ : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧ LE.le (α := ℝ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) 1
Tactic: simp only [Fin.isValue, ρ, neg_div, one_div, ← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re,
    abs_le, le_add_iff_nonneg_right, Int.cast_nonneg_iff, neg_add_le_iff_le_add,
    show (2⁻¹ : ℝ) + 2⁻¹ = 1 by norm_num] at hgzre
Cleared hypotheses: hgzre
-- 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 • ρ ∈ 𝒟
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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hgzre : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧ LE.le (α := ℝ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
have hgzre₁ : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 1
Tactic: rw [← Int.cast_one (R := ℝ), Int.cast_le] at hgzre
Cleared hypotheses: hgzre
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
have this : (↑g : Matrix (Fin 2) (Fin 2) ℤ).det = 1
Tactic: have := g.property
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ).det = 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
have this₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 -
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 =
  1
Tactic: simp_rw [det_fin_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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 = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
Tactic: have : g 0 1 = -g 0 0 - 1 := by
    have := g.property
    simp_rw [det_fin_two] at this
    grind
-- 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
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 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
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 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, ← zpow_neg_one, coe_T_zpow, 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
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 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
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 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