[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
X Y : C
f✝ : X ⟶ Y
S T : (Cover J Y)ᵒᵖ
f : S ⟶ T
I : (Cover.index ((pullback J f✝).op.obj T).unop P).L
⊢ ((diagram J P Y).map f ≫
        (fun S =>
            Multiequalizer.lift (Cover.index ((pullback J f✝).op.obj S).unop P) ((diagram J P Y).obj S)
              (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
              (_ :
                ∀ (I : (Cover.index ((pullback J f✝).op.obj S).unop P).R),
                  Multiequalizer.ι (Cover.index S.unop P)
                        (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                      MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
                    Multiequalizer.ι (Cover.index S.unop P)
                        (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                      MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)))
          T) ≫
      Multiequalizer.ι (Cover.index ((pullback J f✝).op.obj T).unop P) I =
    ((fun S =>
            Multiequalizer.lift (Cover.index ((pullback J f✝).op.obj S).unop P) ((diagram J P Y).obj S)
              (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
              (_ :
                ∀ (I : (Cover.index ((pullback J f✝).op.obj S).unop P).R),
                  Multiequalizer.ι (Cover.index S.unop P)
                        (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                      MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
                    Multiequalizer.ι (Cover.index S.unop P)
                        (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                      MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)))
          S ≫
        ((pullback J f✝).op ⋙ diagram J P X).map f) ≫
      Multiequalizer.ι (Cover.index ((pullback J f✝).op.obj T).unop P) I
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
X Y : C
f✝ : X ⟶ Y
S T : (Cover J Y)ᵒᵖ
f : S ⟶ T
I : (Cover.index ((pullback J f✝).op.obj T).unop P).L
⊢ (Multiequalizer.lift (Cover.index T.unop P) (multiequalizer (Cover.index S.unop P))
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.map I f.unop))
          (_ :
            ∀ (I : (Cover.index T.unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.map I f.unop)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.map I f.unop) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.map I f.unop)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.map I f.unop)) ≫
        Multiequalizer.lift (Cover.index (Cover.pullback T.unop f✝) P) (multiequalizer (Cover.index T.unop P))
          (fun I => Multiequalizer.ι (Cover.index T.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index (Cover.pullback T.unop f✝) P).R),
              Multiequalizer.ι (Cover.index T.unop P)
                    (MulticospanIndex.fstTo (Cover.index T.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index T.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index T.unop P)
                    (MulticospanIndex.sndTo (Cover.index T.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index T.unop P) (Cover.Relation.base I))) ≫
      Multiequalizer.ι (Cover.index (Cover.pullback T.unop f✝) P) I =
    (Multiequalizer.lift (Cover.index (Cover.pullback S.unop f✝) P) (multiequalizer (Cover.index S.unop P))
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index (Cover.pullback S.unop f✝) P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
        Multiequalizer.lift (Cover.index (Cover.pullback T.unop f✝) P)
          (multiequalizer (Cover.index (Cover.pullback S.unop f✝) P))
          (fun I =>
            Multiequalizer.ι (Cover.index (Cover.pullback S.unop f✝) P)
              (Cover.Arrow.map I ((pullback J f✝).map f.unop)))
          (_ :
            ∀ (I : (Cover.index (op (Cover.pullback T.unop f✝)).unop P).R),
              Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f✝)).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op (Cover.pullback S.unop f✝)).unop P)
                      (Cover.Relation.map I ((pullback J f✝).map f.unop).op.unop)) ≫
                  MulticospanIndex.fst (Cover.index (op (Cover.pullback S.unop f✝)).unop P)
                    (Cover.Relation.map I ((pullback J f✝).map f.unop).op.unop) =
                Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f✝)).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op (Cover.pullback S.unop f✝)).unop P)
                      (Cover.Relation.map I ((pullback J f✝).map f.unop).op.unop)) ≫
                  MulticospanIndex.snd (Cover.index (op (Cover.pullback S.unop f✝)).unop P)
                    (Cover.Relation.map I ((pullback J f✝).map f.unop).op.unop))) ≫
      Multiequalizer.ι (Cover.index (Cover.pullback T.unop f✝) P) I
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
X Y : C
f✝ : X ⟶ Y
S T : (Cover J Y)ᵒᵖ
f : S ⟶ T
I : (Cover.index ((pullback J f✝).op.obj T).unop P).L
⊢ Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.map (Cover.Arrow.base I) f.unop) =
    Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base (Cover.Arrow.map I ((pullback J f✝).map f.unop)))
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : C
W : (Cover J X)ᵒᵖ
i : (Cover.index W.unop Q).R
⊢ (fun i => Multiequalizer.ι (Cover.index W.unop P) i ≫ NatTrans.app η (op i.Y))
        (MulticospanIndex.fstTo (Cover.index W.unop Q) i) ≫
      MulticospanIndex.fst (Cover.index W.unop Q) i =
    (fun i => Multiequalizer.ι (Cover.index W.unop P) i ≫ NatTrans.app η (op i.Y))
        (MulticospanIndex.sndTo (Cover.index W.unop Q) i) ≫
      MulticospanIndex.snd (Cover.index W.unop Q) i
[PROOFSTEP]
dsimp only
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : C
W : (Cover J X)ᵒᵖ
i : (Cover.index W.unop Q).R
⊢ (Multiequalizer.ι (Cover.index W.unop P) (MulticospanIndex.fstTo (Cover.index W.unop Q) i) ≫
        NatTrans.app η (op (MulticospanIndex.fstTo (Cover.index W.unop Q) i).Y)) ≫
      MulticospanIndex.fst (Cover.index W.unop Q) i =
    (Multiequalizer.ι (Cover.index W.unop P) (MulticospanIndex.sndTo (Cover.index W.unop Q) i) ≫
        NatTrans.app η (op (MulticospanIndex.sndTo (Cover.index W.unop Q) i).Y)) ≫
      MulticospanIndex.snd (Cover.index W.unop Q) i
