C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
⊢ Presieve.IsSheaf J (toPresheaf (sheafify J G))
intro U S hS x hx
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
let S' := Sieve.bind S fun Y f hf => G.sieveOfSection (x f hf).1
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
this : ∀ (V : C) (i : V ⟶ U), S'.arrows i → S'.arrows i
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
have := fun (V) (i : V ⟶ U) (hi : S' i) => hi
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (fun Y f h => ((fun Y f hf => sieveOfSection G ↑(x f hf)) Y f h).arrows) (W V i hi) (i₂ V i hi)
      (_ : S.arrows (i₂ V i hi)) (i₁ V i hi)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
this : ∀ (V : C) (i : V ⟶ U), S'.arrows i → S'.arrows i
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
choose W i₁ i₂ hi₂ h₁ h₂ using this
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (fun Y f h => ((fun Y f hf => sieveOfSection G ↑(x f hf)) Y f h).arrows) (W V i hi) (i₂ V i hi)
      (_ : S.arrows (i₂ V i hi)) (i₁ V i hi)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
dsimp [-Sieve.bind_apply] at *
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
let x'' : Presieve.FamilyOfElements F S' := fun V i hi => F.map (i₁ V i hi).op (x _ (hi₂ V i hi))
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
have : x''.Compatible := by
  intro V₁ V₂ V₃ g₁ g₂ g₃ g₄ S₁ S₂ e
  rw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply]
  exact
    congr_arg Subtype.val
      (hx (g₁ ≫ i₁ _ _ S₁) (g₂ ≫ i₁ _ _ S₂) (hi₂ _ _ S₁) (hi₂ _ _ S₂)
      (by simp only [Category.assoc, h₂, e]))
case intro.intro
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj U.op
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj U.op), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
obtain ⟨t, ht, ht'⟩ := hF _ (J.bind_covering hS fun V i hi => (x i hi).2) _ this
case intro.intro
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj U.op
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj U.op), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
⊢ t ∈ obj (sheafify J G) U.op
case intro.intro
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj U.op
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj U.op), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
refine' ⟨⟨t, _⟩, (H ⟨t, _⟩).mpr ht, fun y hy => Subtype.ext (ht' _ ((H _).mp hy))⟩
case intro.intro
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj U.op
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj U.op), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
⊢ (Sieve.bind S.arrows fun V i hi => sieveOfSection G ↑(x i hi)) ≤ sieveOfSection G t
case intro.intro
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj U.op
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj U.op), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
⊢ t ∈ obj (sheafify J G) U.op
refine' J.superset_covering _ (J.bind_covering hS fun V i hi => (x i hi).2)
case intro.intro
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj U.op
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj U.op), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
V : C
i : V ⟶ U.op.unop
hi : (Sieve.bind S.arrows fun V i hi => sieveOfSection G ↑(x i hi)).arrows i
⊢ (sieveOfSection G t).arrows i
case intro.intro
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj U.op
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj U.op), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
⊢ (Sieve.bind S.arrows fun V i hi => sieveOfSection G ↑(x i hi)) ≤ sieveOfSection G t
intro V i hi
case intro.intro
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj U.op
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj U.op), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
V : C
i : V ⟶ U.op.unop
hi : (Sieve.bind S.arrows fun V i hi => sieveOfSection G ↑(x i hi)).arrows i
⊢ F.map i.op t ∈ obj G V.op
case intro.intro
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj U.op
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj U.op), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
V : C
i : V ⟶ U.op.unop
hi : (Sieve.bind S.arrows fun V i hi => sieveOfSection G ↑(x i hi)).arrows i
⊢ (sieveOfSection G t).arrows i
dsimp
case intro.intro
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj U.op
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj U.op), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
V : C
i : V ⟶ U.op.unop
hi : (Sieve.bind S.arrows fun V i hi => sieveOfSection G ↑(x i hi)).arrows i
⊢ x'' i hi ∈ obj G V.op
case intro.intro
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj U.op
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj U.op), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
V : C
i : V ⟶ U.op.unop
hi : (Sieve.bind S.arrows fun V i hi => sieveOfSection G ↑(x i hi)).arrows i
⊢ F.map i.op t ∈ obj G V.op
rw [ht _ hi]
no goals
case intro.intro
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj U.op
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj U.op), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
V : C
i : V ⟶ U.op.unop
hi : (Sieve.bind S.arrows fun V i hi => sieveOfSection G ↑(x i hi)).arrows i
⊢ x'' i hi ∈ obj G V.op
exact h₁ _ _ hi
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
⊢ ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
intro s
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x s → Presieve.FamilyOfElements.IsAmalgamation x'' ↑s

