[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
x✝ : OpensLeCover U
⊢ {
          obj := fun V =>
            {
              obj :=
                { left := V.obj, right := { as := PUnit.unit },
                  hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
              property :=
                (_ :
                  ∃ Y_1 h g,
                    presieveOfCoveringAux U Y g ∧
                      h ≫ g =
                        { left := V.obj, right := { as := PUnit.unit },
                            hom :=
                              homOfLE
                                (_ :
                                  (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
          map := fun {x x_1} g => Over.homMk g }.map
      (𝟙 x✝) =
    𝟙
      ({
            obj := fun V =>
              {
                obj :=
                  { left := V.obj, right := { as := PUnit.unit },
                    hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                property :=
                  (_ :
                    ∃ Y_1 h g,
                      presieveOfCoveringAux U Y g ∧
                        h ≫ g =
                          { left := V.obj, right := { as := PUnit.unit },
                              hom :=
                                homOfLE
                                  (_ :
                                    (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
            map := fun {x x_1} g => Over.homMk g }.obj
        x✝)
[PROOFSTEP]
refine Over.OverMorphism.ext ?_
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
x✝ : OpensLeCover U
⊢ ({
            obj := fun V =>
              {
                obj :=
                  { left := V.obj, right := { as := PUnit.unit },
                    hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                property :=
                  (_ :
                    ∃ Y_1 h g,
                      presieveOfCoveringAux U Y g ∧
                        h ≫ g =
                          { left := V.obj, right := { as := PUnit.unit },
                              hom :=
                                homOfLE
                                  (_ :
                                    (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
            map := fun {x x_1} g => Over.homMk g }.map
        (𝟙 x✝)).left =
    (𝟙
        ({
              obj := fun V =>
                {
                  obj :=
                    { left := V.obj, right := { as := PUnit.unit },
                      hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                  property :=
                    (_ :
                      ∃ Y_1 h g,
                        presieveOfCoveringAux U Y g ∧
                          h ≫ g =
                            { left := V.obj, right := { as := PUnit.unit },
                                hom :=
                                  homOfLE
                                    (_ :
                                      (𝟭 (Opens ↑X)).obj V.obj ≤
                                        (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
              map := fun {x x_1} g => Over.homMk g }.obj
          x✝)).left
[PROOFSTEP]
simp only [Functor.id_obj, Sieve.generate_apply, Functor.const_obj_obj, Over.homMk_left, eq_iff_true_of_subsingleton]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
x✝² x✝¹ x✝ : OpensLeCover U
f : x✝² ⟶ x✝¹
g : x✝¹ ⟶ x✝
⊢ {
          obj := fun V =>
            {
              obj :=
                { left := V.obj, right := { as := PUnit.unit },
                  hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
              property :=
                (_ :
                  ∃ Y_1 h g,
                    presieveOfCoveringAux U Y g ∧
                      h ≫ g =
                        { left := V.obj, right := { as := PUnit.unit },
                            hom :=
                              homOfLE
                                (_ :
                                  (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
          map := fun {x x_1} g => Over.homMk g }.map
      (f ≫ g) =
    {
            obj := fun V =>
              {
                obj :=
                  { left := V.obj, right := { as := PUnit.unit },
                    hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                property :=
                  (_ :
                    ∃ Y_1 h g,
                      presieveOfCoveringAux U Y g ∧
                        h ≫ g =
                          { left := V.obj, right := { as := PUnit.unit },
                              hom :=
                                homOfLE
                                  (_ :
                                    (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
            map := fun {x x_1} g => Over.homMk g }.map
        f ≫
      {
            obj := fun V =>
              {
                obj :=
                  { left := V.obj, right := { as := PUnit.unit },
                    hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                property :=
                  (_ :
                    ∃ Y_1 h g,
                      presieveOfCoveringAux U Y g ∧
                        h ≫ g =
                          { left := V.obj, right := { as := PUnit.unit },
                              hom :=
                                homOfLE
                                  (_ :
                                    (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
            map := fun {x x_1} g => Over.homMk g }.map
        g
[PROOFSTEP]
refine Over.OverMorphism.ext ?_
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
x✝² x✝¹ x✝ : OpensLeCover U
f : x✝² ⟶ x✝¹
g : x✝¹ ⟶ x✝
⊢ ({
            obj := fun V =>
              {
                obj :=
                  { left := V.obj, right := { as := PUnit.unit },
                    hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                property :=
                  (_ :
                    ∃ Y_1 h g,
                      presieveOfCoveringAux U Y g ∧
                        h ≫ g =
                          { left := V.obj, right := { as := PUnit.unit },
                              hom :=
                                homOfLE
                                  (_ :
                                    (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
            map := fun {x x_1} g => Over.homMk g }.map
        (f ≫ g)).left =
    ({
              obj := fun V =>
                {
                  obj :=
                    { left := V.obj, right := { as := PUnit.unit },
                      hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                  property :=
                    (_ :
                      ∃ Y_1 h g,
                        presieveOfCoveringAux U Y g ∧
                          h ≫ g =
                            { left := V.obj, right := { as := PUnit.unit },
                                hom :=
                                  homOfLE
                                    (_ :
                                      (𝟭 (Opens ↑X)).obj V.obj ≤
                                        (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
              map := fun {x x_1} g => Over.homMk g }.map
          f ≫
        {
              obj := fun V =>
                {
                  obj :=
                    { left := V.obj, right := { as := PUnit.unit },
                      hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                  property :=
                    (_ :
                      ∃ Y_1 h g,
                        presieveOfCoveringAux U Y g ∧
                          h ≫ g =
                            { left := V.obj, right := { as := PUnit.unit },
                                hom :=
                                  homOfLE
                                    (_ :
                                      (𝟭 (Opens ↑X)).obj V.obj ≤
                                        (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
              map := fun {x x_1} g => Over.homMk g }.map
          g).left
[PROOFSTEP]
simp only [Functor.id_obj, Sieve.generate_apply, Functor.const_obj_obj, Over.homMk_left, eq_iff_true_of_subsingleton]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ∀ (X_1 : FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom),
    (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj X_1 =
      (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj X_1
[PROOFSTEP]
rintro ⟨⟨_, _⟩, _⟩
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
left✝ : Opens ↑X
right✝ : Discrete PUnit
hom✝ : (𝟭 (Opens ↑X)).obj left✝ ⟶ (Functor.fromPUnit Y).obj right✝
property✝ : (Sieve.generate (presieveOfCoveringAux U Y)).arrows { left := left✝, right := right✝, hom := hom✝ }.hom
⊢ (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj
      { obj := { left := left✝, right := right✝, hom := hom✝ }, property := property✝ } =
    (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj
      { obj := { left := left✝, right := right✝, hom := hom✝ }, property := property✝ }
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
left✝ : Opens ↑X
right✝ : Discrete PUnit
hom✝ : (𝟭 (Opens ↑X)).obj left✝ ⟶ (Functor.fromPUnit Y).obj right✝
property✝ : (Sieve.generate (presieveOfCoveringAux U Y)).arrows { left := left✝, right := right✝, hom := hom✝ }.hom
⊢ { obj := { left := left✝, right := right✝, hom := hom✝ }, property := property✝ } =
    (generateEquivalenceOpensLe_inverse' U ?m.44608).obj
      ((generateEquivalenceOpensLe_functor' U ?m.44561).obj
        { obj := { left := left✝, right := right✝, hom := hom✝ }, property := property✝ })
[PROOFSTEP]
congr
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ∀ (X_1 Y_1 : FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom) (f : X_1 ⟶ Y_1),
    (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).map f =
      eqToHom
          (_ :
            (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj X_1 =
              (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj
                X_1) ≫
        (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).map f ≫
          eqToHom
            (_ :
              (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj
                  Y_1 =
                (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj Y_1)
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
X✝ Y✝ : FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).map f✝ =
    eqToHom
        (_ :
          (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj X✝ =
            (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj X✝) ≫
      (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).map f✝ ≫
        eqToHom
          (_ :
            (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj Y✝ =
              (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj Y✝)
[PROOFSTEP]
refine Over.OverMorphism.ext ?_
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
X✝ Y✝ : FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom
f✝ : X✝ ⟶ Y✝
⊢ ((𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).map f✝).left =
    (eqToHom
          (_ :
            (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj X✝ =
              (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj
                X✝) ≫
        (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).map f✝ ≫
          eqToHom
            (_ :
              (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj Y✝ =
                (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj Y✝)).left
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ∀ (X_1 : OpensLeCover U),
    (generateEquivalenceOpensLe_inverse' U (_ : Y = iSup U) ⋙
            generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).obj
        X_1 =
      (𝟭 (OpensLeCover U)).obj X_1
[PROOFSTEP]
intro
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
X✝ : OpensLeCover U
⊢ (generateEquivalenceOpensLe_inverse' U (_ : Y = iSup U) ⋙ generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).obj
      X✝ =
    (𝟭 (OpensLeCover U)).obj X✝
[PROOFSTEP]
refine FullSubcategory.ext _ _ ?_
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
X✝ : OpensLeCover U
⊢ ((generateEquivalenceOpensLe_inverse' U (_ : Y = iSup U) ⋙ generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).obj
        X✝).obj =
    ((𝟭 (OpensLeCover U)).obj X✝).obj
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ∀ (X_1 Y_1 : OpensLeCover U) (f : X_1 ⟶ Y_1),
    HEq
      ((generateEquivalenceOpensLe_inverse' U (_ : Y = iSup U) ⋙
            generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).map
        f)
      ((𝟭 (OpensLeCover U)).map f)
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
X✝ Y✝ : OpensLeCover U
f✝ : X✝ ⟶ Y✝
⊢ HEq
    ((generateEquivalenceOpensLe_inverse' U (_ : Y = iSup U) ⋙
          generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).map
      f✝)
    ((𝟭 (OpensLeCover U)).map f✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map
        (eqToHom
          (_ :
            op (opensLeCoverCocone U).pt =
              op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt)) ≫
      NatTrans.app (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows))).π j =
    NatTrans.app
      (Cone.whisker (Equivalence.op (generateEquivalenceOpensLe U hY)).functor
          (F.mapCone (Cocone.op (opensLeCoverCocone U)))).π
      j
[PROOFSTEP]
erw [← F.map_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map
      (eqToHom
          (_ :
            op (opensLeCoverCocone U).pt =
              op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt) ≫
        NatTrans.app (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows)).π j) =
    NatTrans.app
      (Cone.whisker (Equivalence.op (generateEquivalenceOpensLe U hY)).functor
          (F.mapCone (Cocone.op (opensLeCoverCocone U)))).π
      j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map (eqToHom (_ : op (opensLeCoverCocone U).pt = op Y) ≫ j.unop.obj.hom.op) =
    F.map
      (NatTrans.app (opensLeCoverCocone U).ι ((generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).obj j.unop)).op
[PROOFSTEP]
congr 1
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map
        (eqToHom
          (_ :
            op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt =
              op (opensLeCoverCocone U).pt)) ≫
      NatTrans.app
        (Cone.whisker (Equivalence.op (generateEquivalenceOpensLe U hY)).functor
            (F.mapCone (Cocone.op (opensLeCoverCocone U)))).π
        j =
    NatTrans.app (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows))).π j
[PROOFSTEP]
erw [← F.map_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map
      (eqToHom
          (_ :
            op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt =
              op (opensLeCoverCocone U).pt) ≫
        NatTrans.app (Cocone.op (opensLeCoverCocone U)).π
          ((Equivalence.op (generateEquivalenceOpensLe U hY)).functor.obj j)) =
    NatTrans.app (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows))).π j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map
      (eqToHom (_ : op Y = op (opensLeCoverCocone U).pt) ≫
        (NatTrans.app (opensLeCoverCocone U).ι
            ((generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).obj j.unop)).op) =
    F.map j.unop.obj.hom.op
[PROOFSTEP]
congr 1
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ConeMorphism.mk
        (F.map
          (eqToHom
            (_ :
              op (opensLeCoverCocone U).pt =
                op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt))) ≫
      ConeMorphism.mk
        (F.map
          (eqToHom
            (_ :
              op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt =
                op (opensLeCoverCocone U).pt))) =
    𝟙
      (Cone.whisker (Equivalence.op (generateEquivalenceOpensLe U hY)).functor
        (F.mapCone (Cocone.op (opensLeCoverCocone U))))
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ (ConeMorphism.mk
          (F.map
            (eqToHom
              (_ :
                op (opensLeCoverCocone U).pt =
                  op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt))) ≫
        ConeMorphism.mk
          (F.map
            (eqToHom
              (_ :
                op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt =
                  op (opensLeCoverCocone U).pt)))).Hom =
    (𝟙
        (Cone.whisker (Equivalence.op (generateEquivalenceOpensLe U hY)).functor
          (F.mapCone (Cocone.op (opensLeCoverCocone U))))).Hom
[PROOFSTEP]
simp [eqToHom_map]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ConeMorphism.mk
        (F.map
          (eqToHom
            (_ :
              op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt =
                op (opensLeCoverCocone U).pt))) ≫
      ConeMorphism.mk
        (F.map
          (eqToHom
            (_ :
              op (opensLeCoverCocone U).pt =
                op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt))) =
    𝟙 (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows)))
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ (ConeMorphism.mk
          (F.map
            (eqToHom
              (_ :
                op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt =
                  op (opensLeCoverCocone U).pt))) ≫
        ConeMorphism.mk
          (F.map
            (eqToHom
              (_ :
                op (opensLeCoverCocone U).pt =
                  op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt)))).Hom =
    (𝟙 (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows)))).Hom
[PROOFSTEP]
simp [eqToHom_map]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
R : Presieve Y
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y
⊢ IsLimit (F.mapCone (Cocone.op (opensLeCoverCocone (coveringOfPresieve Y R)))) ≃
    IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate R).arrows)))
[PROOFSTEP]
convert
  isLimitOpensLeEquivGenerate₁ F (coveringOfPresieve Y R)
    (coveringOfPresieve.iSup_eq_of_mem_grothendieck Y R hR).symm using
  1
[GOAL]
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
R : Presieve Y
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y
⊢ IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate R).arrows))) =
    IsLimit
      (F.mapCone
        (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux (coveringOfPresieve Y R) Y)).arrows)))
[PROOFSTEP]
rw [covering_presieve_eq_self R]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ IsSheaf F ↔ IsSheafOpensLeCover F
[PROOFSTEP]
refine' (Presheaf.isSheaf_iff_isLimit _ _).trans _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ (∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
      S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
        Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))) ↔
    IsSheafOpensLeCover F
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ (∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
      S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
        Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))) →
    IsSheafOpensLeCover F
[PROOFSTEP]
intro h ι U
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι✝ : Type w
U✝ : ι✝ → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U✝
h :
  ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
      Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (opensLeCoverCocone U))))
[PROOFSTEP]
rw [(isLimitOpensLeEquivGenerate₁ F U rfl).nonempty_congr]
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι✝ : Type w
U✝ : ι✝ → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U✝
h :
  ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
      Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty
    (IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U (iSup U))).arrows))))
[PROOFSTEP]
apply h
[GOAL]
case mp.a
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι✝ : Type w
U✝ : ι✝ → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U✝
h :
  ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
      Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
ι : Type w
U : ι → Opens ↑X
⊢ Sieve.generate (presieveOfCoveringAux U (iSup U)) ∈
    GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) (iSup U)
[PROOFSTEP]
apply presieveOfCovering.mem_grothendieckTopology
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ IsSheafOpensLeCover F →
    ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
      S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
        Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
[PROOFSTEP]
intro h Y S
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
⊢ S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y →
    Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
[PROOFSTEP]
rw [← Sieve.generate_sieve S]
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
⊢ Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y →
    Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate S.arrows).arrows))))
[PROOFSTEP]
intro hS
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate S.arrows).arrows))))
[PROOFSTEP]
rw [← (isLimitOpensLeEquivGenerate₂ F S.1 hS).nonempty_congr]
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (opensLeCoverCocone (coveringOfPresieve Y S.arrows)))))
[PROOFSTEP]
apply h
