no goals
α β : Type u
S : Sieve β
hs : S ∈ GrothendieckTopology.sieves typesGrothendieckTopology β
x : FamilyOfElements (yoneda.obj α) S.arrows
hx : FamilyOfElements.Compatible x
γ : Type u
f : γ ⟶ β
h : S.arrows f
z : γ.op.unop
⊢ (yoneda.obj α).map f.op (fun y => x (fun x => y) (_ : S.arrows fun x => y) PUnit.unit) z = x f h z
convert congr_fun (hx (𝟙 _) (fun _ => z) (hs <| f z) h rfl) PUnit.unit using 1
no goals
α β : Type u
S : Sieve β
hs : S ∈ GrothendieckTopology.sieves typesGrothendieckTopology β
x : FamilyOfElements (yoneda.obj α) S.arrows
hx : FamilyOfElements.Compatible x
f : (yoneda.obj α).obj β.op
hf : (fun t => FamilyOfElements.IsAmalgamation x t) f
y : β.op.unop
⊢ f y = x (fun x => y) (_ : S.arrows fun x => y) PUnit.unit
convert congr_fun (hf _ (hs y)) PUnit.unit