[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category.{max v u, w₁} D
E : Type w₂
inst✝³ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝¹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
X : C
W : (Cover J X)ᵒᵖ
⊢ (diagram J P X ⋙ F).obj W ≅ (diagram J (P ⋙ F) X).obj W
[PROOFSTEP]
refine' _ ≪≫ HasLimit.isoOfNatIso (W.unop.multicospanComp _ _).symm
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category.{max v u, w₁} D
E : Type w₂
inst✝³ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝¹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
X : C
W : (Cover J X)ᵒᵖ
⊢ (diagram J P X ⋙ F).obj W ≅ limit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F)
[PROOFSTEP]
refine' (isLimitOfPreserves F (limit.isLimit _)).conePointUniqueUpToIso (limit.isLimit _)
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category.{max v u, w₁} D
E : Type w₂
inst✝³ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝¹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
X : C
⊢ ∀ {X_1 Y : (Cover J X)ᵒᵖ} (f : X_1 ⟶ Y),
    (diagram J P X ⋙ F).map f ≫
        ((fun W =>
              IsLimit.conePointUniqueUpToIso
                  (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
                  (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F)) ≪≫
                HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm)
            Y).hom =
      ((fun W =>
              IsLimit.conePointUniqueUpToIso
                  (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
                  (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F)) ≪≫
                HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm)
            X_1).hom ≫
        (diagram J (P ⋙ F) X).map f
[PROOFSTEP]
intro A B f
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category.{max v u, w₁} D
E : Type w₂
inst✝³ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝¹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
X : C
A B : (Cover J X)ᵒᵖ
f : A ⟶ B
⊢ (diagram J P X ⋙ F).map f ≫
      ((fun W =>
            IsLimit.conePointUniqueUpToIso
                (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
                (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F)) ≪≫
              HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm)
          B).hom =
    ((fun W =>
            IsLimit.conePointUniqueUpToIso
                (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
                (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F)) ≪≫
              HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm)
          A).hom ≫
      (diagram J (P ⋙ F) X).map f
[PROOFSTEP]
apply Multiequalizer.hom_ext
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category.{max v u, w₁} D
E : Type w₂
inst✝³ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝¹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
X : C
A B : (Cover J X)ᵒᵖ
f : A ⟶ B
⊢ ∀ (a : (Cover.index B.unop (P ⋙ F)).L),
    ((diagram J P X ⋙ F).map f ≫
          ((fun W =>
                IsLimit.conePointUniqueUpToIso
                    (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
                    (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F)) ≪≫
                  HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm)
              B).hom) ≫
        Multiequalizer.ι (Cover.index B.unop (P ⋙ F)) a =
      (((fun W =>
                IsLimit.conePointUniqueUpToIso
                    (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
                    (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F)) ≪≫
                  HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm)
              A).hom ≫
          (diagram J (P ⋙ F) X).map f) ≫
        Multiequalizer.ι (Cover.index B.unop (P ⋙ F)) a
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category.{max v u, w₁} D
E : Type w₂
inst✝³ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝¹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
X : C
A B : (Cover J X)ᵒᵖ
f : A ⟶ B
⊢ ∀ (a : (Cover.index B.unop (P ⋙ F)).L),
    (F.map
            (Multiequalizer.lift (Cover.index B.unop P) (multiequalizer (Cover.index A.unop P))
              (fun I => Multiequalizer.ι (Cover.index A.unop P) (Cover.Arrow.map I f.unop))
              (_ :
                ∀ (I : (Cover.index B.unop P).R),
                  Multiequalizer.ι (Cover.index A.unop P)
                        (MulticospanIndex.fstTo (Cover.index A.unop P) (Cover.Relation.map I f.unop)) ≫
                      MulticospanIndex.fst (Cover.index A.unop P) (Cover.Relation.map I f.unop) =
                    Multiequalizer.ι (Cover.index A.unop P)
                        (MulticospanIndex.sndTo (Cover.index A.unop P) (Cover.Relation.map I f.unop)) ≫
                      MulticospanIndex.snd (Cover.index A.unop P) (Cover.Relation.map I f.unop))) ≫
          (IsLimit.conePointUniqueUpToIso
                (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index B.unop P))))
                (limit.isLimit (MulticospanIndex.multicospan (Cover.index B.unop P) ⋙ F))).hom ≫
            (HasLimit.isoOfNatIso (Cover.multicospanComp F P B.unop).symm).hom) ≫
        Multiequalizer.ι (Cover.index B.unop (P ⋙ F)) a =
      (((IsLimit.conePointUniqueUpToIso
                (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index A.unop P))))
                (limit.isLimit (MulticospanIndex.multicospan (Cover.index A.unop P) ⋙ F))).hom ≫
            (HasLimit.isoOfNatIso (Cover.multicospanComp F P A.unop).symm).hom) ≫
          Multiequalizer.lift (Cover.index B.unop (P ⋙ F)) (multiequalizer (Cover.index A.unop (P ⋙ F)))
            (fun I => Multiequalizer.ι (Cover.index A.unop (P ⋙ F)) (Cover.Arrow.map I f.unop))
            (_ :
              ∀ (I : (Cover.index B.unop (P ⋙ F)).R),
                Multiequalizer.ι (Cover.index A.unop (P ⋙ F))
                      (MulticospanIndex.fstTo (Cover.index A.unop (P ⋙ F)) (Cover.Relation.map I f.unop)) ≫
                    MulticospanIndex.fst (Cover.index A.unop (P ⋙ F)) (Cover.Relation.map I f.unop) =
                  Multiequalizer.ι (Cover.index A.unop (P ⋙ F))
                      (MulticospanIndex.sndTo (Cover.index A.unop (P ⋙ F)) (Cover.Relation.map I f.unop)) ≫
                    MulticospanIndex.snd (Cover.index A.unop (P ⋙ F)) (Cover.Relation.map I f.unop))) ≫
        Multiequalizer.ι (Cover.index B.unop (P ⋙ F)) a
[PROOFSTEP]
simp only [Functor.mapCone_π_app, Multiequalizer.multifork_π_app_left, Iso.symm_hom, Multiequalizer.lift_ι,
  eqToHom_refl, Category.comp_id, limit.conePointUniqueUpToIso_hom_comp,
  GrothendieckTopology.Cover.multicospanComp_hom_inv_left, HasLimit.isoOfNatIso_hom_π, Category.assoc]
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category.{max v u, w₁} D
E : Type w₂
inst✝³ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝¹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
X : C
A B : (Cover J X)ᵒᵖ
f : A ⟶ B
⊢ ∀ (a : (Cover.index B.unop (P ⋙ F)).L),
    F.map
          (Multiequalizer.lift (Cover.index B.unop P) (multiequalizer (Cover.index A.unop P))
            (fun I => Multiequalizer.ι (Cover.index A.unop P) (Cover.Arrow.map I f.unop))
            (_ :
              ∀ (I : (Cover.index B.unop P).R),
                Multiequalizer.ι (Cover.index A.unop P)
                      (MulticospanIndex.fstTo (Cover.index A.unop P) (Cover.Relation.map I f.unop)) ≫
                    MulticospanIndex.fst (Cover.index A.unop P) (Cover.Relation.map I f.unop) =
                  Multiequalizer.ι (Cover.index A.unop P)
                      (MulticospanIndex.sndTo (Cover.index A.unop P) (Cover.Relation.map I f.unop)) ≫
                    MulticospanIndex.snd (Cover.index A.unop P) (Cover.Relation.map I f.unop))) ≫
        F.map (Multiequalizer.ι (Cover.index B.unop P) a) =
      F.map (Multiequalizer.ι (Cover.index A.unop P) (Cover.Arrow.map a f.unop))
[PROOFSTEP]
simp only [← F.map_comp, limit.lift_π, Multifork.ofι_π_app, implies_true]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category.{max v u, w₁} D
E : Type w₂
inst✝³ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝¹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
X : C
W : (Cover J X)ᵒᵖ
i : Cover.Arrow W.unop
⊢ NatTrans.app (diagramCompIso J F P X).hom W ≫ Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i =
    F.map (Multiequalizer.ι (Cover.index W.unop P) i)
