case hγ
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ toPlus J P ≫ plusMap J η ≫ plusLift J γ hR = η ≫ γ
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ plusMap J η ≫ plusLift J γ hR = plusLift J (η ≫ γ) hR
apply J.plusLift_unique
no goals
case hγ
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ toPlus J P ≫ plusMap J η ≫ plusLift J γ hR = η ≫ γ
rw [← Category.assoc, ← J.toPlus_naturality, Category.assoc, J.toPlus_plusLift]