awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p
nonZ1 : HPow.hPow (α := ℂ) (β := ℕ) (↑(p 0) : ℂ) 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑(p 1) : ℂ) 2 ≠ 0
this : Ne (α := Fin 2 → ℝ) (Int.cast ∘ p) 0
nonZ2 : (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ) ≠ 0
subst :
  ∀ (hp : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1))
    (nonZ1 :
      HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
          HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2 ≠
        0)
    (this : Ne (α := Fin 2 → ℝ) (Int.cast ∘ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) 0)
    (nonZ2 :
      (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0),
    (↑(g • z) : ℂ) =
      (↑((lcRow0 ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
                (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
                  Matrix (Fin 2) (Fin 2) ℝ)) :
            ℂ) /
          (HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
            HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2) +
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) * (↑z : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) /
          ((HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
              HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2) *
            ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)))
⊢ (↑(g • z) : ℂ) =
    (↑((lcRow0 p : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
              (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
                Matrix (Fin 2) (Fin 2) ℝ)) :
          ℂ) /
        (HPow.hPow (α := ℂ) (β := ℕ) (↑(p 0) : ℂ) 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑(p 1) : ℂ) 2) +
      ((↑(p 1) : ℂ) * (↑z : ℂ) - (↑(p 0) : ℂ)) /
        ((HPow.hPow (α := ℂ) (β := ℕ) (↑(p 0) : ℂ) 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑(p 1) : ℂ) 2) *
          ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))

Tactic:
subst hg
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
nonZ1 :
  HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
      HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2 ≠
    0
this : Ne (α := Fin 2 → ℝ) (Int.cast ∘ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) 0
nonZ2 : (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0
rw :
  ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
      ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ)) =
    (↑((lcRow0 ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
              (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
                Matrix (Fin 2) (Fin 2) ℝ)) :
          ℂ) /
        (HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
          HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2) +
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) * (↑z : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) /
        ((HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
            HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2) *
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)))
⊢ (↑(g • z) : ℂ) =
    (↑((lcRow0 ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
              (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
                Matrix (Fin 2) (Fin 2) ℝ)) :
          ℂ) /
        (HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
          HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2) +
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) * (↑z : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) /
        ((HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
            HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2) *
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)))

Tactic:
rw [coe_specialLinearGroup_apply]

Premises used: UpperHalfPlane.coe_specialLinearGroup_apply
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
nonZ1 :
  HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
      HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2 ≠
    0
this : Ne (α := Fin 2 → ℝ) (Int.cast ∘ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) 0
nonZ2 : (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0
⊢ (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0

Tactic:
nonZ2
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
nonZ1 :
  HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
      HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2 ≠
    0
this : Ne (α := Fin 2 → ℝ) (Int.cast ∘ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) 0
nonZ2 : (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0
h :
  (↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)
⊢ (↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0

Tactic:
convert! nonZ2 using 1
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
nonZ1 :
  HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
      HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2 ≠
    0
this : Ne (α := Fin 2 → ℝ) (Int.cast ∘ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) 0
nonZ2 : (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0
⊢ (↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
nonZ1 :
  HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
      HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2 ≠
    0
this : Ne (α := Fin 2 → ℝ) (Int.cast ∘ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) 0
nonZ2 : (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0
⊢ (↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0

Tactic:
replace nonZ2 : z * (g 1 0 : ℂ) + g 1 1 ≠ 0 := by convert! nonZ2 using 1; ring
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
nonZ1 :
  HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
      HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2 ≠
    0
this : Ne (α := Fin 2 → ℝ) (Int.cast ∘ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) 0
nonZ2 : (↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0
⊢ Eq (α := ℂ) (↑(↑g : Matrix (Fin 2) (Fin 2) ℤ).det : ℂ)
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) :
      ℂ)

Tactic:
have H := congr(Int.cast (R := ℂ) $(det_fin_two g))
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
nonZ1 :
  HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
      HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2 ≠
    0
this : Ne (α := Fin 2 → ℝ) (Int.cast ∘ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) 0
nonZ2 : (↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0
H :
  Eq (α := ℂ) (↑(↑g : Matrix (Fin 2) (Fin 2) ℤ).det : ℂ)
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) :
      ℂ)
⊢ 1 =
    HMul.hMul (α := ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) -
      HMul.hMul (α := ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)

Tactic:
simp at H
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
nonZ1 :
  HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
      HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2 ≠
    0
this : Ne (α := Fin 2 → ℝ) (Int.cast ∘ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) 0
nonZ2 : (↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0
H :
  1 =
    HMul.hMul (α := ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) -
      HMul.hMul (α := ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)
simp :
  ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ)) *
      (HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
        HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2) =
    ((↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) *
        (HMul.hMul (α := ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) +
          HMul.hMul (α := ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ)
            (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) +
      ((↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ))
⊢ ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
      ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ)) =
    (↑((lcRow0 ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
              (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
                Matrix (Fin 2) (Fin 2) ℝ)) :
          ℂ) /
        (HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
          HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2) +
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) * (↑z : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) /
        ((HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
            HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2) *
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)))

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
nonZ1 :
  HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
      HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2 ≠
    0
this : Ne (α := Fin 2 → ℝ) (Int.cast ∘ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) 0
nonZ2 : (↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) ≠ 0
H :
  1 =
    HMul.hMul (α := ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) -
      HMul.hMul (α := ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)
⊢ ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ)) *
      (HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) 2 +
        HPow.hPow (α := ℂ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) 2) =
    ((↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) *
        (HMul.hMul (α := ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) +
          HMul.hMul (α := ℂ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ)
            (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) +
      ((↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ))

Tactic:
linear_combination -((z : ℂ) * (g 1 1 : ℂ) - g 1 0) * H

Premises used: Int.cast, HMul.hMul, UpperHalfPlane.coe, HSub.hSub, OfNat.ofNat, Subtype.val
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this :
  Tendsto
    (fun (g : (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type)) ↦
      ((↑g : SL(2, ℤ)) • z).re)
    cofinite (cocompact ℝ)
⊢ Tendsto (β := ℝ) (fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p }) ↦ |((↑g : SL(2, ℤ)) • z).re|)
    cofinite atTop