[PROOFSTEP]
delta diagramCompIso
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category.{max v u, w₁} D
E : Type w₂
inst✝³ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝¹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
X : C
W : (Cover J X)ᵒᵖ
i : Cover.Arrow W.unop
⊢ NatTrans.app
        (NatIso.ofComponents fun W =>
            IsLimit.conePointUniqueUpToIso
                (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
                (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F)) ≪≫
              HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm).hom
        W ≫
      Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i =
    F.map (Multiequalizer.ι (Cover.index W.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
E : Type w₂
inst✝³ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝¹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
X : C
W : (Cover J X)ᵒᵖ
i : Cover.Arrow W.unop
⊢ ((IsLimit.conePointUniqueUpToIso
            (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
            (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F))).hom ≫
        (HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm).hom) ≫
      Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i =
    F.map (Multiequalizer.ι (Cover.index W.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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X : Cᵒᵖ
⊢ (plusObj J P ⋙ F).obj X ≅ (plusObj J (P ⋙ F)).obj X
[PROOFSTEP]
refine' _ ≪≫ HasColimit.isoOfNatIso (J.diagramCompIso F P X.unop)
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X : Cᵒᵖ
⊢ (plusObj J P ⋙ F).obj X ≅ colimit (diagram J P X.unop ⋙ F)
[PROOFSTEP]
refine'
  (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso (colimit.isColimit _)
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (plusObj J P ⋙ F).map f ≫
        ((fun X =>
              IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
                  (colimit.isColimit (diagram J P X.unop ⋙ F)) ≪≫
                HasColimit.isoOfNatIso (diagramCompIso J F P X.unop))
            Y).hom =
      ((fun X =>
              IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
                  (colimit.isColimit (diagram J P X.unop ⋙ F)) ≪≫
                HasColimit.isoOfNatIso (diagramCompIso J F P X.unop))
            X).hom ≫
        (plusObj J (P ⋙ F)).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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (plusObj J P ⋙ F).map f ≫
      ((fun X =>
            IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
                (colimit.isColimit (diagram J P X.unop ⋙ F)) ≪≫
              HasColimit.isoOfNatIso (diagramCompIso J F P X.unop))
          Y).hom =
    ((fun X =>
            IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
                (colimit.isColimit (diagram J P X.unop ⋙ F)) ≪≫
              HasColimit.isoOfNatIso (diagramCompIso J F P X.unop))
          X).hom ≫
      (plusObj J (P ⋙ F)).map f
[PROOFSTEP]
apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_ext
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (j : (Cover J X.unop)ᵒᵖ),
    NatTrans.app (F.mapCocone (colimit.cocone (diagram J P X.unop))).ι j ≫
        (plusObj J P ⋙ F).map f ≫
          ((fun X =>
                IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
                    (colimit.isColimit (diagram J P X.unop ⋙ F)) ≪≫
                  HasColimit.isoOfNatIso (diagramCompIso J F P X.unop))
              Y).hom =
      NatTrans.app (F.mapCocone (colimit.cocone (diagram J P X.unop))).ι j ≫
        ((fun X =>
                IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
                    (colimit.isColimit (diagram J P X.unop ⋙ F)) ≪≫
                  HasColimit.isoOfNatIso (diagramCompIso J F P X.unop))
              X).hom ≫
          (plusObj J (P ⋙ F)).map f
[PROOFSTEP]
intro W
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
⊢ NatTrans.app (F.mapCocone (colimit.cocone (diagram J P X.unop))).ι W ≫
      (plusObj J P ⋙ F).map f ≫
        ((fun X =>
              IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
                  (colimit.isColimit (diagram J P X.unop ⋙ F)) ≪≫
                HasColimit.isoOfNatIso (diagramCompIso J F P X.unop))
            Y).hom =
    NatTrans.app (F.mapCocone (colimit.cocone (diagram J P X.unop))).ι W ≫
      ((fun X =>
              IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
                  (colimit.isColimit (diagram J P X.unop ⋙ F)) ≪≫
                HasColimit.isoOfNatIso (diagramCompIso J F P X.unop))
            X).hom ≫
        (plusObj J (P ⋙ F)).map f
[PROOFSTEP]
dsimp [plusObj, plusMap]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
⊢ F.map (colimit.ι (diagram J P X.unop) W) ≫
      F.map (colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op) ≫
        (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
              (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom ≫
          (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom =
    F.map (colimit.ι (diagram J P X.unop) W) ≫
      ((IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
              (colimit.isColimit (diagram J P X.unop ⋙ F))).hom ≫
          (HasColimit.isoOfNatIso (diagramCompIso J F P X.unop)).hom) ≫
        colimMap (diagramPullback J (P ⋙ F) f.unop) ≫ colimit.pre (diagram J (P ⋙ F) Y.unop) (pullback J f.unop).op
[PROOFSTEP]
simp only [Functor.map_comp, Category.assoc]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
⊢ F.map (colimit.ι (diagram J P X.unop) W) ≫
      F.map (colimMap (diagramPullback J P f.unop)) ≫
        F.map (colimit.pre (diagram J P Y.unop) (pullback J f.unop).op) ≫
          (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
                (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom ≫
            (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom =
    F.map (colimit.ι (diagram J P X.unop) W) ≫
      (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
            (colimit.isColimit (diagram J P X.unop ⋙ F))).hom ≫
        (HasColimit.isoOfNatIso (diagramCompIso J F P X.unop)).hom ≫
          colimMap (diagramPullback J (P ⋙ F) f.unop) ≫ colimit.pre (diagram J (P ⋙ F) Y.unop) (pullback J f.unop).op
[PROOFSTEP]
slice_rhs 1 2 => erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).fac]
[GOAL]
case a.a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map (colimit.ι (diagram J P X.unop) W) ≫
    (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
        (colimit.isColimit (diagram J P X.unop ⋙ F))).hom
case a.a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P X.unop)).hom
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| colimMap (diagramPullback J (P ⋙ F) f.unop)
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| colimit.pre (diagram J (P ⋙ F) Y.unop) (pullback J f.unop).op
[PROOFSTEP]
erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).fac]
[GOAL]
case a.a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map (colimit.ι (diagram J P X.unop) W) ≫
    (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
        (colimit.isColimit (diagram J P X.unop ⋙ F))).hom
case a.a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P X.unop)).hom
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| colimMap (diagramPullback J (P ⋙ F) f.unop)
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| colimit.pre (diagram J (P ⋙ F) Y.unop) (pullback J f.unop).op
[PROOFSTEP]
erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).fac]
[GOAL]
case a.a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map (colimit.ι (diagram J P X.unop) W) ≫
    (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
        (colimit.isColimit (diagram J P X.unop ⋙ F))).hom
case a.a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P X.unop)).hom
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| colimMap (diagramPullback J (P ⋙ F) f.unop)
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| colimit.pre (diagram J (P ⋙ F) Y.unop) (pullback J f.unop).op
[PROOFSTEP]
erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).fac]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
⊢ F.map (colimit.ι (diagram J P X.unop) W) ≫
      F.map (colimMap (diagramPullback J P f.unop)) ≫
        F.map (colimit.pre (diagram J P Y.unop) (pullback J f.unop).op) ≫
          (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
                (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom ≫
            (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom =
    ((NatTrans.app (colimit.cocone (diagram J P X.unop ⋙ F)).ι W ≫
          (HasColimit.isoOfNatIso (diagramCompIso J F P X.unop)).hom) ≫
        colimMap (diagramPullback J (P ⋙ F) f.unop)) ≫
      colimit.pre (diagram J (P ⋙ F) Y.unop) (pullback J f.unop).op
[PROOFSTEP]
slice_lhs 1 3 =>
  simp only [← F.map_comp]
  dsimp [colimMap, IsColimit.map, colimit.pre]
  simp only [colimit.ι_desc_assoc, colimit.ι_desc]
  dsimp [Cocones.precompose]
  simp only [Category.assoc, colimit.ι_desc]
  dsimp [Cocone.whisker]
  rw [F.map_comp]
[GOAL]
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map (colimit.ι (diagram J P X.unop) W) ≫
    F.map (colimMap (diagramPullback J P f.unop)) ≫ F.map (colimit.pre (diagram J P Y.unop) (pullback J f.unop).op)
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
      (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom
[PROOFSTEP]
  simp only [← F.map_comp]
  dsimp [colimMap, IsColimit.map, colimit.pre]
  simp only [colimit.ι_desc_assoc, colimit.ι_desc]
  dsimp [Cocones.precompose]
  simp only [Category.assoc, colimit.ι_desc]
  dsimp [Cocone.whisker]
  rw [F.map_comp]
[GOAL]
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map (colimit.ι (diagram J P X.unop) W) ≫
    F.map (colimMap (diagramPullback J P f.unop)) ≫ F.map (colimit.pre (diagram J P Y.unop) (pullback J f.unop).op)
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
      (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom
[PROOFSTEP]
  simp only [← F.map_comp]
  dsimp [colimMap, IsColimit.map, colimit.pre]
  simp only [colimit.ι_desc_assoc, colimit.ι_desc]
  dsimp [Cocones.precompose]
  simp only [Category.assoc, colimit.ι_desc]
  dsimp [Cocone.whisker]
  rw [F.map_comp]
[GOAL]
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map (colimit.ι (diagram J P X.unop) W) ≫
    F.map (colimMap (diagramPullback J P f.unop)) ≫ F.map (colimit.pre (diagram J P Y.unop) (pullback J f.unop).op)
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
      (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom
[PROOFSTEP]
simp only [← F.map_comp]
[GOAL]
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map
    (colimit.ι (diagram J P X.unop) W ≫
      colimMap (diagramPullback J P f.unop) ≫ colimit.pre (diagram J P Y.unop) (pullback J f.unop).op)
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
      (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom
[PROOFSTEP]
dsimp [colimMap, IsColimit.map, colimit.pre]
[GOAL]
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map
    (colimit.ι (diagram J P X.unop) W ≫
      colimit.desc (diagram J P X.unop)
          ((Cocones.precompose (diagramPullback J P f.unop)).obj
            (colimit.cocone ((pullback J f.unop).op ⋙ diagram J P Y.unop))) ≫
        colimit.desc ((pullback J f.unop).op ⋙ diagram J P Y.unop)
          (Cocone.whisker (pullback J f.unop).op (colimit.cocone (diagram J P Y.unop))))
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
      (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom
[PROOFSTEP]
simp only [colimit.ι_desc_assoc, colimit.ι_desc]
[GOAL]
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map
    (NatTrans.app
        ((Cocones.precompose (diagramPullback J P f.unop)).obj
            (colimit.cocone ((pullback J f.unop).op ⋙ diagram J P Y.unop))).ι
        W ≫
      colimit.desc ((pullback J f.unop).op ⋙ diagram J P Y.unop)
        (Cocone.whisker (pullback J f.unop).op (colimit.cocone (diagram J P Y.unop))))
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
      (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom
[PROOFSTEP]
dsimp [Cocones.precompose]
[GOAL]
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map
    ((Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
          (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
              Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I)) ≫
        colimit.ι ((pullback J f.unop).op ⋙ diagram J P Y.unop) W) ≫
      colimit.desc ((pullback J f.unop).op ⋙ diagram J P Y.unop)
        (Cocone.whisker (pullback J f.unop).op (colimit.cocone (diagram J P Y.unop))))
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
      (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom
[PROOFSTEP]
simp only [Category.assoc, colimit.ι_desc]
[GOAL]
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map
    (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
        (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
            Multiequalizer.ι (Cover.index W.unop P)
                  (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index W.unop P)
                  (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I)) ≫
      NatTrans.app (Cocone.whisker (pullback J f.unop).op (colimit.cocone (diagram J P Y.unop))).ι W)
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
      (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom
[PROOFSTEP]
dsimp [Cocone.whisker]
[GOAL]
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map
    (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
        (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
            Multiequalizer.ι (Cover.index W.unop P)
                  (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index W.unop P)
                  (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I)) ≫
      colimit.ι (diagram J P Y.unop) (op (Cover.pullback W.unop f.unop)))
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
      (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom
[PROOFSTEP]
rw [F.map_comp]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
⊢ ((F.map
            (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
              (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
              (_ :
                ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
                  Multiequalizer.ι (Cover.index W.unop P)
                        (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                      MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
                    Multiequalizer.ι (Cover.index W.unop P)
                        (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                      MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I))) ≫
          F.map (colimit.ι (diagram J P Y.unop) (op (Cover.pullback W.unop f.unop)))) ≫
        (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
            (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom) ≫
      (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom =
    ((NatTrans.app (colimit.cocone (diagram J P X.unop ⋙ F)).ι W ≫
          (HasColimit.isoOfNatIso (diagramCompIso J F P X.unop)).hom) ≫
        colimMap (diagramPullback J (P ⋙ F) f.unop)) ≫
      colimit.pre (diagram J (P ⋙ F) Y.unop) (pullback J f.unop).op
[PROOFSTEP]
simp only [Category.assoc]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
⊢ F.map
        (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
          (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
              Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I))) ≫
      F.map (colimit.ι (diagram J P Y.unop) (op (Cover.pullback W.unop f.unop))) ≫
        (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
              (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom ≫
          (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom =
    NatTrans.app (colimit.cocone (diagram J P X.unop ⋙ F)).ι W ≫
      (HasColimit.isoOfNatIso (diagramCompIso J F P X.unop)).hom ≫
        colimMap (diagramPullback J (P ⋙ F) f.unop) ≫ colimit.pre (diagram J (P ⋙ F) Y.unop) (pullback J f.unop).op
[PROOFSTEP]
slice_lhs 2 3 => erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P Y.unop))).fac]
[GOAL]
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map (colimit.ι (diagram J P Y.unop) (op (Cover.pullback W.unop f.unop))) ≫
    (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
        (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map
    (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
      (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
      (_ :
        ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
          Multiequalizer.ι (Cover.index W.unop P)
                (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
              MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
            Multiequalizer.ι (Cover.index W.unop P)
                (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
              MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I)))
[PROOFSTEP]
erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P Y.unop))).fac]
[GOAL]
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map (colimit.ι (diagram J P Y.unop) (op (Cover.pullback W.unop f.unop))) ≫
    (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
        (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map
    (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
      (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
      (_ :
        ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
          Multiequalizer.ι (Cover.index W.unop P)
                (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
              MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
            Multiequalizer.ι (Cover.index W.unop P)
                (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
              MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I)))
[PROOFSTEP]
erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P Y.unop))).fac]
[GOAL]
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map (colimit.ι (diagram J P Y.unop) (op (Cover.pullback W.unop f.unop))) ≫
    (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P Y.unop)))
        (colimit.isColimit (diagram J P Y.unop ⋙ F))).hom
case a.a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
| F.map
    (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
      (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
      (_ :
        ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
          Multiequalizer.ι (Cover.index W.unop P)
                (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
              MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
            Multiequalizer.ι (Cover.index W.unop P)
                (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
              MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I)))
[PROOFSTEP]
erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P Y.unop))).fac]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
⊢ F.map
        (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
          (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
              Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I))) ≫
      NatTrans.app (colimit.cocone (diagram J P Y.unop ⋙ F)).ι (op (Cover.pullback W.unop f.unop)) ≫
        (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom =
    NatTrans.app (colimit.cocone (diagram J P X.unop ⋙ F)).ι W ≫
      (HasColimit.isoOfNatIso (diagramCompIso J F P X.unop)).hom ≫
        colimMap (diagramPullback J (P ⋙ F) f.unop) ≫ colimit.pre (diagram J (P ⋙ F) Y.unop) (pullback J f.unop).op
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
⊢ F.map
        (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
          (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
              Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I))) ≫
      colimit.ι (diagram J P Y.unop ⋙ F) (op (Cover.pullback W.unop f.unop)) ≫
        (HasColimit.isoOfNatIso (diagramCompIso J F P Y.unop)).hom =
    colimit.ι (diagram J P X.unop ⋙ F) W ≫
      (HasColimit.isoOfNatIso (diagramCompIso J F P X.unop)).hom ≫
        colimMap (diagramPullback J (P ⋙ F) f.unop) ≫ colimit.pre (diagram J (P ⋙ F) Y.unop) (pullback J f.unop).op
[PROOFSTEP]
simp only [HasColimit.isoOfNatIso_ι_hom_assoc, GrothendieckTopology.diagramPullback_app, colimit.ι_pre,
  HasColimit.isoOfNatIso_ι_hom, ι_colimMap_assoc]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
⊢ F.map
        (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
          (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
              Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I))) ≫
      NatTrans.app (diagramCompIso J F P Y.unop).hom (op (Cover.pullback W.unop f.unop)) ≫
        colimit.ι (diagram J (P ⋙ F) Y.unop) (op (Cover.pullback W.unop f.unop)) =
    NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
      Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj W).unop (P ⋙ F)) ((diagram J (P ⋙ F) X.unop).obj W)
          (fun I => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop (P ⋙ F)).R),
              Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                    (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                    (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
        colimit.ι (diagram J (P ⋙ F) Y.unop) ((pullback J f.unop).op.obj W)
[PROOFSTEP]
simp only [← Category.assoc]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
⊢ (F.map
          (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
            (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
            (_ :
              ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
                Multiequalizer.ι (Cover.index W.unop P)
                      (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                    MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
                  Multiequalizer.ι (Cover.index W.unop P)
                      (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                    MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I))) ≫
        NatTrans.app (diagramCompIso J F P Y.unop).hom (op (Cover.pullback W.unop f.unop))) ≫
      colimit.ι (diagram J (P ⋙ F) Y.unop) (op (Cover.pullback W.unop f.unop)) =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index ((pullback J f.unop).op.obj W).unop (P ⋙ F)) ((diagram J (P ⋙ F) X.unop).obj W)
          (fun I => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop (P ⋙ F)).R),
              Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                    (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                    (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I))) ≫
      colimit.ι (diagram J (P ⋙ F) Y.unop) ((pullback J f.unop).op.obj W)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
⊢ (F.map
          (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
            (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
            (_ :
              ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
                Multiequalizer.ι (Cover.index W.unop P)
                      (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                    MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
                  Multiequalizer.ι (Cover.index W.unop P)
                      (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                    MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I))) ≫
        NatTrans.app (diagramCompIso J F P Y.unop).hom (op (Cover.pullback W.unop f.unop))) ≫
      colimit.ι (diagram J (P ⋙ F) Y.unop) (op (Cover.pullback W.unop f.unop)) =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F))
          (multiequalizer (Cover.index W.unop (P ⋙ F)))
          (fun I => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop (P ⋙ F)).R),
              Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                    (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                    (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I))) ≫
      colimit.ι (diagram J (P ⋙ F) Y.unop) (op (Cover.pullback W.unop f.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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
⊢ F.map
        (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
          (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
              Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I))) ≫
      NatTrans.app (diagramCompIso J F P Y.unop).hom (op (Cover.pullback W.unop f.unop)) =
    NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
      Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F))
        (multiequalizer (Cover.index W.unop (P ⋙ F)))
        (fun I => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) (Cover.Arrow.base I))
        (_ :
          ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop (P ⋙ F)).R),
            Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                  (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                MulticospanIndex.fst (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I) =
              Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                  (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                MulticospanIndex.snd (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I))
[PROOFSTEP]
ext
[GOAL]
case e_a.h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
a✝ : (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F)).L
⊢ (F.map
          (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
            (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
            (_ :
              ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
                Multiequalizer.ι (Cover.index W.unop P)
                      (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                    MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
                  Multiequalizer.ι (Cover.index W.unop P)
                      (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                    MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I))) ≫
        NatTrans.app (diagramCompIso J F P Y.unop).hom (op (Cover.pullback W.unop f.unop))) ≫
      Multiequalizer.ι (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F)) a✝ =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F))
          (multiequalizer (Cover.index W.unop (P ⋙ F)))
          (fun I => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop (P ⋙ F)).R),
              Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                    (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                    (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I))) ≫
      Multiequalizer.ι (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F)) a✝