[PROOFSTEP]
erw [Category.assoc, Category.assoc, ← η.naturality, ← η.naturality, Multiequalizer.condition_assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : C
W : (Cover J X)ᵒᵖ
i : (Cover.index W.unop Q).R
⊢ Multiequalizer.ι (Cover.index W.unop P) (MulticospanIndex.sndTo (Cover.index W.unop P) i) ≫
      MulticospanIndex.snd (Cover.index W.unop P) i ≫ NatTrans.app η (op i.Z) =
    Multiequalizer.ι (Cover.index W.unop P) (MulticospanIndex.sndTo (Cover.index W.unop Q) i) ≫
      P.map i.g₂.op ≫ NatTrans.app η (op i.Z)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
X : C
P : Cᵒᵖ ⥤ D
⊢ diagramNatTrans J (𝟙 P) X = 𝟙 (diagram J P X)
[PROOFSTEP]
ext : 2
[GOAL]
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
X : C
P : Cᵒᵖ ⥤ D
x✝ : (Cover J X)ᵒᵖ
⊢ NatTrans.app (diagramNatTrans J (𝟙 P) X) x✝ = NatTrans.app (𝟙 (diagram J P X)) x✝
[PROOFSTEP]
refine' Multiequalizer.hom_ext _ _ _ (fun i => _)
[GOAL]
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
X : C
P : Cᵒᵖ ⥤ D
x✝ : (Cover J X)ᵒᵖ
i : (Cover.index x✝.unop P).L
⊢ NatTrans.app (diagramNatTrans J (𝟙 P) X) x✝ ≫ Multiequalizer.ι (Cover.index x✝.unop P) i =
    NatTrans.app (𝟙 (diagram J P X)) x✝ ≫ Multiequalizer.ι (Cover.index x✝.unop P) i
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
X : C
P : Cᵒᵖ ⥤ D
x✝ : (Cover J X)ᵒᵖ
i : (Cover.index x✝.unop P).L
⊢ Multiequalizer.lift (Cover.index x✝.unop P) (multiequalizer (Cover.index x✝.unop P))
        (fun i => Multiequalizer.ι (Cover.index x✝.unop P) i ≫ 𝟙 (P.obj (op i.Y)))
        (_ :
          ∀ (i : (Cover.index x✝.unop P).R),
            (fun i => Multiequalizer.ι (Cover.index x✝.unop P) i ≫ NatTrans.app (𝟙 P) (op i.Y))
                  (MulticospanIndex.fstTo (Cover.index x✝.unop P) i) ≫
                MulticospanIndex.fst (Cover.index x✝.unop P) i =
              (fun i => Multiequalizer.ι (Cover.index x✝.unop P) i ≫ NatTrans.app (𝟙 P) (op i.Y))
                  (MulticospanIndex.sndTo (Cover.index x✝.unop P) i) ≫
                MulticospanIndex.snd (Cover.index x✝.unop P) i) ≫
      Multiequalizer.ι (Cover.index x✝.unop P) i =
    𝟙 (multiequalizer (Cover.index x✝.unop P)) ≫ Multiequalizer.ι (Cover.index x✝.unop P) i
[PROOFSTEP]
simp only [limit.lift_π, Multifork.ofι_pt, Multifork.ofι_π_app, Category.id_comp]
[GOAL]
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
X : C
P : Cᵒᵖ ⥤ D
x✝ : (Cover J X)ᵒᵖ
i : (Cover.index x✝.unop P).L
⊢ Multiequalizer.ι (Cover.index x✝.unop P) i ≫ 𝟙 (P.obj (op i.Y)) = Multiequalizer.ι (Cover.index x✝.unop P) i
[PROOFSTEP]
erw [Category.comp_id]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
⊢ diagramNatTrans J 0 X = 0
[PROOFSTEP]
ext : 2
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
x✝ : (Cover J X)ᵒᵖ
⊢ NatTrans.app (diagramNatTrans J 0 X) x✝ = NatTrans.app 0 x✝
[PROOFSTEP]
refine' Multiequalizer.hom_ext _ _ _ (fun i => _)
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
x✝ : (Cover J X)ᵒᵖ
i : (Cover.index x✝.unop Q).L
⊢ NatTrans.app (diagramNatTrans J 0 X) x✝ ≫ Multiequalizer.ι (Cover.index x✝.unop Q) i =
    NatTrans.app 0 x✝ ≫ Multiequalizer.ι (Cover.index x✝.unop Q) i
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
x✝ : (Cover J X)ᵒᵖ
i : (Cover.index x✝.unop Q).L
⊢ Multiequalizer.lift (Cover.index x✝.unop Q) (multiequalizer (Cover.index x✝.unop P))
        (fun i => Multiequalizer.ι (Cover.index x✝.unop P) i ≫ 0)
        (_ :
          ∀ (i : (Cover.index x✝.unop Q).R),
            (fun i => Multiequalizer.ι (Cover.index x✝.unop P) i ≫ NatTrans.app 0 (op i.Y))
                  (MulticospanIndex.fstTo (Cover.index x✝.unop Q) i) ≫
                MulticospanIndex.fst (Cover.index x✝.unop Q) i =
              (fun i => Multiequalizer.ι (Cover.index x✝.unop P) i ≫ NatTrans.app 0 (op i.Y))
                  (MulticospanIndex.sndTo (Cover.index x✝.unop Q) i) ≫
                MulticospanIndex.snd (Cover.index x✝.unop Q) i) ≫
      Multiequalizer.ι (Cover.index x✝.unop Q) i =
    0 ≫ Multiequalizer.ι (Cover.index x✝.unop Q) i
[PROOFSTEP]
rw [zero_comp, Multiequalizer.lift_ι, comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
⊢ diagramNatTrans J (η ≫ γ) X = diagramNatTrans J η X ≫ diagramNatTrans J γ X
[PROOFSTEP]
ext : 2
[GOAL]
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
x✝ : (Cover J X)ᵒᵖ
⊢ NatTrans.app (diagramNatTrans J (η ≫ γ) X) x✝ = NatTrans.app (diagramNatTrans J η X ≫ diagramNatTrans J γ X) x✝
[PROOFSTEP]
refine' Multiequalizer.hom_ext _ _ _ (fun i => _)
[GOAL]
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
x✝ : (Cover J X)ᵒᵖ
i : (Cover.index x✝.unop R).L
⊢ NatTrans.app (diagramNatTrans J (η ≫ γ) X) x✝ ≫ Multiequalizer.ι (Cover.index x✝.unop R) i =
    NatTrans.app (diagramNatTrans J η X ≫ diagramNatTrans J γ X) x✝ ≫ Multiequalizer.ι (Cover.index x✝.unop R) i
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
x✝ : (Cover J X)ᵒᵖ
i : (Cover.index x✝.unop R).L
⊢ Multiequalizer.lift (Cover.index x✝.unop R) (multiequalizer (Cover.index x✝.unop P))
        (fun i => Multiequalizer.ι (Cover.index x✝.unop P) i ≫ NatTrans.app η (op i.Y) ≫ NatTrans.app γ (op i.Y))
        (_ :
          ∀ (i : (Cover.index x✝.unop R).R),
            (fun i => Multiequalizer.ι (Cover.index x✝.unop P) i ≫ NatTrans.app (η ≫ γ) (op i.Y))
                  (MulticospanIndex.fstTo (Cover.index x✝.unop R) i) ≫
                MulticospanIndex.fst (Cover.index x✝.unop R) i =
              (fun i => Multiequalizer.ι (Cover.index x✝.unop P) i ≫ NatTrans.app (η ≫ γ) (op i.Y))
                  (MulticospanIndex.sndTo (Cover.index x✝.unop R) i) ≫
                MulticospanIndex.snd (Cover.index x✝.unop R) i) ≫
      Multiequalizer.ι (Cover.index x✝.unop R) i =
    (Multiequalizer.lift (Cover.index x✝.unop Q) (multiequalizer (Cover.index x✝.unop P))
          (fun i => Multiequalizer.ι (Cover.index x✝.unop P) i ≫ NatTrans.app η (op i.Y))
          (_ :
            ∀ (i : (Cover.index x✝.unop Q).R),
              (fun i => Multiequalizer.ι (Cover.index x✝.unop P) i ≫ NatTrans.app η (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index x✝.unop Q) i) ≫
                  MulticospanIndex.fst (Cover.index x✝.unop Q) i =
                (fun i => Multiequalizer.ι (Cover.index x✝.unop P) i ≫ NatTrans.app η (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index x✝.unop Q) i) ≫
                  MulticospanIndex.snd (Cover.index x✝.unop Q) i) ≫
        Multiequalizer.lift (Cover.index x✝.unop R) (multiequalizer (Cover.index x✝.unop Q))
          (fun i => Multiequalizer.ι (Cover.index x✝.unop Q) i ≫ NatTrans.app γ (op i.Y))
          (_ :
            ∀ (i : (Cover.index x✝.unop R).R),
              (fun i => Multiequalizer.ι (Cover.index x✝.unop Q) i ≫ NatTrans.app γ (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index x✝.unop R) i) ≫
                  MulticospanIndex.fst (Cover.index x✝.unop R) i =
                (fun i => Multiequalizer.ι (Cover.index x✝.unop Q) i ≫ NatTrans.app γ (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index x✝.unop R) i) ≫
                  MulticospanIndex.snd (Cover.index x✝.unop R) i)) ≫
      Multiequalizer.ι (Cover.index x✝.unop R) i
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
⊢ ∀ (X : Cᵒᵖ),
    { obj := fun X => colimit (diagram J P X.unop),
            map := fun {X Y} f =>
              colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.map
        (𝟙 X) =
      𝟙
        ({ obj := fun X => colimit (diagram J P X.unop),
              map := fun {X Y} f =>
                colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.obj
          X)
[PROOFSTEP]
intro X
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
⊢ { obj := fun X => colimit (diagram J P X.unop),
          map := fun {X Y} f =>
            colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => colimit (diagram J P X.unop),
            map := fun {X Y} f =>
              colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.obj
        X)
[PROOFSTEP]
refine' colimit.hom_ext (fun S => _)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
⊢ colimit.ι (diagram J P X.unop) S ≫
      { obj := fun X => colimit (diagram J P X.unop),
            map := fun {X Y} f =>
              colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.map
        (𝟙 X) =
    colimit.ι (diagram J P X.unop) S ≫
      𝟙
        ({ obj := fun X => colimit (diagram J P X.unop),
              map := fun {X Y} f =>
                colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.obj
          X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
⊢ colimit.ι (diagram J P X.unop) S ≫
      colimMap (diagramPullback J P (𝟙 X.unop)) ≫ colimit.pre (diagram J P X.unop) (pullback J (𝟙 X.unop)).op =
    colimit.ι (diagram J P X.unop) S ≫ 𝟙 (colimit (diagram J P X.unop))
[PROOFSTEP]
simp only [diagramPullback_app, colimit.ι_pre, ι_colimMap_assoc, Category.comp_id]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
⊢ Multiequalizer.lift (Cover.index ((pullback J (𝟙 X.unop)).op.obj S).unop P) ((diagram J P X.unop).obj S)
        (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J (𝟙 X.unop)).op.obj S).unop P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
      colimit.ι (diagram J P X.unop) ((pullback J (𝟙 X.unop)).op.obj S) =
    colimit.ι (diagram J P X.unop) S
[PROOFSTEP]
let e := S.unop.pullbackId
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (𝟙 X.unop) ≅ S.unop := Cover.pullbackId S.unop
⊢ Multiequalizer.lift (Cover.index ((pullback J (𝟙 X.unop)).op.obj S).unop P) ((diagram J P X.unop).obj S)
        (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J (𝟙 X.unop)).op.obj S).unop P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
      colimit.ι (diagram J P X.unop) ((pullback J (𝟙 X.unop)).op.obj S) =
    colimit.ι (diagram J P X.unop) S
[PROOFSTEP]
dsimp only [Functor.op, pullback_obj]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (𝟙 X.unop) ≅ S.unop := Cover.pullbackId S.unop
⊢ Multiequalizer.lift (Cover.index (op (Cover.pullback S.unop (𝟙 X.unop))).unop P) ((diagram J P X.unop).obj S)
        (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J (𝟙 X.unop)).op.obj S).unop P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
      colimit.ι (diagram J P X.unop) (op (Cover.pullback S.unop (𝟙 X.unop))) =
    colimit.ι (diagram J P X.unop) S
[PROOFSTEP]
erw [← colimit.w _ e.inv.op, ← Category.assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (𝟙 X.unop) ≅ S.unop := Cover.pullbackId S.unop
⊢ (Multiequalizer.lift (Cover.index (op (Cover.pullback S.unop (𝟙 X.unop))).unop P) ((diagram J P X.unop).obj S)
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J (𝟙 X.unop)).op.obj S).unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
        (diagram J P X.unop).map e.inv.op) ≫
      colimit.ι (diagram J P X.unop) (op S.unop) =
    colimit.ι (diagram J P X.unop) S
[PROOFSTEP]
convert Category.id_comp (colimit.ι (diagram J P (unop X)) S)
[GOAL]
case h.e'_2.h.h.e'_6.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (𝟙 X.unop) ≅ S.unop := Cover.pullbackId S.unop
e_1✝ :
  (multiequalizer (Cover.index S.unop P) ⟶ colimit (diagram J P X.unop)) =
    ((diagram J P X.unop).obj S ⟶ colimit (diagram J P X.unop))
e_4✝ : (diagram J P X.unop).obj (op S.unop) = (diagram J P X.unop).obj S
⊢ Multiequalizer.lift (Cover.index (op (Cover.pullback S.unop (𝟙 X.unop))).unop P) ((diagram J P X.unop).obj S)
        (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J (𝟙 X.unop)).op.obj S).unop P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
      (diagram J P X.unop).map e.inv.op =
    𝟙 ((diagram J P X.unop).obj S)
[PROOFSTEP]
refine' Multiequalizer.hom_ext _ _ _ (fun I => _)
[GOAL]
case h.e'_2.h.h.e'_6.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (𝟙 X.unop) ≅ S.unop := Cover.pullbackId S.unop
e_1✝ :
  (multiequalizer (Cover.index S.unop P) ⟶ colimit (diagram J P X.unop)) =
    ((diagram J P X.unop).obj S ⟶ colimit (diagram J P X.unop))
e_4✝ : (diagram J P X.unop).obj (op S.unop) = (diagram J P X.unop).obj S
I : (Cover.index (op S.unop).unop P).L
⊢ (Multiequalizer.lift (Cover.index (op (Cover.pullback S.unop (𝟙 X.unop))).unop P) ((diagram J P X.unop).obj S)
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J (𝟙 X.unop)).op.obj S).unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
        (diagram J P X.unop).map e.inv.op) ≫
      Multiequalizer.ι (Cover.index (op S.unop).unop P) I =
    𝟙 ((diagram J P X.unop).obj S) ≫ Multiequalizer.ι (Cover.index (op S.unop).unop P) I
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_2.h.h.e'_6.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (𝟙 X.unop) ≅ S.unop := Cover.pullbackId S.unop
e_1✝ :
  (multiequalizer (Cover.index S.unop P) ⟶ colimit (diagram J P X.unop)) =
    ((diagram J P X.unop).obj S ⟶ colimit (diagram J P X.unop))
e_4✝ : (diagram J P X.unop).obj (op S.unop) = (diagram J P X.unop).obj S
I : (Cover.index (op S.unop).unop P).L
⊢ (Multiequalizer.lift (Cover.index (Cover.pullback S.unop (𝟙 X.unop)) P) (multiequalizer (Cover.index S.unop P))
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J (𝟙 X.unop)).op.obj S).unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
        Multiequalizer.lift (Cover.index S.unop P) (multiequalizer (Cover.index (Cover.pullback S.unop (𝟙 X.unop)) P))
          (fun I =>
            Multiequalizer.ι (Cover.index (Cover.pullback S.unop (𝟙 X.unop)) P)
              (Cover.Arrow.map I (Cover.pullbackId S.unop).inv))
          (_ :
            ∀ (I : (Cover.index S.unop P).R),
              Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop (𝟙 X.unop))).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op (Cover.pullback S.unop (𝟙 X.unop))).unop P)
                      (Cover.Relation.map I (Cover.pullbackId S.unop).inv.op.unop)) ≫
                  MulticospanIndex.fst (Cover.index (op (Cover.pullback S.unop (𝟙 X.unop))).unop P)
                    (Cover.Relation.map I (Cover.pullbackId S.unop).inv.op.unop) =
                Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop (𝟙 X.unop))).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op (Cover.pullback S.unop (𝟙 X.unop))).unop P)
                      (Cover.Relation.map I (Cover.pullbackId S.unop).inv.op.unop)) ≫
                  MulticospanIndex.snd (Cover.index (op (Cover.pullback S.unop (𝟙 X.unop))).unop P)
                    (Cover.Relation.map I (Cover.pullbackId S.unop).inv.op.unop))) ≫
      Multiequalizer.ι (Cover.index S.unop P) I =
    𝟙 (multiequalizer (Cover.index S.unop P)) ≫ Multiequalizer.ι (Cover.index S.unop P) I
[PROOFSTEP]
simp only [Multiequalizer.lift_ι, Category.id_comp, Category.assoc]
[GOAL]
case h.e'_2.h.h.e'_6.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (𝟙 X.unop) ≅ S.unop := Cover.pullbackId S.unop
e_1✝ :
  (multiequalizer (Cover.index S.unop P) ⟶ colimit (diagram J P X.unop)) =
    ((diagram J P X.unop).obj S ⟶ colimit (diagram J P X.unop))
e_4✝ : (diagram J P X.unop).obj (op S.unop) = (diagram J P X.unop).obj S
I : (Cover.index (op S.unop).unop P).L
⊢ Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base (Cover.Arrow.map I (Cover.pullbackId S.unop).inv)) =
    Multiequalizer.ι (Cover.index S.unop P) I
[PROOFSTEP]
dsimp [Cover.Arrow.map, Cover.Arrow.base]
[GOAL]
case h.e'_2.h.h.e'_6.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (𝟙 X.unop) ≅ S.unop := Cover.pullbackId S.unop
e_1✝ :
  (multiequalizer (Cover.index S.unop P) ⟶ colimit (diagram J P X.unop)) =
    ((diagram J P X.unop).obj S ⟶ colimit (diagram J P X.unop))
e_4✝ : (diagram J P X.unop).obj (op S.unop) = (diagram J P X.unop).obj S
I : (Cover.index (op S.unop).unop P).L
⊢ Multiequalizer.ι (Cover.index S.unop P)
      { Y := I.Y, f := I.f ≫ 𝟙 X.unop,
        hf :=
          (_ :
            (Cover.sieve (Cover.pullback S.unop (𝟙 X.unop))).arrows
              { Y := I.Y, f := I.f, hf := (_ : ((fun a => ↑a) (Cover.pullback S.unop (𝟙 X.unop))).arrows I.f) }.f) } =
    Multiequalizer.ι (Cover.index S.unop P) I
[PROOFSTEP]
cases I
[GOAL]
case h.e'_2.h.h.e'_6.h.mk
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (𝟙 X.unop) ≅ S.unop := Cover.pullbackId S.unop
e_1✝ :
  (multiequalizer (Cover.index S.unop P) ⟶ colimit (diagram J P X.unop)) =
    ((diagram J P X.unop).obj S ⟶ colimit (diagram J P X.unop))
e_4✝ : (diagram J P X.unop).obj (op S.unop) = (diagram J P X.unop).obj S
Y✝ : C
f✝ : Y✝ ⟶ X.unop
hf✝ : (Cover.sieve (op S.unop).unop).arrows f✝
⊢ Multiequalizer.ι (Cover.index S.unop P)
      { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f ≫ 𝟙 X.unop,
        hf :=
          (_ :
            (Cover.sieve (Cover.pullback S.unop (𝟙 X.unop))).arrows
              { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f,
                  hf :=
                    (_ :
                      ((fun a => ↑a) (Cover.pullback S.unop (𝟙 X.unop))).arrows
                        { Y := Y✝, f := f✝, hf := hf✝ }.f) }.f) } =
    Multiequalizer.ι (Cover.index S.unop P) { Y := Y✝, f := f✝, hf := hf✝ }
[PROOFSTEP]
congr
[GOAL]
case h.e'_2.h.h.e'_6.h.mk.h.e_5.h.e_f
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (𝟙 X.unop) ≅ S.unop := Cover.pullbackId S.unop
e_1✝ :
  (multiequalizer (Cover.index S.unop P) ⟶ colimit (diagram J P X.unop)) =
    ((diagram J P X.unop).obj S ⟶ colimit (diagram J P X.unop))
