-- Mathlib/CategoryTheory/Sites/Canonical.lean
theorem isSheafFor_bind (P : Cᵒᵖ ⥤ Type v) (U : Sieve X) (B : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, U f → Sieve Y)
    (hU : Presieve.IsSheafFor P (U : Presieve X))
    (hB : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), Presieve.IsSheafFor P (B hf : Presieve Y))
    (hB' : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (h : U f) ⦃Z⦄ (g : Z ⟶ Y),
      Presieve.IsSeparatedFor P (((B h).pullback g) : Presieve Z)) :
    Presieve.IsSheafFor P (Sieve.bind (U : Presieve X) B : Presieve X)

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : Presieve.IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), Presieve.IsSheafFor P (B hf).arrows
hB' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : Presieve.FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → Presieve.FamilyOfElements P (B hf).arrows :=
  fun Y f hf Z g hg => s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : Presieve.FamilyOfElements P U.arrows := fun Y f hf => ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
hT : t.Compatible
⊢ ∀ (y : P.obj (Opposite.op X)), (fun t => s.IsAmalgamation t) y → y = hU.amalgamate t hT

Tactic:
intro y hy

Result:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : Presieve.IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), Presieve.IsSheafFor P (B hf).arrows
hB' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : Presieve.FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y✝ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → Presieve.FamilyOfElements P (B hf).arrows :=
  fun Y f hf Z g hg => s (g ≫ f) ⋯
hy✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y✝ hf).Compatible
t : Presieve.FamilyOfElements P U.arrows := fun Y f hf => ⋯.amalgamate (y✝ hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y✝ hf).IsAmalgamation (t f hf)
hT : t.Compatible
y : P.obj (Opposite.op X)
hy : s.IsAmalgamation y
⊢ y = hU.amalgamate t hT

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : Presieve.IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), Presieve.IsSheafFor P (B hf).arrows
hB' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : Presieve.FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → Presieve.FamilyOfElements P (B hf).arrows :=
  fun Y f hf Z g hg => s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : Presieve.FamilyOfElements P U.arrows := fun Y f hf => ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
Y : C
l : Y ⟶ W
hl : (B ⋯).arrows l
⊢ P.map l.op (t (h ≫ f) ⋯) = P.map l.op (P.map h.op (t f hf))

Tactic:
apply (hB' hf (l ≫ h)).ext

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : Presieve.IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), Presieve.IsSheafFor P (B hf).arrows
hB' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : Presieve.FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → Presieve.FamilyOfElements P (B hf).arrows :=
  fun Y f hf Z g hg => s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : Presieve.FamilyOfElements P U.arrows := fun Y f hf => ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
Y : C
l : Y ⟶ W
hl : (B ⋯).arrows l
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (Sieve.pullback (l ≫ h) (B hf)).arrows f_1 →
      P.map f_1.op (P.map l.op (t (h ≫ f) ⋯)) = P.map f_1.op (P.map l.op (P.map h.op (t f hf)))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : Presieve.IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), Presieve.IsSheafFor P (B hf).arrows
hB' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : Presieve.FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → Presieve.FamilyOfElements P (B hf).arrows :=
  fun Y f hf Z g hg => s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : Presieve.FamilyOfElements P U.arrows := fun Y f hf => ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
⊢ t.Compatible

Tactic:
rw [Presieve.compatible_iff_sieveCompatible]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : Presieve.IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), Presieve.IsSheafFor P (B hf).arrows
hB' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : Presieve.FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → Presieve.FamilyOfElements P (B hf).arrows :=
  fun Y f hf Z g hg => s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : Presieve.FamilyOfElements P U.arrows := fun Y f hf => ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
⊢ t.SieveCompatible

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : Presieve.IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), Presieve.IsSheafFor P (B hf).arrows
hB' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : Presieve.FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → Presieve.FamilyOfElements P (B hf).arrows :=
  fun Y f hf Z g hg => s (g ≫ f) ⋯
Y : C
f : Y ⟶ X
H : U.arrows f
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
hf₁ : (B H).arrows f₁
hf₂ : (B H).arrows f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ g₁ ≫ f₁ ≫ f = g₂ ≫ f₂ ≫ f

Tactic:
apply reassoc_of% comm

Result:
no goals