case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s → Presieve.FamilyOfElements.IsAmalgamation x s
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
constructor
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map i.op ↑s = x'' i hi
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x s → Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
intro H V i hi
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map i.op ↑s = F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map i.op ↑s = x'' i hi
dsimp only [show x'' = fun V i hi => F.map (i₁ V i hi).op (x _ (hi₂ V i hi)) from rfl]
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map (i₁ V i hi ≫ i₂ V i hi).op ↑s = F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map i.op ↑s = F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
conv_lhs => rw [← h₂ _ _ hi]
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map (i₁ V i hi ≫ i₂ V i hi).op ↑s = F.map (i₁ V i hi).op ↑((toPresheaf (sheafify J G)).map (i₂ V i hi).op s)
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map (i₁ V i hi ≫ i₂ V i hi).op ↑s = F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
rw [← H _ (hi₂ _ _ hi)]
no goals
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map (i₁ V i hi ≫ i₂ V i hi).op ↑s = F.map (i₁ V i hi).op ↑((toPresheaf (sheafify J G)).map (i₂ V i hi).op s)
exact FunctorToTypes.map_comp_apply F (i₂ _ _ hi).op (i₁ _ _ hi).op _
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
⊢ (toPresheaf (sheafify J G)).map i.op s = x i hi
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s → Presieve.FamilyOfElements.IsAmalgamation x s
intro H V i hi
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
⊢ ↑((toPresheaf (sheafify J G)).map i.op s) = ↑(x i hi)
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
⊢ (toPresheaf (sheafify J G)).map i.op s = x i hi
refine Subtype.ext ?_
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ V.op.unop⦄,
    (sieveOfSection G ↑(x i hi)).arrows f → F.map f.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map f.op ↑(x i hi)
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
⊢ ↑((toPresheaf (sheafify J G)).map i.op s) = ↑(x i hi)
apply (hF _ (x i hi).2).isSeparatedFor.ext
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ V.op.unop
hi' : (sieveOfSection G ↑(x i hi)).arrows i'
⊢ F.map i'.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map i'.op ↑(x i hi)
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ V.op.unop⦄,
    (sieveOfSection G ↑(x i hi)).arrows f → F.map f.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map f.op ↑(x i hi)
intro V' i' hi'
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ V.op.unop
hi' : (sieveOfSection G ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
⊢ F.map i'.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map i'.op ↑(x i hi)
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ V.op.unop
hi' : (sieveOfSection G ↑(x i hi)).arrows i'
⊢ F.map i'.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map i'.op ↑(x i hi)
have hi'' : S' (i' ≫ i) := ⟨_, _, _, hi, hi', rfl⟩
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ V.op.unop
hi' : (sieveOfSection G ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : F.map (i' ≫ i).op ↑s = x'' (i' ≫ i) hi''
⊢ F.map i'.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map i'.op ↑(x i hi)
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ V.op.unop
hi' : (sieveOfSection G ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
⊢ F.map i'.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map i'.op ↑(x i hi)
have := H _ hi''
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ V.op.unop
hi' : (sieveOfSection G ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : (F.map i.op ≫ F.map i'.op) ↑s = x'' (i' ≫ i) hi''
⊢ F.map i'.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map i'.op ↑(x i hi)
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ V.op.unop
hi' : (sieveOfSection G ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : F.map (i' ≫ i).op ↑s = x'' (i' ≫ i) hi''
⊢ F.map i'.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map i'.op ↑(x i hi)
rw [op_comp, F.map_comp] at this
no goals
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj U.op
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ V.op.unop
hi' : (sieveOfSection G ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : (F.map i.op ≫ F.map i'.op) ↑s = x'' (i' ≫ i) hi''
⊢ F.map i'.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map i'.op ↑(x i hi)
refine' this.trans (congr_arg Subtype.val (hx _ _ (hi₂ _ _ hi'') hi (h₂ _ _ hi'')))
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ F.map g₁.op (x'' g₃ S₁) = F.map g₂.op (x'' g₄ S₂)
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
⊢ Presieve.FamilyOfElements.Compatible x''
intro V₁ V₂ V₃ g₁ g₂ g₃ g₄ S₁ S₂ e
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ F.map ((i₁ V₁ g₃ S₁).op ≫ g₁.op) ↑(x (i₂ V₁ g₃ S₁) (_ : S.arrows (i₂ V₁ g₃ S₁))) =
    F.map ((i₁ V₂ g₄ S₂).op ≫ g₂.op) ↑(x (i₂ V₂ g₄ S₂) (_ : S.arrows (i₂ V₂ g₄ S₂)))
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ F.map g₁.op (x'' g₃ S₁) = F.map g₂.op (x'' g₄ S₂)
rw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply]
no goals
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ F.map ((i₁ V₁ g₃ S₁).op ≫ g₁.op) ↑(x (i₂ V₁ g₃ S₁) (_ : S.arrows (i₂ V₁ g₃ S₁))) =
    F.map ((i₁ V₂ g₄ S₂).op ≫ g₂.op) ↑(x (i₂ V₂ g₄ S₂) (_ : S.arrows (i₂ V₂ g₄ S₂)))
exact
  congr_arg Subtype.val
    (hx (g₁ ≫ i₁ _ _ S₁) (g₂ ≫ i₁ _ _ S₂) (hi₂ _ _ S₁) (hi₂ _ _ S₂)
    (by simp only [Category.assoc, h₂, e]))
no goals
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G V.op
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj U.op),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ (g₁ ≫ i₁ V₁ g₃ S₁) ≫ i₂ V₁ g₃ S₁ = (g₂ ≫ i₁ V₂ g₄ S₂) ≫ i₂ V₂ g₄ S₂
simp only [Category.assoc, h₂, e]