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
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
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
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
⊢ (↑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 1 = -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0
Tactic: simp
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
i j : Fin 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, 1] i j
have a : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -1 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0
Tactic: fin_cases i <;> fin_cases j <;> [tauto; simp; tauto; tauto]
Cleared hypotheses: i, 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 = 1
⊢ (g = S * T ∨ g = T * S * T) ∧ z = ρ
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, coe_T, mul_fin_two, mul_fin_two]
    ring_nf
    ext i j
    fin_cases i <;> fin_cases j <;> [tauto; simp; tauto; tauto]
    grind [g.property, det_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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
⊢ (g = S * T ∨ g = T * S * T) ∧ z = ρ
have rw : (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 = ρ
Tactic: rw [hgeq]
-- 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
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) ∧ z.re = -1 / 2
have hnorm : LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) + 1) : ℝ) (1 : ℝ)
Tactic: have hnorm : normSq ((z : ℂ) + 1) ≤ 1 := by simpa [denom, hc, hd, norm_def] using hg'
-- 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 : 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
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T
hnorm : LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) + 1) : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) ∧ z.re = -1 / 2
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
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)
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) ∧ z.re = -1 / 2
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 (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)
⊢ 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
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)
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
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)
⊢ 0 ≤ 2 * z.re + 1
have linarith : 2 * z.re + 1 < 0 → 2 / 2 = 1
Tactic: 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 : 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 : 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 [(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 : 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 : 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 [(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 : 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 : 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 [(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 : 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 : ℝ)
have linarith : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) →
  HSub.hSub (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) +
      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 (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 :
  LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) →
    HSub.hSub (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) +
        HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) =
      0
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
have linarith₁ : LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) →
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (2 * z.re + 1) - 1 +
        HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) +
      (0 - (2 * z.re + 1)) =
    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 (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)
⊢ z.re = -1 / 2
have linarith : z.re < -1 / 2 → 2 / 2 = 1
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 (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
⊢ z.re = -1 / 2
have linarith₁ : z.re < -1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
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 (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
⊢ z.re = -1 / 2
have linarith₂ : z.re < -1 / 2 → GT.gt (α := ℝ) 2 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 (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
⊢ z.re = -1 / 2
have linarith₃ : z.re < -1 / 2 → 2 * z.re - -HMul.hMul (α := ℝ) 1 1 + (0 - (2 * z.re + 1)) = 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 (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
⊢ z.re = -1 / 2
have linarith₄ : -1 / 2 < z.re → 2 / 2 = 1
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 (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
⊢ z.re = -1 / 2
have linarith₅ : -1 / 2 < z.re → HMul.hMul (α := ℝ) 1 2 = 2
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 (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
⊢ z.re = -1 / 2
have linarith₆ : -1 / 2 < z.re → GT.gt (α := ℝ) 2 0
Tactic: linarith [hz.1, show 0 ≤ 2 * z.re + 1 by linarith [(neg_le_abs _).trans hz.2]]