-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ ∀ (G : ℕᵒᵖ ⥤ LightProfinite),
    (∀ (n : ℕ),
        Function.Surjective (α :=
          (↑((G.obj (Opposite.op n.succ)).toTop (P := fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
            Type u_1))
          (β :=
          (↑((G.obj (Opposite.op n)).toTop (P := fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
            Type u_1))
          (⇑(ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    CompHausLike fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦
                        TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧
                          SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                    Type u_1),
                  (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦
                        TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧
                          SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                    Type u_1)))
                (CC :=
                fun
                  (X :
                    CompHausLike fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                  Type u_1))
                (G.map (homOfLE ⋯).op)) :
            (a : (↑(G.obj (Opposite.op n.succ)).toTop : Type u_1)) → (↑(G.obj (Opposite.op n)).toTop : Type u_1))) →
      Function.Surjective (α :=
        (↑((limit G).toTop (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
          Type u_1))
        (β :=
        (↑((G.obj (Opposite.op 0)).toTop (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
          Type u_1))
        (⇑(ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  CompHausLike fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                  Type u_1),
                (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                  Type u_1)))
              (CC :=
              fun
                (X :
                  CompHausLike fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                Type u_1))
              (X := limit G) (Y := G.obj (Opposite.op 0)) (limit.π G (Opposite.op 0))) :
          (a : (↑(limit G).toTop : Type u_1)) → (↑(G.obj (Opposite.op 0)).toTop : Type u_1))

Tactic:
exact fun x h ↦ Concrete.surjective_π_app_zero_of_surjective_map (limit.isLimit x) h

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.Concrete.surjective_π_app_zero_of_surjective_map