-- Mathlib/Condensed/TopComparison.lean
theorem equalizerCondition_yonedaPresheaf
    [∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G]
    (hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap (G.map π)) :
      EqualizerCondition (yonedaPresheaf G X)

Proof state:
case hP
C : Type u
inst✝² : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝¹ : TopologicalSpace X
inst✝ : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
⊢ ∀ (X_1 B : C) (π : X_1 ⟶ B) [inst : EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective (MapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)

Tactic:
intro Z B π _ _

Result:
case hP
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ Function.Bijective (MapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)

Proof state:
case hP.refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
a b : (yonedaPresheaf G X).obj (op B)
h : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map π)) = ⇑b ∘ ⇑(TopCat.Hom.hom (G.map π))
⊢ a = b

Tactic:
ext x

Result:
case hP.refine_1.h
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
a b : (yonedaPresheaf G X).obj (op B)
h : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map π)) = ⇑b ∘ ⇑(TopCat.Hom.hom (G.map π))
x : ↑(G.obj (unop (op B)))
⊢ a x = b x

Proof state:
case hP.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
x✝ : ↑{x | (yonedaPresheaf G X).map (pullback.fst π π).op x = (yonedaPresheaf G X).map (pullback.snd π π).op x}
a : (yonedaPresheaf G X).obj (op Z)
ha : a ∈ {x | (yonedaPresheaf G X).map (pullback.fst π π).op x = (yonedaPresheaf G X).map (pullback.snd π π).op x}
⊢ ∃ a_1, MapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯ a_1 = ⟨a, ha⟩

Tactic:
simp only [yonedaPresheaf, comp, unop_op, Quiver.Hom.unop_op, Set.mem_setOf_eq,
  ContinuousMap.mk.injEq] at ha

Result:
case hP.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
x✝ : ↑{x | (yonedaPresheaf G X).map (pullback.fst π π).op x = (yonedaPresheaf G X).map (pullback.snd π π).op x}
a : (yonedaPresheaf G X).obj (op Z)
ha✝ : a ∈ {x | (yonedaPresheaf G X).map (pullback.fst π π).op x = (yonedaPresheaf G X).map (pullback.snd π π).op x}
ha : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(TopCat.Hom.hom (G.map (pullback.snd π π)))
⊢ ∃ a_1, MapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯ a_1 = ⟨a, ha✝⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝¹ : TopologicalSpace X
inst✝ : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
⊢ EqualizerCondition (yonedaPresheaf G X)

Tactic:
apply EqualizerCondition.mk

Result:
case hP
C : Type u
inst✝² : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝¹ : TopologicalSpace X
inst✝ : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
⊢ ∀ (X_1 B : C) (π : X_1 ⟶ B) [inst : EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective (MapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)