-- 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 π π
hP :
  ∀ (a b : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B)))
    (h :
      Eq (α :=
        (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')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯) :
              (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))) →
                (fun (X : Type (max w w')) ↦ X)
                  (↑{x : (yonedaPresheaf G X).obj (op Z) |
                        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op) :
                              (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 =
                          (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op) :
                              (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} :
                    Type (max w w')))
            a :
          (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')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯) :
              (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))) →
                (fun (X : Type (max w w')) ↦ X)
                  (↑{x : (yonedaPresheaf G X).obj (op Z) |
                        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op) :
                              (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 =
                          (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op) :
                              (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} :
                    Type (max w w')))
            b :
          (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 = b
hP₁ :
  ∀
    (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 : (yonedaPresheaf G X).obj (op Z))
    (ha :
      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),
    ∃ (a_1 : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))),
      (ConcreteCategory.hom (FC := TypeCat.Fun)
              (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯) :
            (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))) →
              (fun (X : Type (max w w')) ↦ X)
                (↑{x : (yonedaPresheaf G X).obj (op Z) |
                      (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op) :
                            (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 =
                        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op) :
                            (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} :
                  Type (max w w')))
          a_1 =
        Subtype.mk (p := fun (x : (yonedaPresheaf G X).obj (op Z)) ↦
          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 π π))))}
            x)
          a ha
⊢ Function.Bijective (α := (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))) (β :=
    (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')))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) :
      (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))) →
        (fun (X : Type (max w w')) ↦ X)
          (↑{x : (yonedaPresheaf G X).obj (op Z) |
                (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op) :
                      (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 =
                  (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op) :
                      (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} :
            Type (max w w')))

Tactic:
refine ⟨fun a b h ↦ ?_, fun ⟨a, ha⟩ ↦ ?_⟩