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 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 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
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 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
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 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
-- 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
j : Fin 2
a :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : 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, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (↑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) (⟨1, 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) ⟨1, 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 = -1
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 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 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, -1]
      ((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 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, -1]
    ((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 = -1
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 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 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, -1]
      ((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 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, -1]
      ((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 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, -1]
    ((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 (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
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)) ((fun (i : Fin 2) ↦ i) (⟨1, 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) ⟨1, sorry⟩)
Tactic: fin_cases i <;> fin_cases j <;> [tauto; skip; tauto; tauto]
Cleared hypotheses: 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
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : 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, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
have a : -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1 = -1 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0
Tactic: simp [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
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
Tactic: have hgeq : g = T ^ g 0 0 * S * T⁻¹ := by
    refine Subtype.ext ?_
    rw [coe_mul, coe_mul, coe_T_zpow, coe_S, ← zpow_neg_one, coe_T_zpow, mul_fin_two, mul_fin_two]
    ring_nf
    ext i j
    fin_cases i <;> fin_cases j <;> [tauto; skip; tauto; tauto]
    simp [this]
    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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
⊢ ‖(↑z : ℂ) - 1‖ ≤ 1
have h : (↑z : ℂ) - 1 =
  denom
    ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
      ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
    (↑z : ℂ)
Tactic: convert! hg' using 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
this : (↑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⁻¹
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hnorm : ‖(↑z : ℂ) - 1‖ ≤ 1
Tactic: have hnorm : ‖(z : ℂ) - 1‖ ≤ 1 := by
    convert! hg' using 2
    simp [denom, hc, hd, sub_eq_add_neg]
-- 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) ℤ) 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 : ‖(↑z : ℂ) - 1‖ ≤ 1
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hnorm₁ : LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) : ℝ) (1 : ℝ)
Tactic: rw [norm_def, Real.sqrt_le_one] at hnorm
Cleared hypotheses: hnorm
-- 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) : ℝ) (1 : ℝ)
⊢ (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
have simp : (z.re - 1) * (z.re - 1) + z.im * z.im = z.re * z.re + z.im * z.im + (-(2 * z.re) + 1)
Tactic: simp [normSq]
-- 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) ℤ) 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 : LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) : ℝ) (1 : ℝ)
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have this₁ : (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
Tactic: have : normSq (z - 1) = normSq z + (-2 * z.re + 1) := by
    simp [normSq]
    ring
-- 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 : LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) : ℝ) (1 : ℝ)
this : (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = HVAdd.hVAdd (α := ℝ) 1 ρ
have hnorm₁ : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
Tactic: rw [this] at hnorm
Cleared hypotheses: hnorm, 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
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)
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) ∧ z.re = 1 / 2
have this₁ : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
Tactic: have : 1 ≤ normSq z := hz.1
-- 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_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
this : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
⊢ 0 ≤ -2 * z.re + 1
have linarith : -2 * z.re + 1 < 0 → 2 / 2 = 1
Tactic: linarith [(le_abs_self _).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
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)
this : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
linarith : -2 * z.re + 1 < 0 → 2 / 2 = 1
⊢ 0 ≤ -2 * z.re + 1
have linarith₁ : -2 * z.re + 1 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [(le_abs_self _).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
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)
this : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
linarith : -2 * z.re + 1 < 0 → 2 / 2 = 1
linarith₁ : -2 * z.re + 1 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ -2 * z.re + 1
have linarith₂ : -2 * z.re + 1 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [(le_abs_self _).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
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)
this : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
linarith : -2 * z.re + 1 < 0 → 2 / 2 = 1
linarith₁ : -2 * z.re + 1 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -2 * z.re + 1 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ -2 * z.re + 1
have linarith₃ : -2 * z.re + 1 < 0 → -2 * z.re + 1 - 0 + (2 * z.re - HMul.hMul (α := ℝ) 1 1) = 0
Tactic: linarith [(le_abs_self _).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
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)
this : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) ∧ z.re = 1 / 2
have this₁ : 0 ≤ -2 * z.re + 1
Tactic: have : 0 ≤ -2 * z.re + 1 := by linarith [(le_abs_self _).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
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)
this_3 : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
this : 0 ≤ -2 * z.re + 1
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) ∧ z.re = 1 / 2
have left : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
Tactic: constructor
-- 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_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
this_3 : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
this : 0 ≤ -2 * z.re + 1
left : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) ∧ z.re = 1 / 2
have right : z.re = 1 / 2
Tactic: constructor
-- 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_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
this_3 : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
this : 0 ≤ -2 * z.re + 1
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
have linarith : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) →
  HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) +
      HSub.hSub (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) =
    0
Tactic: linarith