-- 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:
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

Tactic:
intro Z W f h hf

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
⊢ t (h ≫ f) ⋯ = 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)
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)))

Tactic:
intro M m hm

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
M : C
m : M ⟶ Y
hm : (Sieve.pullback (l ≫ h) (B hf)).arrows m
⊢ P.map m.op (P.map l.op (t (h ≫ f) ⋯)) = P.map m.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
⊢ Presieve.IsSheafFor P (Sieve.bind U.arrows B).arrows

Tactic:
intro s hs

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
⊢ ∃! t, s.IsAmalgamation t

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, s.IsAmalgamation t

Tactic:
let t : Presieve.FamilyOfElements P (U : Presieve X) :=
  fun Y f hf => (hB hf).amalgamate (y hf) (hy hf)

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) ⋯
⊢ ∃! t, s.IsAmalgamation t