-- 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
Z B : C
π : Z ⟶ B
inst_2 : HasPullback π π
inst_3 : PreservesLimit (cospan π π) G
a : ContinuousMap.{w, w'} (↑(G.obj Z) : Type w) X
ha :
  Eq (α := (↑(G.obj (pullback π π)) : Type w) → X)
    (Function.comp (β := (↑(G.obj Z) : Type w)) (⇑a : (a : (↑(G.obj Z) : Type w)) → X)
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            (X := G.obj (pullback π π)) (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)
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            (X := G.obj (pullback π π)) (G.map (pullback.snd π π))) :
        (a : (↑(G.obj (pullback π π)) : Type w)) → (↑(G.obj Z) : Type w)))
x y : (↑(G.obj Z) : Type w)
hxy :
  Eq (α := (↑(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))
        x :
      (↑(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))
        y :
      (↑(G.obj B) : Type w))
xy : (↑(G.obj (pullback π π)) : Type w) :=
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) (X :=
        pullback (G.map π) (G.map π)) (Y := G.obj (pullback π π)) (Iso.inv (PreservesPullback.iso G π π)) :
      (a : (↑(pullback (G.map π) (G.map π)) : Type w)) → (↑(G.obj (pullback π π)) : Type w))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv :
          (a :
              (↑(TopCat.of
                    { p : (↑(G.obj Z) : Type w) × (↑(G.obj Z) : Type w) //
                      (ConcreteCategory.hom (G.map π) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)) p.1 =
                        (ConcreteCategory.hom (G.map π) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)) p.2 }) :
                Type w)) →
            (↑(pullback (G.map π) (G.map π)) : Type w))
        (Subtype.mk (p := fun (p : (↑(G.obj Z) : Type w) × (↑(G.obj Z) : Type w)) ↦
          Eq (α := (↑(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))
                p.1 :
              (↑(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))
                p.2 :
              (↑(G.obj B) : Type w)))
          (x, y) hxy) :
      (↑(pullback (G.map π) (G.map π)) : Type w))
ha' :
  Eq.{w' + 1} (α := X)
    ((a : (a : (↑(G.obj Z) : Type w)) → X)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                (X := G.obj (pullback π π)) (G.map (pullback.fst π π)) :
              (a : (↑(G.obj (pullback π π)) : Type w)) → (↑(G.obj Z) : Type w))
            xy :
          (↑(G.obj Z) : Type w)) :
      X)
    ((a : (a : (↑(G.obj Z) : Type w)) → X)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                (X := G.obj (pullback π π)) (G.map (pullback.snd π π)) :
              (a : (↑(G.obj (pullback π π)) : Type w)) → (↑(G.obj Z) : Type w))
            xy :
          (↑(G.obj Z) : Type w)) :
      X)
⊢ ∀ (y : (↑(pullback (G.map π) (G.map π)) : Type w)),
    Eq (α := (↑(G.obj Z) : Type w))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
              (X := G.obj (pullback π π)) (G.map (pullback.fst π π)) :
            (a : (↑(G.obj (pullback π π)) : Type w)) → (↑(G.obj Z) : Type w))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                  (X := pullback (G.map π) (G.map π)) (Y := G.obj (pullback π π))
                  (Iso.inv (PreservesPullback.iso G π π)) :
                (a : (↑(pullback (G.map π) (G.map π)) : Type w)) → (↑(G.obj (pullback π π)) : Type w))
              y :
            (↑(G.obj (pullback π π)) : Type w)) :
        (↑(G.obj Z) : Type w))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
              (X := pullback (G.map π) (G.map π)) (pullback.fst (G.map π) (G.map π)) :
            (a : (↑(pullback (G.map π) (G.map π)) : Type w)) → (↑(G.obj Z) : Type w))
          y :
        (↑(G.obj Z) : Type w))

Tactic:
have h₁ : ∀ y, G.map (pullback.fst _ _) ((PreservesPullback.iso G π π).inv y) =
      pullback.fst (G.map π) (G.map π) y := by
    simp only [← PreservesPullback.iso_inv_fst]; intro y; rfl