e_4✝ : (diagram J P X.unop).obj (op S.unop) = (diagram J P X.unop).obj S
Y✝ : C
f✝ : Y✝ ⟶ X.unop
hf✝ : (Cover.sieve (op S.unop).unop).arrows f✝
⊢ { Y := Y✝, f := f✝, hf := hf✝ }.f ≫ 𝟙 X.unop = f✝
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
⊢ ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun X => colimit (diagram J P X.unop),
            map := fun {X Y} f =>
              colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.map
        (f ≫ g) =
      { obj := fun X => colimit (diagram J P X.unop),
              map := fun {X Y} f =>
                colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.map
          f ≫
        { obj := fun X => colimit (diagram J P X.unop),
              map := fun {X Y} f =>
                colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.map
          g
[PROOFSTEP]
intro X Y Z f g
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ { obj := fun X => colimit (diagram J P X.unop),
          map := fun {X Y} f =>
            colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.map
      (f ≫ g) =
    { obj := fun X => colimit (diagram J P X.unop),
            map := fun {X Y} f =>
              colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.map
        f ≫
      { obj := fun X => colimit (diagram J P X.unop),
            map := fun {X Y} f =>
              colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.map
        g
[PROOFSTEP]
refine' colimit.hom_ext (fun S => _)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
⊢ colimit.ι (diagram J P X.unop) S ≫
      { obj := fun X => colimit (diagram J P X.unop),
            map := fun {X Y} f =>
              colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.map
        (f ≫ g) =
    colimit.ι (diagram J P X.unop) S ≫
      { obj := fun X => colimit (diagram J P X.unop),
              map := fun {X Y} f =>
                colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.map
          f ≫
        { obj := fun X => colimit (diagram J P X.unop),
              map := fun {X Y} f =>
                colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }.map
          g
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
⊢ colimit.ι (diagram J P X.unop) S ≫
      colimMap (diagramPullback J P (g.unop ≫ f.unop)) ≫
        colimit.pre (diagram J P Z.unop) (pullback J (g.unop ≫ f.unop)).op =
    colimit.ι (diagram J P X.unop) S ≫
      (colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op) ≫
        colimMap (diagramPullback J P g.unop) ≫ colimit.pre (diagram J P Z.unop) (pullback J g.unop).op
[PROOFSTEP]
simp only [diagramPullback_app, colimit.ι_pre_assoc, colimit.ι_pre, ι_colimMap_assoc, Category.assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
⊢ Multiequalizer.lift (Cover.index ((pullback J (g.unop ≫ f.unop)).op.obj S).unop P) ((diagram J P X.unop).obj S)
        (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J (g.unop ≫ f.unop)).op.obj S).unop P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
      colimit.ι (diagram J P Z.unop) ((pullback J (g.unop ≫ f.unop)).op.obj S) =
    Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj S).unop P) ((diagram J P X.unop).obj S)
        (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J f.unop).op.obj S).unop P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
      Multiequalizer.lift (Cover.index ((pullback J g.unop).op.obj ((pullback J f.unop).op.obj S)).unop P)
          ((diagram J P Y.unop).obj ((pullback J f.unop).op.obj S))
          (fun I => Multiequalizer.ι (Cover.index ((pullback J f.unop).op.obj S).unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J g.unop).op.obj ((pullback J f.unop).op.obj S)).unop P).R),
              Multiequalizer.ι (Cover.index ((pullback J f.unop).op.obj S).unop P)
                    (MulticospanIndex.fstTo (Cover.index ((pullback J f.unop).op.obj S).unop P)
                      (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index ((pullback J f.unop).op.obj S).unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index ((pullback J f.unop).op.obj S).unop P)
                    (MulticospanIndex.sndTo (Cover.index ((pullback J f.unop).op.obj S).unop P)
                      (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index ((pullback J f.unop).op.obj S).unop P) (Cover.Relation.base I)) ≫
        colimit.ι (diagram J P Z.unop) ((pullback J g.unop).op.obj ((pullback J f.unop).op.obj S))
[PROOFSTEP]
let e := S.unop.pullbackComp g.unop f.unop
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (g.unop ≫ f.unop) ≅ Cover.pullback (Cover.pullback S.unop f.unop) g.unop :=
  Cover.pullbackComp S.unop g.unop f.unop
⊢ Multiequalizer.lift (Cover.index ((pullback J (g.unop ≫ f.unop)).op.obj S).unop P) ((diagram J P X.unop).obj S)
        (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J (g.unop ≫ f.unop)).op.obj S).unop P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
      colimit.ι (diagram J P Z.unop) ((pullback J (g.unop ≫ f.unop)).op.obj S) =
    Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj S).unop P) ((diagram J P X.unop).obj S)
        (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J f.unop).op.obj S).unop P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
      Multiequalizer.lift (Cover.index ((pullback J g.unop).op.obj ((pullback J f.unop).op.obj S)).unop P)
          ((diagram J P Y.unop).obj ((pullback J f.unop).op.obj S))
          (fun I => Multiequalizer.ι (Cover.index ((pullback J f.unop).op.obj S).unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J g.unop).op.obj ((pullback J f.unop).op.obj S)).unop P).R),
              Multiequalizer.ι (Cover.index ((pullback J f.unop).op.obj S).unop P)
                    (MulticospanIndex.fstTo (Cover.index ((pullback J f.unop).op.obj S).unop P)
                      (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index ((pullback J f.unop).op.obj S).unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index ((pullback J f.unop).op.obj S).unop P)
                    (MulticospanIndex.sndTo (Cover.index ((pullback J f.unop).op.obj S).unop P)
                      (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index ((pullback J f.unop).op.obj S).unop P) (Cover.Relation.base I)) ≫
        colimit.ι (diagram J P Z.unop) ((pullback J g.unop).op.obj ((pullback J f.unop).op.obj S))
[PROOFSTEP]
dsimp only [Functor.op, pullback_obj]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (g.unop ≫ f.unop) ≅ Cover.pullback (Cover.pullback S.unop f.unop) g.unop :=
  Cover.pullbackComp S.unop g.unop f.unop
⊢ Multiequalizer.lift (Cover.index (op (Cover.pullback S.unop (g.unop ≫ f.unop))).unop P) ((diagram J P X.unop).obj S)
        (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J (g.unop ≫ f.unop)).op.obj S).unop P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
      colimit.ι (diagram J P Z.unop) (op (Cover.pullback S.unop (g.unop ≫ f.unop))) =
    Multiequalizer.lift (Cover.index (op (Cover.pullback S.unop f.unop)).unop P) ((diagram J P X.unop).obj S)
        (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J f.unop).op.obj S).unop P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
      Multiequalizer.lift (Cover.index (op (Cover.pullback (op (Cover.pullback S.unop f.unop)).unop g.unop)).unop P)
          ((diagram J P Y.unop).obj (op (Cover.pullback S.unop f.unop)))
          (fun I => Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J g.unop).op.obj (op (Cover.pullback S.unop f.unop))).unop P).R),
              Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                      (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                      (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (Cover.Relation.base I)) ≫
        colimit.ι (diagram J P Z.unop) (op (Cover.pullback (op (Cover.pullback S.unop f.unop)).unop g.unop))
[PROOFSTEP]
erw [← colimit.w _ e.inv.op, ← Category.assoc, ← Category.assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (g.unop ≫ f.unop) ≅ Cover.pullback (Cover.pullback S.unop f.unop) g.unop :=
  Cover.pullbackComp S.unop g.unop f.unop
⊢ (Multiequalizer.lift (Cover.index (op (Cover.pullback S.unop (g.unop ≫ f.unop))).unop P) ((diagram J P X.unop).obj S)
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J (g.unop ≫ f.unop)).op.obj S).unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
        (diagram J P Z.unop).map e.inv.op) ≫
      colimit.ι (diagram J P Z.unop) (op (Cover.pullback (Cover.pullback S.unop f.unop) g.unop)) =
    (Multiequalizer.lift (Cover.index (op (Cover.pullback S.unop f.unop)).unop P) ((diagram J P X.unop).obj S)
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj S).unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
        Multiequalizer.lift (Cover.index (op (Cover.pullback (op (Cover.pullback S.unop f.unop)).unop g.unop)).unop P)
          ((diagram J P Y.unop).obj (op (Cover.pullback S.unop f.unop)))
          (fun I => Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J g.unop).op.obj (op (Cover.pullback S.unop f.unop))).unop P).R),
              Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                      (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                      (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (Cover.Relation.base I))) ≫
      colimit.ι (diagram J P Z.unop) (op (Cover.pullback (op (Cover.pullback S.unop f.unop)).unop g.unop))
[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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (g.unop ≫ f.unop) ≅ Cover.pullback (Cover.pullback S.unop f.unop) g.unop :=
  Cover.pullbackComp S.unop g.unop f.unop
⊢ Multiequalizer.lift (Cover.index (op (Cover.pullback S.unop (g.unop ≫ f.unop))).unop P) ((diagram J P X.unop).obj S)
        (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J (g.unop ≫ f.unop)).op.obj S).unop P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
      (diagram J P Z.unop).map e.inv.op =
    Multiequalizer.lift (Cover.index (op (Cover.pullback S.unop f.unop)).unop P) ((diagram J P X.unop).obj S)
        (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J f.unop).op.obj S).unop P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
      Multiequalizer.lift (Cover.index (op (Cover.pullback (op (Cover.pullback S.unop f.unop)).unop g.unop)).unop P)
        ((diagram J P Y.unop).obj (op (Cover.pullback S.unop f.unop)))
        (fun I => Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J g.unop).op.obj (op (Cover.pullback S.unop f.unop))).unop P).R),
            Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                  (MulticospanIndex.fstTo (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index (op (Cover.pullback S.unop f.unop)).unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                  (MulticospanIndex.sndTo (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index (op (Cover.pullback S.unop f.unop)).unop P) (Cover.Relation.base I))
[PROOFSTEP]
refine' Multiequalizer.hom_ext _ _ _ (fun I => _)
[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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (g.unop ≫ f.unop) ≅ Cover.pullback (Cover.pullback S.unop f.unop) g.unop :=
  Cover.pullbackComp S.unop g.unop f.unop
I : (Cover.index (op (Cover.pullback (Cover.pullback S.unop f.unop) g.unop)).unop P).L
⊢ (Multiequalizer.lift (Cover.index (op (Cover.pullback S.unop (g.unop ≫ f.unop))).unop P) ((diagram J P X.unop).obj S)
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J (g.unop ≫ f.unop)).op.obj S).unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
        (diagram J P Z.unop).map e.inv.op) ≫
      Multiequalizer.ι (Cover.index (op (Cover.pullback (Cover.pullback S.unop f.unop) g.unop)).unop P) I =
    (Multiequalizer.lift (Cover.index (op (Cover.pullback S.unop f.unop)).unop P) ((diagram J P X.unop).obj S)
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj S).unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
        Multiequalizer.lift (Cover.index (op (Cover.pullback (op (Cover.pullback S.unop f.unop)).unop g.unop)).unop P)
          ((diagram J P Y.unop).obj (op (Cover.pullback S.unop f.unop)))
          (fun I => Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J g.unop).op.obj (op (Cover.pullback S.unop f.unop))).unop P).R),
              Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                      (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                      (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (Cover.Relation.base I))) ≫
      Multiequalizer.ι (Cover.index (op (Cover.pullback (Cover.pullback S.unop f.unop) g.unop)).unop P) I
[PROOFSTEP]
dsimp
[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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (g.unop ≫ f.unop) ≅ Cover.pullback (Cover.pullback S.unop f.unop) g.unop :=
  Cover.pullbackComp S.unop g.unop f.unop
I : (Cover.index (op (Cover.pullback (Cover.pullback S.unop f.unop) g.unop)).unop P).L
⊢ (Multiequalizer.lift (Cover.index (Cover.pullback S.unop (g.unop ≫ f.unop)) P) (multiequalizer (Cover.index S.unop P))
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J (g.unop ≫ f.unop)).op.obj S).unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
        Multiequalizer.lift (Cover.index (Cover.pullback (Cover.pullback S.unop f.unop) g.unop) P)
          (multiequalizer (Cover.index (Cover.pullback S.unop (g.unop ≫ f.unop)) P))
          (fun I =>
            Multiequalizer.ι (Cover.index (Cover.pullback S.unop (g.unop ≫ f.unop)) P)
              (Cover.Arrow.map I (Cover.pullbackComp S.unop g.unop f.unop).inv))
          (_ :
            ∀ (I : (Cover.index (op (Cover.pullback (Cover.pullback S.unop f.unop) g.unop)).unop P).R),
              Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop (g.unop ≫ f.unop))).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op (Cover.pullback S.unop (g.unop ≫ f.unop))).unop P)
                      (Cover.Relation.map I (Cover.pullbackComp S.unop g.unop f.unop).inv.op.unop)) ≫
                  MulticospanIndex.fst (Cover.index (op (Cover.pullback S.unop (g.unop ≫ f.unop))).unop P)
                    (Cover.Relation.map I (Cover.pullbackComp S.unop g.unop f.unop).inv.op.unop) =
                Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop (g.unop ≫ f.unop))).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op (Cover.pullback S.unop (g.unop ≫ f.unop))).unop P)
                      (Cover.Relation.map I (Cover.pullbackComp S.unop g.unop f.unop).inv.op.unop)) ≫
                  MulticospanIndex.snd (Cover.index (op (Cover.pullback S.unop (g.unop ≫ f.unop))).unop P)
                    (Cover.Relation.map I (Cover.pullbackComp S.unop g.unop f.unop).inv.op.unop))) ≫
      Multiequalizer.ι (Cover.index (Cover.pullback (Cover.pullback S.unop f.unop) g.unop) P) I =
    (Multiequalizer.lift (Cover.index (Cover.pullback S.unop f.unop) P) (multiequalizer (Cover.index S.unop P))
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj S).unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I)) ≫
        Multiequalizer.lift (Cover.index (Cover.pullback (Cover.pullback S.unop f.unop) g.unop) P)
          (multiequalizer (Cover.index (Cover.pullback S.unop f.unop) P))
          (fun I => Multiequalizer.ι (Cover.index (Cover.pullback S.unop f.unop) P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J g.unop).op.obj (op (Cover.pullback S.unop f.unop))).unop P).R),
              Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                      (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                      (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index (op (Cover.pullback S.unop f.unop)).unop P)
                    (Cover.Relation.base I))) ≫
      Multiequalizer.ι (Cover.index (Cover.pullback (Cover.pullback S.unop f.unop) g.unop) P) I
