-- 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.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

Tactic:
obtain ⟨y, hy⟩ := (hq Z B π).surjective x

Result:
case hP.refine_1.h.intro
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)))
y : ↑(G.obj Z)
hy : (ConcreteCategory.hom (G.map π)) y = x
⊢ a x = b x

Proof state:
case hP.refine_1.h.intro
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)))
y : ↑(G.obj Z)
hy : (ConcreteCategory.hom (G.map π)) y = x
⊢ a x = b x

Tactic:
rw [← hy]

Result:
case hP.refine_1.h.intro
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)))
y : ↑(G.obj Z)
hy : (ConcreteCategory.hom (G.map π)) y = x
⊢ a ((ConcreteCategory.hom (G.map π)) y) = b ((ConcreteCategory.hom (G.map π)) y)

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}
ha : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(TopCat.Hom.hom (G.map (pullback.snd π π)))
⊢ ∃ a_1, { toFun := ⇑a_1 ∘ ⇑(TopCat.Hom.hom (G.map π)), continuous_toFun := ⋯ } = a

Tactic:
simp only [yonedaPresheaf, unop_op] at a

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 : C(↑(G.obj Z), X)
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, { toFun := ⇑a_1 ∘ ⇑(TopCat.Hom.hom (G.map π)), continuous_toFun := ⋯ } = a

Proof state:
case hP.refine_1.h.intro
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)))
y : ↑(G.obj Z)
hy : (ConcreteCategory.hom (G.map π)) y = x
⊢ a ((ConcreteCategory.hom (G.map π)) y) = b ((ConcreteCategory.hom (G.map π)) y)

Tactic:
exact congr_fun h y

Result:
no goals

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 π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ Function.Bijective (MapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)

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

Result:
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 :
  MapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯ a =
    MapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯ b
⊢ a = b

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⟩