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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
j : Fin 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have a : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: 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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
j : Fin 2
a :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have a₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1; 1, 0] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- 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 = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1
hz' : ‖(↑z : ℂ)‖ = 1
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hg'₁ : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S
Tactic: have hg' : g = T ^ g 0 0 * S := by
    ext i j
    simp only [coe_mul, coe_S, coe_T_zpow, Matrix.mul_fin_two, mul_zero, mul_one, zero_add,
      one_mul, add_zero, zero_mul]
    fin_cases i <;> fin_cases j <;> tauto
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • 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
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z ∈ 𝒟
Tactic: rw [hg', mul_smul] at hg
Cleared hypotheses: hg, hg'_1, hc, hd, hb, hz', hg'
-- 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
⊢ (S • z).re = -z.re
have rw : { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := sorry : ℍ }.re = -z.re
Tactic: rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
rw : { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }.re = -z.re
⊢ (S • z).re = -z.re
have rw₁ : (↑{ coe := (-(↑z : ℂ))⁻¹, coe_im_pos := sorry : ℍ } : ℂ).re = -z.re
Tactic: rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
rw : { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }.re = -z.re
rw₁ : (↑{ coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } : ℂ).re = -z.re
⊢ (S • z).re = -z.re
have rw₂ : (-(↑z : ℂ))⁻¹.re = -z.re
Tactic: rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
rw : { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }.re = -z.re
rw₁ : (↑{ coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } : ℂ).re = -z.re
rw₂ : (-(↑z : ℂ))⁻¹.re = -z.re
⊢ (S • z).re = -z.re
have rw₃ : HDiv.hDiv (β := ℝ) (-(↑z : ℂ)).re ((normSq : (a : ℂ) → ℝ) (-(↑z : ℂ)) : ℝ) = -z.re
Tactic: rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
rw : { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }.re = -z.re
rw₁ : (↑{ coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } : ℂ).re = -z.re
rw₂ : (-(↑z : ℂ))⁻¹.re = -z.re
rw₃ : HDiv.hDiv (β := ℝ) (-(↑z : ℂ)).re ((normSq : (a : ℂ) → ℝ) (-(↑z : ℂ)) : ℝ) = -z.re
⊢ (S • z).re = -z.re
have rw₄ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖-(↑z : ℂ)‖ 2 = -z.re
Tactic: rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
rw : { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }.re = -z.re
rw₁ : (↑{ coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } : ℂ).re = -z.re
rw₂ : (-(↑z : ℂ))⁻¹.re = -z.re
rw₃ : HDiv.hDiv (β := ℝ) (-(↑z : ℂ)).re ((normSq : (a : ℂ) → ℝ) (-(↑z : ℂ)) : ℝ) = -z.re
rw₄ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖-(↑z : ℂ)‖ 2 = -z.re
⊢ (S • z).re = -z.re
have rw₅ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 = -z.re
Tactic: rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
rw : { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }.re = -z.re
rw₁ : (↑{ coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } : ℂ).re = -z.re
rw₂ : (-(↑z : ℂ))⁻¹.re = -z.re
rw₃ : HDiv.hDiv (β := ℝ) (-(↑z : ℂ)).re ((normSq : (a : ℂ) → ℝ) (-(↑z : ℂ)) : ℝ) = -z.re
rw₄ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖-(↑z : ℂ)‖ 2 = -z.re
rw₅ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 = -z.re
⊢ (S • z).re = -z.re
have rw₆ : (-(↑z : ℂ)).re / HPow.hPow (α := ℝ) (β := ℕ) 1 2 = -z.re
Tactic: rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
rw : { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }.re = -z.re
rw₁ : (↑{ coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } : ℂ).re = -z.re
rw₂ : (-(↑z : ℂ))⁻¹.re = -z.re
rw₃ : HDiv.hDiv (β := ℝ) (-(↑z : ℂ)).re ((normSq : (a : ℂ) → ℝ) (-(↑z : ℂ)) : ℝ) = -z.re
rw₄ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖-(↑z : ℂ)‖ 2 = -z.re
rw₅ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 = -z.re
rw₆ : (-(↑z : ℂ)).re / HPow.hPow (α := ℝ) (β := ℕ) 1 2 = -z.re
⊢ (S • z).re = -z.re
have rw₇ : (-(↑z : ℂ)).re / 1 = -z.re
Tactic: rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
rw : { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }.re = -z.re
rw₁ : (↑{ coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } : ℂ).re = -z.re
rw₂ : (-(↑z : ℂ))⁻¹.re = -z.re
rw₃ : HDiv.hDiv (β := ℝ) (-(↑z : ℂ)).re ((normSq : (a : ℂ) → ℝ) (-(↑z : ℂ)) : ℝ) = -z.re
rw₄ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖-(↑z : ℂ)‖ 2 = -z.re
rw₅ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 = -z.re
rw₆ : (-(↑z : ℂ)).re / HPow.hPow (α := ℝ) (β := ℕ) 1 2 = -z.re
rw₇ : (-(↑z : ℂ)).re / 1 = -z.re
⊢ (S • z).re = -z.re
have rw₈ : (-(↑z : ℂ)).re = -z.re
Tactic: rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
rw : { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }.re = -z.re
rw₁ : (↑{ coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } : ℂ).re = -z.re
rw₂ : (-(↑z : ℂ))⁻¹.re = -z.re
rw₃ : HDiv.hDiv (β := ℝ) (-(↑z : ℂ)).re ((normSq : (a : ℂ) → ℝ) (-(↑z : ℂ)) : ℝ) = -z.re
rw₄ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖-(↑z : ℂ)‖ 2 = -z.re
rw₅ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 = -z.re
rw₆ : (-(↑z : ℂ)).re / HPow.hPow (α := ℝ) (β := ℕ) 1 2 = -z.re
rw₇ : (-(↑z : ℂ)).re / 1 = -z.re
rw₈ : (-(↑z : ℂ)).re = -z.re
⊢ (S • z).re = -z.re
have rw₉ : -(↑z : ℂ).re = -z.re
Tactic: rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
rw : { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }.re = -z.re
rw₁ : (↑{ coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } : ℂ).re = -z.re
rw₂ : (-(↑z : ℂ))⁻¹.re = -z.re
rw₃ : HDiv.hDiv (β := ℝ) (-(↑z : ℂ)).re ((normSq : (a : ℂ) → ℝ) (-(↑z : ℂ)) : ℝ) = -z.re
rw₄ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖-(↑z : ℂ)‖ 2 = -z.re
rw₅ : (-(↑z : ℂ)).re / HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 = -z.re
rw₆ : (-(↑z : ℂ)).re / HPow.hPow (α := ℝ) (β := ℕ) 1 2 = -z.re
rw₇ : (-(↑z : ℂ)).re / 1 = -z.re
rw₈ : (-(↑z : ℂ)).re = -z.re
rw₉ : -(↑z : ℂ).re = -z.re
⊢ (S • z).re = -z.re
have rw₁₀ : -z.re = -z.re
Tactic: rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hSre : (S • z).re = -z.re
Tactic: have hSre : re (S • z) = -z.re := by
    rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
-- 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
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have this : |(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • z).re| ≤ 1 / 2
Tactic: have := 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 • 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 : |(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • S • 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) : ℝ) + -z.re| ≤ 1 / 2
Tactic: rw [← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re, add_comm, coe_re, hSre] 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
⊢ 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) : ℝ)| - |(-z.re)| ≤ 1 / 2
Tactic: have := (abs_sub_abs_le_abs_add _ _).trans 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_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| - |(-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) : ℝ)| ≤ 1 / 2 + |z.re|
Tactic: rw [abs_neg, sub_le_iff_le_add] 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
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|
⊢ g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have inl : ∀ (hzre : |z.re| < 1 / 2), g = S ∧ ‖(↑z : ℂ)‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rcases lt_or_eq_of_le hz.2 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
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|
inl : ∀ (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 lt_or_eq_of_le hz.2 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
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) : ℝ)| < 1 / 2 + 1 / 2
Tactic: have := this.trans_lt ((add_lt_add_iff_left _).mpr 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
this_1 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) + -z.re| ≤ 1 / 2
this_2 : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| ≤ 1 / 2 + |z.re|
hzre : |z.re| < 1 / 2
this : |(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ)| < 1 / 2 + 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| < 1
Tactic: rw [add_halves, ← Int.cast_abs, ← Int.cast_one (R := ℝ), Int.cast_lt] at this
Cleared hypotheses: this