[PROOFSTEP]
dsimp
[GOAL]
case e_a.h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
a✝ : (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F)).L
⊢ (F.map
          (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
            (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
            (_ :
              ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
                Multiequalizer.ι (Cover.index W.unop P)
                      (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                    MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
                  Multiequalizer.ι (Cover.index W.unop P)
                      (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                    MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I))) ≫
        NatTrans.app (diagramCompIso J F P Y.unop).hom (op (Cover.pullback W.unop f.unop))) ≫
      Multiequalizer.ι (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F)) a✝ =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F))
          (multiequalizer (Cover.index W.unop (P ⋙ F)))
          (fun I => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop (P ⋙ F)).R),
              Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                    (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                    (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I))) ≫
      Multiequalizer.ι (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F)) a✝
[PROOFSTEP]
simp only [Category.assoc]
[GOAL]
case e_a.h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (Cover J X.unop)ᵒᵖ
a✝ : (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F)).L
⊢ F.map
        (Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) P) (multiequalizer (Cover.index W.unop P))
          (fun I => Multiequalizer.ι (Cover.index W.unop P) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop P).R),
              Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.fstTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop P) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop P)
                    (MulticospanIndex.sndTo (Cover.index W.unop P) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop P) (Cover.Relation.base I))) ≫
      NatTrans.app (diagramCompIso J F P Y.unop).hom (op (Cover.pullback W.unop f.unop)) ≫
        Multiequalizer.ι (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F)) a✝ =
    NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
      Multiequalizer.lift (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F))
          (multiequalizer (Cover.index W.unop (P ⋙ F)))
          (fun I => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) (Cover.Arrow.base I))
          (_ :
            ∀ (I : (Cover.index ((pullback J f.unop).op.obj W).unop (P ⋙ F)).R),
              Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                    (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                  MulticospanIndex.fst (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I) =
                Multiequalizer.ι (Cover.index W.unop (P ⋙ F))
                    (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
                  MulticospanIndex.snd (Cover.index W.unop (P ⋙ F)) (Cover.Relation.base I)) ≫
        Multiequalizer.ι (Cover.index (Cover.pullback W.unop f.unop) (P ⋙ F)) a✝
[PROOFSTEP]
erw [Multiequalizer.lift_ι, diagramCompIso_hom_ι, diagramCompIso_hom_ι, ← F.map_comp, Multiequalizer.lift_ι]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ F.map (colimit.ι (diagram J P X.unop) W) ≫ NatTrans.app (plusCompIso J F P).hom X =
    NatTrans.app (diagramCompIso J F P X.unop).hom W ≫ colimit.ι (diagram J (P ⋙ F) X.unop) W
[PROOFSTEP]
delta diagramCompIso plusCompIso
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ F.map (colimit.ι (diagram J P X.unop) W) ≫
      NatTrans.app
        (NatIso.ofComponents fun X =>
            IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
                (colimit.isColimit (diagram J P X.unop ⋙ F)) ≪≫
              HasColimit.isoOfNatIso
                (NatIso.ofComponents fun W =>
                  IsLimit.conePointUniqueUpToIso
                      (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
                      (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F)) ≪≫
                    HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm)).hom
        X =
    NatTrans.app
        (NatIso.ofComponents fun W =>
            IsLimit.conePointUniqueUpToIso
                (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
                (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F)) ≪≫
              HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm).hom
        W ≫
      colimit.ι (diagram J (P ⋙ F) X.unop) W
[PROOFSTEP]
simp only [IsColimit.descCoconeMorphism_Hom, IsColimit.uniqueUpToIso_hom, Cocones.forget_map, Iso.trans_hom,
  NatIso.ofComponents_hom_app, Functor.mapIso_hom, ← Category.assoc]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ (F.map (colimit.ι (diagram J P X.unop) W) ≫
        (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (diagram J P X.unop)))
            (colimit.isColimit (diagram J P X.unop ⋙ F))).hom) ≫
      (HasColimit.isoOfNatIso
          (NatIso.ofComponents fun W =>
            IsLimit.conePointUniqueUpToIso
                (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
                (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F)) ≪≫
              HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm)).hom =
    ((IsLimit.conePointUniqueUpToIso
            (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
            (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F))).hom ≫
        (HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm).hom) ≫
      colimit.ι (diagram J (P ⋙ F) X.unop) W
