-- 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.h.h.mk.a
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)
i j : Fin 2
⊢ (mB ∘ fun g_1 => (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ i j =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) ⟨g, ⋯⟩ i j

Tactic:
fin_cases i <;> [fin_cases j; skip]

Result:
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, ⋯⟩)

case h.e'_3.h.h.mk.a.«0».«1»
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) ⟨1, ⋯⟩) =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) ⟨g, ⋯⟩ ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)

case h.e'_3.h.h.mk.a.«1»
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)
j : Fin 2
⊢ (mB ∘ fun g_1 => (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ ((fun i => i) ⟨1, ⋯⟩)
      j =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) ⟨g, ⋯⟩ ((fun i => i) ⟨1, ⋯⟩) 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
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) ℝ))

Tactic:
have cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (fun m : Matrix (Fin 2) (Fin 2) ℤ => Matrix.map m ((↑) : ℤ → ℝ)) cofinite
    (cocompact _) := by
  simpa only [coprodᵢ_cofinite, coprodᵢ_cocompact] using
    Tendsto.pi_map_coprodᵢ fun _ : Fin 2 =>
      Tendsto.pi_map_coprodᵢ fun _ : Fin 2 => Int.tendsto_coe_cofinite

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) ℝ))
⊢ 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
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)
⊢ (mB ∘ fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) =
    ⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a

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

Result:
case h.e'_3.h.h.mk.a
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)
i j : Fin 2
⊢ (mB ∘ fun g_1 => (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ i j =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) ⟨g, ⋯⟩ i j

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)
⊢ -(↑(↑g 1 1) * ↑(↑g 0 0)) + ↑(↑g 1 0) * ↑(↑g 0 1) = ↑(↑g 0 1) * ↑(↑g 1 0) - ↑(↑g 0 0) * ↑(↑g 1 1)

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_3.h.h.mk.a.«1»
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)
j : Fin 2
⊢ (mB ∘ fun g_1 => (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ ((fun i => i) ⟨1, ⋯⟩)
      j =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a) ⟨g, ⋯⟩ ((fun i => i) ⟨1, ⋯⟩) j

Tactic:
rfl

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
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => (↑g).map Int.cast
⊢ Tendsto (fun m => m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))

Tactic:
simpa only [coprodᵢ_cofinite, coprodᵢ_cocompact] using
  Tendsto.pi_map_coprodᵢ fun _ : Fin 2 =>
    Tendsto.pi_map_coprodᵢ fun _ : Fin 2 => Int.tendsto_coe_cofinite

Result:
no goals

Proof state:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ Tendsto (fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)

Tactic:
let mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, (-(1 : ℤ) : ℝ)], (↑) ∘ cd]

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