English
Glueing data of a presheaf on discrete types to obtain sections on general α.
Русский
Соединение данных presheaf по дискретным типам для получения секций на произвольном α.
LaTeX
$$$ typesGlue(S,hs,α,f) = \\mathrm{amalgamate}\\;...$$$
Lean4
theorem typesGlue_eval {S hs α} (s) : typesGlue.{u} S hs α (eval S α s) = s :=
by
apply (hs.isSheafFor _ _ (generate_discretePresieve_mem α)).isSeparatedFor.ext
intro β f hf
apply (IsSheafFor.valid_glue _ _ _ hf).trans
apply (FunctorToTypes.map_comp_apply _ _ _ _).symm.trans
rw [← op_comp]
--congr 2 -- Porting note: This tactic didn't work. Find an alternative.
suffices ((↾fun _ ↦ PUnit.unit) ≫ ↾fun _ ↦ f (Classical.choose hf)) = f by rw [this]
funext x
exact congr_arg f (Classical.choose_spec hf x).symm
