awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
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
rw :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) =
    !![(HMul.hMul (α := ℤ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 1) * 1 +
          (HMul.hMul (α := ℤ) 1 (-1) + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 0) * 0,
        (HMul.hMul (α := ℤ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 1) * -1 +
          (HMul.hMul (α := ℤ) 1 (-1) + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 0) * 1;
      (HMul.hMul (α := ℤ) 0 0 + HMul.hMul (α := ℤ) 1 1) * 1 + (HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 0) * 0,
        (HMul.hMul (α := ℤ) 0 0 + HMul.hMul (α := ℤ) 1 1) * -1 +
          (HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 0) * 1]
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) = (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹) : Matrix (Fin 2) (Fin 2) ℤ)

Tactic:
rw [coe_mul, coe_mul, coe_T_zpow, coe_S, ← zpow_neg_one, coe_T_zpow, mul_fin_two, mul_fin_two]

Premises used: zpow_neg_one, Matrix.mul_fin_two, ModularGroup.coe_T_zpow, ModularGroup.coe_S, Matrix.SpecialLinearGroup.coe_mul
-- Module: Mathlib.NumberTheory.Modular
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
ring_nf :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, -1]
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) =
    !![(HMul.hMul (α := ℤ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 1) * 1 +
          (HMul.hMul (α := ℤ) 1 (-1) + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 0) * 0,
        (HMul.hMul (α := ℤ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 1) * -1 +
          (HMul.hMul (α := ℤ) 1 (-1) + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * 0) * 1;
      (HMul.hMul (α := ℤ) 0 0 + HMul.hMul (α := ℤ) 1 1) * 1 + (HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 0) * 0,
        (HMul.hMul (α := ℤ) 0 0 + HMul.hMul (α := ℤ) 1 1) * -1 +
          (HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 0) * 1]

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Modular
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
a :
  ∀ (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
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) =
    !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, -1 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0; 1, -1]

Tactic:
ext i j
-- Module: Mathlib.NumberTheory.Modular
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
a₁ :
  (↑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
⊢ (↑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

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.Modular
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, ⋯⟩)
a₁ :
  (↑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, ⋯⟩)
⊢ (↑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

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

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

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

Tactic:
tauto
-- Module: Mathlib.NumberTheory.Modular
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) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

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

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

Tactic:
simp [this]
-- Module: Mathlib.NumberTheory.Modular
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) ℤ) 0 0 - 1 = -1 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Modular
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 = 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
-- Module: Mathlib.NumberTheory.Modular
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⁻¹
⊢ ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1

Tactic:
hg'
-- Module: Mathlib.NumberTheory.Modular
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⁻¹
h :
  (↑z : ℂ) - 1 =
    denom
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
      (↑z : ℂ)
⊢ ‖(↑z : ℂ) - 1‖ ≤ 1

Tactic:
convert! hg' using 2
-- Module: Mathlib.NumberTheory.Modular
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 =
    denom
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
      (↑z : ℂ)

Tactic:
simp [denom, hc, hd, sub_eq_add_neg]

Premises used: sub_eq_add_neg, UpperHalfPlane.denom
-- Module: Mathlib.NumberTheory.Modular
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

Tactic:
have hnorm : ‖(z : ℂ) - 1‖ ≤ 1 := by
    convert! hg' using 2
    simp [denom, hc, hd, sub_eq_add_neg]
-- Module: Mathlib.NumberTheory.Modular
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
⊢ LE.le (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) : ℝ) (1 : ℝ)

Tactic:
rw [norm_def, Real.sqrt_le_one] at hnorm

Premises used: Real.sqrt_le_one, Complex.norm_def
-- Module: Mathlib.NumberTheory.Modular
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 : ℝ)
simp : (z.re - 1) * (z.re - 1) + z.im * z.im = z.re * z.re + z.im * z.im + (-(2 * z.re) + 1)
⊢ (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)

Tactic:
simp [normSq]

Premises used: Complex.normSq
-- Module: Mathlib.NumberTheory.Modular
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 : ℝ)
⊢ (z.re - 1) * (z.re - 1) + z.im * z.im = z.re * z.re + z.im * z.im + (-(2 * z.re) + 1)

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

Tactic:
have : normSq (z - 1) = normSq z + (-2 * z.re + 1) := by
    simp [normSq]
    ring
-- Module: Mathlib.NumberTheory.Modular
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)
⊢ HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1

Tactic:
rw [this] at hnorm
-- Module: Mathlib.NumberTheory.Modular
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)
hnorm₁ : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
⊢ (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)

Tactic:
rw [this] at hnorm
-- Module: Mathlib.NumberTheory.Modular
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)
⊢ LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)

Tactic:
have : 1 ≤ normSq z := hz.1
-- Module: Mathlib.NumberTheory.Modular
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
linarith₃ : -2 * z.re + 1 < 0 → -2 * z.re + 1 - 0 + (2 * z.re - HMul.hMul (α := ℝ) 1 1) = 0
⊢ 0 ≤ -2 * z.re + 1

Tactic:
linarith [(le_abs_self _).trans hz.2]

Premises used: le_abs_self, And.right, LE.le.trans
-- Module: Mathlib.NumberTheory.Modular
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

Tactic:
have : 0 ≤ -2 * z.re + 1 := by linarith [(le_abs_self _).trans hz.2]
-- Module: Mathlib.NumberTheory.Modular
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 : ℝ)
right : z.re = 1 / 2
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) ∧ z.re = 1 / 2

Tactic:
constructor