[GOAL]
α β : 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 : (Opposite.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
[PROOFSTEP]
convert congr_fun (hx (𝟙 _) (fun _ => z) (hs <| f z) h rfl) PUnit.unit using 1
[GOAL]
α β : Type u
S : Sieve β
hs : S ∈ GrothendieckTopology.sieves typesGrothendieckTopology β
x : FamilyOfElements (yoneda.obj α) S.arrows
hx : FamilyOfElements.Compatible x
f : (yoneda.obj α).obj (Opposite.op β)
hf : (fun t => FamilyOfElements.IsAmalgamation x t) f
y : (Opposite.op β).unop
⊢ f y = x (fun x => y) (_ : S.arrows fun x => y) PUnit.unit
[PROOFSTEP]
convert congr_fun (hf _ (hs y)) PUnit.unit
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit)
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
⊢ S.map g.op (S.map g₁.op ((fun β g hg => S.map (↾fun x => PUnit.unit).op (f (g (Classical.choose hg)))) β f₁ hf₁)) =
    S.map g.op (S.map g₂.op ((fun β g hg => S.map (↾fun x => PUnit.unit).op (f (g (Classical.choose hg)))) γ f₂ hf₂))
[PROOFSTEP]
have : f₁ (Classical.choose hf₁) = f₂ (Classical.choose hf₂) :=
  Classical.choose_spec hf₁ (g₁ <| g x) ▸ Classical.choose_spec hf₂ (g₂ <| g x) ▸ congr_fun h _
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit)
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : f₁ (Classical.choose hf₁) = f₂ (Classical.choose hf₂)
⊢ S.map g.op (S.map g₁.op ((fun β g hg => S.map (↾fun x => PUnit.unit).op (f (g (Classical.choose hg)))) β f₁ hf₁)) =
    S.map g.op (S.map g₂.op ((fun β g hg => S.map (↾fun x => PUnit.unit).op (f (g (Classical.choose hg)))) γ f₂ hf₂))
[PROOFSTEP]
simp_rw [← FunctorToTypes.map_comp_apply, this, ← op_comp]
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit)
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : f₁ (Classical.choose hf₁) = f₂ (Classical.choose hf₂)
⊢ S.map (g ≫ g₁ ≫ ↾fun x => PUnit.unit).op (f (f₂ (Classical.choose hf₂))) =
    S.map (g ≫ g₂ ≫ ↾fun x => PUnit.unit).op (f (f₂ (Classical.choose hf₂)))
