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
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 : (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hnorm₁ : √((normSq : (a : ℂ) → ℝ) (↑z : ℂ)) = ‖(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖
hnorm₂ : √1 = ‖(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖
hnorm₃ : √1 = ‖(↑1 : ℂ) + (↑ρ : ℂ)‖
hnorm₄ : √1 = ‖1 + (↑ρ : ℂ)‖
hnorm₅ : √1 = ‖-HPow.hPow (β := ℕ) (↑ρ : ℂ) 2‖
hnorm₆ : √1 = ‖HPow.hPow (β := ℕ) (↑ρ : ℂ) 2‖
hnorm₇ : √1 = HPow.hPow (β := ℕ) ‖(↑ρ : ℂ)‖ 2
⊢ ‖(↑z : ℂ)‖ = ‖(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖
have hnorm₈ : √1 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
Tactic: rw [norm_def, h, coe_vadd, ofReal_one,
        show 1 + (ρ : ℂ) = -ρ ^ 2 by grind [ρ_sq], norm_neg, norm_pow, norm_ρ, Real.sqrt_one,
        one_pow]
-- 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_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 : (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hnorm₁ : √((normSq : (a : ℂ) → ℝ) (↑z : ℂ)) = ‖(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖
hnorm₂ : √1 = ‖(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖
hnorm₃ : √1 = ‖(↑1 : ℂ) + (↑ρ : ℂ)‖
hnorm₄ : √1 = ‖1 + (↑ρ : ℂ)‖
hnorm₅ : √1 = ‖-HPow.hPow (β := ℕ) (↑ρ : ℂ) 2‖
hnorm₆ : √1 = ‖HPow.hPow (β := ℕ) (↑ρ : ℂ) 2‖
hnorm₇ : √1 = HPow.hPow (β := ℕ) ‖(↑ρ : ℂ)‖ 2
hnorm₈ : √1 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
⊢ ‖(↑z : ℂ)‖ = ‖(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖
have hnorm₉ : 1 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
Tactic: rw [norm_def, h, coe_vadd, ofReal_one,
        show 1 + (ρ : ℂ) = -ρ ^ 2 by grind [ρ_sq], norm_neg, norm_pow, norm_ρ, Real.sqrt_one,
        one_pow]
-- 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_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 : (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hnorm₁ : √((normSq : (a : ℂ) → ℝ) (↑z : ℂ)) = ‖(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖
hnorm₂ : √1 = ‖(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖
hnorm₃ : √1 = ‖(↑1 : ℂ) + (↑ρ : ℂ)‖
hnorm₄ : √1 = ‖1 + (↑ρ : ℂ)‖
hnorm₅ : √1 = ‖-HPow.hPow (β := ℕ) (↑ρ : ℂ) 2‖
hnorm₆ : √1 = ‖HPow.hPow (β := ℕ) (↑ρ : ℂ) 2‖
hnorm₇ : √1 = HPow.hPow (β := ℕ) ‖(↑ρ : ℂ)‖ 2
hnorm₈ : √1 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
hnorm₉ : 1 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
⊢ ‖(↑z : ℂ)‖ = ‖(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ)‖
have hnorm₁₀ : Eq (α := ℝ) 1 1
Tactic: rw [norm_def, h, coe_vadd, ofReal_one,
        show 1 + (ρ : ℂ) = -ρ ^ 2 by grind [ρ_sq], norm_neg, norm_pow, norm_ρ, Real.sqrt_one,
        one_pow]
-- 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_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 : (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: have hρ : z = (1 : ℝ) +ᵥ ρ := by
    apply eq_of_re_of_norm
    · norm_num [h', ρ]
    · rw [norm_def, h, coe_vadd, ofReal_one,
        show 1 + (ρ : ℂ) = -ρ ^ 2 by grind [ρ_sq], norm_neg, norm_pow, norm_ρ, Real.sqrt_one,
        one_pow]
-- 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_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 : (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 ρ
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have refine : g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹
Tactic: refine ⟨?_, hρ⟩
-- 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_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 : (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 ρ
⊢ g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹
have hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
Tactic: rw [hgeq, hρ, mul_assoc, mul_smul] at hg
Cleared hypotheses: hg, hg', hc, hd, this_1, hgeq, hnorm, this, h, h', hρ
-- 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 * 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 : (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 • ρ
have rw : 1 = -(↑ρ : ℂ) * ((↑1 : ℂ) + (↑ρ : ℂ))
Tactic: rw [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 : 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 : (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 ρ
⊢ g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹
have this₁ : S • ρ = T • ρ
Tactic: have : S • ρ = T • ρ := by
    rw [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 (goal)
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 : S • ρ = T • ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- 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 * 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 : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- 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 * 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 : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₂ : S⁻¹ • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- 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 * 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 : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₂ : S⁻¹ • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₃ : T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- 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 * 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 : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₂ : S⁻¹ • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₃ : T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₄ : HPow.hPow (β := ℤ) T (-1) • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- 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 * 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 : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₂ : S⁻¹ • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₃ : T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₄ : HPow.hPow (β := ℤ) T (-1) • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₅ : HVAdd.hVAdd (α := ℝ) (↑(-1) : ℝ) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- 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 * 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 : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₂ : S⁻¹ • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₃ : T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₄ : HPow.hPow (β := ℤ) T (-1) • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₅ : HVAdd.hVAdd (α := ℝ) (↑(-1) : ℝ) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₆ : HVAdd.hVAdd (α := ℝ) (-(↑1 : ℝ)) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- 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 * 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 : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₂ : S⁻¹ • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₃ : T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₄ : HPow.hPow (β := ℤ) T (-1) • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₅ : HVAdd.hVAdd (α := ℝ) (↑(-1) : ℝ) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₆ : HVAdd.hVAdd (α := ℝ) (-(↑1 : ℝ)) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₇ : HVAdd.hVAdd (α := ℝ) (-1) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]