[PROOFSTEP]
simp only [Multiequalizer.lift_ι, Category.assoc]
[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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (g.unop ≫ f.unop) ≅ Cover.pullback (Cover.pullback S.unop f.unop) g.unop :=
  Cover.pullbackComp S.unop g.unop f.unop
I : (Cover.index (op (Cover.pullback (Cover.pullback S.unop f.unop) g.unop)).unop P).L
⊢ Multiequalizer.ι (Cover.index S.unop P)
      (Cover.Arrow.base (Cover.Arrow.map I (Cover.pullbackComp S.unop g.unop f.unop).inv)) =
    Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base (Cover.Arrow.base I))
[PROOFSTEP]
cases I
[GOAL]
case e_a.mk
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (g.unop ≫ f.unop) ≅ Cover.pullback (Cover.pullback S.unop f.unop) g.unop :=
  Cover.pullbackComp S.unop g.unop f.unop
Y✝ : C
f✝ : Y✝ ⟶ Z.unop
hf✝ : (Cover.sieve (op (Cover.pullback (Cover.pullback S.unop f.unop) g.unop)).unop).arrows f✝
⊢ Multiequalizer.ι (Cover.index S.unop P)
      (Cover.Arrow.base
        (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } (Cover.pullbackComp S.unop g.unop f.unop).inv)) =
    Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base (Cover.Arrow.base { Y := Y✝, f := f✝, hf := hf✝ }))
[PROOFSTEP]
dsimp only [Cover.Arrow.base, Cover.Arrow.map]
[GOAL]
case e_a.mk
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (g.unop ≫ f.unop) ≅ Cover.pullback (Cover.pullback S.unop f.unop) g.unop :=
  Cover.pullbackComp S.unop g.unop f.unop
Y✝ : C
f✝ : Y✝ ⟶ Z.unop
hf✝ : (Cover.sieve (op (Cover.pullback (Cover.pullback S.unop f.unop) g.unop)).unop).arrows f✝
⊢ Multiequalizer.ι (Cover.index S.unop P)
      { Y := Y✝, f := f✝ ≫ g.unop ≫ f.unop,
        hf :=
          (_ :
            (Cover.sieve (Cover.pullback S.unop (g.unop ≫ f.unop))).arrows
              { Y := Y✝, f := f✝,
                  hf :=
                    (_ :
                      ((fun a => ↑a) (Cover.pullback S.unop (g.unop ≫ f.unop))).arrows
                        { Y := Y✝, f := f✝, hf := hf✝ }.f) }.f) } =
    Multiequalizer.ι (Cover.index S.unop P)
      { Y := Y✝, f := (f✝ ≫ g.unop) ≫ f.unop,
        hf :=
          (_ :
            (Cover.sieve (Cover.pullback S.unop f.unop)).arrows
              { Y := Y✝, f := f✝ ≫ g.unop,
                  hf :=
                    (_ :
                      (Cover.sieve (Cover.pullback (Cover.pullback S.unop f.unop) g.unop)).arrows
                        { Y := Y✝, f := f✝, hf := hf✝ }.f) }.f) }
[PROOFSTEP]
congr 2
[GOAL]
case e_a.mk.h.e_5.h.e_f
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (Cover J X.unop)ᵒᵖ
e : Cover.pullback S.unop (g.unop ≫ f.unop) ≅ Cover.pullback (Cover.pullback S.unop f.unop) g.unop :=
  Cover.pullbackComp S.unop g.unop f.unop
Y✝ : C
f✝ : Y✝ ⟶ Z.unop
hf✝ : (Cover.sieve (op (Cover.pullback (Cover.pullback S.unop f.unop) g.unop)).unop).arrows f✝
⊢ f✝ ≫ g.unop ≫ f.unop = (f✝ ≫ g.unop) ≫ f.unop
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    (plusObj J P).map f ≫ (fun X => colimMap (diagramNatTrans J η X.unop)) Y =
      (fun X => colimMap (diagramNatTrans J η X.unop)) X ≫ (plusObj J Q).map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (plusObj J P).map f ≫ (fun X => colimMap (diagramNatTrans J η X.unop)) Y =
    (fun X => colimMap (diagramNatTrans J η X.unop)) X ≫ (plusObj J Q).map f
[PROOFSTEP]
dsimp [plusObj]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op) ≫
      colimMap (diagramNatTrans J η Y.unop) =
    colimMap (diagramNatTrans J η X.unop) ≫
      colimMap (diagramPullback J Q f.unop) ≫ colimit.pre (diagram J Q Y.unop) (pullback J f.unop).op
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (Cover J X.unop)ᵒᵖ
⊢ colimit.ι (diagram J P X.unop) j✝ ≫
      (colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op) ≫
        colimMap (diagramNatTrans J η Y.unop) =
    colimit.ι (diagram J P X.unop) j✝ ≫
      colimMap (diagramNatTrans J η X.unop) ≫
        colimMap (diagramPullback J Q f.unop) ≫ colimit.pre (diagram J Q Y.unop) (pullback J f.unop).op
[PROOFSTEP]
simp only [diagramPullback_app, ι_colimMap, colimit.ι_pre_assoc, colimit.ι_pre, ι_colimMap_assoc, Category.assoc]
[GOAL]
case w
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (Cover J X.unop)ᵒᵖ
⊢ Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj j✝).unop P) ((diagram J P X.unop).obj j✝)
        (fun I => Multiequalizer.ι (Cover.index j✝.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J f.unop).op.obj j✝).unop P).R),
            Multiequalizer.ι (Cover.index j✝.unop P)
                  (MulticospanIndex.fstTo (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index j✝.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index j✝.unop P)
                  (MulticospanIndex.sndTo (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
      NatTrans.app (diagramNatTrans J η Y.unop) ((pullback J f.unop).op.obj j✝) ≫
        colimit.ι (diagram J Q Y.unop) ((pullback J f.unop).op.obj j✝) =
    NatTrans.app (diagramNatTrans J η X.unop) j✝ ≫
      Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj j✝).unop Q) ((diagram J Q X.unop).obj j✝)
          (fun I => Multiequalizer.ι (Cover.index j✝.unop Q) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj j✝).unop Q).R),
              Multiequalizer.ι (Cover.index j✝.unop Q)
                    (MulticospanIndex.fstTo (Cover.index j✝.unop Q) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index j✝.unop Q) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index j✝.unop Q)
                    (MulticospanIndex.sndTo (Cover.index j✝.unop Q) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index j✝.unop Q) (Cover.Relation.base I)) ≫
        colimit.ι (diagram J Q Y.unop) ((pullback J f.unop).op.obj j✝)
[PROOFSTEP]
simp_rw [← Category.assoc]
[GOAL]
case w
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (Cover J X.unop)ᵒᵖ
⊢ (Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj j✝).unop P) ((diagram J P X.unop).obj j✝)
          (fun I => Multiequalizer.ι (Cover.index j✝.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj j✝).unop P).R),
              Multiequalizer.ι (Cover.index j✝.unop P)
                    (MulticospanIndex.fstTo (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index j✝.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index j✝.unop P)
                    (MulticospanIndex.sndTo (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
        NatTrans.app (diagramNatTrans J η Y.unop) ((pullback J f.unop).op.obj j✝)) ≫
      colimit.ι (diagram J Q Y.unop) ((pullback J f.unop).op.obj j✝) =
    (NatTrans.app (diagramNatTrans J η X.unop) j✝ ≫
        Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj j✝).unop Q) ((diagram J Q X.unop).obj j✝)
          (fun I => Multiequalizer.ι (Cover.index j✝.unop Q) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj j✝).unop Q).R),
              Multiequalizer.ι (Cover.index j✝.unop Q)
                    (MulticospanIndex.fstTo (Cover.index j✝.unop Q) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index j✝.unop Q) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index j✝.unop Q)
                    (MulticospanIndex.sndTo (Cover.index j✝.unop Q) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index j✝.unop Q) (Cover.Relation.base I))) ≫
      colimit.ι (diagram J Q Y.unop) ((pullback J f.unop).op.obj j✝)
[PROOFSTEP]
congr 1
[GOAL]
case w.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (Cover J X.unop)ᵒᵖ
⊢ Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj j✝).unop P) ((diagram J P X.unop).obj j✝)
        (fun I => Multiequalizer.ι (Cover.index j✝.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J f.unop).op.obj j✝).unop P).R),
            Multiequalizer.ι (Cover.index j✝.unop P)
                  (MulticospanIndex.fstTo (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index j✝.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index j✝.unop P)
                  (MulticospanIndex.sndTo (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
      NatTrans.app (diagramNatTrans J η Y.unop) ((pullback J f.unop).op.obj j✝) =
    NatTrans.app (diagramNatTrans J η X.unop) j✝ ≫
      Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj j✝).unop Q) ((diagram J Q X.unop).obj j✝)
        (fun I => Multiequalizer.ι (Cover.index j✝.unop Q) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J f.unop).op.obj j✝).unop Q).R),
            Multiequalizer.ι (Cover.index j✝.unop Q)
                  (MulticospanIndex.fstTo (Cover.index j✝.unop Q) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index j✝.unop Q) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index j✝.unop Q)
                  (MulticospanIndex.sndTo (Cover.index j✝.unop Q) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index j✝.unop Q) (Cover.Relation.base I))
[PROOFSTEP]
exact Multiequalizer.hom_ext _ _ _ (fun I => by dsimp; simp)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (Cover J X.unop)ᵒᵖ
I : (Cover.index ((pullback J f.unop).op.obj j✝).unop Q).L
⊢ (Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj j✝).unop P) ((diagram J P X.unop).obj j✝)
          (fun I => Multiequalizer.ι (Cover.index j✝.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj j✝).unop P).R),
              Multiequalizer.ι (Cover.index j✝.unop P)
                    (MulticospanIndex.fstTo (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index j✝.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index j✝.unop P)
                    (MulticospanIndex.sndTo (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
        NatTrans.app (diagramNatTrans J η Y.unop) ((pullback J f.unop).op.obj j✝)) ≫
      Multiequalizer.ι (Cover.index ((pullback J f.unop).op.obj j✝).unop Q) I =
    (NatTrans.app (diagramNatTrans J η X.unop) j✝ ≫
        Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj j✝).unop Q) ((diagram J Q X.unop).obj j✝)
          (fun I => Multiequalizer.ι (Cover.index j✝.unop Q) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj j✝).unop Q).R),
              Multiequalizer.ι (Cover.index j✝.unop Q)
                    (MulticospanIndex.fstTo (Cover.index j✝.unop Q) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index j✝.unop Q) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index j✝.unop Q)
                    (MulticospanIndex.sndTo (Cover.index j✝.unop Q) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index j✝.unop Q) (Cover.Relation.base I))) ≫
      Multiequalizer.ι (Cover.index ((pullback J f.unop).op.obj j✝).unop Q) I
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (Cover J X.unop)ᵒᵖ
I : (Cover.index ((pullback J f.unop).op.obj j✝).unop Q).L
⊢ (Multiequalizer.lift (Cover.index (Cover.pullback j✝.unop f.unop) P) (multiequalizer (Cover.index j✝.unop P))
          (fun I => Multiequalizer.ι (Cover.index j✝.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj j✝).unop P).R),
              Multiequalizer.ι (Cover.index j✝.unop P)
                    (MulticospanIndex.fstTo (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index j✝.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index j✝.unop P)
                    (MulticospanIndex.sndTo (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index j✝.unop P) (Cover.Relation.base I)) ≫
        Multiequalizer.lift (Cover.index (Cover.pullback j✝.unop f.unop) Q)
          (multiequalizer (Cover.index (Cover.pullback j✝.unop f.unop) P))
          (fun i => Multiequalizer.ι (Cover.index (Cover.pullback j✝.unop f.unop) P) i ≫ NatTrans.app η (op i.Y))
          (_ :
            ∀ (i : (Cover.index (op (Cover.pullback j✝.unop f.unop)).unop Q).R),
              (fun i =>
                      Multiequalizer.ι (Cover.index (op (Cover.pullback j✝.unop f.unop)).unop P) i ≫
                        NatTrans.app η (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index (op (Cover.pullback j✝.unop f.unop)).unop Q) i) ≫
                  MulticospanIndex.fst (Cover.index (op (Cover.pullback j✝.unop f.unop)).unop Q) i =
                (fun i =>
                      Multiequalizer.ι (Cover.index (op (Cover.pullback j✝.unop f.unop)).unop P) i ≫
                        NatTrans.app η (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index (op (Cover.pullback j✝.unop f.unop)).unop Q) i) ≫
                  MulticospanIndex.snd (Cover.index (op (Cover.pullback j✝.unop f.unop)).unop Q) i)) ≫
      Multiequalizer.ι (Cover.index (Cover.pullback j✝.unop f.unop) Q) I =
    (Multiequalizer.lift (Cover.index j✝.unop Q) (multiequalizer (Cover.index j✝.unop P))
          (fun i => Multiequalizer.ι (Cover.index j✝.unop P) i ≫ NatTrans.app η (op i.Y))
          (_ :
            ∀ (i : (Cover.index j✝.unop Q).R),
              (fun i => Multiequalizer.ι (Cover.index j✝.unop P) i ≫ NatTrans.app η (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index j✝.unop Q) i) ≫
                  MulticospanIndex.fst (Cover.index j✝.unop Q) i =
                (fun i => Multiequalizer.ι (Cover.index j✝.unop P) i ≫ NatTrans.app η (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index j✝.unop Q) i) ≫
                  MulticospanIndex.snd (Cover.index j✝.unop Q) i) ≫
        Multiequalizer.lift (Cover.index (Cover.pullback j✝.unop f.unop) Q) (multiequalizer (Cover.index j✝.unop Q))
          (fun I => Multiequalizer.ι (Cover.index j✝.unop Q) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj j✝).unop Q).R),
              Multiequalizer.ι (Cover.index j✝.unop Q)
                    (MulticospanIndex.fstTo (Cover.index j✝.unop Q) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index j✝.unop Q) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index j✝.unop Q)
                    (MulticospanIndex.sndTo (Cover.index j✝.unop Q) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index j✝.unop Q) (Cover.Relation.base I))) ≫
      Multiequalizer.ι (Cover.index (Cover.pullback j✝.unop f.unop) Q) I
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
⊢ plusMap J (𝟙 P) = 𝟙 (plusObj J P)
[PROOFSTEP]
ext : 2
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ NatTrans.app (plusMap J (𝟙 P)) x✝ = NatTrans.app (𝟙 (plusObj J P)) x✝
[PROOFSTEP]
dsimp only [plusMap, plusObj]
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ colimMap (diagramNatTrans J (𝟙 P) x✝.unop) =
    NatTrans.app
      (𝟙
        (Functor.mk
          { obj := fun X => colimit (diagram J P X.unop),
            map := fun {X Y} f =>
              colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }))
      x✝