[PROOFSTEP]
erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).fac]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ NatTrans.app (colimit.cocone (diagram J P X.unop ⋙ F)).ι W ≫
      (HasColimit.isoOfNatIso
          (NatIso.ofComponents fun W =>
            IsLimit.conePointUniqueUpToIso
                (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
                (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F)) ≪≫
              HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm)).hom =
    ((IsLimit.conePointUniqueUpToIso
            (isLimitOfPreserves F (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P))))
            (limit.isLimit (MulticospanIndex.multicospan (Cover.index W.unop P) ⋙ F))).hom ≫
        (HasLimit.isoOfNatIso (Cover.multicospanComp F P W.unop).symm).hom) ≫
      colimit.ι (diagram J (P ⋙ F) X.unop) W
[PROOFSTEP]
simp only [Category.assoc, HasLimit.isoOfNatIso_hom_π, Iso.symm_hom, Cover.multicospanComp_hom_inv_left, eqToHom_refl,
  Category.comp_id, limit.conePointUniqueUpToIso_hom_comp, Functor.mapCone_π_app, Multiequalizer.multifork_π_app_left,
  Multiequalizer.lift_ι, Functor.map_comp, eq_self_iff_true, Category.assoc, Iso.trans_hom, Iso.cancel_iso_hom_left,
  NatIso.ofComponents_hom_app, colimit.cocone_ι, Category.assoc, HasColimit.isoOfNatIso_ι_hom]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝¹¹ : Category.{max v u, w₁} D
