-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X : Type w'
inst_1 : TopologicalSpace X
inst_2 : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq :
  ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π],
    IsQuotientMap (X := (↑(G.obj Z) : Type w)) (Y := (↑(G.obj B) : Type w))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            (G.map π)) :
        (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
Z B : C
π : Z ⟶ B
inst_3 : EffectiveEpi π
inst_4 : HasPullback π π
x :
  (fun (X : Type (max w w')) ↦ X)
    (↑{x : (yonedaPresheaf G X).obj (op Z) |
          Eq (α := (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaPresheaf G X).map (Quiver.Hom.op (pullback.fst π π))) :
                  (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op Z))) →
                    (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
                x :
              (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaPresheaf G X).map (Quiver.Hom.op (pullback.snd π π))) :
                  (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op Z))) →
                    (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
                x :
              (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))} :
      Type (max w w'))
a : ContinuousMap.{w, w'} (↑(G.obj Z) : Type w) X
ha_1 :
  Membership.mem (γ := Set ((yonedaPresheaf G X).obj (op Z)))
    {x : (yonedaPresheaf G X).obj (op Z) |
      Eq (α := (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaPresheaf G X).map (Quiver.Hom.op (pullback.fst π π))) :
              (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op Z))) →
                (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
            x :
          (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaPresheaf G X).map (Quiver.Hom.op (pullback.snd π π))) :
              (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op Z))) →
                (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
            x :
          (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))}
    a
ha :
  Eq (α := (↑(G.obj (pullback π π)) : Type w) → X)
    (Function.comp (β := (↑(G.obj Z) : Type w)) (⇑a : (a : (↑(G.obj Z) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map (pullback.fst π π))) : (a : (↑(G.obj (pullback π π)) : Type w)) → (↑(G.obj Z) : Type w)))
    (Function.comp (β := (↑(G.obj Z) : Type w)) (⇑a : (a : (↑(G.obj Z) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map (pullback.snd π π))) : (a : (↑(G.obj (pullback π π)) : Type w)) → (↑(G.obj Z) : Type w)))
hP :
  {
      toFun :=
        Function.comp (β := (↑(G.obj B) : Type w)) (⇑(⋯.lift a ⋯) : (a : (↑(G.obj B) : Type w)) → X)
          (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)),
      continuous_toFun := ⋯ : ContinuousMap.{w, w'} (↑(G.obj Z) : Type w) X } =
    a
⊢ ∃ (a_1 : ContinuousMap.{w, w'} (↑(G.obj B) : Type w) X),
    {
        toFun :=
          Function.comp (β := (↑(G.obj B) : Type w)) (⇑a_1 : (a : (↑(G.obj B) : Type w)) → X)
            (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)),
        continuous_toFun := ⋯ : ContinuousMap.{w, w'} (↑(G.obj Z) : Type w) X } =
      a

Tactic:
refine ⟨(hq Z B π).lift a (factorsThrough_of_pullbackCondition G X ha), ?_⟩