-- 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_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✝⟩

Tactic:
simp only [yonedaPresheaf, comp, unop_op, Quiver.Hom.unop_op, Set.coe_setOf,
  MapToEqualizer, Set.mem_setOf_eq, Subtype.mk.injEq]

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

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

Tactic:
refine ⟨(hq Z B π).lift a (factorsThrough_of_pullbackCondition G X 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 : 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 π π)))
⊢ { toFun := ⇑(⋯.lift a ⋯) ∘ ⇑(TopCat.Hom.hom (G.map π)), continuous_toFun := ⋯ } = a

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

Tactic:
simp only [yonedaPresheaf, unop_op, Quiver.Hom.unop_op, Set.coe_setOf, MapToEqualizer,
  Set.mem_setOf_eq, Subtype.mk.injEq, comp, ContinuousMap.mk.injEq] at h

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 : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map π)) = ⇑b ∘ ⇑(TopCat.Hom.hom (G.map π))
⊢ a = b

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

Tactic:
congr

Result:
case hP.refine_2.e_toFun
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 π π)))
⊢ ⇑(⋯.lift a ⋯) ∘ ⇑(TopCat.Hom.hom (G.map π)) = a.toFun

Proof state:
case hP.refine_2.e_toFun
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 π π)))
⊢ ⇑(⋯.lift a ⋯) ∘ ⇑(TopCat.Hom.hom (G.map π)) = a.toFun

Tactic:
exact DFunLike.ext'_iff.mp ((hq Z B π).lift_comp a (factorsThrough_of_pullbackCondition G X ha))

Result:
no goals