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 ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
h₁ :
  HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4
h₂ :
  HPow.hPow (β := ℕ) (c * z.im) 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 ≤
    1
⊢ 9 * HPow.hPow (β := ℕ) c 4 ≤ HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 2 * HPow.hPow (β := ℕ) (g • z).im 2 * 16
have linarith : HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 2 * HPow.hPow (β := ℕ) (g • z).im 2 * 16 < 9 * HPow.hPow (β := ℕ) c 4 →
  HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 -
        4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4 +
      (HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 2 * HPow.hPow (β := ℕ) (g • z).im 2 * 16 -
        9 * HPow.hPow (β := ℕ) c 4) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
h₁ :
  HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4
h₂ :
  HPow.hPow (β := ℕ) (c * z.im) 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 ≤
    1
⊢ HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 4 /
        HPow.hPow (α := ℝ) (β := ℕ)
          ((normSq : (a : ℂ) → ℝ)
              (denom
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                  ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                (↑z : ℂ)) :
            ℝ)
          2 *
      16 ≤
    16
have rw : HPow.hPow (β := ℕ) (c * z.im) 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 *
    16 ≤
  16
Tactic: rw [← mul_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
h₁ :
  HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4
h₂ :
  HPow.hPow (β := ℕ) (c * z.im) 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 ≤
    1
⊢ HPow.hPow (β := ℕ) (c * z.im) 4 /
        HPow.hPow (α := ℝ) (β := ℕ)
          ((normSq : (a : ℂ) → ℝ)
              (denom
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                  ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                (↑z : ℂ)) :
            ℝ)
          2 *
      16 ≤
    16
have linarith : 16 <
    HPow.hPow (β := ℕ) (c * z.im) 4 /
        HPow.hPow (α := ℝ) (β := ℕ)
          ((normSq : (a : ℂ) → ℝ)
              (denom
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                  ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                (↑z : ℂ)) :
            ℝ)
          2 *
      16 →
  HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
h₁ :
  HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4
h₂ :
  HPow.hPow (β := ℕ) (c * z.im) 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 ≤
    1
linarith :
  16 <
      HPow.hPow (β := ℕ) (c * z.im) 4 /
          HPow.hPow (α := ℝ) (β := ℕ)
            ((normSq : (a : ℂ) → ℝ)
                (denom
                  ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                    ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                  (↑z : ℂ)) :
              ℝ)
            2 *
        16 →
    HMul.hMul (α := ℝ) 1 1 = 1
⊢ HPow.hPow (β := ℕ) (c * z.im) 4 /
        HPow.hPow (α := ℝ) (β := ℕ)
          ((normSq : (a : ℂ) → ℝ)
              (denom
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                  ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                (↑z : ℂ)) :
            ℝ)
          2 *
      16 ≤
    16
have linarith₁ : 16 <
    HPow.hPow (β := ℕ) (c * z.im) 4 /
        HPow.hPow (α := ℝ) (β := ℕ)
          ((normSq : (a : ℂ) → ℝ)
              (denom
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                  ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                (↑z : ℂ)) :
            ℝ)
          2 *
      16 →
  16 *
        (1 *
            (HPow.hPow (β := ℕ) (c * z.im) 4 /
              HPow.hPow (α := ℝ) (β := ℕ)
                ((normSq : (a : ℂ) → ℝ)
                    (denom
                      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                        ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                      (↑z : ℂ)) :
                  ℝ)
                2) -
          HMul.hMul (α := ℝ) 1 1) +
      (HMul.hMul (α := ℝ) 1 16 -
        1 *
            (HPow.hPow (β := ℕ) (c * z.im) 4 /
              HPow.hPow (α := ℝ) (β := ℕ)
                ((normSq : (a : ℂ) → ℝ)
                    (denom
                      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                        ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                      (↑z : ℂ)) :
                  ℝ)
                2) *
          HMul.hMul (α := ℝ) 1 16) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
h₁ :
  HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4
h₂ :
  HPow.hPow (β := ℕ) (c * z.im) 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 ≤
    1
⊢ 9 * HPow.hPow (β := ℕ) c 4 ≤ 16
have c₁ : 9 * HPow.hPow (β := ℕ) c 4 ≤ HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 2 * HPow.hPow (β := ℕ) (g • z).im 2 * 16
Tactic: calc
    9 * c ^ 4 ≤ c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16 := by linarith
    _ = c ^ 4 * z.im ^ 4 / normSq (denom g z) ^ 2 * 16 := by grind [im_smul_eq_div_normSq]
    _ ≤ 16 := by rw [← mul_pow]; linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
h₁ :
  HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4
h₂ :
  HPow.hPow (β := ℕ) (c * z.im) 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 ≤
    1
c₁ :
  9 * HPow.hPow (β := ℕ) c 4 ≤ HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 2 * HPow.hPow (β := ℕ) (g • z).im 2 * 16
⊢ 9 * HPow.hPow (β := ℕ) c 4 ≤ 16
have c₂ : HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 2 * HPow.hPow (β := ℕ) (g • z).im 2 * 16 =
  HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 *
    16
Tactic: calc
    9 * c ^ 4 ≤ c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16 := by linarith
    _ = c ^ 4 * z.im ^ 4 / normSq (denom g z) ^ 2 * 16 := by grind [im_smul_eq_div_normSq]
    _ ≤ 16 := by rw [← mul_pow]; linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
h₁ :
  HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4
h₂ :
  HPow.hPow (β := ℕ) (c * z.im) 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 ≤
    1
c₁ :
  9 * HPow.hPow (β := ℕ) c 4 ≤ HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 2 * HPow.hPow (β := ℕ) (g • z).im 2 * 16
c₂ :
  HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 2 * HPow.hPow (β := ℕ) (g • z).im 2 * 16 =
    HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 4 /
        HPow.hPow (α := ℝ) (β := ℕ)
          ((normSq : (a : ℂ) → ℝ)
              (denom
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                  ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                (↑z : ℂ)) :
            ℝ)
          2 *
      16
⊢ 9 * HPow.hPow (β := ℕ) c 4 ≤ 16
have c₃ : HPow.hPow (β := ℕ) c 4 * HPow.hPow (β := ℕ) z.im 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 *
    16 ≤
  16
Tactic: calc
    9 * c ^ 4 ≤ c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16 := by linarith
    _ = c ^ 4 * z.im ^ 4 / normSq (denom g z) ^ 2 * 16 := by grind [im_smul_eq_div_normSq]
    _ ≤ 16 := by rw [← mul_pow]; linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
have inr : ∀
  (this :
    ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0)
      (hd : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1),
      (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1)
  (hd : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1),
  (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
Tactic: wlog hd : 0 ≤ g 1 1
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
inr :
  ∀
    (this :
      ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0)
        (hd : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1),
        (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1)
    (hd : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1),
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
have wlog : ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0)
  (hd : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1),
  (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
Tactic: wlog hd : 0 ≤ g 1 1
Cleared hypotheses: hz, hg, hc
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0)
    (hd : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1),
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
hd : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
have inr : 0 ≤ (↑(-g) : Matrix (Fin 2) (Fin 2) ℤ) 1 1
Tactic: specialize this hz (g := -g) (SL_neg_smul g z ▸ hg) (by simpa using hc) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0)
    (hd : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1),
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
hd : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1
inr : 0 ≤ (↑(-g) : Matrix (Fin 2) (Fin 2) ℤ) 1 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
have inr₁ : ∀ (this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1),
  (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
Tactic: specialize this hz (g := -g) (SL_neg_smul g z ▸ hg) (by simpa using hc) ?_
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
have h : g = T ∨ g = -T ↔ -g = T ∨ -g = -T
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
h : g = T ∨ g = -T ↔ -g = T ∨ -g = -T
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
have h₁ : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ↔ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : ¬0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
h : g = T ∨ g = -T ↔ -g = T ∨ -g = -T
h₁ : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ↔ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
have h₂ : g = 1 ∨ g = -1 ↔ -g = 1 ∨ -g = -1
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
have hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
Tactic: have hd' : g 1 1 = 1 ∨ g 1 1 = -1 := by
    simpa [hc, isCoprime_zero_left, Int.isUnit_iff] using bottom_row_coprime g
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
have hd₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
Tactic: replace hd : g 1 1 = 1 := by grind
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
have ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
Tactic: have ha : g 0 0 = 1 := by grind [det_fin_two, g.property]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
⊢ g = T ^ b
have a : ∀ (i j : Fin 2), (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(T ^ b) : Matrix (Fin 2) (Fin 2) ℤ) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
i j : Fin 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(T ^ b) : Matrix (Fin 2) (Fin 2) ℤ) i j
have a : (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = !![1, b; 0, 1] i j
Tactic: rw [coe_T_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
i j : Fin 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = !![1, b; 0, 1] i j
have a : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) j =
  !![1, b; 0, 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_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
i j : Fin 2
a :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = !![1, b; 0, 1] i j
have a₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j =
  !![1, b; 0, 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_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
j : Fin 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    !![1, b; 0, 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)) =
  !![1, b; 0, 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_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 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)) =
    !![1, b; 0, 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 =
    !![1, b; 0, 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)) =
  !![1, b; 0, 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_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
j : Fin 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    !![1, b; 0, 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)) =
  !![1, b; 0, 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_1 : SL(2, ℤ)
z_1 : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
b : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 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)) =
    !![1, b; 0, 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 =
    !![1, b; 0, 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)) =
  !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j