[PROOFSTEP]
rfl
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit)
⊢ eval S α (typesGlue S hs α f) = f
[PROOFSTEP]
funext x
[GOAL]
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit)
x : α
⊢ eval S α (typesGlue S hs α f) x = f x
[PROOFSTEP]
apply (IsSheafFor.valid_glue _ _ _ <| ⟨PUnit.unit, fun _ => Subsingleton.elim _ _⟩).trans
[GOAL]
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit)
x : α
⊢ S.map (↾fun x => PUnit.unit).op (f ((↾fun x_1 => x) (Classical.choose (_ : ∃ x, ∀ (y : PUnit), y = x)))) = f x
[PROOFSTEP]
convert FunctorToTypes.map_id_apply S _
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
⊢ typesGlue S hs α (eval S α s) = s
[PROOFSTEP]
apply (hs.isSheafFor _ _ (generate_discretePresieve_mem α)).isSeparatedFor.ext
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
⊢ ∀ ⦃Y : Type u⦄ ⦃f : Y ⟶ α⦄, discretePresieve α f → S.map f.op (typesGlue S hs α (eval S α s)) = S.map f.op s
[PROOFSTEP]
intro β f hf
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map f.op (typesGlue S hs α (eval S α s)) = S.map f.op s
[PROOFSTEP]
apply (IsSheafFor.valid_glue _ _ _ hf).trans
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map (↾fun x => PUnit.unit).op (eval S α s (f (Classical.choose hf))) = S.map f.op s
[PROOFSTEP]
apply (FunctorToTypes.map_comp_apply _ _ _ _).symm.trans
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map ((↾fun x => f (Classical.choose hf)).op ≫ (↾fun x => PUnit.unit).op) s = S.map f.op s
[PROOFSTEP]
rw [← op_comp]
  --congr 2 -- Porting note: This tactic didn't work. Find an alternative.
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)).op s = S.map f.op s
[PROOFSTEP]
suffices ((↾fun _ ↦ PUnit.unit) ≫ ↾fun _ ↦ f (Classical.choose hf)) = f by rw [this]
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
this : ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) = f
⊢ S.map ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)).op s = S.map f.op s
[PROOFSTEP]
rw [this]
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) = f
[PROOFSTEP]
funext x
[GOAL]
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
x : β
⊢ ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) x = f x
[PROOFSTEP]
exact congr_arg f (Classical.choose_spec hf x).symm
[GOAL]
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : S.obj (op α)
x : β
⊢ eval S β (S.map f.op s) x = eval S α s (f x)
[PROOFSTEP]
simp_rw [eval, ← FunctorToTypes.map_comp_apply, ← op_comp]
[GOAL]
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : S.obj (op α)
x : β
⊢ S.map ((↾fun x_1 => x) ≫ f).op s = S.map (↾fun x_1 => f x).op s
[PROOFSTEP]
rfl
[GOAL]
S : SheafOfTypes typesGrothendieckTopology
⊢ { val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).hom } ≫
      { val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).inv } =
    𝟙 S
[PROOFSTEP]
ext1
[GOAL]
case w
S : SheafOfTypes typesGrothendieckTopology
⊢ ({ val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).hom } ≫
        { val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).inv }).val =
    (𝟙 S).val
[PROOFSTEP]
apply (equivYoneda S.1 S.2).hom_inv_id
[GOAL]
S : SheafOfTypes typesGrothendieckTopology
⊢ { val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).inv } ≫
      { val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).hom } =
    𝟙 (yoneda'.obj (S.val.obj (op PUnit)))
[PROOFSTEP]
ext1
[GOAL]
case w
S : SheafOfTypes typesGrothendieckTopology
⊢ ({ val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).inv } ≫
        { val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).hom }).val =
    (𝟙 (yoneda'.obj (S.val.obj (op PUnit)))).val
[PROOFSTEP]
apply (equivYoneda S.1 S.2).inv_hom_id
[GOAL]
⊢ typesGrothendieckTopology = Sheaf.canonicalTopology (Type u)
[PROOFSTEP]
refine' le_antisymm subcanonical_typesGrothendieckTopology (sInf_le _)
[GOAL]
⊢ typesGrothendieckTopology ∈ Sheaf.finestTopologySingle '' Set.range yoneda.toPrefunctor.obj
[PROOFSTEP]
refine' ⟨yoneda.obj (ULift Bool), ⟨_, rfl⟩, GrothendieckTopology.ext _⟩
[GOAL]
⊢ (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))).sieves = typesGrothendieckTopology.sieves
[PROOFSTEP]
funext α
[GOAL]
case h
α : Type u
⊢ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α =
    GrothendieckTopology.sieves typesGrothendieckTopology α
[PROOFSTEP]
ext S
[GOAL]
case h.h
α : Type u
S : Sieve α
⊢ S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α ↔
    S ∈ GrothendieckTopology.sieves typesGrothendieckTopology α
[PROOFSTEP]
refine' ⟨fun hs x => _, fun hs β f => isSheaf_yoneda' _ fun y => hs _⟩
[GOAL]
case h.h
α : Type u
S : Sieve α
hs : S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α
x : α
⊢ S.arrows fun x_1 => x
[PROOFSTEP]
by_contra hsx
[GOAL]
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
[PROOFSTEP]
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
[GOAL]
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
[PROOFSTEP]
simp at this 
