awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (β := Matrix (Fin 2) (Fin 2) ℝ) (fun (m : Matrix (Fin 2) (Fin 2) ℤ) ↦ m.map Int.cast) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦
    (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ)
      ![![t, -(↑1 : ℝ)], Int.cast ∘ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1]
hmB : Continuous mB
hf₂ :
  IsClosedEmbedding (X := Matrix (Fin 2) (Fin 2) ℝ) (Y := Matrix (Fin 2) (Fin 2) ℝ)
    (⇑(lcRow0Extend hcd) : (a : Matrix (Fin 2) (Fin 2) ℝ) → Matrix (Fin 2) (Fin 2) ℝ)
⊢ Eq (α := ℝ)
    (Function.comp (α := { g_1 : SL(2, ℤ) // (↑g_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 })
      (⇑(lcRow0Extend hcd) : (a : Matrix (Fin 2) (Fin 2) ℝ) → Matrix (Fin 2) (Fin 2) ℝ)
      (f₁ ∘ fun (a : { g_1 : SL(2, ℤ) // (↑g_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 }) ↦
        (↑a : SL(2, ℤ)))
      (Subtype.mk (p := fun (g_1 : SL(2, ℤ)) ↦ (↑g_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1)
        g ⋯)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))
    (-(↑(↑g : Matrix (Fin 2) (Fin 2) ℤ).det : ℝ))
have h : Eq (α := ℝ)
  (∑ x : Fin 2,
    (↑(planeConformalMatrix (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ))
              sorry) :
          Matrix (Fin 2) (Fin 2) ℝ)
        (⟨1, sorry⟩ : Fin 2) x *
      (↑g : Matrix (Fin 2) (Fin 2) ℤ).map Int.cast 0 x)
  (-(↑((↑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: simp only [Fin.zero_eta, Function.comp_apply, lcRow0Extend_apply, cons_val_zero,
      LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLin,
      mulVecLin_apply, mulVec, dotProduct, det_fin_two, f₁]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (β := Matrix (Fin 2) (Fin 2) ℝ) (fun (m : Matrix (Fin 2) (Fin 2) ℤ) ↦ m.map Int.cast) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦
    (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ)
      ![![t, -(↑1 : ℝ)], Int.cast ∘ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1]
hmB : Continuous mB
hf₂ :
  IsClosedEmbedding (X := Matrix (Fin 2) (Fin 2) ℝ) (Y := Matrix (Fin 2) (Fin 2) ℝ)
    (⇑(lcRow0Extend hcd) : (a : Matrix (Fin 2) (Fin 2) ℝ) → Matrix (Fin 2) (Fin 2) ℝ)
⊢ Eq (α := ℝ)
    (∑ x : Fin 2,
      (↑(planeConformalMatrix (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ)
                (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) ⋯) :
            Matrix (Fin 2) (Fin 2) ℝ)
          (⟨1, ⋯⟩ : Fin 2) x *
        (↑g : Matrix (Fin 2) (Fin 2) ℤ).map Int.cast 0 x)
    (-(↑((↑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) :
        ℝ))
have h : -HMul.hMul (α := ℝ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) +
    HMul.hMul (α := ℝ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℝ) =
  HMul.hMul (α := ℝ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℝ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) -
    HMul.hMul (α := ℝ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)
Tactic: simp only [Fin.isValue, Fin.mk_one, val_planeConformalMatrix, neg_neg, of_apply, cons_val',
      empty_val', cons_val_fin_one, cons_val_one, map_apply, Fin.sum_univ_two,
      cons_val_zero, neg_mul, Int.cast_sub, Int.cast_mul, neg_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p
⊢ (↑(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) : ℂ)))
have nonZ1 : HPow.hPow (α := ℂ) (β := ℕ) (↑(p 0) : ℂ) 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑(p 1) : ℂ) 2 ≠ 0
Tactic: have nonZ1 : (p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2 ≠ 0 := mod_cast hp.sq_add_sq_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
h : Eq (α := Fin 2 → ℝ) (Int.cast ∘ p) 0
⊢ p = 0
have h₁ : ∀ (i : Fin 2), p i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
⊢ (↑(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) : ℂ)))
have this : Ne (α := Fin 2 → ℝ) (Int.cast ∘ p) 0
Tactic: have : ((↑) : ℤ → ℝ) ∘ p ≠ 0 := fun h => hp.ne_zero (by ext i; simpa using congr_fun h i)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
⊢ (↑(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) : ℂ)))
have nonZ2 : (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ) ≠ 0
Tactic: have nonZ2 : (p 0 : ℂ) * z + p 1 ≠ 0 := by simpa using linear_ne_zero z this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑(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) : ℂ)))
have 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) : ℂ)))
Tactic: subst hg
Cleared hypotheses: p, hp, hg, nonZ1, this, nonZ2
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 • 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) : ℂ)))
have 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) : ℂ)))
Tactic: rw [coe_specialLinearGroup_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
have 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) : ℂ)
Tactic: convert! nonZ2 using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
⊢ ((↑((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) : ℂ)))
have nonZ2₁ : (↑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
Cleared hypotheses: nonZ2
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
⊢ ((↑((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) : ℂ)))
have 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) :
    ℂ)
Tactic: have H := congr(Int.cast (R := ℂ) $(det_fin_two g))
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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) :
      ℂ)
⊢ ((↑((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) : ℂ)))
have 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) : ℂ)
Tactic: simp at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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) : ℂ)
⊢ ((↑((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) : ℂ)))
have 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) : ℂ))
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ Tendsto (β := ℝ) (fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = p }) ↦ |((↑g : SL(2, ℤ)) • z).re|)
    cofinite atTop
have Tendsto : 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: 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
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ (HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2)⁻¹ ≠ 0
have h : HPow.hPow (α := ℝ) (β := ℕ) (↑(p 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (↑(p 1) : ℝ) 2 ≠ 0
Tactic: apply inv_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ 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 ℝ)
have this : (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