-- Mathlib/CategoryTheory/Sites/Canonical.lean
theorem isSheafFor_trans (P : Cᵒᵖ ⥤ Type v) (R S : Sieve X)
    (hR : Presieve.IsSheafFor P (R : Presieve X))
    (hR' : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (_ : S f), Presieve.IsSeparatedFor P (R.pullback f : Presieve Y))
    (hS : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (_ : R f), Presieve.IsSheafFor P (S.pullback f : Presieve Y)) :
    Presieve.IsSheafFor P (S : Presieve X)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S) = Sieve.pullback f R

Tactic:
ext Z g

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S)).arrows g ↔ (Sieve.pullback f R).arrows g

Proof state:
case trans
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this✝ : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
this : Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S) = Sieve.pullback f R
⊢ Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows

Tactic:
apply hR' hf

Result:
no goals

Proof state:
case hS
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows

Tactic:
intro Y f hf Z g

Result:
case hS
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
have : (bind R fun Y f _ => S.pullback f : Presieve X) ≤ S := by
  rintro Z f ⟨W, f, g, hg, hf : S _, rfl⟩
  apply hf

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
⊢ Presieve.IsSheafFor P S.arrows

Proof state:
case trans
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this✝ : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
this : Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S) = Sieve.pullback f R
⊢ Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S)).arrows

Tactic:
rw [this]

Result:
case trans
C : Type u
inst✝ : Category.{v, u} C
X : C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this✝ : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
this : Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S) = Sieve.pullback f R
⊢ Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows