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), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁴ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
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✝
P✝ P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : (F : D ⥤ E) → (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝ :
  (F : D ⥤ E) →
    (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
⊢ (plusCompIso J F (plusObj J P)).hom ≫ plusMap J (plusCompIso J F P).hom ≫ 𝟙 (plusObj J (plusObj J (P ⋙ F))) =
    (plusCompIso J F (plusObj J P)).hom ≫ plusMap J (plusCompIso J F P).hom
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), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁴ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
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✝
P✝ P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : (F : D ⥤ E) → (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝ :
  (F : D ⥤ E) →
    (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
⊢ (sheafificationWhiskerLeftIso J P).hom.app F = (sheafifyCompIso J F P).hom
dsimp [sheafificationWhiskerLeftIso, sheafifyCompIso]
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), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁴ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
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✝
P✝ P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : (F : D ⥤ E) → (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝ :
  (F : D ⥤ E) →
    (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
⊢ (plusCompIso J F (plusObj J P)).hom ≫ plusMap J (plusCompIso J F P).hom ≫ 𝟙 (plusObj J (plusObj J (P ⋙ F))) =
    (plusCompIso J F (plusObj J P)).hom ≫ plusMap J (plusCompIso J F P).hom
rw [Category.comp_id]