C : Type u
inst✝⁵ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category D
E : Type w₂
inst✝³ : Category 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
⊢ (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.app
        W ≫
      Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i =
    F.map (Multiequalizer.ι (Cover.index W.unop P) i)
C : Type u
inst✝⁵ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category D
E : Type w₂
inst✝³ : Category 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
⊢ (diagramCompIso J F P X).hom.app W ≫ Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i =
    F.map (Multiequalizer.ι (Cover.index W.unop P) i)
delta diagramCompIso
C : Type u
inst✝⁵ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category D
E : Type w₂
inst✝³ : Category 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)
C : Type u
inst✝⁵ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category D
E : Type w₂
inst✝³ : Category 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
⊢ (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.app
        W ≫
      Multiequalizer.ι (Cover.index W.unop (P ⋙ F)) i =
    F.map (Multiequalizer.ι (Cover.index W.unop P) i)
dsimp
no goals
C : Type u
inst✝⁵ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁴ : Category D
E : Type w₂
inst✝³ : Category 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)
simp