-- 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) ℝ)
i j : Fin 2
h :
  (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)) 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) ⟨0, ⋯⟩) j
⊢ (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
have h₁ : (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
      sorry)
    ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : 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
      sorry)
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i