[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
k : K
⊢ ∀ (b : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
          (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) b) ≫
        MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) b =
      (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
          (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) b) ≫
        MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) b
[PROOFSTEP]
intro i
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
k : K
i : (GrothendieckTopology.Cover.index W (F.obj k).val).R
⊢ (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
        (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
      MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
        (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
      MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i
[PROOFSTEP]
simp only [Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
k : K
i : (GrothendieckTopology.Cover.index W (F.obj k).val).R
⊢ Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
      NatTrans.app (NatTrans.app E.π k)
          (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i).Y) ≫
        MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
    Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
      NatTrans.app (NatTrans.app E.π k)
          (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i).Y) ≫
        MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i
[PROOFSTEP]
erw [← (E.π.app k).naturality, ← (E.π.app k).naturality]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
k : K
i : (GrothendieckTopology.Cover.index W (F.obj k).val).R
⊢ Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
      (((Functor.const K).obj E.pt).obj k).map i.g₁.op ≫ NatTrans.app (NatTrans.app E.π k) (op i.Z) =
    Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
      (((Functor.const K).obj E.pt).obj k).map i.g₂.op ≫ NatTrans.app (NatTrans.app E.π k) (op i.Z)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
k : K
i : (GrothendieckTopology.Cover.index W (F.obj k).val).R
⊢ Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
      E.pt.map i.g₁.op ≫ NatTrans.app (NatTrans.app E.π k) (op i.Z) =
    Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
      E.pt.map i.g₂.op ≫ NatTrans.app (NatTrans.app E.π k) (op i.Z)
[PROOFSTEP]
simp only [← Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
k : K
i : (GrothendieckTopology.Cover.index W (F.obj k).val).R
⊢ (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫ E.pt.map i.g₁.op) ≫
      NatTrans.app (NatTrans.app E.π k) (op i.Z) =
    (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫ E.pt.map i.g₂.op) ≫
      NatTrans.app (NatTrans.app E.π k) (op i.Z)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
k : K
i : (GrothendieckTopology.Cover.index W (F.obj k).val).R
⊢ Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫ E.pt.map i.g₁.op =
    Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫ E.pt.map i.g₂.op
[PROOFSTEP]
apply S.condition
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
⊢ ∀ ⦃X_1 Y : K⦄ (f : X_1 ⟶ Y),
    ((Functor.const K).obj S.pt).map f ≫
        (fun k =>
            IsLimit.lift (Presheaf.isLimitOfIsSheaf J (F.obj k).val W (_ : Presheaf.IsSheaf J (F.obj k).val))
              (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj k).val) S.pt
                (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                (_ :
                  ∀ (i : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                          (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                        MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
                      (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                          (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                        MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i)))
          Y =
      (fun k =>
            IsLimit.lift (Presheaf.isLimitOfIsSheaf J (F.obj k).val W (_ : Presheaf.IsSheaf J (F.obj k).val))
              (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj k).val) S.pt
                (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                (_ :
                  ∀ (i : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                          (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                        MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
                      (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                          (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                        MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i)))
          X_1 ≫
        (F ⋙ sheafToPresheaf J D ⋙ (evaluation Cᵒᵖ D).obj (op X)).map f
[PROOFSTEP]
intro i j f
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i j : K
f : i ⟶ j
⊢ ((Functor.const K).obj S.pt).map f ≫
      (fun k =>
          IsLimit.lift (Presheaf.isLimitOfIsSheaf J (F.obj k).val W (_ : Presheaf.IsSheaf J (F.obj k).val))
            (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj k).val) S.pt
              (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
              (_ :
                ∀ (i : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
                  (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                        (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                      MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                        (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                      MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i)))
        j =
    (fun k =>
          IsLimit.lift (Presheaf.isLimitOfIsSheaf J (F.obj k).val W (_ : Presheaf.IsSheaf J (F.obj k).val))
            (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj k).val) S.pt
              (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
              (_ :
                ∀ (i : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
                  (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                        (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                      MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                        (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                      MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i)))
        i ≫
      (F ⋙ sheafToPresheaf J D ⋙ (evaluation Cᵒᵖ D).obj (op X)).map f
[PROOFSTEP]
dsimp [Presheaf.isLimitOfIsSheaf]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i j : K
f : i ⟶ j
⊢ 𝟙 S.pt ≫
      Presheaf.IsSheaf.amalgamate (_ : Presheaf.IsSheaf J (F.obj j).val) W
        (fun I =>
          Multifork.ι
            (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
              (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
              (_ :
                ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
                  (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                        NatTrans.app (NatTrans.app E.π j)
                          (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                      MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
                    (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                        NatTrans.app (NatTrans.app E.π j)
                          (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                      MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
            I)
        (_ :
          ∀ (I : GrothendieckTopology.Cover.Relation W),
            Multifork.ι
                  (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
                    (_ :
                      ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
                        (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                              NatTrans.app (NatTrans.app E.π j)
                                (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                            MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
                          (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                              NatTrans.app (NatTrans.app E.π j)
                                (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                            MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) I) ≫
                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) I =
              Multifork.ι
                  (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
                    (_ :
                      ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
                        (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                              NatTrans.app (NatTrans.app E.π j)
                                (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                            MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
                          (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                              NatTrans.app (NatTrans.app E.π j)
                                (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                            MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) I) ≫
                MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) I) =
    Presheaf.IsSheaf.amalgamate (_ : Presheaf.IsSheaf J (F.obj i).val) W
        (fun I =>
          Multifork.ι
            (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
              (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
              (_ :
                ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
                  (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                        NatTrans.app (NatTrans.app E.π i)
                          (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                      MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                    (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                        NatTrans.app (NatTrans.app E.π i)
                          (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                      MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
            I)
        (_ :
          ∀ (I : GrothendieckTopology.Cover.Relation W),
            Multifork.ι
                  (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
                    (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
                    (_ :
                      ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
                        (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                              NatTrans.app (NatTrans.app E.π i)
                                (op
                                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                            MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                          (Multifork.ι S
                                (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                              NatTrans.app (NatTrans.app E.π i)
                                (op
                                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                            MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) I) ≫
                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) I =
              Multifork.ι
                  (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
                    (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
                    (_ :
                      ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
                        (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                              NatTrans.app (NatTrans.app E.π i)
                                (op
                                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                            MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                          (Multifork.ι S
                                (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                              NatTrans.app (NatTrans.app E.π i)
                                (op
                                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                            MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) I) ≫
                MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) I) ≫
      NatTrans.app (F.map f).val (op X)
[PROOFSTEP]
rw [Category.id_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i j : K
f : i ⟶ j
⊢ Presheaf.IsSheaf.amalgamate (_ : Presheaf.IsSheaf J (F.obj j).val) W
      (fun I =>
        Multifork.ι
          (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
            (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
            (_ :
              ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
                (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                      NatTrans.app (NatTrans.app E.π j)
                        (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                    MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
                  (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                      NatTrans.app (NatTrans.app E.π j)
                        (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                    MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
          I)
      (_ :
        ∀ (I : GrothendieckTopology.Cover.Relation W),
          Multifork.ι
                (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
                  (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
                  (_ :
                    ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
                      (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                            NatTrans.app (NatTrans.app E.π j)
                              (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                          MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
                        (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                            NatTrans.app (NatTrans.app E.π j)
                              (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                          MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
                (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) I) ≫
              MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) I =
            Multifork.ι
                (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
                  (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
                  (_ :
                    ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
                      (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                            NatTrans.app (NatTrans.app E.π j)
                              (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                          MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
                        (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                            NatTrans.app (NatTrans.app E.π j)
                              (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                          MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
                (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) I) ≫
              MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) I) =
    Presheaf.IsSheaf.amalgamate (_ : Presheaf.IsSheaf J (F.obj i).val) W
        (fun I =>
          Multifork.ι
            (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
              (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
              (_ :
                ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
                  (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                        NatTrans.app (NatTrans.app E.π i)
                          (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                      MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                    (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                        NatTrans.app (NatTrans.app E.π i)
                          (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                      MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
            I)
        (_ :
          ∀ (I : GrothendieckTopology.Cover.Relation W),
            Multifork.ι
                  (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
                    (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
                    (_ :
                      ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
                        (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                              NatTrans.app (NatTrans.app E.π i)
                                (op
                                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                            MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                          (Multifork.ι S
                                (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                              NatTrans.app (NatTrans.app E.π i)
                                (op
                                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                            MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) I) ≫
                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) I =
              Multifork.ι
                  (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
                    (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
                    (_ :
                      ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
                        (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                              NatTrans.app (NatTrans.app E.π i)
                                (op
                                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                            MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                          (Multifork.ι S
                                (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                              NatTrans.app (NatTrans.app E.π i)
                                (op
                                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                            MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) I) ≫
                MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) I) ≫
      NatTrans.app (F.map f).val (op X)
[PROOFSTEP]
apply Presheaf.IsSheaf.hom_ext (F.obj j).2 W
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i j : K
f : i ⟶ j
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow W),
    Presheaf.IsSheaf.amalgamate (_ : Presheaf.IsSheaf J (F.obj j).val) W
          (fun I =>
            Multifork.ι
              (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
                (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
                (_ :
                  ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
                    (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                          NatTrans.app (NatTrans.app E.π j)
                            (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                        MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
                      (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                          NatTrans.app (NatTrans.app E.π j)
                            (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                        MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
              I)
          (_ :
            ∀ (I : GrothendieckTopology.Cover.Relation W),
              Multifork.ι
                    (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
                      (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
                      (_ :
                        ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
                          (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                                NatTrans.app (NatTrans.app E.π j)
                                  (op
                                    (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                              MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
                            (Multifork.ι S
                                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                                NatTrans.app (NatTrans.app E.π j)
                                  (op
                                    (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                              MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
                    (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) I) ≫
                  MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) I =
                Multifork.ι
                    (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
                      (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
                      (_ :
                        ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
                          (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                                NatTrans.app (NatTrans.app E.π j)
                                  (op
                                    (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                              MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
                            (Multifork.ι S
                                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                                NatTrans.app (NatTrans.app E.π j)
                                  (op
                                    (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                              MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
                    (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) I) ≫
                  MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) I) ≫
        (F.obj j).val.map I.f.op =
      (Presheaf.IsSheaf.amalgamate (_ : Presheaf.IsSheaf J (F.obj i).val) W
            (fun I =>
              Multifork.ι
                (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
                  (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
                  (_ :
                    ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
                      (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                            NatTrans.app (NatTrans.app E.π i)
                              (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                          MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                        (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                            NatTrans.app (NatTrans.app E.π i)
                              (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                          MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
                I)
            (_ :
              ∀ (I : GrothendieckTopology.Cover.Relation W),
                Multifork.ι
                      (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
                        (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
                        (_ :
                          ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
                            (Multifork.ι S
                                    (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                                  NatTrans.app (NatTrans.app E.π i)
                                    (op
                                      (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val)
                                          i_1).Y)) ≫
                                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                              (Multifork.ι S
                                    (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                                  NatTrans.app (NatTrans.app E.π i)
                                    (op
                                      (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val)
                                          i_1).Y)) ≫
                                MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
                      (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) I) ≫
                    MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) I =
                  Multifork.ι
                      (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
                        (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
                        (_ :
                          ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
                            (Multifork.ι S
                                    (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                                  NatTrans.app (NatTrans.app E.π i)
                                    (op
                                      (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val)
                                          i_1).Y)) ≫
                                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                              (Multifork.ι S
                                    (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                                  NatTrans.app (NatTrans.app E.π i)
                                    (op
                                      (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val)
                                          i_1).Y)) ≫
                                MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
                      (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) I) ≫
                    MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) I) ≫
          NatTrans.app (F.map f).val (op X)) ≫
        (F.obj j).val.map I.f.op
[PROOFSTEP]
intro ii
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i j : K
f : i ⟶ j
ii : GrothendieckTopology.Cover.Arrow W
⊢ Presheaf.IsSheaf.amalgamate (_ : Presheaf.IsSheaf J (F.obj j).val) W
        (fun I =>
          Multifork.ι
            (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
              (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
              (_ :
                ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
                  (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                        NatTrans.app (NatTrans.app E.π j)
                          (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                      MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
                    (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                        NatTrans.app (NatTrans.app E.π j)
                          (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                      MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
            I)
        (_ :
          ∀ (I : GrothendieckTopology.Cover.Relation W),
            Multifork.ι
                  (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
                    (_ :
                      ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
                        (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                              NatTrans.app (NatTrans.app E.π j)
                                (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                            MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
                          (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                              NatTrans.app (NatTrans.app E.π j)
                                (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                            MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) I) ≫
                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) I =
              Multifork.ι
                  (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
                    (_ :
                      ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
                        (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                              NatTrans.app (NatTrans.app E.π j)
                                (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                            MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
                          (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                              NatTrans.app (NatTrans.app E.π j)
                                (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                            MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) I) ≫
                MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) I) ≫
      (F.obj j).val.map ii.f.op =
    (Presheaf.IsSheaf.amalgamate (_ : Presheaf.IsSheaf J (F.obj i).val) W
          (fun I =>
            Multifork.ι
              (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
                (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
                (_ :
                  ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
                    (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                          NatTrans.app (NatTrans.app E.π i)
                            (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                        MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                      (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                          NatTrans.app (NatTrans.app E.π i)
                            (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                        MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
              I)
          (_ :
            ∀ (I : GrothendieckTopology.Cover.Relation W),
              Multifork.ι
                    (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
                      (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
                      (_ :
                        ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
                          (Multifork.ι S
                                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                                NatTrans.app (NatTrans.app E.π i)
                                  (op
                                    (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val)
                                        i_1).Y)) ≫
                              MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                            (Multifork.ι S
                                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                                NatTrans.app (NatTrans.app E.π i)
                                  (op
                                    (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val)
                                        i_1).Y)) ≫
                              MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
                    (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) I) ≫
                  MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) I =
                Multifork.ι
                    (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
                      (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
                      (_ :
                        ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
                          (Multifork.ι S
                                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                                NatTrans.app (NatTrans.app E.π i)
                                  (op
                                    (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val)
                                        i_1).Y)) ≫
                              MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                            (Multifork.ι S
                                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                                NatTrans.app (NatTrans.app E.π i)
                                  (op
                                    (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val)
                                        i_1).Y)) ≫
                              MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
                    (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) I) ≫
                  MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) I) ≫
        NatTrans.app (F.map f).val (op X)) ≫
      (F.obj j).val.map ii.f.op
[PROOFSTEP]
rw [Presheaf.IsSheaf.amalgamate_map, Category.assoc, ← (F.map f).val.naturality, ← Category.assoc,
  Presheaf.IsSheaf.amalgamate_map]
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i j : K
f : i ⟶ j
ii : GrothendieckTopology.Cover.Arrow W
⊢ Multifork.ι
      (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj j).val) S.pt
        (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π j) (op i.Y))
        (_ :
          ∀ (i : (GrothendieckTopology.Cover.index W (F.obj j).val).R),
            (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                  NatTrans.app (NatTrans.app E.π j)
                    (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) i =
              (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i) ≫
                  NatTrans.app (NatTrans.app E.π j)
                    (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj j).val) i).Y)) ≫
                MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj j).val) i))
      ii =
    Multifork.ι
        (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj i).val) S.pt
          (fun i_1 => Multifork.ι S i_1 ≫ NatTrans.app (NatTrans.app E.π i) (op i_1.Y))
          (_ :
            ∀ (i_1 : (GrothendieckTopology.Cover.index W (F.obj i).val).R),
              (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                    NatTrans.app (NatTrans.app E.π i)
                      (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                  MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) i_1 =
                (Multifork.ι S (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1) ≫
                    NatTrans.app (NatTrans.app E.π i)
                      (op (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj i).val) i_1).Y)) ≫
                  MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj i).val) i_1))
        ii ≫
      NatTrans.app (F.map f).val (op ii.Y)
[PROOFSTEP]
dsimp [Multifork.ofι]
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i j : K
f : i ⟶ j
ii : GrothendieckTopology.Cover.Arrow W
⊢ Multifork.ι
      { pt := S.pt,
        π :=
          NatTrans.mk fun x =>
            match x with
            | WalkingMulticospan.left a => Multifork.ι S a ≫ NatTrans.app (NatTrans.app E.π j) (op a.Y)
            | WalkingMulticospan.right b =>
              (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) b) ≫
                  NatTrans.app (NatTrans.app E.π j)
                    (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) b).Y)) ≫
                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) b }
      ii =
    Multifork.ι
        { pt := S.pt,
          π :=
            NatTrans.mk fun x =>
              match x with
              | WalkingMulticospan.left a => Multifork.ι S a ≫ NatTrans.app (NatTrans.app E.π i) (op a.Y)
              | WalkingMulticospan.right b =>
                (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) b) ≫
                    NatTrans.app (NatTrans.app E.π i)
                      (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj i).val) b).Y)) ≫
                  MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj i).val) b }
        ii ≫
      NatTrans.app (F.map f).val (op ii.Y)
[PROOFSTEP]
erw [Category.assoc, ← E.w f]
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
K : Type z
inst✝ : SmallCategory K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i j : K
f : i ⟶ j
ii : GrothendieckTopology.Cover.Arrow W
⊢ Multifork.ι
      { pt := S.pt,
        π :=
          NatTrans.mk fun x =>
            match x with
            | WalkingMulticospan.left a =>
              Multifork.ι S a ≫ NatTrans.app (NatTrans.app E.π i ≫ (F ⋙ sheafToPresheaf J D).map f) (op a.Y)
            | WalkingMulticospan.right b =>
              (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) b) ≫
                  NatTrans.app (NatTrans.app E.π i ≫ (F ⋙ sheafToPresheaf J D).map f)
                    (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj j).val) b).Y)) ≫
                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj j).val) b }
      ii =
    Multifork.ι S ii ≫ NatTrans.app (NatTrans.app E.π i) (op ii.Y) ≫ NatTrans.app (F.map f).val (op ii.Y)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
⊢ ∀ (E_1 : Multifork (GrothendieckTopology.Cover.index W E.pt)) (i : (GrothendieckTopology.Cover.index W E.pt).L),
    (fun S => IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S))
          E_1 ≫
        Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i =
      Multifork.ι E_1 i
[PROOFSTEP]
intro S i
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i : (GrothendieckTopology.Cover.index W E.pt).L
⊢ (fun S => IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S))
        S ≫
      Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i =
    Multifork.ι S i
[PROOFSTEP]
apply (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op i.Y)) hE).hom_ext
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i : (GrothendieckTopology.Cover.index W E.pt).L
⊢ ∀ (j : K),
    ((fun S => IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S))
            S ≫
          Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i) ≫
        NatTrans.app (((evaluation Cᵒᵖ D).obj (op i.Y)).mapCone E).π j =
      Multifork.ι S i ≫ NatTrans.app (((evaluation Cᵒᵖ D).obj (op i.Y)).mapCone E).π j
[PROOFSTEP]
intro k
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i : (GrothendieckTopology.Cover.index W E.pt).L
k : K
⊢ ((fun S => IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S))
          S ≫
        Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i) ≫
      NatTrans.app (((evaluation Cᵒᵖ D).obj (op i.Y)).mapCone E).π k =
    Multifork.ι S i ≫ NatTrans.app (((evaluation Cᵒᵖ D).obj (op i.Y)).mapCone E).π k
[PROOFSTEP]
dsimp [Multifork.ofι]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i : (GrothendieckTopology.Cover.index W E.pt).L
k : K
⊢ (IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
        Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i) ≫
      NatTrans.app (NatTrans.app E.π k) (op i.Y) =
    Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y)
[PROOFSTEP]
erw [Category.assoc, (E.π.app k).naturality]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i : (GrothendieckTopology.Cover.index W E.pt).L
k : K
⊢ IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
      NatTrans.app (NatTrans.app E.π k) (op X) ≫ ((F ⋙ sheafToPresheaf J D).obj k).map i.f.op =
    Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i : (GrothendieckTopology.Cover.index W E.pt).L
k : K
⊢ IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
      NatTrans.app (NatTrans.app E.π k) (op X) ≫ (F.obj k).val.map i.f.op =
    Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y)
[PROOFSTEP]
rw [← Category.assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i : (GrothendieckTopology.Cover.index W E.pt).L
k : K
⊢ (IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
        NatTrans.app (NatTrans.app E.π k) (op X)) ≫
      (F.obj k).val.map i.f.op =
    Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y)
[PROOFSTEP]
erw [(isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).fac (multiforkEvaluationCone F E X W S)]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i : (GrothendieckTopology.Cover.index W E.pt).L
k : K
⊢ NatTrans.app (multiforkEvaluationCone F E X W S).π k ≫ (F.obj k).val.map i.f.op =
    Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y)
[PROOFSTEP]
dsimp [multiforkEvaluationCone, Presheaf.isLimitOfIsSheaf]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i : (GrothendieckTopology.Cover.index W E.pt).L
k : K
⊢ Presheaf.IsSheaf.amalgamate (_ : Presheaf.IsSheaf J (F.obj k).val) W
        (fun I =>
          Multifork.ι
            (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj k).val) S.pt
              (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
              (_ :
                ∀ (i : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
                  (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                        (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                      MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                        (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                      MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i))
            I)
        (_ :
          ∀ (I : GrothendieckTopology.Cover.Relation W),
            Multifork.ι
                  (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj k).val) S.pt
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                    (_ :
                      ∀ (i : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
                        (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                              (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                            MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
                          (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                              (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                            MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i))
                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) I) ≫
                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) I =
              Multifork.ι
                  (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj k).val) S.pt
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                    (_ :
                      ∀ (i : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
                        (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                              (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                            MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
                          (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                              (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                            MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i))
                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) I) ≫
                MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) I) ≫
      (F.obj k).val.map i.f.op =
    Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y)
[PROOFSTEP]
erw [Presheaf.IsSheaf.amalgamate_map]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
i : (GrothendieckTopology.Cover.index W E.pt).L
k : K
⊢ Multifork.ι
      (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj k).val) S.pt
        (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
        (_ :
          ∀ (i : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
            (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
              (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i))
      i =
    Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
⊢ ∀ (E_1 : Multifork (GrothendieckTopology.Cover.index W E.pt))
    (m : E_1.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt),
    (∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
        m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι E_1 i) →
      m =
        (fun S =>
            IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S))
          E_1
[PROOFSTEP]
intro S m hm
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
m : S.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt
hm :
  ∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι S i
⊢ m =
    (fun S => IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S))
      S
[PROOFSTEP]
apply (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).hom_ext
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
m : S.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt
hm :
  ∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι S i
⊢ ∀ (j : K),
    m ≫ NatTrans.app (((evaluation Cᵒᵖ D).obj (op X)).mapCone E).π j =
      (fun S =>
            IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S))
          S ≫
        NatTrans.app (((evaluation Cᵒᵖ D).obj (op X)).mapCone E).π j
[PROOFSTEP]
intro k
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
m : S.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt
hm :
  ∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι S i
k : K
⊢ m ≫ NatTrans.app (((evaluation Cᵒᵖ D).obj (op X)).mapCone E).π k =
    (fun S => IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S))
        S ≫
      NatTrans.app (((evaluation Cᵒᵖ D).obj (op X)).mapCone E).π k
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
m : S.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt
hm :
  ∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι S i
k : K
⊢ m ≫ NatTrans.app (NatTrans.app E.π k) (op X) =
    IsLimit.lift (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
      NatTrans.app (NatTrans.app E.π k) (op X)
[PROOFSTEP]
erw [(isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).fac]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
m : S.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt
hm :
  ∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι S i
k : K
⊢ m ≫ NatTrans.app (NatTrans.app E.π k) (op X) = NatTrans.app (multiforkEvaluationCone F E X W S).π k
[PROOFSTEP]
apply Presheaf.IsSheaf.hom_ext (F.obj k).2 W
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
m : S.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt
hm :
  ∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι S i
k : K
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow W),
    (m ≫ NatTrans.app (NatTrans.app E.π k) (op X)) ≫ (F.obj k).val.map I.f.op =
      NatTrans.app (multiforkEvaluationCone F E X W S).π k ≫ (F.obj k).val.map I.f.op
[PROOFSTEP]
intro i
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
m : S.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt
hm :
  ∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι S i
k : K
i : GrothendieckTopology.Cover.Arrow W
⊢ (m ≫ NatTrans.app (NatTrans.app E.π k) (op X)) ≫ (F.obj k).val.map i.f.op =
    NatTrans.app (multiforkEvaluationCone F E X W S).π k ≫ (F.obj k).val.map i.f.op
[PROOFSTEP]
dsimp only [multiforkEvaluationCone, Presheaf.isLimitOfIsSheaf]
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
m : S.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt
hm :
  ∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι S i
k : K
i : GrothendieckTopology.Cover.Arrow W
⊢ (m ≫ NatTrans.app (NatTrans.app E.π k) (op X)) ≫ (F.obj k).val.map i.f.op =
    Presheaf.IsSheaf.amalgamate (_ : Presheaf.IsSheaf J (F.obj k).val) W
        (fun I =>
          Multifork.ι
            (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj k).val) S.pt
              (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
              (_ :
                ∀ (i : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
                  (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                        (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                      MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                        (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                      MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i))
            I)
        (_ :
          ∀ (I : GrothendieckTopology.Cover.Relation W),
            Multifork.ι
                  (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj k).val) S.pt
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                    (_ :
                      ∀ (i : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
                        (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                              (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                            MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
                          (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                              (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                            MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i))
                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) I) ≫
                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) I =
              Multifork.ι
                  (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj k).val) S.pt
                    (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                    (_ :
                      ∀ (i : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
                        (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                              (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                            MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
                          (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                              (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                            MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i))
                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) I) ≫
                MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) I) ≫
      (F.obj k).val.map i.f.op
[PROOFSTEP]
rw [(F.obj k).cond.amalgamate_map]
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
m : S.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt
hm :
  ∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι S i
k : K
i : GrothendieckTopology.Cover.Arrow W
⊢ (m ≫ NatTrans.app (NatTrans.app E.π k) (op X)) ≫ (F.obj k).val.map i.f.op =
    Multifork.ι
      (Multifork.ofι (GrothendieckTopology.Cover.index W (F.obj k).val) S.pt
        (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
        (_ :
          ∀ (i : (GrothendieckTopology.Cover.index W (F.obj k).val).R),
            (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                  (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) i =
              (fun i => Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y))
                  (MulticospanIndex.sndTo (GrothendieckTopology.Cover.index W (F.obj k).val) i) ≫
                MulticospanIndex.snd (GrothendieckTopology.Cover.index W (F.obj k).val) i))
      i
[PROOFSTEP]
dsimp [Multifork.ofι]
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
m : S.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt
hm :
  ∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι S i
k : K
i : GrothendieckTopology.Cover.Arrow W
⊢ (m ≫ NatTrans.app (NatTrans.app E.π k) (op X)) ≫ (F.obj k).val.map i.f.op =
    Multifork.ι
      { pt := S.pt,
        π :=
          NatTrans.mk fun x =>
            match x with
            | WalkingMulticospan.left a => Multifork.ι S a ≫ NatTrans.app (NatTrans.app E.π k) (op a.Y)
            | WalkingMulticospan.right b =>
              (Multifork.ι S (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) b) ≫
                  NatTrans.app (NatTrans.app E.π k)
                    (op (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index W (F.obj k).val) b).Y)) ≫
                MulticospanIndex.fst (GrothendieckTopology.Cover.index W (F.obj k).val) b }
      i
[PROOFSTEP]
change _ = S.ι i ≫ _
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
m : S.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt
hm :
  ∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι S i
k : K
i : GrothendieckTopology.Cover.Arrow W
⊢ (m ≫ NatTrans.app (NatTrans.app E.π k) (op X)) ≫ (F.obj k).val.map i.f.op =
    Multifork.ι S i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y)
[PROOFSTEP]
erw [← hm, Category.assoc, ← (E.π.app k).naturality, Category.assoc]
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : GrothendieckTopology.Cover J X
S : Multifork (GrothendieckTopology.Cover.index W E.pt)
m : S.pt ⟶ (GrothendieckTopology.Cover.multifork W E.pt).pt
hm :
  ∀ (i : (GrothendieckTopology.Cover.index W E.pt).L),
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i = Multifork.ι S i
k : K
i : GrothendieckTopology.Cover.Arrow W
⊢ m ≫ (((Functor.const K).obj E.pt).obj k).map i.f.op ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y) =
    m ≫ Multifork.ι (GrothendieckTopology.Cover.multifork W E.pt) i ≫ NatTrans.app (NatTrans.app E.π k) (op i.Y)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ Presheaf.IsSheaf J E.pt
[PROOFSTEP]
rw [Presheaf.isSheaf_iff_multifork]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S E.pt))
[PROOFSTEP]
intro X S
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
S : GrothendieckTopology.Cover J X
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S E.pt))
[PROOFSTEP]
exact ⟨isLimitMultiforkOfIsLimit _ _ hE _ _⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
j : K
⊢ NatTrans.app
      ((sheafToPresheaf J D).mapCone
          { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
            π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).π
      j =
    (eqToIso
          (_ :
            ((sheafToPresheaf J D).mapCone
                  { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                    π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt =
              ((sheafToPresheaf J D).mapCone
                  { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                    π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt)).hom ≫
      NatTrans.app E.π j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
j : K
⊢ NatTrans.app E.π j = 𝟙 E.pt ≫ NatTrans.app E.π j
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
S : Cone F
j : K
⊢ (fun S => { val := IsLimit.lift hE ((sheafToPresheaf J D).mapCone S) }) S ≫
      NatTrans.app
        {
              liftedCone :=
                { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                  π := NatTrans.mk fun t => { val := NatTrans.app E.π t } },
              validLift :=
                Cones.ext
                  (eqToIso
                    (_ :
                      ((sheafToPresheaf J D).mapCone
                            { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                              π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt =
                        ((sheafToPresheaf J D).mapCone
                            { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                              π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt)) }.liftedCone.π
        j =
    NatTrans.app S.π j
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
S : Cone F
j : K
⊢ ((fun S => { val := IsLimit.lift hE ((sheafToPresheaf J D).mapCone S) }) S ≫
        NatTrans.app
          {
                liftedCone :=
                  { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                    π := NatTrans.mk fun t => { val := NatTrans.app E.π t } },
                validLift :=
                  Cones.ext
                    (eqToIso
                      (_ :
                        ((sheafToPresheaf J D).mapCone
                              { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                                π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt =
                          ((sheafToPresheaf J D).mapCone
                              { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                                π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt)) }.liftedCone.π
          j).val =
    (NatTrans.app S.π j).val
[PROOFSTEP]
apply hE.fac ((sheafToPresheaf J D).mapCone S) j
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
S : Cone F
m :
  S.pt ⟶
    {
          liftedCone :=
            { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
              π := NatTrans.mk fun t => { val := NatTrans.app E.π t } },
          validLift :=
            Cones.ext
              (eqToIso
                (_ :
                  ((sheafToPresheaf J D).mapCone
                        { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                          π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt =
                    ((sheafToPresheaf J D).mapCone
                        { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                          π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt)) }.liftedCone.pt
hm :
  ∀ (j : K),
    m ≫
        NatTrans.app
          {
                liftedCone :=
                  { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                    π := NatTrans.mk fun t => { val := NatTrans.app E.π t } },
                validLift :=
                  Cones.ext
                    (eqToIso
                      (_ :
                        ((sheafToPresheaf J D).mapCone
                              { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                                π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt =
                          ((sheafToPresheaf J D).mapCone
                              { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                                π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt)) }.liftedCone.π
          j =
      NatTrans.app S.π j
⊢ m = (fun S => { val := IsLimit.lift hE ((sheafToPresheaf J D).mapCone S) }) S
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
S : Cone F
m :
  S.pt ⟶
    {
          liftedCone :=
            { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
              π := NatTrans.mk fun t => { val := NatTrans.app E.π t } },
          validLift :=
            Cones.ext
              (eqToIso
                (_ :
                  ((sheafToPresheaf J D).mapCone
                        { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                          π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt =
                    ((sheafToPresheaf J D).mapCone
                        { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                          π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt)) }.liftedCone.pt
hm :
  ∀ (j : K),
    m ≫
        NatTrans.app
          {
                liftedCone :=
                  { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                    π := NatTrans.mk fun t => { val := NatTrans.app E.π t } },
                validLift :=
                  Cones.ext
                    (eqToIso
                      (_ :
                        ((sheafToPresheaf J D).mapCone
                              { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                                π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt =
                          ((sheafToPresheaf J D).mapCone
                              { pt := { val := E.pt, cond := (_ : Presheaf.IsSheaf J E.pt) },
                                π := NatTrans.mk fun t => { val := NatTrans.app E.π t } }).pt)) }.liftedCone.π
          j =
      NatTrans.app S.π j
⊢ m.val = ((fun S => { val := IsLimit.lift hE ((sheafToPresheaf J D).mapCone S) }) S).val
[PROOFSTEP]
exact hE.uniq ((sheafToPresheaf J D).mapCone S) m.val fun j => congr_arg Hom.val (hm j)
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
i j : K
f : i ⟶ j
⊢ F.map f ≫ (fun k => { val := NatTrans.app E.ι k ≫ GrothendieckTopology.toSheafify J E.pt }) j =
    (fun k => { val := NatTrans.app E.ι k ≫ GrothendieckTopology.toSheafify J E.pt }) i ≫
      ((Functor.const K).obj
            { val := GrothendieckTopology.sheafify J E.pt,
              cond :=
                (_ : Presheaf.IsSheaf J (GrothendieckTopology.plusObj J (GrothendieckTopology.plusObj J E.pt))) }).map
        f
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
i j : K
f : i ⟶ j
⊢ (F.map f ≫ (fun k => { val := NatTrans.app E.ι k ≫ GrothendieckTopology.toSheafify J E.pt }) j).val =
    ((fun k => { val := NatTrans.app E.ι k ≫ GrothendieckTopology.toSheafify J E.pt }) i ≫
        ((Functor.const K).obj
              { val := GrothendieckTopology.sheafify J E.pt,
                cond :=
                  (_ : Presheaf.IsSheaf J (GrothendieckTopology.plusObj J (GrothendieckTopology.plusObj J E.pt))) }).map
          f).val
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
i j : K
f : i ⟶ j
⊢ (F.map f).val ≫ NatTrans.app E.ι j ≫ GrothendieckTopology.toSheafify J E.pt =
    (NatTrans.app E.ι i ≫ GrothendieckTopology.toSheafify J E.pt) ≫ 𝟙 (GrothendieckTopology.sheafify J E.pt)
[PROOFSTEP]
erw [Category.comp_id, ← Category.assoc, E.w f]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
⊢ ∀ (s : Cocone F) (j : K),
    NatTrans.app (sheafifyCocone E).ι j ≫
        (fun S =>
            {
              val :=
                GrothendieckTopology.sheafifyLift J (IsColimit.desc hE ((sheafToPresheaf J D).mapCocone S))
                  (_ : Presheaf.IsSheaf J S.pt.val) })
          s =
      NatTrans.app s.ι j
[PROOFSTEP]
intro S j
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ NatTrans.app (sheafifyCocone E).ι j ≫
      (fun S =>
          {
            val :=
              GrothendieckTopology.sheafifyLift J (IsColimit.desc hE ((sheafToPresheaf J D).mapCocone S))
                (_ : Presheaf.IsSheaf J S.pt.val) })
        S =
    NatTrans.app S.ι j
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ (NatTrans.app (sheafifyCocone E).ι j ≫
        (fun S =>
            {
              val :=
                GrothendieckTopology.sheafifyLift J (IsColimit.desc hE ((sheafToPresheaf J D).mapCocone S))
                  (_ : Presheaf.IsSheaf J S.pt.val) })
          S).val =
    (NatTrans.app S.ι j).val
[PROOFSTEP]
dsimp [sheafifyCocone]
[GOAL]
case h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ (NatTrans.app E.ι j ≫ GrothendieckTopology.toSheafify J E.pt) ≫
      GrothendieckTopology.sheafifyLift J (IsColimit.desc hE ((sheafToPresheaf J D).mapCocone S))
        (_ : Presheaf.IsSheaf J S.pt.val) =
    (NatTrans.app S.ι j).val
[PROOFSTEP]
erw [Category.assoc, J.toSheafify_sheafifyLift, hE.fac]
[GOAL]
case h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ NatTrans.app ((sheafToPresheaf J D).mapCocone S).ι j = (NatTrans.app S.ι j).val
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
⊢ ∀ (s : Cocone F) (m : (sheafifyCocone E).pt ⟶ s.pt),
    (∀ (j : K), NatTrans.app (sheafifyCocone E).ι j ≫ m = NatTrans.app s.ι j) →
      m =
        (fun S =>
            {
              val :=
                GrothendieckTopology.sheafifyLift J (IsColimit.desc hE ((sheafToPresheaf J D).mapCocone S))
                  (_ : Presheaf.IsSheaf J S.pt.val) })
          s
[PROOFSTEP]
intro S m hm
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m : (sheafifyCocone E).pt ⟶ S.pt
hm : ∀ (j : K), NatTrans.app (sheafifyCocone E).ι j ≫ m = NatTrans.app S.ι j
⊢ m =
    (fun S =>
        {
          val :=
            GrothendieckTopology.sheafifyLift J (IsColimit.desc hE ((sheafToPresheaf J D).mapCocone S))
              (_ : Presheaf.IsSheaf J S.pt.val) })
      S
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m : (sheafifyCocone E).pt ⟶ S.pt
hm : ∀ (j : K), NatTrans.app (sheafifyCocone E).ι j ≫ m = NatTrans.app S.ι j
⊢ m.val =
    ((fun S =>
          {
            val :=
              GrothendieckTopology.sheafifyLift J (IsColimit.desc hE ((sheafToPresheaf J D).mapCocone S))
                (_ : Presheaf.IsSheaf J S.pt.val) })
        S).val
[PROOFSTEP]
apply J.sheafifyLift_unique
[GOAL]
case h.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m : (sheafifyCocone E).pt ⟶ S.pt
hm : ∀ (j : K), NatTrans.app (sheafifyCocone E).ι j ≫ m = NatTrans.app S.ι j
⊢ GrothendieckTopology.toSheafify J E.pt ≫ m.val = IsColimit.desc hE ((sheafToPresheaf J D).mapCocone S)
[PROOFSTEP]
apply hE.uniq ((sheafToPresheaf J D).mapCocone S)
[GOAL]
case h.a.x
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m : (sheafifyCocone E).pt ⟶ S.pt
hm : ∀ (j : K), NatTrans.app (sheafifyCocone E).ι j ≫ m = NatTrans.app S.ι j
⊢ ∀ (j : K),
    NatTrans.app E.ι j ≫ GrothendieckTopology.toSheafify J E.pt ≫ m.val =
      NatTrans.app ((sheafToPresheaf J D).mapCocone S).ι j
[PROOFSTEP]
intro j
[GOAL]
case h.a.x
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m : (sheafifyCocone E).pt ⟶ S.pt
hm : ∀ (j : K), NatTrans.app (sheafifyCocone E).ι j ≫ m = NatTrans.app S.ι j
j : K
⊢ NatTrans.app E.ι j ≫ GrothendieckTopology.toSheafify J E.pt ≫ m.val =
    NatTrans.app ((sheafToPresheaf J D).mapCocone S).ι j
[PROOFSTEP]
dsimp
[GOAL]
case h.a.x
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m : (sheafifyCocone E).pt ⟶ S.pt
hm : ∀ (j : K), NatTrans.app (sheafifyCocone E).ι j ≫ m = NatTrans.app S.ι j
j : K
⊢ NatTrans.app E.ι j ≫ GrothendieckTopology.toSheafify J E.pt ≫ m.val = (NatTrans.app S.ι j).val
[PROOFSTEP]
simp only [← Category.assoc, ← hm]
  -- Porting note: was `simpa only [...]`
[GOAL]
case h.a.x
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{max v u, w} D
K : Type (max v u)
inst✝⁶ : SmallCategory K
inst✝⁵ : ConcreteCategory D
inst✝⁴ :
  ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m : (sheafifyCocone E).pt ⟶ S.pt
hm : ∀ (j : K), NatTrans.app (sheafifyCocone E).ι j ≫ m = NatTrans.app S.ι j
j : K
⊢ (NatTrans.app E.ι j ≫ GrothendieckTopology.toSheafify J E.pt) ≫ m.val = (NatTrans.app (sheafifyCocone E).ι j ≫ m).val
[PROOFSTEP]
rfl