E : Type w₂
inst✝¹⁰ : Category.{max v u, w₂} E
F✝ : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F✝
P✝ : Cᵒᵖ ⥤ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁴ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F✝
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝² : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ G
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) G
⊢ whiskerLeft (plusObj J P) η ≫ (plusCompIso J G P).hom = (plusCompIso J F P).hom ≫ plusMap J (whiskerLeft P η)
[PROOFSTEP]
ext X
[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
E : Type w₂
inst✝¹⁰ : Category.{max v u, w₂} E
F✝ : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F✝
P✝ : Cᵒᵖ ⥤ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁴ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F✝
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝² : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ G
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) G
X : Cᵒᵖ
⊢ NatTrans.app (whiskerLeft (plusObj J P) η ≫ (plusCompIso J G P).hom) X =
    NatTrans.app ((plusCompIso J F P).hom ≫ plusMap J (whiskerLeft P η)) X
[PROOFSTEP]
apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_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
E : Type w₂
inst✝¹⁰ : Category.{max v u, w₂} E
F✝ : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F✝
P✝ : Cᵒᵖ ⥤ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁴ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F✝
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝² : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ G
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) G
X : Cᵒᵖ
⊢ ∀ (j : (Cover J X.unop)ᵒᵖ),
    NatTrans.app (F.mapCocone (colimit.cocone (diagram J P X.unop))).ι j ≫
        NatTrans.app (whiskerLeft (plusObj J P) η ≫ (plusCompIso J G P).hom) X =
      NatTrans.app (F.mapCocone (colimit.cocone (diagram J P X.unop))).ι j ≫
        NatTrans.app ((plusCompIso J F P).hom ≫ plusMap J (whiskerLeft P η)) X
[PROOFSTEP]
intro W
[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
E : Type w₂
inst✝¹⁰ : Category.{max v u, w₂} E
F✝ : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F✝
P✝ : Cᵒᵖ ⥤ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁴ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F✝
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝² : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ G
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) G
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ NatTrans.app (F.mapCocone (colimit.cocone (diagram J P X.unop))).ι W ≫
      NatTrans.app (whiskerLeft (plusObj J P) η ≫ (plusCompIso J G P).hom) X =
    NatTrans.app (F.mapCocone (colimit.cocone (diagram J P X.unop))).ι W ≫
      NatTrans.app ((plusCompIso J F P).hom ≫ plusMap J (whiskerLeft P η)) X
[PROOFSTEP]
dsimp [plusObj, 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
E : Type w₂
inst✝¹⁰ : Category.{max v u, w₂} E
F✝ : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F✝
P✝ : Cᵒᵖ ⥤ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁴ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F✝
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝² : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ G
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) G
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ F.map (colimit.ι (diagram J P X.unop) W) ≫
      NatTrans.app η (colimit (diagram J P X.unop)) ≫ NatTrans.app (plusCompIso J G P).hom X =
    F.map (colimit.ι (diagram J P X.unop) W) ≫
      NatTrans.app (plusCompIso J F P).hom X ≫ colimMap (diagramNatTrans J (whiskerLeft P η) X.unop)
[PROOFSTEP]
simp only [ι_plusCompIso_hom, ι_colimMap, whiskerLeft_app, ι_plusCompIso_hom_assoc, NatTrans.naturality_assoc,
  GrothendieckTopology.diagramNatTrans_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
E : Type w₂
inst✝¹⁰ : Category.{max v u, w₂} E
F✝ : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F✝
P✝ : Cᵒᵖ ⥤ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁴ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F✝
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝² : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ G
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) G
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ NatTrans.app η (multiequalizer (Cover.index W.unop P)) ≫
      NatTrans.app (diagramCompIso J G P X.unop).hom W ≫ colimit.ι (diagram J (P ⋙ G) X.unop) W =
    NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
      Multiequalizer.lift (Cover.index W.unop (P ⋙ G)) ((diagram J (P ⋙ F) X.unop).obj W)
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
          (_ :
            ∀ (b : (Cover.index W.unop (P ⋙ G)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
                    (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ G)) b) ≫
                  MulticospanIndex.fst (Cover.index W.unop (P ⋙ G)) b =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
                    (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ G)) b) ≫
                  MulticospanIndex.snd (Cover.index W.unop (P ⋙ G)) b) ≫
        colimit.ι (diagram J (P ⋙ G) X.unop) W
[PROOFSTEP]
simp only [← 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
E : Type w₂
inst✝¹⁰ : Category.{max v u, w₂} E
F✝ : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F✝
P✝ : Cᵒᵖ ⥤ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁴ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F✝
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝² : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ G
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) G
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ (NatTrans.app η (multiequalizer (Cover.index W.unop P)) ≫ NatTrans.app (diagramCompIso J G P X.unop).hom W) ≫
      colimit.ι (diagram J (P ⋙ G) X.unop) W =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index W.unop (P ⋙ G)) ((diagram J (P ⋙ F) X.unop).obj W)
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
          (_ :
            ∀ (b : (Cover.index W.unop (P ⋙ G)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
                    (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ G)) b) ≫
                  MulticospanIndex.fst (Cover.index W.unop (P ⋙ G)) b =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
                    (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ G)) b) ≫
                  MulticospanIndex.snd (Cover.index W.unop (P ⋙ G)) b)) ≫
      colimit.ι (diagram J (P ⋙ G) X.unop) W
[PROOFSTEP]
congr 1
  -- porting note: this used to work with `ext`
    -- See https://github.com/leanprover-community/mathlib4/issues/5229
[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
E : Type w₂
inst✝¹⁰ : Category.{max v u, w₂} E
F✝ : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F✝
P✝ : Cᵒᵖ ⥤ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁴ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F✝
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝² : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ G
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) G
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ NatTrans.app η (multiequalizer (Cover.index W.unop P)) ≫ NatTrans.app (diagramCompIso J G P X.unop).hom W =
    NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
      Multiequalizer.lift (Cover.index W.unop (P ⋙ G)) ((diagram J (P ⋙ F) X.unop).obj W)
        (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
        (_ :
          ∀ (b : (Cover.index W.unop (P ⋙ G)).R),
            (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
                  (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ G)) b) ≫
                MulticospanIndex.fst (Cover.index W.unop (P ⋙ G)) b =
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
                  (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ G)) b) ≫
                MulticospanIndex.snd (Cover.index W.unop (P ⋙ G)) b)
