awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
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
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
⊢ 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:
rw [← mul_pow]

Premises used: mul_pow
-- Module: Mathlib.NumberTheory.Modular
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
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
⊢ 9 * HPow.hPow (β := ℕ) c 4 ≤ 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

Premises used: Real, UpperHalfPlane.coe, Complex.normSq, UpperHalfPlane.denom, UpperHalfPlane.im, Matrix.SpecialLinearGroup.map, Int.castRingHom, HSMul.hSMul, DFunLike.coe, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.Modular
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
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
⊢ (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

Premises used: OfNat.ofNat, Subtype.val
-- Module: Mathlib.NumberTheory.Modular
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) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0

Tactic:
simpa using hc
-- Module: Mathlib.NumberTheory.Modular
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
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
⊢ (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) ?_

Premises used: Eq.rec, Eq.symm, ModularGroup.SL_neg_smul
-- Module: Mathlib.NumberTheory.Modular
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
⊢ 0 ≤ (↑(-g) : Matrix (Fin 2) (Fin 2) ℤ) 1 1

Tactic:
simpa using (not_le.mp hd).le

Premises used: not_le, LT.lt.le, Iff.mp
-- Module: Mathlib.NumberTheory.Modular
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

Tactic:
this
-- Module: Mathlib.NumberTheory.Modular
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
h₂ : g = 1 ∨ g = -1 ↔ -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:
convert! this using 2
-- Module: Mathlib.NumberTheory.Modular
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 ↔ -g = T ∨ -g = -T

Tactic:
simp [neg_eq_iff_eq_neg, or_comm]

Premises used: neg_eq_iff_eq_neg, or_comm
-- Module: Mathlib.NumberTheory.Modular
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

Tactic:
simp [neg_eq_iff_eq_neg, or_comm]

Premises used: neg_eq_iff_eq_neg, or_comm
-- Module: Mathlib.NumberTheory.Modular
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 = 1 ∨ g = -1 ↔ -g = 1 ∨ -g = -1

Tactic:
simp [neg_eq_iff_eq_neg, or_comm]

Premises used: neg_eq_iff_eq_neg, or_comm
-- Module: Mathlib.NumberTheory.Modular
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 : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1

Tactic:
simpa [hc, isCoprime_zero_left, Int.isUnit_iff] using bottom_row_coprime g

Premises used: ModularGroup.bottom_row_coprime, isCoprime_zero_left, Int.isUnit_iff
-- Module: Mathlib.NumberTheory.Modular
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 : 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
-- Module: Mathlib.NumberTheory.Modular
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 : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.Modular
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 : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1

Tactic:
replace hd : g 1 1 = 1 := by grind
-- Module: Mathlib.NumberTheory.Modular
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 : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1

Tactic:
grind [det_fin_two, g.property]

Premises used: Matrix.det_fin_two, Subtype.property
-- Module: Mathlib.NumberTheory.Modular
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 : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1

Tactic:
have ha : g 0 0 = 1 := by grind [det_fin_two, g.property]
-- Module: Mathlib.NumberTheory.Modular
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
a : ∀ (i j : Fin 2), (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(T ^ b) : Matrix (Fin 2) (Fin 2) ℤ) i j
⊢ g = T ^ b

Tactic:
ext i j
-- Module: Mathlib.NumberTheory.Modular
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) ℤ) i j = !![1, b; 0, 1] i j
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(T ^ b) : Matrix (Fin 2) (Fin 2) ℤ) i j

Tactic:
rw [coe_T_zpow]

Premises used: ModularGroup.coe_T_zpow
-- Module: Mathlib.NumberTheory.Modular
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
a₁ :
  (↑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
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = !![1, b; 0, 1] i j

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.Modular
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, ⋯⟩)
a₁ :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑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

Tactic:
fin_cases j
-- Module: Mathlib.NumberTheory.Modular
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, ⋯⟩)
a₁ :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑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

Tactic:
fin_cases j
-- Module: Mathlib.NumberTheory.Modular
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 : 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, ⋯⟩)

Tactic:
tauto
-- Module: Mathlib.NumberTheory.Modular
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 : 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, ⋯⟩)

