awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
hmB : Continuous mB
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) ℝ))
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) ℝ)
⊢ Tendsto (α := { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }) (β := Matrix (Fin 2) (Fin 2) ℝ)
    ((⇑(lcRow0Extend hcd) : (a : Matrix (Fin 2) (Fin 2) ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ∘
      f₁ ∘ fun (a : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }) ↦ (↑a : SL(2, ℤ)))
    cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))

Tactic:
hf₂.tendsto_cocompact.comp (hf₁.comp Subtype.coe_injective.tendsto_cofinite)

Premises used: Subtype.coe_injective, Topology.IsClosedEmbedding.tendsto_cocompact, Function.Injective.tendsto_cofinite, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
hmB : Continuous mB
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) ℝ))
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) ℝ)
h :
  Eq (α := { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd } → Matrix (Fin 2) (Fin 2) ℝ)
    (mB ∘ fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }) ↦
      (lcRow0 cd : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
        (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (↑g : SL(2, ℤ))) :
          Matrix (Fin 2) (Fin 2) ℝ))
    ((⇑(lcRow0Extend hcd) : (a : Matrix (Fin 2) (Fin 2) ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ∘
      f₁ ∘ fun (a : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }) ↦ (↑a : SL(2, ℤ)))
⊢ Tendsto (α := { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd })
    (mB ∘ fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }) ↦
      (lcRow0 cd : (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 (Matrix (Fin 2) (Fin 2) ℝ))

Tactic:
convert! hf₂.tendsto_cocompact.comp (hf₁.comp Subtype.coe_injective.tendsto_cofinite) using 1

Premises used: Subtype.coe_injective, Topology.IsClosedEmbedding.tendsto_cocompact, Function.Injective.tendsto_cofinite, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
hmB : Continuous mB
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) ℝ))
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) ℝ)
h :
  ∀ (g : SL(2, ℤ)) (hcd : IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1)),
    let 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) ℝ))
      (i j : Fin 2),
      (mB ∘ fun (g_1 : { g_1 : SL(2, ℤ) // (↑g_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 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_1 : SL(2, ℤ))) :
                Matrix (Fin 2) (Fin 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 ⋯)
          i j =
        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 ⋯)
          i j
⊢ Eq (α := { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd } → Matrix (Fin 2) (Fin 2) ℝ)
    (mB ∘ fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }) ↦
      (lcRow0 cd : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
        (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (↑g : SL(2, ℤ))) :
          Matrix (Fin 2) (Fin 2) ℝ))
    ((⇑(lcRow0Extend hcd) : (a : Matrix (Fin 2) (Fin 2) ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ∘
      f₁ ∘ fun (a : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }) ↦ (↑a : SL(2, ℤ)))

Tactic:
ext ⟨g, rfl⟩ i j : 3

Premises used: rfl
-- Module: Mathlib.NumberTheory.Modular
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) ℝ)
⊢ (mB ∘ fun (g_1 : { g_1 : SL(2, ℤ) // (↑g_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 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_1 : SL(2, ℤ))) :
            Matrix (Fin 2) (Fin 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, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    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) ⟨0, ⋯⟩)

Tactic:
simp only [Fin.isValue, Int.cast_one, map_apply_coe, RingHom.mapMatrix_apply,
      Int.coe_castRingHom, lcRow0_apply, map_apply, Fin.zero_eta, Function.comp_apply,
      of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one, lcRow0Extend_apply,
      LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLin,
      val_planeConformalMatrix, neg_neg, mulVecLin_apply, mulVec, dotProduct, Fin.sum_univ_two,
      cons_val_one, mB, f₁]

Premises used: RingHom.mapMatrix_apply, Matrix.mulVecLin_apply, Matrix.GeneralLinearGroup.coe_toLin, dotProduct, Int.coe_castRingHom, Matrix.cons_val_one, Matrix.SpecialLinearGroup.map_apply_coe, Matrix.cons_val_zero, Matrix.map_apply, ModularGroup.lcRow0Extend_apply, Matrix.empty_val', neg_neg, Matrix.cons_val_fin_one, Matrix.of_apply, Matrix.val_planeConformalMatrix, Fin.zero_eta, Fin.isValue, Function.comp_apply, ModularGroup.lcRow0_apply, Fin.sum_univ_two, Matrix.mulVec, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, Int.cast_one, Matrix.cons_val'
-- Module: Mathlib.NumberTheory.Modular
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 (α := ℝ) ((fun (n : ℤ) ↦ (-(↑n : ℝ) : ℝ)) 1) ((fun (n : ℤ) ↦ (-(↑n : ℝ) : ℝ)) (↑g : Matrix (Fin 2) (Fin 2) ℤ).det)

Tactic:
congr_arg (fun n : ℤ => (-n : ℝ)) g.det_coe.symm

Premises used: Int.cast, Matrix.SpecialLinearGroup.det_coe, congr_arg, Eq.symm, Neg.neg
-- Module: Mathlib.NumberTheory.Modular
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) ℝ)
h :
  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 : ℝ))