[PROOFSTEP]
apply Multiequalizer.hom_ext
[GOAL]
case w.h.e_a.h
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝¹¹ : Category.{max v u, w₁} D
E : Type w₂
inst✝¹⁰ : Category.{max v u, w₂} E
F✝ : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F✝
P✝ : Cᵒᵖ ⥤ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁴ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F✝
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝² : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ G
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) G
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ ∀ (a : (Cover.index W.unop (P ⋙ G)).L),
    (NatTrans.app η (multiequalizer (Cover.index W.unop P)) ≫ NatTrans.app (diagramCompIso J G P X.unop).hom W) ≫
        Multiequalizer.ι (Cover.index W.unop (P ⋙ G)) a =
      (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
          Multiequalizer.lift (Cover.index W.unop (P ⋙ G)) ((diagram J (P ⋙ F) X.unop).obj W)
            (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
            (_ :
              ∀ (b : (Cover.index W.unop (P ⋙ G)).R),
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
                      (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ G)) b) ≫
                    MulticospanIndex.fst (Cover.index W.unop (P ⋙ G)) b =
                  (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
                      (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ G)) b) ≫
                    MulticospanIndex.snd (Cover.index W.unop (P ⋙ G)) b)) ≫
        Multiequalizer.ι (Cover.index W.unop (P ⋙ G)) a
[PROOFSTEP]
intro a
[GOAL]
case w.h.e_a.h
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝¹¹ : Category.{max v u, w₁} D
E : Type w₂
inst✝¹⁰ : Category.{max v u, w₂} E
F✝ : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F✝
P✝ : Cᵒᵖ ⥤ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁴ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F✝
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝² : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ G
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) G
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
a : (Cover.index W.unop (P ⋙ G)).L
⊢ (NatTrans.app η (multiequalizer (Cover.index W.unop P)) ≫ NatTrans.app (diagramCompIso J G P X.unop).hom W) ≫
      Multiequalizer.ι (Cover.index W.unop (P ⋙ G)) a =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index W.unop (P ⋙ G)) ((diagram J (P ⋙ F) X.unop).obj W)
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
          (_ :
            ∀ (b : (Cover.index W.unop (P ⋙ G)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
                    (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ G)) b) ≫
                  MulticospanIndex.fst (Cover.index W.unop (P ⋙ G)) b =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
                    (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ G)) b) ≫
                  MulticospanIndex.snd (Cover.index W.unop (P ⋙ G)) b)) ≫
      Multiequalizer.ι (Cover.index W.unop (P ⋙ G)) a
[PROOFSTEP]
dsimp
[GOAL]
case w.h.e_a.h
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝¹¹ : Category.{max v u, w₁} D
E : Type w₂
inst✝¹⁰ : Category.{max v u, w₂} E
F✝ : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F✝
P✝ : Cᵒᵖ ⥤ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁴ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F✝
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝² : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ G
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) G
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
a : (Cover.index W.unop (P ⋙ G)).L
⊢ (NatTrans.app η (multiequalizer (Cover.index W.unop P)) ≫ NatTrans.app (diagramCompIso J G P X.unop).hom W) ≫
      Multiequalizer.ι (Cover.index W.unop (P ⋙ G)) a =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index W.unop (P ⋙ G)) (multiequalizer (Cover.index W.unop (P ⋙ F)))
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app η (P.obj (op i.Y)))
          (_ :
            ∀ (i : (Cover.index W.unop (P ⋙ G)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerLeft P η) (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index W.unop (P ⋙ G)) i) ≫
                  MulticospanIndex.fst (Cover.index W.unop (P ⋙ G)) i =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerLeft P η) (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index W.unop (P ⋙ G)) i) ≫
                  MulticospanIndex.snd (Cover.index W.unop (P ⋙ G)) i)) ≫
      Multiequalizer.ι (Cover.index W.unop (P ⋙ G)) a
[PROOFSTEP]
simp
  -- Porting note: in mathlib3 `simp` managed to apply this.
[GOAL]
case w.h.e_a.h
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝¹¹ : Category.{max v u, w₁} D
E : Type w₂
inst✝¹⁰ : Category.{max v u, w₂} E
F✝ : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F✝
P✝ : Cᵒᵖ ⥤ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁴ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F✝
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝² : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ G
inst✝ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) G
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
a : (Cover.index W.unop (P ⋙ G)).L
⊢ NatTrans.app η (multiequalizer (Cover.index W.unop P)) ≫ G.map (Multiequalizer.ι (Cover.index W.unop P) a) =
    F.map (Multiequalizer.ι (Cover.index W.unop P) a) ≫ NatTrans.app η (P.obj (op a.Y))