[PROOFSTEP]
rw [J.diagramNatTrans_id, NatTrans.id_app]
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ colimMap (𝟙 (diagram J P x✝.unop)) =
    𝟙
      ((Functor.mk
            { obj := fun X => colimit (diagram J P X.unop),
              map := fun {X Y} f =>
                colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }).obj
        x✝)
[PROOFSTEP]
ext
[GOAL]
case w.h.w
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
j✝ : (Cover J x✝.unop)ᵒᵖ
⊢ colimit.ι (diagram J P x✝.unop) j✝ ≫ colimMap (𝟙 (diagram J P x✝.unop)) =
    colimit.ι (diagram J P x✝.unop) j✝ ≫
      𝟙
        ((Functor.mk
              { obj := fun X => colimit (diagram J P X.unop),
                map := fun {X Y} f =>
                  colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op }).obj
          x✝)
[PROOFSTEP]
dsimp
[GOAL]
case w.h.w
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
j✝ : (Cover J x✝.unop)ᵒᵖ
⊢ colimit.ι (diagram J P x✝.unop) j✝ ≫ colimMap (𝟙 (diagram J P x✝.unop)) =
    colimit.ι (diagram J P x✝.unop) j✝ ≫ 𝟙 (colimit (diagram J P x✝.unop))
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{max v u, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
⊢ plusMap J 0 = 0
[PROOFSTEP]
ext : 2
[GOAL]
case w.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{max v u, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ NatTrans.app (plusMap J 0) x✝ = NatTrans.app 0 x✝
[PROOFSTEP]
refine' colimit.hom_ext (fun S => _)
[GOAL]
case w.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{max v u, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
S : (Cover J x✝.unop)ᵒᵖ
⊢ colimit.ι (diagram J P x✝.unop) S ≫ NatTrans.app (plusMap J 0) x✝ =
    colimit.ι (diagram J P x✝.unop) S ≫ NatTrans.app 0 x✝
[PROOFSTEP]
erw [comp_zero, colimit.ι_map, J.diagramNatTrans_zero, zero_comp]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
⊢ plusMap J (η ≫ γ) = plusMap J η ≫ plusMap J γ
[PROOFSTEP]
ext : 2
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
x✝ : Cᵒᵖ
⊢ NatTrans.app (plusMap J (η ≫ γ)) x✝ = NatTrans.app (plusMap J η ≫ plusMap J γ) x✝
[PROOFSTEP]
refine' colimit.hom_ext (fun S => _)
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
x✝ : Cᵒᵖ
S : (Cover J x✝.unop)ᵒᵖ
⊢ colimit.ι (diagram J P x✝.unop) S ≫ NatTrans.app (plusMap J (η ≫ γ)) x✝ =
    colimit.ι (diagram J P x✝.unop) S ≫ NatTrans.app (plusMap J η ≫ plusMap J γ) x✝
[PROOFSTEP]
simp [plusMap, J.diagramNatTrans_comp]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    P.map f ≫ (fun X => Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P X.unop) (op ⊤)) Y =
      (fun X => Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P X.unop) (op ⊤)) X ≫ (plusObj J P).map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ P.map f ≫ (fun X => Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P X.unop) (op ⊤)) Y =
    (fun X => Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P X.unop) (op ⊤)) X ≫ (plusObj J P).map f
[PROOFSTEP]
dsimp [plusObj]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ P.map f ≫ Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P Y.unop) (op ⊤) =
    (Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P X.unop) (op ⊤)) ≫
      colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op
[PROOFSTEP]
delta Cover.toMultiequalizer
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ P.map f ≫
      Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op Y.unop)) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        colimit.ι (diagram J P Y.unop) (op ⊤) =
    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X.unop)) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        colimit.ι (diagram J P X.unop) (op ⊤)) ≫
      colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op
[PROOFSTEP]
simp only [diagramPullback_app, colimit.ι_pre, ι_colimMap_assoc, Category.assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ P.map f ≫
      Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op Y.unop)) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        colimit.ι (diagram J P Y.unop) (op ⊤) =
    Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X.unop)) (fun I => P.map I.f.op)
        (_ :
          ∀ (I : (Cover.index ⊤ P).R),
            (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.fst (Cover.index ⊤ P) I =
              (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
      Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj (op ⊤)).unop P) ((diagram J P X.unop).obj (op ⊤))
          (fun I => Multiequalizer.ι (Cover.index (op ⊤).unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj (op ⊤)).unop P).R),
              Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index (op ⊤).unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
        colimit.ι (diagram J P Y.unop) ((pullback J f.unop).op.obj (op ⊤))
[PROOFSTEP]
dsimp only [Functor.op, unop_op]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ P.map f ≫
      Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op Y.unop)) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        colimit.ι (diagram J P Y.unop) (op ⊤) =
    Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X.unop)) (fun I => P.map I.f.op)
        (_ :
          ∀ (I : (Cover.index ⊤ P).R),
            (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.fst (Cover.index ⊤ P) I =
              (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
      Multiequalizer.lift (Cover.index ((pullback J f.unop).obj ⊤) P) ((diagram J P X.unop).obj (op ⊤))
          (fun I => Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj (op ⊤)).unop P).R),
              Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index (op ⊤).unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
        colimit.ι (diagram J P Y.unop) (op ((pullback J f.unop).obj ⊤))
[PROOFSTEP]
let e : (J.pullback f.unop).obj ⊤ ⟶ ⊤ := homOfLE (OrderTop.le_top _)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (pullback J f.unop).obj ⊤ ⟶ ⊤ := homOfLE (_ : (pullback J f.unop).obj ⊤ ≤ ⊤)
⊢ P.map f ≫
      Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op Y.unop)) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        colimit.ι (diagram J P Y.unop) (op ⊤) =
    Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X.unop)) (fun I => P.map I.f.op)
        (_ :
          ∀ (I : (Cover.index ⊤ P).R),
            (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.fst (Cover.index ⊤ P) I =
              (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
      Multiequalizer.lift (Cover.index ((pullback J f.unop).obj ⊤) P) ((diagram J P X.unop).obj (op ⊤))
          (fun I => Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj (op ⊤)).unop P).R),
              Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index (op ⊤).unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
        colimit.ι (diagram J P Y.unop) (op ((pullback J f.unop).obj ⊤))
[PROOFSTEP]
rw [← colimit.w _ e.op, ← Category.assoc, ← Category.assoc, ← Category.assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (pullback J f.unop).obj ⊤ ⟶ ⊤ := homOfLE (_ : (pullback J f.unop).obj ⊤ ≤ ⊤)
⊢ ((P.map f ≫
          Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op Y.unop)) (fun I => P.map I.f.op)
            (_ :
              ∀ (I : (Cover.index ⊤ P).R),
                (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                    MulticospanIndex.fst (Cover.index ⊤ P) I =
                  (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                    MulticospanIndex.snd (Cover.index ⊤ P) I)) ≫
        (diagram J P Y.unop).map e.op) ≫
      colimit.ι (diagram J P Y.unop) (op ((pullback J f.unop).obj ⊤)) =
    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X.unop)) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        Multiequalizer.lift (Cover.index ((pullback J f.unop).obj ⊤) P) ((diagram J P X.unop).obj (op ⊤))
          (fun I => Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj (op ⊤)).unop P).R),
              Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index (op ⊤).unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index (op ⊤).unop P) (Cover.Relation.base I))) ≫
      colimit.ι (diagram J P Y.unop) (op ((pullback J f.unop).obj ⊤))
[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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (pullback J f.unop).obj ⊤ ⟶ ⊤ := homOfLE (_ : (pullback J f.unop).obj ⊤ ≤ ⊤)
⊢ (P.map f ≫
        Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op Y.unop)) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I)) ≫
      (diagram J P Y.unop).map e.op =
    Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X.unop)) (fun I => P.map I.f.op)
        (_ :
          ∀ (I : (Cover.index ⊤ P).R),
            (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.fst (Cover.index ⊤ P) I =
              (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
      Multiequalizer.lift (Cover.index ((pullback J f.unop).obj ⊤) P) ((diagram J P X.unop).obj (op ⊤))
        (fun I => Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J f.unop).op.obj (op ⊤)).unop P).R),
            Multiequalizer.ι (Cover.index (op ⊤).unop P)
                  (MulticospanIndex.fstTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index (op ⊤).unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index (op ⊤).unop P)
                  (MulticospanIndex.sndTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index (op ⊤).unop P) (Cover.Relation.base I))
[PROOFSTEP]
refine' Multiequalizer.hom_ext _ _ _ (fun I => _)
[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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (pullback J f.unop).obj ⊤ ⟶ ⊤ := homOfLE (_ : (pullback J f.unop).obj ⊤ ≤ ⊤)
I : (Cover.index (op ((pullback J f.unop).obj ⊤)).unop P).L
⊢ ((P.map f ≫
          Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op Y.unop)) (fun I => P.map I.f.op)
            (_ :
              ∀ (I : (Cover.index ⊤ P).R),
                (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                    MulticospanIndex.fst (Cover.index ⊤ P) I =
                  (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                    MulticospanIndex.snd (Cover.index ⊤ P) I)) ≫
        (diagram J P Y.unop).map e.op) ≫
      Multiequalizer.ι (Cover.index (op ((pullback J f.unop).obj ⊤)).unop P) I =
    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X.unop)) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        Multiequalizer.lift (Cover.index ((pullback J f.unop).obj ⊤) P) ((diagram J P X.unop).obj (op ⊤))
          (fun I => Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj (op ⊤)).unop P).R),
              Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index (op ⊤).unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index (op ⊤).unop P) (Cover.Relation.base I))) ≫
      Multiequalizer.ι (Cover.index (op ((pullback J f.unop).obj ⊤)).unop P) I
