-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst_1 : Epi f
S : LightProfinite
p : Functor.obj (LightCondensed.free R) S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite.{u})
    (y :
      (Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
        (Opposite.op S)),
    ∃ (S' : LightProfinite.{u}) (φ : S' ⟶ S) (_ :
      Function.Surjective (α :=
        (fun
              (X :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u))
          S')
        (β :=
        (fun
              (X :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u))
          S)
        (⇑(ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  CompHausLike fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                  Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                  Type u)))
              (CC :=
              fun
                (X :
                  CompHausLike fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u))
              φ) :
          (a :
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                  (↑X.toTop : Type u))
                S') →
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                (↑X.toTop : Type u))
              S))
      (x :
      (Functor.obj (LightCondensed.forget R) X).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
        (Opposite.op S')),
      Eq (α :=
        (fun (X : Type u) ↦ X)
          ((Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
            (Opposite.op S')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (LightCondensed.forget R) f))
                  (Opposite.op S')) :
              (a : (fun (X : Type u) ↦ X) (((LightCondensed.forget R).obj X).obj.obj (Opposite.op S'))) →
                (fun (X : Type u) ↦ X) (((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S')))
            x :
          (fun (X : Type u) ↦ X)
            ((Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
              (Opposite.op S')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((Functor.obj (LightCondensed.forget R) Y).obj (P :=
                      Presheaf.IsSheaf (coherentTopology LightProfinite)).map
                  (Opposite.op φ)) :
              (a : (fun (X : Type u) ↦ X) (((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S))) →
                (fun (X : Type u) ↦ X) (((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S')))
            y :
          (fun (X : Type u) ↦ X)
            ((Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
              (Opposite.op S')))
T : LightProfinite
π : T ⟶ S
hπ :
  Function.Surjective (α :=
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u))
      T)
    (β :=
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u))
      S)
    (⇑(ConcreteCategory.hom (FC :=
          fun
            (x1 x2 :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u)))
          (CC :=
          fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
          π) :
      (a :
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
              (↑X.toTop : Type u))
            T) →
        (fun
              (X :
                CompHausLike fun (X : TopCat) ↦
                  TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
            (↑X.toTop : Type u))
          S)
x :
  (Functor.obj (LightCondensed.forget R) X).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
    (Opposite.op T)
hx :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      ((Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
        (Opposite.op T)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (LightCondensed.forget R) f))
              (Opposite.op T)) :
          (a : (fun (X : Type u) ↦ X) (((LightCondensed.forget R).obj X).obj.obj (Opposite.op T))) →
            (fun (X : Type u) ↦ X) (((LightCondensed.forget R).obj Y).obj.obj (Opposite.op T)))
        x :
      (fun (X : Type u) ↦ X)
        ((Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
          (Opposite.op T)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
              (Opposite.op π)) :
          (a : (fun (X : Type u) ↦ X) (((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S))) →
            (fun (X : Type u) ↦ X) (((LightCondensed.forget R).obj Y).obj.obj (Opposite.op T)))
        ((GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite) :
              (a : (coherentTopology LightProfinite).yoneda.obj S ⟶ (LightCondensed.forget R).obj Y) →
                ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S))
            ((Adjunction.homEquiv (LightCondensed.freeForgetAdjunction R) S.toCondensed Y :
                (a : (LightCondensed.free R).obj S.toCondensed ⟶ Y) → S.toCondensed ⟶ (LightCondensed.forget R).obj Y)
              p) :
          (Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
            (Opposite.op S)) :
      (fun (X : Type u) ↦ X)
        ((Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
          (Opposite.op T)))
rw :
  Eq (α :=
    (lightProfiniteToLightCondSet.obj T).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)) ⟶
      (Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)))
    (InducedCategory.Hom.hom
      (lightProfiniteToLightCondSet.map π ≫
        (Adjunction.homEquiv (LightCondensed.freeForgetAdjunction R) (lightProfiniteToLightCondSet.obj S) Y :
            (a : (LightCondensed.free R).obj (lightProfiniteToLightCondSet.obj S) ⟶ Y) →
              lightProfiniteToLightCondSet.obj S ⟶ (LightCondensed.forget R).obj Y)
          p))
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        Functor.obj (GrothendieckTopology.yoneda (coherentTopology LightProfinite)) (Opposite.unop (Opposite.op S)))
        ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite)) :
            (a :
                ((coherentTopology LightProfinite).yoneda.obj (Opposite.unop (Opposite.op S))).obj.obj
                  (Opposite.op T)) →
              (coherentTopology LightProfinite).yoneda.obj T ⟶
                (coherentTopology LightProfinite).yoneda.obj (Opposite.unop (Opposite.op S)))
          (Quiver.Hom.unop (Opposite.op π)))
        ((Adjunction.homEquiv (LightCondensed.freeForgetAdjunction R) S.toCondensed Y :
            (a : (LightCondensed.free R).obj S.toCondensed ⟶ Y) → S.toCondensed ⟶ (LightCondensed.forget R).obj Y)
          p)))
⊢ Eq (α := Functor.obj (lightProfiniteToLightCondSet ⋙ LightCondensed.free R) T ⟶ Y)
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ LightCondensed.free R) π ≫ p)
    ((Equiv.symm (Adjunction.homEquiv (LightCondensed.freeForgetAdjunction R) T.toCondensed X) :
          (a : T.toCondensed ⟶ (LightCondensed.forget R).obj X) → (LightCondensed.free R).obj T.toCondensed ⟶ X)
        ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology LightProfinite)) :
            (a : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)) →
              (coherentTopology LightProfinite).yoneda.obj T ⟶ (LightCondensed.forget R).obj X)
          x) ≫
      f)

Tactic:
rw [Functor.comp_map, ← Adjunction.homEquiv_naturality_left_square_iff
    (LightCondensed.freeForgetAdjunction R), Sheaf.hom_ext_iff, Equiv.apply_symm_apply,
    GrothendieckTopology.yonedaEquiv_symm_naturality_right, hx,
    GrothendieckTopology.map_yonedaEquiv', ← GrothendieckTopology.yonedaEquiv_symm_naturality_right]

Premises used: Equiv.apply_symm_apply, LightCondensed.freeForgetAdjunction, CategoryTheory.GrothendieckTopology.map_yonedaEquiv', CategoryTheory.Adjunction.homEquiv_naturality_left_square_iff, CategoryTheory.Sheaf.hom_ext_iff, CategoryTheory.Functor.comp_map, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right