[PROOFSTEP]
erw [η.naturality]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
⊢ whiskerRight (plusMap J η) F ≫ (plusCompIso J F Q).hom = (plusCompIso J F P).hom ≫ plusMap J (whiskerRight η F)
[PROOFSTEP]
ext X
[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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
⊢ NatTrans.app (whiskerRight (plusMap J η) F ≫ (plusCompIso J F Q).hom) X =
    NatTrans.app ((plusCompIso J F P).hom ≫ plusMap J (whiskerRight η F)) X
[PROOFSTEP]
apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
⊢ ∀ (j : (Cover J X.unop)ᵒᵖ),
    NatTrans.app (F.mapCocone (colimit.cocone (diagram J P X.unop))).ι j ≫
        NatTrans.app (whiskerRight (plusMap J η) F ≫ (plusCompIso J F Q).hom) X =
      NatTrans.app (F.mapCocone (colimit.cocone (diagram J P X.unop))).ι j ≫
        NatTrans.app ((plusCompIso J F P).hom ≫ plusMap J (whiskerRight η F)) X
[PROOFSTEP]
intro W
[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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ NatTrans.app (F.mapCocone (colimit.cocone (diagram J P X.unop))).ι W ≫
      NatTrans.app (whiskerRight (plusMap J η) F ≫ (plusCompIso J F Q).hom) X =
    NatTrans.app (F.mapCocone (colimit.cocone (diagram J P X.unop))).ι W ≫
      NatTrans.app ((plusCompIso J F P).hom ≫ plusMap J (whiskerRight η F)) X
[PROOFSTEP]
dsimp [plusObj, 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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ F.map (colimit.ι (diagram J P X.unop) W) ≫
      F.map (colimMap (diagramNatTrans J η X.unop)) ≫ NatTrans.app (plusCompIso J F Q).hom X =
    F.map (colimit.ι (diagram J P X.unop) W) ≫
      NatTrans.app (plusCompIso J F P).hom X ≫ colimMap (diagramNatTrans J (whiskerRight η F) X.unop)
[PROOFSTEP]
simp only [ι_colimMap, whiskerRight_app, ι_plusCompIso_hom_assoc, GrothendieckTopology.diagramNatTrans_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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ F.map (colimit.ι (diagram J P X.unop) W) ≫
      F.map (colimMap (diagramNatTrans J η X.unop)) ≫ NatTrans.app (plusCompIso J F Q).hom X =
    NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
      Multiequalizer.lift (Cover.index W.unop (Q ⋙ F)) ((diagram J (P ⋙ F) X.unop).obj W)
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
          (_ :
            ∀ (b : (Cover.index W.unop (Q ⋙ F)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
                    (MulticospanIndex.fstTo (Cover.index W.unop (Q ⋙ F)) b) ≫
                  MulticospanIndex.fst (Cover.index W.unop (Q ⋙ F)) b =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
                    (MulticospanIndex.sndTo (Cover.index W.unop (Q ⋙ F)) b) ≫
                  MulticospanIndex.snd (Cover.index W.unop (Q ⋙ F)) b) ≫
        colimit.ι (diagram J (Q ⋙ F) X.unop) W
[PROOFSTEP]
simp only [← Category.assoc, ← F.map_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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ F.map (colimit.ι (diagram J P X.unop) W ≫ colimMap (diagramNatTrans J η X.unop)) ≫
      NatTrans.app (plusCompIso J F Q).hom X =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index W.unop (Q ⋙ F)) ((diagram J (P ⋙ F) X.unop).obj W)
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
          (_ :
            ∀ (b : (Cover.index W.unop (Q ⋙ F)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
                    (MulticospanIndex.fstTo (Cover.index W.unop (Q ⋙ F)) b) ≫
                  MulticospanIndex.fst (Cover.index W.unop (Q ⋙ F)) b =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
                    (MulticospanIndex.sndTo (Cover.index W.unop (Q ⋙ F)) b) ≫
                  MulticospanIndex.snd (Cover.index W.unop (Q ⋙ F)) b)) ≫
      colimit.ι (diagram J (Q ⋙ F) X.unop) W
[PROOFSTEP]
dsimp [colimMap, IsColimit.map]
[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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ F.map
        (colimit.ι (diagram J P X.unop) W ≫
          colimit.desc (diagram J P X.unop)
            ((Cocones.precompose (diagramNatTrans J η X.unop)).obj (colimit.cocone (diagram J Q X.unop)))) ≫
      NatTrans.app (plusCompIso J F Q).hom X =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index W.unop (Q ⋙ F)) (multiequalizer (Cover.index W.unop (P ⋙ F)))
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
          (_ :
            ∀ (i : (Cover.index W.unop (Q ⋙ F)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.fst (Cover.index W.unop (Q ⋙ F)) i =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.snd (Cover.index W.unop (Q ⋙ F)) i)) ≫
      colimit.ι (diagram J (Q ⋙ F) X.unop) W
[PROOFSTEP]
simp only [colimit.ι_desc]
[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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ F.map
        (NatTrans.app ((Cocones.precompose (diagramNatTrans J η X.unop)).obj (colimit.cocone (diagram J Q X.unop))).ι
          W) ≫
      NatTrans.app (plusCompIso J F Q).hom X =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index W.unop (Q ⋙ F)) (multiequalizer (Cover.index W.unop (P ⋙ F)))
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
          (_ :
            ∀ (i : (Cover.index W.unop (Q ⋙ F)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.fst (Cover.index W.unop (Q ⋙ F)) i =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.snd (Cover.index W.unop (Q ⋙ F)) i)) ≫
      colimit.ι (diagram J (Q ⋙ F) X.unop) W
[PROOFSTEP]
dsimp [Cocones.precompose]
[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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ F.map
        (Multiequalizer.lift (Cover.index W.unop Q) (multiequalizer (Cover.index W.unop P))
            (fun i => Multiequalizer.ι (Cover.index W.unop P) i ≫ NatTrans.app η (op i.Y))
            (_ :
              ∀ (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) ≫
          colimit.ι (diagram J Q X.unop) W) ≫
      NatTrans.app (plusCompIso J F Q).hom X =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index W.unop (Q ⋙ F)) (multiequalizer (Cover.index W.unop (P ⋙ F)))
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
          (_ :
            ∀ (i : (Cover.index W.unop (Q ⋙ F)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.fst (Cover.index W.unop (Q ⋙ F)) i =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.snd (Cover.index W.unop (Q ⋙ F)) i)) ≫
      colimit.ι (diagram J (Q ⋙ F) X.unop) W
[PROOFSTEP]
simp only [Functor.map_comp, Category.assoc, ι_plusCompIso_hom]
[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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ F.map
        (Multiequalizer.lift (Cover.index W.unop Q) (multiequalizer (Cover.index W.unop P))
          (fun i => Multiequalizer.ι (Cover.index W.unop P) i ≫ NatTrans.app η (op i.Y))
          (_ :
            ∀ (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)) ≫
      NatTrans.app (diagramCompIso J F Q X.unop).hom W ≫ colimit.ι (diagram J (Q ⋙ F) X.unop) W =
    NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
      Multiequalizer.lift (Cover.index W.unop (Q ⋙ F)) (multiequalizer (Cover.index W.unop (P ⋙ F)))
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
          (_ :
            ∀ (i : (Cover.index W.unop (Q ⋙ F)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.fst (Cover.index W.unop (Q ⋙ F)) i =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.snd (Cover.index W.unop (Q ⋙ F)) i) ≫
        colimit.ι (diagram J (Q ⋙ F) X.unop) W
[PROOFSTEP]
simp only [← 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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ (F.map
          (Multiequalizer.lift (Cover.index W.unop Q) (multiequalizer (Cover.index W.unop P))
            (fun i => Multiequalizer.ι (Cover.index W.unop P) i ≫ NatTrans.app η (op i.Y))
            (_ :
              ∀ (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)) ≫
        NatTrans.app (diagramCompIso J F Q X.unop).hom W) ≫
      colimit.ι (diagram J (Q ⋙ F) X.unop) W =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index W.unop (Q ⋙ F)) (multiequalizer (Cover.index W.unop (P ⋙ F)))
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
          (_ :
            ∀ (i : (Cover.index W.unop (Q ⋙ F)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.fst (Cover.index W.unop (Q ⋙ F)) i =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.snd (Cover.index W.unop (Q ⋙ F)) i)) ≫
      colimit.ι (diagram J (Q ⋙ F) X.unop) W
[PROOFSTEP]
congr 1
  -- porting note: this used to work with `ext`
    -- See https://github.com/leanprover-community/mathlib4/issues/5229
[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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ F.map
        (Multiequalizer.lift (Cover.index W.unop Q) (multiequalizer (Cover.index W.unop P))
          (fun i => Multiequalizer.ι (Cover.index W.unop P) i ≫ NatTrans.app η (op i.Y))
          (_ :
            ∀ (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)) ≫
      NatTrans.app (diagramCompIso J F Q X.unop).hom W =
    NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
      Multiequalizer.lift (Cover.index W.unop (Q ⋙ F)) (multiequalizer (Cover.index W.unop (P ⋙ F)))
        (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
        (_ :
          ∀ (i : (Cover.index W.unop (Q ⋙ F)).R),
            (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                  (MulticospanIndex.fstTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                MulticospanIndex.fst (Cover.index W.unop (Q ⋙ F)) i =
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                  (MulticospanIndex.sndTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                MulticospanIndex.snd (Cover.index W.unop (Q ⋙ F)) i)
[PROOFSTEP]
apply Multiequalizer.hom_ext
[GOAL]
case w.h.e_a.h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
⊢ ∀ (a : (Cover.index W.unop (Q ⋙ F)).L),
    (F.map
            (Multiequalizer.lift (Cover.index W.unop Q) (multiequalizer (Cover.index W.unop P))
              (fun i => Multiequalizer.ι (Cover.index W.unop P) i ≫ NatTrans.app η (op i.Y))
              (_ :
                ∀ (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)) ≫
          NatTrans.app (diagramCompIso J F Q X.unop).hom W) ≫
        Multiequalizer.ι (Cover.index W.unop (Q ⋙ F)) a =
      (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
          Multiequalizer.lift (Cover.index W.unop (Q ⋙ F)) (multiequalizer (Cover.index W.unop (P ⋙ F)))
            (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
            (_ :
              ∀ (i : (Cover.index W.unop (Q ⋙ F)).R),
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                      (MulticospanIndex.fstTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                    MulticospanIndex.fst (Cover.index W.unop (Q ⋙ F)) i =
                  (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                      (MulticospanIndex.sndTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                    MulticospanIndex.snd (Cover.index W.unop (Q ⋙ F)) i)) ≫
        Multiequalizer.ι (Cover.index W.unop (Q ⋙ F)) a
[PROOFSTEP]
intro a
[GOAL]
case w.h.e_a.h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
a : (Cover.index W.unop (Q ⋙ F)).L
⊢ (F.map
          (Multiequalizer.lift (Cover.index W.unop Q) (multiequalizer (Cover.index W.unop P))
            (fun i => Multiequalizer.ι (Cover.index W.unop P) i ≫ NatTrans.app η (op i.Y))
            (_ :
              ∀ (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)) ≫
        NatTrans.app (diagramCompIso J F Q X.unop).hom W) ≫
      Multiequalizer.ι (Cover.index W.unop (Q ⋙ F)) a =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index W.unop (Q ⋙ F)) (multiequalizer (Cover.index W.unop (P ⋙ F)))
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
          (_ :
            ∀ (i : (Cover.index W.unop (Q ⋙ F)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.fst (Cover.index W.unop (Q ⋙ F)) i =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.snd (Cover.index W.unop (Q ⋙ F)) i)) ≫
      Multiequalizer.ι (Cover.index W.unop (Q ⋙ F)) a
[PROOFSTEP]
dsimp
[GOAL]
case w.h.e_a.h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
a : (Cover.index W.unop (Q ⋙ F)).L
⊢ (F.map
          (Multiequalizer.lift (Cover.index W.unop Q) (multiequalizer (Cover.index W.unop P))
            (fun i => Multiequalizer.ι (Cover.index W.unop P) i ≫ NatTrans.app η (op i.Y))
            (_ :
              ∀ (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)) ≫
        NatTrans.app (diagramCompIso J F Q X.unop).hom W) ≫
      Multiequalizer.ι (Cover.index W.unop (Q ⋙ F)) a =
    (NatTrans.app (diagramCompIso J F P X.unop).hom W ≫
        Multiequalizer.lift (Cover.index W.unop (Q ⋙ F)) (multiequalizer (Cover.index W.unop (P ⋙ F)))
          (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ F.map (NatTrans.app η (op i.Y)))
          (_ :
            ∀ (i : (Cover.index W.unop (Q ⋙ F)).R),
              (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.fstTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.fst (Cover.index W.unop (Q ⋙ F)) i =
                (fun i => Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i ≫ NatTrans.app (whiskerRight η F) (op i.Y))
                    (MulticospanIndex.sndTo (Cover.index W.unop (Q ⋙ F)) i) ≫
                  MulticospanIndex.snd (Cover.index W.unop (Q ⋙ F)) i)) ≫
      Multiequalizer.ι (Cover.index W.unop (Q ⋙ F)) a
[PROOFSTEP]
simp only [diagramCompIso_hom_ι_assoc, Multiequalizer.lift_ι, diagramCompIso_hom_ι, Category.assoc]
[GOAL]
case w.h.e_a.h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P✝ : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (Cover J X.unop)ᵒᵖ
a : (Cover.index W.unop (Q ⋙ F)).L
⊢ F.map
        (Multiequalizer.lift (Cover.index W.unop Q) (multiequalizer (Cover.index W.unop P))
          (fun i => Multiequalizer.ι (Cover.index W.unop P) i ≫ NatTrans.app η (op i.Y))
          (_ :
            ∀ (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)) ≫
      F.map (Multiequalizer.ι (Cover.index W.unop Q) a) =
    F.map (Multiequalizer.ι (Cover.index W.unop P) a) ≫ F.map (NatTrans.app η (op a.Y))
[PROOFSTEP]
simp only [← F.map_comp, Multiequalizer.lift_ι]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
⊢ whiskerRight (toPlus J P) F ≫ (plusCompIso J F P).hom = toPlus J (P ⋙ F)
[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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
x✝ : Cᵒᵖ
⊢ NatTrans.app (whiskerRight (toPlus J P) F ≫ (plusCompIso J F P).hom) x✝ = NatTrans.app (toPlus J (P ⋙ F)) x✝
[PROOFSTEP]
dsimp [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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
x✝ : Cᵒᵖ
⊢ F.map (Cover.toMultiequalizer ⊤ P ≫ colimit.ι (diagram J P x✝.unop) (op ⊤)) ≫
      NatTrans.app (plusCompIso J F P).hom x✝ =
    Cover.toMultiequalizer ⊤ (P ⋙ F) ≫ colimit.ι (diagram J (P ⋙ F) x✝.unop) (op ⊤)
[PROOFSTEP]
simp only [ι_plusCompIso_hom, Functor.map_comp, 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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
x✝ : Cᵒᵖ
⊢ F.map (Cover.toMultiequalizer ⊤ P) ≫
      NatTrans.app (diagramCompIso J F P x✝.unop).hom (op ⊤) ≫ colimit.ι (diagram J (P ⋙ F) x✝.unop) (op ⊤) =
    Cover.toMultiequalizer ⊤ (P ⋙ F) ≫ colimit.ι (diagram J (P ⋙ F) x✝.unop) (op ⊤)
[PROOFSTEP]
simp only [← 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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
x✝ : Cᵒᵖ
⊢ (F.map (Cover.toMultiequalizer ⊤ P) ≫ NatTrans.app (diagramCompIso J F P x✝.unop).hom (op ⊤)) ≫
      colimit.ι (diagram J (P ⋙ F) x✝.unop) (op ⊤) =
    Cover.toMultiequalizer ⊤ (P ⋙ F) ≫ colimit.ι (diagram J (P ⋙ F) x✝.unop) (op ⊤)
[PROOFSTEP]
congr 1
  -- porting note: this used to work with `ext`
    -- See https://github.com/leanprover-community/mathlib4/issues/5229
[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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
x✝ : Cᵒᵖ
⊢ F.map (Cover.toMultiequalizer ⊤ P) ≫ NatTrans.app (diagramCompIso J F P x✝.unop).hom (op ⊤) =
    Cover.toMultiequalizer ⊤ (P ⋙ F)
[PROOFSTEP]
apply Multiequalizer.hom_ext
[GOAL]
case w.h.e_a.h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
x✝ : Cᵒᵖ
⊢ ∀ (a : (Cover.index (op ⊤).unop (P ⋙ F)).L),
    (F.map (Cover.toMultiequalizer ⊤ P) ≫ NatTrans.app (diagramCompIso J F P x✝.unop).hom (op ⊤)) ≫
        Multiequalizer.ι (Cover.index (op ⊤).unop (P ⋙ F)) a =
      Cover.toMultiequalizer ⊤ (P ⋙ F) ≫ Multiequalizer.ι (Cover.index (op ⊤).unop (P ⋙ F)) a
[PROOFSTEP]
delta Cover.toMultiequalizer
[GOAL]
case w.h.e_a.h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
x✝ : Cᵒᵖ
⊢ ∀ (a : (Cover.index (op ⊤).unop (P ⋙ F)).L),
    (F.map
            (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 (diagramCompIso J F P x✝.unop).hom (op ⊤)) ≫
        Multiequalizer.ι (Cover.index (op ⊤).unop (P ⋙ F)) a =
      Multiequalizer.lift (Cover.index ⊤ (P ⋙ F)) ((P ⋙ F).obj (op x✝.unop)) (fun I => (P ⋙ F).map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ (P ⋙ F)).R),
              (fun I => (P ⋙ F).map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ (P ⋙ F)) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ (P ⋙ F)) I =
                (fun I => (P ⋙ F).map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ (P ⋙ F)) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ (P ⋙ F)) I) ≫
        Multiequalizer.ι (Cover.index (op ⊤).unop (P ⋙ F)) a
[PROOFSTEP]
simp only [diagramCompIso_hom_ι, Category.assoc, ← F.map_comp]
[GOAL]
case w.h.e_a.h
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
x✝ : Cᵒᵖ
⊢ ∀ (a : (Cover.index (op ⊤).unop (P ⋙ F)).L),
    F.map
        (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.ι (Cover.index (op ⊤).unop P) a) =
      Multiequalizer.lift (Cover.index ⊤ (P ⋙ F)) ((P ⋙ F).obj (op x✝.unop)) (fun I => (P ⋙ F).map I.f.op)
          (_ :
            ∀ (I : (Cover.index ⊤ (P ⋙ F)).R),
              (fun I => (P ⋙ F).map I.f.op) (MulticospanIndex.fstTo (Cover.index ⊤ (P ⋙ F)) I) ≫
                  MulticospanIndex.fst (Cover.index ⊤ (P ⋙ F)) I =
                (fun I => (P ⋙ F).map I.f.op) (MulticospanIndex.sndTo (Cover.index ⊤ (P ⋙ F)) I) ≫
                  MulticospanIndex.snd (Cover.index ⊤ (P ⋙ F)) I) ≫
        Multiequalizer.ι (Cover.index (op ⊤).unop (P ⋙ F)) a
[PROOFSTEP]
simp only [unop_op, limit.lift_π, Multifork.ofι_π_app, Functor.comp_obj, Functor.comp_map, implies_true]
[GOAL]
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
⊢ toPlus J (P ⋙ F) ≫ (plusCompIso J F P).inv = whiskerRight (toPlus J P) F
[PROOFSTEP]
simp [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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
hP : Presheaf.IsSheaf J (plusObj J P ⋙ F)
⊢ (plusCompIso J F P).inv = plusLift J (whiskerRight (toPlus J P) F) 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
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
hP : Presheaf.IsSheaf J (plusObj J P ⋙ F)
⊢ toPlus J (P ⋙ F) ≫ (plusCompIso J F P).inv = whiskerRight (toPlus J P) F
[PROOFSTEP]
simp [Iso.comp_inv_eq]
