case mk
C : Type u₁
inst✝² : Category C
A✝ : Type u₂
inst✝¹ : Category A✝
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category A
E : A
X : C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
S : GrothendieckTopology.Cover J X
x : (I : GrothendieckTopology.Cover.Arrow S) → E ⟶ P.obj I.Y.op
hx :
  ∀ (I : GrothendieckTopology.Cover.Relation S),
    x (GrothendieckTopology.Cover.Relation.fst I) ≫ P.map I.g₁.op =
      x (GrothendieckTopology.Cover.Relation.snd I) ≫ P.map I.g₂.op
Y : C
f : Y ⟶ X
hf : (GrothendieckTopology.Cover.sieve S).arrows f
⊢ amalgamate hP S x hx ≫ P.map { Y := Y, f := f, hf := hf }.f.op = x { Y := Y, f := f, hf := hf }
C : Type u₁
inst✝² : Category C
A✝ : Type u₂
inst✝¹ : Category A✝
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category A
E : A
X : C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
S : GrothendieckTopology.Cover J X
x : (I : GrothendieckTopology.Cover.Arrow S) → E ⟶ P.obj I.Y.op
hx :
  ∀ (I : GrothendieckTopology.Cover.Relation S),
    x (GrothendieckTopology.Cover.Relation.fst I) ≫ P.map I.g₁.op =
      x (GrothendieckTopology.Cover.Relation.snd I) ≫ P.map I.g₂.op
I : GrothendieckTopology.Cover.Arrow S
⊢ amalgamate hP S x hx ≫ P.map I.f.op = x I
rcases I with ⟨Y, f, hf⟩
no goals
case mk
C : Type u₁
inst✝² : Category C
A✝ : Type u₂
inst✝¹ : Category A✝
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category A
E : A
X : C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
S : GrothendieckTopology.Cover J X
x : (I : GrothendieckTopology.Cover.Arrow S) → E ⟶ P.obj I.Y.op
hx :
  ∀ (I : GrothendieckTopology.Cover.Relation S),
    x (GrothendieckTopology.Cover.Relation.fst I) ≫ P.map I.g₁.op =
      x (GrothendieckTopology.Cover.Relation.snd I) ≫ P.map I.g₂.op
Y : C
f : Y ⟶ X
hf : (GrothendieckTopology.Cover.sieve S).arrows f
⊢ amalgamate hP S x hx ≫ P.map { Y := Y, f := f, hf := hf }.f.op = x { Y := Y, f := f, hf := hf }
apply
  @Presieve.IsSheafFor.valid_glue _ _ _ _ _ _ (hP _ _ S.condition) (fun Y f hf => x ⟨Y, f, hf⟩)
    (fun Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ w => hx ⟨Y₁, Y₂, Z, g₁, g₂, f₁, f₂, h₁, h₂, w⟩) f hf