⊢ typesGrothendieckTopology ∈ Sheaf.finestTopologySingle '' Set.range yoneda.toPrefunctor.obj
⊢ typesGrothendieckTopology = Sheaf.canonicalTopology (Type u)
refine' le_antisymm subcanonical_typesGrothendieckTopology (sInf_le _)
⊢ (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))).sieves = typesGrothendieckTopology.sieves
⊢ typesGrothendieckTopology ∈ Sheaf.finestTopologySingle '' Set.range yoneda.toPrefunctor.obj
refine' ⟨yoneda.obj (ULift Bool), ⟨_, rfl⟩, GrothendieckTopology.ext _⟩
case h
α : Type u
⊢ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α =
    GrothendieckTopology.sieves typesGrothendieckTopology α
⊢ (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))).sieves = typesGrothendieckTopology.sieves
funext α
case h.h
α : Type u
S : Sieve α
⊢ S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α ↔
    S ∈ GrothendieckTopology.sieves typesGrothendieckTopology α
case h
α : Type u
⊢ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α =
    GrothendieckTopology.sieves typesGrothendieckTopology α
ext S
case h.h
α : Type u
S : Sieve α
hs : S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α
x : α
⊢ S.arrows fun x_1 => x
case h.h
α : Type u
S : Sieve α
⊢ S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α ↔
    S ∈ GrothendieckTopology.sieves typesGrothendieckTopology α
refine' ⟨fun hs x => _, fun hs β f => isSheaf_yoneda' _ fun y => hs _⟩
case h.h
α : Type u
S : Sieve α
hs : S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α
x : α
hsx : ¬S.arrows fun x_1 => x
⊢ False
case h.h
α : Type u
S : Sieve α
hs : S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α
x : α
⊢ S.arrows fun x_1 => x
by_contra hsx
case h.h
α : Type u
S : Sieve α
hs : S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α
x : α
hsx : ¬S.arrows fun x_1 => x
this : (fun x => { down := true }) = fun x => { down := false }
⊢ False
case h.h
α : Type u
S : Sieve α
hs : S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α
x : α
hsx : ¬S.arrows fun x_1 => x
⊢ False
have : (fun _ => ULift.up true) = fun _ => ULift.up false :=
  (hs PUnit fun _ => x).isSeparatedFor.ext
    fun β f hf => funext fun y => hsx.elim <| S.2 hf fun _ => y
no goals
case h.h
α : Type u
S : Sieve α
hs : S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α
x : α
hsx : ¬S.arrows fun x_1 => x
this : (fun x => { down := true }) = fun x => { down := false }
⊢ False
simp at this