-- Mathlib/Condensed/TopComparison.lean
theorem factorsThrough_of_pullbackCondition {Z B : C} {π : Z ⟶ B} [HasPullback π π]
    [PreservesLimit (cospan π π) G]
    {a : C(G.obj Z, X)}
    (ha : a ∘ (G.map (pullback.fst _ _)) = a ∘ (G.map (pullback.snd π π))) :
    Function.FactorsThrough a (G.map π)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
⊢ a x = a y

Tactic:
let xy : G.obj (pullback π π) := (PreservesPullback.iso G π π).inv <|
  (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv ⟨(x, y), hxy⟩

Result:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)
⊢ a x = a y

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)
ha' :
  a ((ConcreteCategory.hom (G.map (pullback.fst π π))) xy) = a ((ConcreteCategory.hom (G.map (pullback.snd π π))) xy)
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
⊢ ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.snd (G.map π) (G.map π))) y

Tactic:
simp only [← PreservesPullback.iso_inv_snd]

Result:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)
ha' :
  a ((ConcreteCategory.hom (G.map (pullback.fst π π))) xy) = a ((ConcreteCategory.hom (G.map (pullback.snd π π))) xy)
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
⊢ ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom ((PreservesPullback.iso G π π).inv ≫ G.map (pullback.snd π π))) y

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)
ha' :
  a ((ConcreteCategory.hom (G.map (pullback.fst π π))) xy) = a ((ConcreteCategory.hom (G.map (pullback.snd π π))) xy)
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
⊢ a x = a y

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

Result:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)
ha' :
  a ((ConcreteCategory.hom (G.map (pullback.fst π π))) xy) = a ((ConcreteCategory.hom (G.map (pullback.snd π π))) xy)
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
h₂ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.snd (G.map π) (G.map π))) y
⊢ a x = a y

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)
ha' : a (↑⟨(x, y), hxy⟩).1 = a (↑⟨(x, y), hxy⟩).2
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
h₂ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.snd (G.map π) (G.map π))) y
⊢ a x = a y

Tactic:
simpa using ha'

Result:
no goals