-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X_1 : Type w'
inst_1 : TopologicalSpace X_1
P : TopCat.{u} → Prop
X : TopCat
inst_2 : CompHausLike.HasExplicitFiniteCoproducts P
inst_3 : CompHausLike.HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
X_2 Y : TopCat
f : X_2 ⟶ Y
⊢ ∀ ⦃X Y_1 : (CompHausLike P)ᵒᵖ⦄ (f_1 : X ⟶ Y_1),
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
              (TopCat.toSheafCompHausLike.{w, u} P X_2 hs :
                have this := ⋯;
                Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))).map
          f_1 ≫
        (fun (x : (CompHausLike P)ᵒᵖ) ↦
            (↾fun
                  (g :
                    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
                          (TopCat.toSheafCompHausLike.{w, u} P X_2 hs :
                            have this := ⋯;
                            Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))).obj
                      x) ↦
                (TopCat.Hom.hom f).comp g :
              (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
                      (TopCat.toSheafCompHausLike.{w, u} P X_2 hs :
                        have this := ⋯;
                        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))).obj
                  x ⟶
                (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
                      (TopCat.toSheafCompHausLike.{w, u} P Y hs :
                        have this := ⋯;
                        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))).obj
                  x))
          Y_1 =
      (fun (x : (CompHausLike P)ᵒᵖ) ↦
            (↾fun
                  (g :
                    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
                          (TopCat.toSheafCompHausLike.{w, u} P X_2 hs :
                            have this := ⋯;
                            Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))).obj
                      x) ↦
                (TopCat.Hom.hom f).comp g :
              (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
                      (TopCat.toSheafCompHausLike.{w, u} P X_2 hs :
                        have this := ⋯;
                        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))).obj
                  x ⟶
                (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
                      (TopCat.toSheafCompHausLike.{w, u} P Y hs :
                        have this := ⋯;
                        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))).obj
                  x))
          X ≫
        (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
              (TopCat.toSheafCompHausLike.{w, u} P Y hs :
                have this := ⋯;
                Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))).map
          f_1

Tactic:
aesop