Tactic:
tendsto_norm_cocompact_atTop.comp this

Premises used: abs, Set.Mem, setOf, Set.preimage, Set.singleton, Filter.Tendsto.comp, tendsto_norm_cocompact_atTop
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this :
  Tendsto
    (fun (g : (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type)) ↦
      ((↑g : SL(2, ℤ)) • z).re)
    cofinite (cocompact ℝ)
⊢ Tendsto (β := ℝ) (fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p }) ↦ |((↑g : SL(2, ℤ)) • z).re|)
    cofinite atTop

Tactic:
exact tendsto_norm_cocompact_atTop.comp this

Premises used: Filter.Tendsto.comp, tendsto_norm_cocompact_atTop
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
Tendsto :
  Filter.Tendsto
    (fun (g : (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type)) ↦
      ((↑g : SL(2, ℤ)) • z).re)
    cofinite (cocompact ℝ)
⊢ Filter.Tendsto (β := ℝ)
    (fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p }) ↦ |((↑g : SL(2, ℤ)) • z).re|) cofinite atTop

Tactic:
suffices
    Tendsto (fun g : (fun g : SL(2, ℤ) => g 1) ⁻¹' {p} => ((g : SL(2, ℤ)) • z).re) cofinite
      (cocompact ℝ)
    by exact tendsto_norm_cocompact_atTop.comp this
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
h : HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2 ≠ 0
⊢ (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ ≠ 0

Tactic:
apply inv_ne_zero

Premises used: inv_ne_zero
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2 ≠ 0

Tactic:
mod_cast hp.sq_add_sq_ne_zero

Premises used: Int.cast, congrArg, Int.cast_zero, cast, Ne, Nat.cast, Int.cast_inj._simp_1, HPow.hPow, HAdd.hAdd, congr, Int.cast_pow._simp_1, Int.cast_add._simp_1, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq, Not, IsCoprime.sq_add_sq_ne_zero, Eq.trans
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2 ≠ 0

Tactic:
exact mod_cast hp.sq_add_sq_ne_zero

Premises used: IsCoprime.sq_add_sq_ne_zero
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ ≠ 0

Tactic:
have : ((p 0 : ℝ) ^ 2 + (p 1 : ℝ) ^ 2)⁻¹ ≠ 0 := by
    apply inv_ne_zero
    exact mod_cast hp.sq_add_sq_ne_zero
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ ≠ 0
f : ℝ ≃ₜ ℝ :=
  Homeomorph.mulRight₀ (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ this
ff : ℝ ≃ₜ ℝ :=
  Homeomorph.addRight
    (((↑(p 1) : ℂ) * (↑z : ℂ) - (↑(p 0) : ℂ)) /
        ((HPow.hPow (α := ℂ) (β := ℕ) (↑(p 0) : ℂ) 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑(p 1) : ℂ) 2) *
          ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))).re
⊢ Tendsto (α := { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p })
    (Function.comp (β := ℝ) (⇑(f.trans ff) : (a : ℝ) → ℝ)
      fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p }) ↦
      (lcRow0 p : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
        (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (↑g : SL(2, ℤ))) :
          Matrix (Fin 2) (Fin 2) ℝ))
    cofinite (cocompact ℝ)