[PROOFSTEP]
simp only [Multiequalizer.lift_ι, Category.assoc]
[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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (pullback J f.unop).obj ⊤ ⟶ ⊤ := homOfLE (_ : (pullback J f.unop).obj ⊤ ≤ ⊤)
I : (Cover.index (op ((pullback J f.unop).obj ⊤)).unop P).L
⊢ P.map f ≫
      Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op Y.unop)) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        (diagram J P Y.unop).map (homOfLE (_ : (pullback J f.unop).obj ⊤ ≤ ⊤)).op ≫
          Multiequalizer.ι (Cover.index (op ((pullback J f.unop).obj ⊤)).unop P) I =
    Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X.unop)) (fun I => P.map I.f.op)
        (_ :
          ∀ (I : (Cover.index ⊤ P).R),
            (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.fst (Cover.index ⊤ P) I =
              (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
      Multiequalizer.lift (Cover.index ((pullback J f.unop).obj ⊤) P) ((diagram J P X.unop).obj (op ⊤))
          (fun I => Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj (op ⊤)).unop P).R),
              Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index (op ⊤).unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
        Multiequalizer.ι (Cover.index (op ((pullback J f.unop).obj ⊤)).unop P) I
[PROOFSTEP]
dsimp [Cover.Arrow.base]
[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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (pullback J f.unop).obj ⊤ ⟶ ⊤ := homOfLE (_ : (pullback J f.unop).obj ⊤ ≤ ⊤)
I : (Cover.index (op ((pullback J f.unop).obj ⊤)).unop P).L
⊢ P.map f ≫
      Multiequalizer.lift (Cover.index ⊤ P) (P.obj Y) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        Multiequalizer.lift (Cover.index (Cover.pullback ⊤ f.unop) P) (multiequalizer (Cover.index ⊤ P))
            (fun I =>
              Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.map I (homOfLE (_ : Cover.pullback ⊤ f.unop ≤ ⊤))))
            (_ :
              ∀ (I : (Cover.index (op (Cover.pullback ⊤ f.unop)).unop P).R),
                Multiequalizer.ι (Cover.index (op ⊤).unop P)
                      (MulticospanIndex.fstTo (Cover.index (op ⊤).unop P)
                        (Cover.Relation.map I (homOfLE (_ : Cover.pullback ⊤ f.unop ≤ ⊤)).op.unop)) ≫
                    MulticospanIndex.fst (Cover.index (op ⊤).unop P)
                      (Cover.Relation.map I (homOfLE (_ : Cover.pullback ⊤ f.unop ≤ ⊤)).op.unop) =
                  Multiequalizer.ι (Cover.index (op ⊤).unop P)
                      (MulticospanIndex.sndTo (Cover.index (op ⊤).unop P)
                        (Cover.Relation.map I (homOfLE (_ : Cover.pullback ⊤ f.unop ≤ ⊤)).op.unop)) ≫
                    MulticospanIndex.snd (Cover.index (op ⊤).unop P)
                      (Cover.Relation.map I (homOfLE (_ : Cover.pullback ⊤ f.unop ≤ ⊤)).op.unop)) ≫
          Multiequalizer.ι (Cover.index (Cover.pullback ⊤ f.unop) P) I =
    Multiequalizer.lift (Cover.index ⊤ P) (P.obj X) (fun I => P.map I.f.op)
        (_ :
          ∀ (I : (Cover.index ⊤ P).R),
            (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.fst (Cover.index ⊤ P) I =
              (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
      Multiequalizer.lift (Cover.index (Cover.pullback ⊤ f.unop) P) (multiequalizer (Cover.index ⊤ P))
          (fun I =>
            Multiequalizer.ι (Cover.index ⊤ P)
              { Y := I.Y, f := I.f ≫ f.unop, hf := (_ : (Cover.sieve (Cover.pullback ⊤ f.unop)).arrows I.f) })
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj (op ⊤)).unop P).R),
              Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index (op ⊤).unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index (op ⊤).unop P) (Cover.Relation.base I)) ≫
        Multiequalizer.ι (Cover.index (Cover.pullback ⊤ f.unop) P) I
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
⊢ η ≫ toPlus J Q = toPlus J P ≫ plusMap J η
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ NatTrans.app (η ≫ toPlus J Q) x✝ = NatTrans.app (toPlus J P ≫ plusMap J η) x✝
[PROOFSTEP]
dsimp [toPlus, plusMap]
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ NatTrans.app η x✝ ≫ Cover.toMultiequalizer ⊤ Q ≫ colimit.ι (diagram J Q x✝.unop) (op ⊤) =
    (Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P x✝.unop) (op ⊤)) ≫ colimMap (diagramNatTrans J η x✝.unop)
[PROOFSTEP]
delta Cover.toMultiequalizer
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ NatTrans.app η x✝ ≫
      Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj (op x✝.unop)) (fun I => Q.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ Q).R),
              (fun I => Q.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ Q) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ Q) I =
                (fun I => Q.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ Q) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ Q) I) ≫
        colimit.ι (diagram J Q x✝.unop) (op ⊤) =
    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op x✝.unop)) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        colimit.ι (diagram J P x✝.unop) (op ⊤)) ≫
      colimMap (diagramNatTrans J η x✝.unop)
[PROOFSTEP]
simp only [ι_colimMap, Category.assoc]
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ NatTrans.app η x✝ ≫
      Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj (op x✝.unop)) (fun I => Q.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ Q).R),
              (fun I => Q.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ Q) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ Q) I =
                (fun I => Q.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ Q) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ Q) I) ≫
        colimit.ι (diagram J Q x✝.unop) (op ⊤) =
    Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op x✝.unop)) (fun I => P.map I.f.op)
        (_ :
          ∀ (I : (Cover.index ⊤ P).R),
            (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.fst (Cover.index ⊤ P) I =
              (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
      NatTrans.app (diagramNatTrans J η x✝.unop) (op ⊤) ≫ colimit.ι (diagram J Q x✝.unop) (op ⊤)
[PROOFSTEP]
simp_rw [← Category.assoc]
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ (NatTrans.app η x✝ ≫
        Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj (op x✝.unop)) (fun I => Q.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ Q).R),
              (fun I => Q.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ Q) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ Q) I =
                (fun I => Q.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ Q) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ Q) I)) ≫
      colimit.ι (diagram J Q x✝.unop) (op ⊤) =
    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op x✝.unop)) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        NatTrans.app (diagramNatTrans J η x✝.unop) (op ⊤)) ≫
      colimit.ι (diagram J Q x✝.unop) (op ⊤)
[PROOFSTEP]
congr 1
[GOAL]
case w.h.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ NatTrans.app η x✝ ≫
      Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj (op x✝.unop)) (fun I => Q.map I.f.op)
        (_ :
          ∀ (I : (Cover.index ⊤ Q).R),
            (fun I => Q.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ Q) I) ≫
                MulticospanIndex.fst (Cover.index ⊤ Q) I =
              (fun I => Q.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ Q) I) ≫
                MulticospanIndex.snd (Cover.index ⊤ Q) I) =
    Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op x✝.unop)) (fun I => P.map I.f.op)
        (_ :
          ∀ (I : (Cover.index ⊤ P).R),
            (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.fst (Cover.index ⊤ P) I =
              (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
      NatTrans.app (diagramNatTrans J η x✝.unop) (op ⊤)
[PROOFSTEP]
exact Multiequalizer.hom_ext _ _ _ (fun I => by dsimp; simp)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
I : (Cover.index ⊤ Q).L
⊢ (NatTrans.app η x✝ ≫
        Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj (op x✝.unop)) (fun I => Q.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ Q).R),
              (fun I => Q.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ Q) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ Q) I =
                (fun I => Q.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ Q) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ Q) I)) ≫
      Multiequalizer.ι (Cover.index ⊤ Q) I =
    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op x✝.unop)) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        NatTrans.app (diagramNatTrans J η x✝.unop) (op ⊤)) ≫
      Multiequalizer.ι (Cover.index ⊤ Q) I
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
I : (Cover.index ⊤ Q).L
⊢ (NatTrans.app η x✝ ≫
        Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj x✝) (fun I => Q.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ Q).R),
              (fun I => Q.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ Q) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ Q) I =
                (fun I => Q.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ Q) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ Q) I)) ≫
      Multiequalizer.ι (Cover.index ⊤ Q) I =
    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj x✝) (fun I => P.map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ P).R),
              (fun I => P.map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ P) I =
                (fun I => P.map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ P) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ P) I) ≫
        Multiequalizer.lift (Cover.index ⊤ Q) (multiequalizer (Cover.index ⊤ P))
          (fun i => Multiequalizer.ι (Cover.index ⊤ P) i ≫ NatTrans.app η (op i.Y))
          (_ :
            ∀ (i : (Cover.index (op ⊤).unop Q).R),
              (fun i => Multiequalizer.ι (Cover.index (op ⊤).unop P) i ≫ NatTrans.app η (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index (op ⊤).unop Q) i) ≫
                  MulticospanIndex.fst (Cover.index (op ⊤).unop Q) i =
                (fun i => Multiequalizer.ι (Cover.index (op ⊤).unop P) i ≫ NatTrans.app η (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index (op ⊤).unop Q) i) ≫
                  MulticospanIndex.snd (Cover.index (op ⊤).unop Q) i)) ≫
      Multiequalizer.ι (Cover.index ⊤ Q) I
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
⊢ plusMap J (toPlus J P) = toPlus J (plusObj J P)
[PROOFSTEP]
ext X : 2
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
⊢ NatTrans.app (plusMap J (toPlus J P)) X = NatTrans.app (toPlus J (plusObj J P)) X
[PROOFSTEP]
refine' colimit.hom_ext (fun S => _)
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
⊢ colimit.ι (diagram J P X.unop) S ≫ NatTrans.app (plusMap J (toPlus J P)) X =
    colimit.ι (diagram J P X.unop) S ≫ NatTrans.app (toPlus J (plusObj J P)) X
[PROOFSTEP]
dsimp only [plusMap, toPlus]
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
⊢ colimit.ι (diagram J P X.unop) S ≫
      colimMap
        (diagramNatTrans J (NatTrans.mk fun X => Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P X.unop) (op ⊤))
          X.unop) =
    colimit.ι (diagram J P X.unop) S ≫
      Cover.toMultiequalizer ⊤ (plusObj J P) ≫ colimit.ι (diagram J (plusObj J P) X.unop) (op ⊤)
[PROOFSTEP]
let e : S.unop ⟶ ⊤ := homOfLE (OrderTop.le_top _)
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
⊢ colimit.ι (diagram J P X.unop) S ≫
      colimMap
        (diagramNatTrans J (NatTrans.mk fun X => Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P X.unop) (op ⊤))
          X.unop) =
    colimit.ι (diagram J P X.unop) S ≫
      Cover.toMultiequalizer ⊤ (plusObj J P) ≫ colimit.ι (diagram J (plusObj J P) X.unop) (op ⊤)
[PROOFSTEP]
rw [ι_colimMap, ← colimit.w _ e.op, ← Category.assoc, ← Category.assoc]
[GOAL]
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
⊢ NatTrans.app
        (diagramNatTrans J (NatTrans.mk fun X => Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P X.unop) (op ⊤))
          X.unop)
        S ≫
      colimit.ι (diagram J (plusObj J P) X.unop) S =
    ((colimit.ι (diagram J P X.unop) S ≫ Cover.toMultiequalizer ⊤ (plusObj J P)) ≫
        (diagram J (plusObj J P) X.unop).map e.op) ≫
      colimit.ι (diagram J (plusObj J P) X.unop) (op S.unop)
[PROOFSTEP]
congr 1
[GOAL]
case w.h.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
⊢ NatTrans.app
      (diagramNatTrans J (NatTrans.mk fun X => Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P X.unop) (op ⊤))
        X.unop)
      S =
    (colimit.ι (diagram J P X.unop) S ≫ Cover.toMultiequalizer ⊤ (plusObj J P)) ≫
      (diagram J (plusObj J P) X.unop).map e.op
[PROOFSTEP]
refine' Multiequalizer.hom_ext _ _ _ (fun I => _)
[GOAL]
case w.h.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
⊢ NatTrans.app
        (diagramNatTrans J (NatTrans.mk fun X => Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P X.unop) (op ⊤))
          X.unop)
        S ≫
      Multiequalizer.ι (Cover.index S.unop (plusObj J P)) I =
    ((colimit.ι (diagram J P X.unop) S ≫ Cover.toMultiequalizer ⊤ (plusObj J P)) ≫
        (diagram J (plusObj J P) X.unop).map e.op) ≫
      Multiequalizer.ι (Cover.index S.unop (plusObj J P)) I
[PROOFSTEP]
erw [Multiequalizer.lift_ι]
[GOAL]
case w.h.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
⊢ Multiequalizer.ι (Cover.index S.unop P) I ≫
      NatTrans.app (NatTrans.mk fun X => Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P X.unop) (op ⊤)) (op I.Y) =
    ((colimit.ι (diagram J P X.unop) S ≫ Cover.toMultiequalizer ⊤ (plusObj J P)) ≫
        (diagram J (plusObj J P) X.unop).map e.op) ≫
      Multiequalizer.ι (Cover.index S.unop (plusObj J P)) I
[PROOFSTEP]
simp only [unop_op, op_unop, diagram_map, Category.assoc, limit.lift_π, Multifork.ofι_π_app]
[GOAL]
case w.h.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
⊢ Multiequalizer.ι (Cover.index S.unop P) I ≫ Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P I.Y) (op ⊤) =
    colimit.ι (diagram J P X.unop) S ≫ (plusObj J P).map (Cover.Arrow.map I (homOfLE (_ : S.unop ≤ ⊤)).op.unop).f.op
[PROOFSTEP]
let ee : (J.pullback (I.map e).f).obj S.unop ⟶ ⊤ := homOfLE (OrderTop.le_top _)
[GOAL]
case w.h.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
ee : (pullback J (Cover.Arrow.map I e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map I e).f).obj S.unop ≤ ⊤)
⊢ Multiequalizer.ι (Cover.index S.unop P) I ≫ Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P I.Y) (op ⊤) =
    colimit.ι (diagram J P X.unop) S ≫ (plusObj J P).map (Cover.Arrow.map I (homOfLE (_ : S.unop ≤ ⊤)).op.unop).f.op
