case hsep
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
⊢ ∀ (X : C) (S : Cover J X) (x y : (forget D).obj ((plusObj J P).obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map ((plusObj J P).map I.f.op) x = (forget D).map ((plusObj J P).map I.f.op) y) →
      x = y
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
⊢ Presheaf.IsSheaf J (plusObj J (plusObj J P))
apply isSheaf_of_sep
case hsep
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
X : C
S : Cover J X
x y : (forget D).obj ((plusObj J P).obj X.op)
⊢ (∀ (I : Cover.Arrow S), (forget D).map ((plusObj J P).map I.f.op) x = (forget D).map ((plusObj J P).map I.f.op) y) →
    x = y
case hsep
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
⊢ ∀ (X : C) (S : Cover J X) (x y : (forget D).obj ((plusObj J P).obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map ((plusObj J P).map I.f.op) x = (forget D).map ((plusObj J P).map I.f.op) y) →
      x = y
intro X S x y
no goals
case hsep
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
X : C
S : Cover J X
x y : (forget D).obj ((plusObj J P).obj X.op)
⊢ (∀ (I : Cover.Arrow S), (forget D).map ((plusObj J P).map I.f.op) x = (forget D).map ((plusObj J P).map I.f.op) y) →
    x = y
apply sep