⊢ (mB ∘ fun (g_1 : { g_1 : SL(2, ℤ) // (↑g_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 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_1 : SL(2, ℤ))) :
            Matrix (Fin 2) (Fin 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, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    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, ⋯⟩)

Tactic:
convert! congr_arg (fun n : ℤ => (-n : ℝ)) g.det_coe.symm using 1

Premises used: Int.cast, Matrix.SpecialLinearGroup.det_coe, congr_arg, Eq.symm, Neg.neg
-- Module: Mathlib.NumberTheory.Modular
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) ℝ)
h :
  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) :
        ℝ))
⊢ 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 : ℝ))

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₁]

Premises used: Matrix.mulVecLin_apply, Matrix.GeneralLinearGroup.coe_toLin, dotProduct, Matrix.cons_val_zero, ModularGroup.lcRow0Extend_apply, Fin.zero_eta, Function.comp_apply, Matrix.det_fin_two, Matrix.mulVec, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv
-- Module: Mathlib.NumberTheory.Modular
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) ℝ)
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) : ℝ)
⊢ 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) :
        ℝ))

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]

Premises used: Fin.mk_one, neg_sub, Int.cast_sub, Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.map_apply, Matrix.empty_val', neg_neg, Matrix.cons_val_fin_one, Matrix.of_apply, Matrix.val_planeConformalMatrix, Int.cast_mul, Fin.isValue, neg_mul, Fin.sum_univ_two, Matrix.cons_val'
-- Module: Mathlib.NumberTheory.Modular
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) ℝ)
⊢ -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:
ring
-- Module: Mathlib.NumberTheory.Modular
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) ℝ)
j : Fin 2
⊢ (mB ∘ fun (g_1 : { g_1 : SL(2, ℤ) // (↑g_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 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_1 : SL(2, ℤ))) :
            Matrix (Fin 2) (Fin 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) (⟨1, ⋯⟩ : Fin 2)) j =
    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) ⟨1, ⋯⟩) j

Tactic:
rfl
-- 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
⊢ 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
-- 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
h : Eq (α := Fin 2 → ℝ) (Int.cast ∘ p) 0
h₁ : ∀ (i : Fin 2), p i = 0 i
⊢ p = 0

Tactic:
ext i
-- 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
h : Eq (α := Fin 2 → ℝ) (Int.cast ∘ p) 0
i : Fin 2
⊢ p i = 0 i

Tactic:
simpa using congr_fun h i

Premises used: congr_fun
-- 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
⊢ 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)
-- 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
⊢ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ) ≠ 0

Tactic:
simpa using linear_ne_zero z this

Premises used: UpperHalfPlane.linear_ne_zero
-- 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
⊢ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ) ≠ 0

Tactic:
have nonZ2 : (p 0 : ℂ) * z + p 1 ≠ 0 := by simpa using linear_ne_zero z this