[PROOFSTEP]
erw [← colimit.w _ ee.op, ι_colimMap_assoc, colimit.ι_pre, diagramPullback_app, ← Category.assoc, ← Category.assoc]
[GOAL]
case w.h.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
ee : (pullback J (Cover.Arrow.map I e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map I e).f).obj S.unop ≤ ⊤)
⊢ ((Multiequalizer.ι (Cover.index S.unop P) I ≫ Cover.toMultiequalizer ⊤ P) ≫ (diagram J P I.Y).map ee.op) ≫
      colimit.ι (diagram J P I.Y) (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)) =
    Multiequalizer.lift
        (Cover.index ((pullback J (Cover.Arrow.map I (homOfLE (_ : S.unop ≤ ⊤)).op.unop).f.op.unop).op.obj S).unop P)
        ((diagram J P X.unop).obj S) (fun I_1 => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I_1))
        (_ :
          ∀
            (I_1 :
              (Cover.index ((pullback J (Cover.Arrow.map I (homOfLE (_ : S.unop ≤ ⊤)).op.unop).f.op.unop).op.obj S).unop
                  P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I_1)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I_1) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I_1)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I_1)) ≫
      colimit.ι (diagram J P (op (Cover.Arrow.map I (homOfLE (_ : S.unop ≤ ⊤)).op.unop).Y).unop)
        ((pullback J (Cover.Arrow.map I (homOfLE (_ : S.unop ≤ ⊤)).op.unop).f.op.unop).op.obj S)
[PROOFSTEP]
congr 1
[GOAL]
case w.h.e_a.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
ee : (pullback J (Cover.Arrow.map I e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map I e).f).obj S.unop ≤ ⊤)
⊢ (Multiequalizer.ι (Cover.index S.unop P) I ≫ Cover.toMultiequalizer ⊤ P) ≫ (diagram J P I.Y).map ee.op =
    Multiequalizer.lift
      (Cover.index ((pullback J (Cover.Arrow.map I (homOfLE (_ : S.unop ≤ ⊤)).op.unop).f.op.unop).op.obj S).unop P)
      ((diagram J P X.unop).obj S) (fun I_1 => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I_1))
      (_ :
        ∀
          (I_1 :
            (Cover.index ((pullback J (Cover.Arrow.map I (homOfLE (_ : S.unop ≤ ⊤)).op.unop).f.op.unop).op.obj S).unop
                P).R),
          Multiequalizer.ι (Cover.index S.unop P)
                (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I_1)) ≫
              MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I_1) =
            Multiequalizer.ι (Cover.index S.unop P)
                (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I_1)) ≫
              MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I_1))
[PROOFSTEP]
refine' Multiequalizer.hom_ext _ _ _ (fun II => _)
[GOAL]
case w.h.e_a.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
ee : (pullback J (Cover.Arrow.map I e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map I e).f).obj S.unop ≤ ⊤)
II : (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P).L
⊢ ((Multiequalizer.ι (Cover.index S.unop P) I ≫ Cover.toMultiequalizer ⊤ P) ≫ (diagram J P I.Y).map ee.op) ≫
      Multiequalizer.ι (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P) II =
    Multiequalizer.lift
        (Cover.index ((pullback J (Cover.Arrow.map I (homOfLE (_ : S.unop ≤ ⊤)).op.unop).f.op.unop).op.obj S).unop P)
        ((diagram J P X.unop).obj S) (fun I_1 => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I_1))
        (_ :
          ∀
            (I_1 :
              (Cover.index ((pullback J (Cover.Arrow.map I (homOfLE (_ : S.unop ≤ ⊤)).op.unop).f.op.unop).op.obj S).unop
                  P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I_1)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I_1) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I_1)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I_1)) ≫
      Multiequalizer.ι (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P) II
[PROOFSTEP]
convert
  (Multiequalizer.condition (S.unop.index P)
    ⟨_, _, _, II.f, 𝟙 _, I.f, II.f ≫ I.f, I.hf, Sieve.downward_closed _ I.hf _, by simp⟩) using
  1
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
ee : (pullback J (Cover.Arrow.map I e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map I e).f).obj S.unop ≤ ⊤)
II : (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P).L
⊢ II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
ee : (pullback J (Cover.Arrow.map I e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map I e).f).obj S.unop ≤ ⊤)
II : (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P).L
e_1✝ :
  ((diagram J P X.unop).obj S ⟶
      MulticospanIndex.left (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P) II) =
    (multiequalizer (Cover.index S.unop P) ⟶
      MulticospanIndex.right (Cover.index S.unop P)
        { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
          w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) })
⊢ ((Multiequalizer.ι (Cover.index S.unop P) I ≫ Cover.toMultiequalizer ⊤ P) ≫ (diagram J P I.Y).map ee.op) ≫
      Multiequalizer.ι (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P) II =
    Multiequalizer.ι (Cover.index S.unop P)
        (MulticospanIndex.fstTo (Cover.index S.unop P)
          { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
            h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
            w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) }) ≫
      MulticospanIndex.fst (Cover.index S.unop P)
        { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
          w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) }
[PROOFSTEP]
dsimp [diagram]
[GOAL]
case h.e'_2.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
ee : (pullback J (Cover.Arrow.map I e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map I e).f).obj S.unop ≤ ⊤)
II : (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P).L
e_1✝ :
  ((diagram J P X.unop).obj S ⟶
      MulticospanIndex.left (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P) II) =
    (multiequalizer (Cover.index S.unop P) ⟶
      MulticospanIndex.right (Cover.index S.unop P)
        { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
          w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) })
⊢ ((Multiequalizer.ι (Cover.index S.unop P) I ≫ Cover.toMultiequalizer ⊤ P) ≫
        Multiequalizer.lift (Cover.index (Cover.pullback S.unop I.f) P) (multiequalizer (Cover.index ⊤ P))
          (fun I_1 =>
            Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.map I_1 (homOfLE (_ : Cover.pullback S.unop I.f ≤ ⊤))))
          (_ :
            ∀ (I_1 : (Cover.index (op (Cover.pullback S.unop I.f)).unop P).R),
              Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op ⊤).unop P)
                      (Cover.Relation.map I_1 (homOfLE (_ : Cover.pullback S.unop I.f ≤ ⊤)).op.unop)) ≫
                  MulticospanIndex.fst (Cover.index (op ⊤).unop P)
                    (Cover.Relation.map I_1 (homOfLE (_ : Cover.pullback S.unop I.f ≤ ⊤)).op.unop) =
                Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op ⊤).unop P)
                      (Cover.Relation.map I_1 (homOfLE (_ : Cover.pullback S.unop I.f ≤ ⊤)).op.unop)) ≫
                  MulticospanIndex.snd (Cover.index (op ⊤).unop P)
                    (Cover.Relation.map I_1 (homOfLE (_ : Cover.pullback S.unop I.f ≤ ⊤)).op.unop))) ≫
      Multiequalizer.ι (Cover.index (Cover.pullback S.unop I.f) P) II =
    Multiequalizer.ι (Cover.index S.unop P)
        (MulticospanIndex.fstTo (Cover.index S.unop P)
          { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
            h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
            w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) }) ≫
      MulticospanIndex.fst (Cover.index S.unop P)
        { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
          w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) }
[PROOFSTEP]
cases I
[GOAL]
case h.e'_2.h.mk
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
Y✝ : C
f✝ : Y✝ ⟶ X.unop
hf✝ : (Cover.sieve S.unop).arrows f✝
ee : (pullback J (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } e).f).obj S.unop ≤ ⊤)
II : (Cover.index (op ((pullback J (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } e).f).obj S.unop)).unop P).L
e_1✝ :
  ((diagram J P X.unop).obj S ⟶
      MulticospanIndex.left
        (Cover.index (op ((pullback J (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } e).f).obj S.unop)).unop P) II) =
    (multiequalizer (Cover.index S.unop P) ⟶
      MulticospanIndex.right (Cover.index S.unop P)
        { Y₁ := { Y := Y✝, f := f✝, hf := hf✝ }.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y,
          f₁ := { Y := Y✝, f := f✝, hf := hf✝ }.f, f₂ := II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows { Y := Y✝, f := f✝, hf := hf✝ }.f),
          h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f)),
          w := (_ : II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f = 𝟙 II.Y ≫ II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f) })
⊢ ((Multiequalizer.ι (Cover.index S.unop P) { Y := Y✝, f := f✝, hf := hf✝ } ≫ Cover.toMultiequalizer ⊤ P) ≫
        Multiequalizer.lift (Cover.index (Cover.pullback S.unop { Y := Y✝, f := f✝, hf := hf✝ }.f) P)
          (multiequalizer (Cover.index ⊤ P))
          (fun I =>
            Multiequalizer.ι (Cover.index ⊤ P)
              (Cover.Arrow.map I (homOfLE (_ : Cover.pullback S.unop { Y := Y✝, f := f✝, hf := hf✝ }.f ≤ ⊤))))
          (_ :
            ∀ (I : (Cover.index (op (Cover.pullback S.unop { Y := Y✝, f := f✝, hf := hf✝ }.f)).unop P).R),
              Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.fstTo (Cover.index (op ⊤).unop P)
                      (Cover.Relation.map I
                        (homOfLE (_ : Cover.pullback S.unop { Y := Y✝, f := f✝, hf := hf✝ }.f ≤ ⊤)).op.unop)) ≫
                  MulticospanIndex.fst (Cover.index (op ⊤).unop P)
                    (Cover.Relation.map I
                      (homOfLE (_ : Cover.pullback S.unop { Y := Y✝, f := f✝, hf := hf✝ }.f ≤ ⊤)).op.unop) =
                Multiequalizer.ι (Cover.index (op ⊤).unop P)
                    (MulticospanIndex.sndTo (Cover.index (op ⊤).unop P)
                      (Cover.Relation.map I
                        (homOfLE (_ : Cover.pullback S.unop { Y := Y✝, f := f✝, hf := hf✝ }.f ≤ ⊤)).op.unop)) ≫
                  MulticospanIndex.snd (Cover.index (op ⊤).unop P)
                    (Cover.Relation.map I
                      (homOfLE (_ : Cover.pullback S.unop { Y := Y✝, f := f✝, hf := hf✝ }.f ≤ ⊤)).op.unop))) ≫
      Multiequalizer.ι (Cover.index (Cover.pullback S.unop { Y := Y✝, f := f✝, hf := hf✝ }.f) P) II =
    Multiequalizer.ι (Cover.index S.unop P)
        (MulticospanIndex.fstTo (Cover.index S.unop P)
          { Y₁ := { Y := Y✝, f := f✝, hf := hf✝ }.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y,
            f₁ := { Y := Y✝, f := f✝, hf := hf✝ }.f, f₂ := II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f,
            h₁ := (_ : (Cover.sieve S.unop).arrows { Y := Y✝, f := f✝, hf := hf✝ }.f),
            h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f)),
            w := (_ : II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f = 𝟙 II.Y ≫ II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f) }) ≫
      MulticospanIndex.fst (Cover.index S.unop P)
        { Y₁ := { Y := Y✝, f := f✝, hf := hf✝ }.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y,
          f₁ := { Y := Y✝, f := f✝, hf := hf✝ }.f, f₂ := II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows { Y := Y✝, f := f✝, hf := hf✝ }.f),
          h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f)),
          w := (_ : II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f = 𝟙 II.Y ≫ II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f) }
[PROOFSTEP]
simp only [Category.assoc, limit.lift_π, Multifork.ofι_pt, Multifork.ofι_π_app, Cover.Arrow.map_Y, Cover.Arrow.map_f]
[GOAL]
case h.e'_2.h.mk
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
Y✝ : C
f✝ : Y✝ ⟶ X.unop
hf✝ : (Cover.sieve S.unop).arrows f✝
ee : (pullback J (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } e).f).obj S.unop ≤ ⊤)
II : (Cover.index (op ((pullback J (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } e).f).obj S.unop)).unop P).L
e_1✝ :
  ((diagram J P X.unop).obj S ⟶
      MulticospanIndex.left
        (Cover.index (op ((pullback J (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } e).f).obj S.unop)).unop P) II) =
    (multiequalizer (Cover.index S.unop P) ⟶
      MulticospanIndex.right (Cover.index S.unop P)
        { Y₁ := { Y := Y✝, f := f✝, hf := hf✝ }.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y,
          f₁ := { Y := Y✝, f := f✝, hf := hf✝ }.f, f₂ := II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows { Y := Y✝, f := f✝, hf := hf✝ }.f),
          h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f)),
          w := (_ : II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f = 𝟙 II.Y ≫ II.f ≫ { Y := Y✝, f := f✝, hf := hf✝ }.f) })
⊢ Multiequalizer.ι (Cover.index S.unop P) { Y := Y✝, f := f✝, hf := hf✝ } ≫ P.map II.f.op =
    Multiequalizer.ι (Cover.index S.unop P)
        (MulticospanIndex.fstTo (Cover.index S.unop P)
          { Y₁ := Y✝, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := f✝, f₂ := II.f ≫ f✝, h₁ := hf✝,
            h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ f✝)), w := (_ : II.f ≫ f✝ = 𝟙 II.Y ≫ II.f ≫ f✝) }) ≫
      MulticospanIndex.fst (Cover.index S.unop P)
        { Y₁ := Y✝, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := f✝, f₂ := II.f ≫ f✝, h₁ := hf✝,
          h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ f✝)), w := (_ : II.f ≫ f✝ = 𝟙 II.Y ≫ II.f ≫ f✝) }
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
ee : (pullback J (Cover.Arrow.map I e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map I e).f).obj S.unop ≤ ⊤)
II : (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P).L
e_1✝ :
  ((diagram J P X.unop).obj S ⟶
      MulticospanIndex.left (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P) II) =
    (multiequalizer (Cover.index S.unop P) ⟶
      MulticospanIndex.right (Cover.index S.unop P)
        { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
          w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) })
