no goals
C : Type u
inst✝ : Category C
X : TopCat
F✝ : Presheaf C X
ι : Type v
U✝ : ι → Opens ↑X
F : Presheaf (Discrete Unit) X
x✝² : Discrete Unit
U : Opens ↑X
S : Sieve U
x✝¹ : S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : Presieve.FamilyOfElements (F ⋙ coyoneda.obj x✝².op) S.arrows
x✝ : Presieve.FamilyOfElements.Compatible x
⊢ (fun t => Presieve.FamilyOfElements.IsAmalgamation x t) (eqToHom (_ : x✝².op.unop = F.obj U.op))
aesop_cat
no goals
C : Type u
inst✝ : Category C
X : TopCat
F✝ : Presheaf C X
ι : Type v
U✝ : ι → Opens ↑X
F : Presheaf (Discrete Unit) X
x✝³ : Discrete Unit
U : Opens ↑X
S : Sieve U
x✝² : S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : Presieve.FamilyOfElements (F ⋙ coyoneda.obj x✝³.op) S.arrows
x✝¹ : Presieve.FamilyOfElements.Compatible x
x✝ : (F ⋙ coyoneda.obj x✝³.op).obj U.op
⊢ (fun t => Presieve.FamilyOfElements.IsAmalgamation x t) x✝ → x✝ = eqToHom (_ : x✝³.op.unop = F.obj U.op)
aesop_cat