-- Mathlib/NumberTheory/Modular.lean
theorem tendsto_lcRow0 {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0) (cd 1)) :
    Tendsto (fun g : { g : SL(2, ℤ) // g 1 = cd } => lcRow0 cd ↑(↑g : SL(2, ℝ))) cofinite
      (cocompact ℝ)

Proof state:
case h.e'_3
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m => 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 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
⊢ (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) ⟨g, ⋯⟩ ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = -↑(↑g).det

Tactic:
simp only [Fin.zero_eta, id_eq, Function.comp_apply, lcRow0Extend_apply, cons_val_zero,
  LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLin,
  mulVecLin_apply, mulVec, dotProduct, det_fin_two, f₁]

Result:
case h.e'_3
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m => 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 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
⊢ ∑ x : Fin 2, ↑(planeConformalMatrix (↑(↑g 1 0)) (-↑(↑g 1 1)) ⋯) ⟨1, ⋯⟩ x * (↑g).map Int.cast 0 x =
    -↑(↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0)

Proof state:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m => m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
⊢ Tendsto (mB ∘ fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))

Tactic:
have hf₂ : IsClosedEmbedding (lcRow0Extend hcd) :=
  (lcRow0Extend hcd).toContinuousLinearEquiv.toHomeomorph.isClosedEmbedding

Result:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m => m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
⊢ Tendsto (mB ∘ fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))

Proof state:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]
⊢ Continuous mB

Tactic:
refine continuous_matrix ?_

Result:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]
⊢ ∀ (i j : Fin 2), Continuous fun a => mB a i j

Proof state:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
⊢ Tendsto (mB ∘ fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))

Tactic:
let f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g =>
  Matrix.map (↑g : Matrix _ _ ℤ) ((↑) : ℤ → ℝ)

Result:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => (↑g).map Int.cast
⊢ Tendsto (mB ∘ fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))

Proof state:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]
⊢ ∀ (i j : Fin 2), Continuous fun a => mB a i j

Tactic:
simp only [mB, Fin.forall_fin_two, continuous_const, continuous_id', of_apply, cons_val_zero,
  cons_val_one, and_self_iff]

Result:
no goals

Proof state:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
⊢ Tendsto (fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)

Tactic:
refine Filter.Tendsto.of_tendsto_comp ?_ (comap_cocompact_le hmB)

Result:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
⊢ Tendsto (mB ∘ fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))

Proof state:
case h.e'_3.h.h.mk.a.«0».«0»
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m => 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 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
⊢ (mB ∘ fun g_1 => (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ ((fun i => i) ⟨0, ⋯⟩)
      ((fun i => i) ⟨0, ⋯⟩) =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) ⟨g, ⋯⟩ ((fun i => i) ⟨0, ⋯⟩) ((fun i => 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, id_eq, 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, head_cons, mB, f₁]

Result:
no goals