Tactic:
tauto
-- Module: Mathlib.NumberTheory.Modular
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 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    !![1, b; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
tauto
-- Module: Mathlib.NumberTheory.Modular
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

Tactic:
have hgz : g = T ^ b := by
    ext i j
    rw [coe_T_zpow]
    fin_cases i <;> fin_cases j <;> tauto
-- Module: Mathlib.NumberTheory.Modular
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
hgz : g = T ^ b
rw : (T ^ b • z).re = (↑b : ℝ) + z.re
rw₁ : (↑(T ^ b • z) : ℂ).re = (↑b : ℝ) + z.re
rw₂ : ((↑z : ℂ) + (↑b : ℂ)).re = (↑b : ℝ) + z.re
rw₃ : (↑z : ℂ).re + Complex.re (↑b : ℂ) = (↑b : ℝ) + z.re
rw₄ : z.re + Complex.re (↑b : ℂ) = (↑b : ℝ) + z.re
rw₅ : z.re + (↑b : ℝ) = (↑b : ℝ) + z.re
rw₆ rw₇ : (↑b : ℝ) + z.re = (↑b : ℝ) + z.re
⊢ (g • z).re = (↑b : ℝ) + z.re

Tactic:
rw [hgz, ← coe_re, coe_T_zpow_smul_eq, add_re, coe_re, intCast_re, add_comm]

Premises used: ModularGroup.coe_T_zpow_smul_eq, Complex.add_re, Complex.intCast_re, add_comm, UpperHalfPlane.coe_re
-- Module: Mathlib.NumberTheory.Modular
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
hgz : g = T ^ b
⊢ (g • z).re = (↑b : ℝ) + z.re

Tactic:
have hre : (g • z).re = b + z.re := by
    rw [hgz, ← coe_re, coe_T_zpow_smul_eq, add_re, coe_re, intCast_re, add_comm]
-- Module: Mathlib.NumberTheory.Modular
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
hgz : g = T ^ b
hre : (g • z).re = (↑b : ℝ) + z.re
⊢ |(↑b : ℝ)| - |z.re| ≤ 1 / 2

Tactic:
have := (abs_sub_abs_le_abs_add ..).trans (hre ▸ hg.2)
-- Module: Mathlib.NumberTheory.Modular
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
hgz : g = T ^ b
hre : (g • z).re = (↑b : ℝ) + z.re
this : |(↑b : ℝ)| - |z.re| ≤ 1 / 2
⊢ b = 0 ∨ b = 1 ∨ b = -1

Tactic:
grw [sub_le_iff_le_add, hz.2, add_halves, ← Int.cast_abs, ← Int.cast_one, Int.cast_le,
    Int.abs_le_one_iff] at this

Premises used: Int.cast_abs, Int.cast_le, add_halves, sub_le_iff_le_add, Int.abs_le_one_iff, And.right, Int.cast_one
-- Module: Mathlib.NumberTheory.Modular
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
hgz : g = T ^ b
hre : (g • z).re = (↑b : ℝ) + z.re
this : b = 0 ∨ b = 1 ∨ b = -1
inl : ∀ (hb : b = 0), (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
inr : ∀ (hb : b = 1), (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
inr₁ : ∀ (hb : b = -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

Tactic:
rcases this with hb | hb | hb
-- Module: Mathlib.NumberTheory.Modular
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
hgz : g = T ^ b
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = 0
⊢ g = HPow.hPow (β := ℤ) T 0

Tactic:
rw [hb] at hgz
-- Module: Mathlib.NumberTheory.Modular
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
hgz : g = T ^ b
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = 0
hgz₁ : g = HPow.hPow (β := ℤ) T 0
⊢ (g • z).re = (↑b : ℝ) + z.re

Tactic:
rw [hb] at hgz
-- Module: Mathlib.NumberTheory.Modular
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
hgz : g = T ^ b
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = 0
hgz₁ : g = HPow.hPow (β := ℤ) T 0
hre₁ : (g • z).re = (↑b : ℝ) + z.re
⊢ b = 0

Tactic:
rw [hb] at hgz
-- Module: Mathlib.NumberTheory.Modular
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
hgz : g = T ^ b
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = 1
⊢ g = HPow.hPow (β := ℤ) T 1

Tactic:
rw [hb] at hgz
-- Module: Mathlib.NumberTheory.Modular
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
hgz : g = T ^ b
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = 1
hgz₁ : g = HPow.hPow (β := ℤ) T 1
⊢ (g • z).re = (↑b : ℝ) + z.re

Tactic:
rw [hb] at hgz
-- Module: Mathlib.NumberTheory.Modular
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
hgz : g = T ^ b
hre : (g • z).re = (↑b : ℝ) + z.re
hb : b = 1
hgz₁ : g = HPow.hPow (β := ℤ) T 1
hre₁ : (g • z).re = (↑b : ℝ) + z.re
⊢ b = 1

Tactic:
rw [hb] at hgz