Tactic:
(f.trans ff).isClosedEmbedding.tendsto_cocompact.comp (tendsto_lcRow0 hp)

Premises used: Topology.IsClosedEmbedding.tendsto_cocompact, ModularGroup.tendsto_lcRow0, Homeomorph.trans, Filter.Tendsto.comp, Homeomorph.isClosedEmbedding
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ ≠ 0
f : ℝ ≃ₜ ℝ :=
  Homeomorph.mulRight₀ (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ this
ff : ℝ ≃ₜ ℝ :=
  Homeomorph.addRight
    (((↑(p 1) : ℂ) * (↑z : ℂ) - (↑(p 0) : ℂ)) /
        ((HPow.hPow (α := ℂ) (β := ℕ) (↑(p 0) : ℂ) 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑(p 1) : ℂ) 2) *
          ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))).re
h :
  (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type) =
      { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p } →
    ∀ (g : (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type)),
      ((↑g : SL(2, ℤ)) • z).re =
        Function.comp (β := ℝ) (⇑(f.trans ff) : (a : ℝ) → ℝ)
          (fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p }) ↦
            (lcRow0 p : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
              (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (↑g : SL(2, ℤ))) :
                Matrix (Fin 2) (Fin 2) ℝ))
          g
⊢ Tendsto
    (fun (g : (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type)) ↦
      ((↑g : SL(2, ℤ)) • z).re)
    cofinite (cocompact ℝ)

Tactic:
convert! (f.trans ff).isClosedEmbedding.tendsto_cocompact.comp (tendsto_lcRow0 hp) with _ _ g

Premises used: Topology.IsClosedEmbedding.tendsto_cocompact, ModularGroup.tendsto_lcRow0, Homeomorph.trans, Filter.Tendsto.comp, Homeomorph.isClosedEmbedding
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ ≠ 0
f : ℝ ≃ₜ ℝ :=
  Homeomorph.mulRight₀ (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ this
ff : ℝ ≃ₜ ℝ :=
  Homeomorph.addRight
    (((↑(p 1) : ℂ) * (↑z : ℂ) - (↑(p 0) : ℂ)) /
        ((HPow.hPow (α := ℂ) (β := ℕ) (↑(p 0) : ℂ) 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑(p 1) : ℂ) 2) *
          ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))).re
e_1 :
  (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type) =
    { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p }
g : (↑(Set.preimage (β := Fin 2 → ℤ) (fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1) {p}) : Type)
h :
  ((↑g : SL(2, ℤ)) • z).re =
    HDiv.hDiv (α := ℝ)
        ((lcRow0 p : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
            (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (↑g : SL(2, ℤ))) :
              Matrix (Fin 2) (Fin 2) ℝ) :
          ℝ)
        (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2) +
      (((↑(p 1) : ℂ) * (↑z : ℂ) - (↑(p 0) : ℂ)) /
          ((HPow.hPow (α := ℂ) (β := ℕ) (↑(p 0) : ℂ) 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑(p 1) : ℂ) 2) *
            ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))).re
⊢ ((↑g : SL(2, ℤ)) • z).re =
    Function.comp (β := ℝ) (⇑(f.trans ff) : (a : ℝ) → ℝ)
      (fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p }) ↦
        (lcRow0 p : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
          (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (↑g : SL(2, ℤ))) :
            Matrix (Fin 2) (Fin 2) ℝ))
      g

Tactic:
change
    ((g : SL(2, ℤ)) • z).re =
      lcRow0 p ↑(↑g : SL(2, ℝ)) / ((p 0 : ℝ) ^ 2 + (p 1 : ℝ) ^ 2) +
        Complex.re (((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1)))

Premises used: Int.cast, Real, HMul.hMul, UpperHalfPlane.coe, HSub.hSub, HDiv.hDiv, Complex.re, HPow.hPow, HAdd.hAdd, Matrix.SpecialLinearGroup.map, Int.castRingHom, HSMul.hSMul, OfNat.ofNat, Subtype.val, DFunLike.coe, UpperHalfPlane.re, ModularGroup.lcRow0