⊢ Multiequalizer.lift
        (Cover.index ((pullback J (Cover.Arrow.map I (homOfLE (_ : S.unop ≤ ⊤)).op.unop).f.op.unop).op.obj S).unop P)
        ((diagram J P X.unop).obj S) (fun I_1 => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base I_1))
        (_ :
          ∀
            (I_1 :
              (Cover.index ((pullback J (Cover.Arrow.map I (homOfLE (_ : S.unop ≤ ⊤)).op.unop).f.op.unop).op.obj S).unop
                  P).R),
            Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.base I_1)) ≫
                MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.base I_1) =
              Multiequalizer.ι (Cover.index S.unop P)
                  (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.base I_1)) ≫
                MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.base I_1)) ≫
      Multiequalizer.ι (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P) II =
    Multiequalizer.ι (Cover.index S.unop P)
        (MulticospanIndex.sndTo (Cover.index S.unop P)
          { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
            h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
            w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) }) ≫
      MulticospanIndex.snd (Cover.index S.unop P)
        { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
          w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) }
[PROOFSTEP]
erw [Multiequalizer.lift_ι]
[GOAL]
case h.e'_3.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
ee : (pullback J (Cover.Arrow.map I e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map I e).f).obj S.unop ≤ ⊤)
II : (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P).L
e_1✝ :
  ((diagram J P X.unop).obj S ⟶
      MulticospanIndex.left (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P) II) =
    (multiequalizer (Cover.index S.unop P) ⟶
      MulticospanIndex.right (Cover.index S.unop P)
        { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
          w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) })
⊢ Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.base II) =
    Multiequalizer.ι (Cover.index S.unop P)
        (MulticospanIndex.sndTo (Cover.index S.unop P)
          { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
            h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
            w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) }) ≫
      MulticospanIndex.snd (Cover.index S.unop P)
        { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
          w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) }
[PROOFSTEP]
dsimp [Cover.index]
[GOAL]
case h.e'_3.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
ee : (pullback J (Cover.Arrow.map I e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map I e).f).obj S.unop ≤ ⊤)
II : (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P).L
e_1✝ :
  ((diagram J P X.unop).obj S ⟶
      MulticospanIndex.left (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P) II) =
    (multiequalizer (Cover.index S.unop P) ⟶
      MulticospanIndex.right (Cover.index S.unop P)
        { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
          w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) })
⊢ Multiequalizer.ι
      { L := Cover.Arrow S.unop, R := Cover.Relation S.unop, fstTo := fun I => Cover.Relation.fst I,
        sndTo := fun I => Cover.Relation.snd I, left := fun I => P.obj (op I.Y), right := fun I => P.obj (op I.Z),
        fst := fun I => P.map I.g₁.op, snd := fun I => P.map I.g₂.op }
      (Cover.Arrow.base II) =
    Multiequalizer.ι
        { L := Cover.Arrow S.unop, R := Cover.Relation S.unop, fstTo := fun I => Cover.Relation.fst I,
          sndTo := fun I => Cover.Relation.snd I, left := fun I => P.obj (op I.Y), right := fun I => P.obj (op I.Z),
          fst := fun I => P.map I.g₁.op, snd := fun I => P.map I.g₂.op }
        (Cover.Relation.snd
          { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
            h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
            w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) }) ≫
      P.map (𝟙 (op II.Y))
[PROOFSTEP]
simp only [Functor.map_id, Category.comp_id]
[GOAL]
case h.e'_3.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
X : Cᵒᵖ
S : (Cover J X.unop)ᵒᵖ
e : S.unop ⟶ ⊤ := homOfLE (_ : S.unop ≤ ⊤)
I : (Cover.index S.unop (plusObj J P)).L
ee : (pullback J (Cover.Arrow.map I e).f).obj S.unop ⟶ ⊤ :=
  homOfLE (_ : (pullback J (Cover.Arrow.map I e).f).obj S.unop ≤ ⊤)
II : (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P).L
e_1✝ :
  ((diagram J P X.unop).obj S ⟶
      MulticospanIndex.left (Cover.index (op ((pullback J (Cover.Arrow.map I e).f).obj S.unop)).unop P) II) =
    (multiequalizer (Cover.index S.unop P) ⟶
      MulticospanIndex.right (Cover.index S.unop P)
        { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
          w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) })
⊢ Multiequalizer.ι
      { L := Cover.Arrow S.unop, R := Cover.Relation S.unop, fstTo := fun I => Cover.Relation.fst I,
        sndTo := fun I => Cover.Relation.snd I, left := fun I => P.obj (op I.Y), right := fun I => P.obj (op I.Z),
        fst := fun I => P.map I.g₁.op, snd := fun I => P.map I.g₂.op }
      (Cover.Arrow.base II) =
    Multiequalizer.ι
      { L := Cover.Arrow S.unop, R := Cover.Relation S.unop, fstTo := fun I => Cover.Relation.fst I,
        sndTo := fun I => Cover.Relation.snd I, left := fun I => P.obj (op I.Y), right := fun I => P.obj (op I.Z),
        fst := fun I => P.map I.g₁.op, snd := fun I => P.map I.g₂.op }
      (Cover.Relation.snd
        { Y₁ := I.Y, Y₂ := II.Y, Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, f₁ := I.f, f₂ := II.f ≫ I.f,
          h₁ := (_ : (Cover.sieve S.unop).arrows I.f), h₂ := (_ : (Cover.sieve S.unop).arrows (II.f ≫ I.f)),
          w := (_ : II.f ≫ I.f = 𝟙 II.Y ≫ II.f ≫ I.f) })
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (toPlus J P)
[PROOFSTEP]
rw [Presheaf.isSheaf_iff_multiequalizer] at hP
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
⊢ IsIso (toPlus J P)
[PROOFSTEP]
suffices : ∀ X, IsIso ((J.toPlus P).app X)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
this : ∀ (X : Cᵒᵖ), IsIso (NatTrans.app (toPlus J P) X)
⊢ IsIso (toPlus J P)
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
⊢ ∀ (X : Cᵒᵖ), IsIso (NatTrans.app (toPlus J P) X)
[PROOFSTEP]
intro X
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
⊢ IsIso (NatTrans.app (toPlus J P) X)
[PROOFSTEP]
suffices : IsIso (colimit.ι (J.diagram P X.unop) (op ⊤))
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
this : IsIso (colimit.ι (diagram J P X.unop) (op ⊤))
⊢ IsIso (NatTrans.app (toPlus J P) X)
[PROOFSTEP]
apply IsIso.comp_isIso
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
⊢ IsIso (colimit.ι (diagram J P X.unop) (op ⊤))
[PROOFSTEP]
suffices : ∀ (S T : (J.Cover X.unop)ᵒᵖ) (f : S ⟶ T), IsIso ((J.diagram P X.unop).map f)
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
this : ∀ (S T : (Cover J X.unop)ᵒᵖ) (f : S ⟶ T), IsIso ((diagram J P X.unop).map f)
⊢ IsIso (colimit.ι (diagram J P X.unop) (op ⊤))
[PROOFSTEP]
apply isIso_ι_of_isInitial (initialOpOfTerminal isTerminalTop)
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
⊢ ∀ (S T : (Cover J X.unop)ᵒᵖ) (f : S ⟶ T), IsIso ((diagram J P X.unop).map f)
[PROOFSTEP]
intro S T e
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
⊢ IsIso ((diagram J P X.unop).map e)
[PROOFSTEP]
have : S.unop.toMultiequalizer P ≫ (J.diagram P X.unop).map e = T.unop.toMultiequalizer P :=
  Multiequalizer.hom_ext _ _ _ (fun II => by dsimp; simp)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
II : (Cover.index T.unop P).L
⊢ (Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e) ≫ Multiequalizer.ι (Cover.index T.unop P) II =
    Cover.toMultiequalizer T.unop P ≫ Multiequalizer.ι (Cover.index T.unop P) II
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
II : (Cover.index T.unop P).L
⊢ (Cover.toMultiequalizer S.unop P ≫
        Multiequalizer.lift (Cover.index T.unop P) (multiequalizer (Cover.index S.unop P))
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.map I e.unop))
          (_ :
            ∀ (I : (Cover.index T.unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.map I e.unop)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.map I e.unop) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.map I e.unop)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.map I e.unop))) ≫
      Multiequalizer.ι (Cover.index T.unop P) II =
    Cover.toMultiequalizer T.unop P ≫ Multiequalizer.ι (Cover.index T.unop P) II
[PROOFSTEP]
simp
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
this : Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e = Cover.toMultiequalizer T.unop P
⊢ IsIso ((diagram J P X.unop).map e)
[PROOFSTEP]
have : (J.diagram P X.unop).map e = inv (S.unop.toMultiequalizer P) ≫ T.unop.toMultiequalizer P := by simp [← this]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
this : Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e = Cover.toMultiequalizer T.unop P
⊢ (diagram J P X.unop).map e = inv (Cover.toMultiequalizer S.unop P) ≫ Cover.toMultiequalizer T.unop P
[PROOFSTEP]
simp [← this]
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
this✝ : Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e = Cover.toMultiequalizer T.unop P
this : (diagram J P X.unop).map e = inv (Cover.toMultiequalizer S.unop P) ≫ Cover.toMultiequalizer T.unop P
⊢ IsIso ((diagram J P X.unop).map e)
[PROOFSTEP]
rw [this]
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
this✝ : Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e = Cover.toMultiequalizer T.unop P
this : (diagram J P X.unop).map e = inv (Cover.toMultiequalizer S.unop P) ≫ Cover.toMultiequalizer T.unop P
⊢ IsIso (inv (Cover.toMultiequalizer S.unop P) ≫ Cover.toMultiequalizer T.unop P)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ toPlus J P ≫ plusLift J η hQ = η
[PROOFSTEP]
dsimp [plusLift]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ toPlus J P ≫ plusMap J η ≫ (isoToPlus J Q hQ).inv = η
[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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ (toPlus J P ≫ plusMap J η) ≫ (isoToPlus J Q hQ).inv = η
[PROOFSTEP]
rw [Iso.comp_inv_eq]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ toPlus J P ≫ plusMap J η = η ≫ (isoToPlus J Q hQ).hom
[PROOFSTEP]
dsimp only [isoToPlus, asIso]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ toPlus J P ≫ plusMap J η = η ≫ toPlus J Q
[PROOFSTEP]
rw [toPlus_naturality]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : plusObj J P ⟶ Q
hγ : toPlus J P ≫ γ = η
⊢ γ = plusLift J η hQ
[PROOFSTEP]
dsimp only [plusLift]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : plusObj J P ⟶ Q
hγ : toPlus J P ≫ γ = η
⊢ γ = plusMap J η ≫ (isoToPlus J Q hQ).inv
[PROOFSTEP]
rw [Iso.eq_comp_inv, ← hγ, plusMap_comp]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : plusObj J P ⟶ Q
hγ : toPlus J P ≫ γ = η
⊢ γ ≫ (isoToPlus J Q hQ).hom = plusMap J (toPlus J P) ≫ plusMap 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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
⊢ η = γ
[PROOFSTEP]
have : γ = J.plusLift (J.toPlus P ≫ γ) hQ := by
  apply plusLift_unique
  rfl
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
⊢ γ = plusLift J (toPlus J P ≫ γ) hQ
[PROOFSTEP]
apply plusLift_unique
[GOAL]
case hγ
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
⊢ toPlus J P ≫ γ = toPlus J P ≫ γ
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
this : γ = plusLift J (toPlus J P ≫ γ) hQ
⊢ η = γ
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
this : γ = plusLift J (toPlus J P ≫ γ) hQ
⊢ η = plusLift J (toPlus J P ≫ γ) hQ
[PROOFSTEP]
apply plusLift_unique
[GOAL]
case hγ
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
this : γ = plusLift J (toPlus J P ≫ γ) hQ
⊢ toPlus J P ≫ η = toPlus J P ≫ γ
[PROOFSTEP]
exact h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ (isoToPlus J P hP).inv = plusLift J (𝟙 P) hP
[PROOFSTEP]
apply J.plusLift_unique
[GOAL]
case hγ
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ toPlus J P ≫ (isoToPlus J P hP).inv = 𝟙 P
[PROOFSTEP]
rw [Iso.comp_inv_eq, Category.id_comp]
[GOAL]
case hγ
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ toPlus J P = (isoToPlus J P hP).hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ plusMap J η ≫ plusLift J γ hR = plusLift J (η ≫ γ) hR
[PROOFSTEP]
apply J.plusLift_unique
[GOAL]
case hγ
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ toPlus J P ≫ plusMap J η ≫ plusLift J γ hR = η ≫ γ
[PROOFSTEP]
rw [← Category.assoc, ← J.toPlus_naturality, Category.assoc, J.toPlus_plusLift]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{max v u, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝ : Preadditive D
F G : Cᵒᵖ ⥤ D
⊢ (plusFunctor J D).map 0 = 0
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{max v u, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝ : Preadditive D
F G : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ NatTrans.app ((plusFunctor J D).map 0) x✝ = NatTrans.app 0 x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{max v u, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝ : Preadditive D
F G : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ NatTrans.app (plusMap J 0) x✝ = 0
[PROOFSTEP]
rw [J.plusMap_zero, NatTrans.app_zero]