-- 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:
case intro.intro.intro.intro.intro
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
Z W : C
f : Z ⟶ W
g : W ⟶ X
hg : R.arrows g
hf : S.arrows (f ≫ g)
⊢ f ≫ g ∈ S.arrows

Tactic:
apply hf

Result:
no goals

Proof state:
case h.mpr
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
a : (Sieve.pullback f R).arrows g
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S)).arrows g

Tactic:
refine ⟨Z, 𝟙 Z, _, a, ?_⟩

Result:
case h.mpr
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
a : (Sieve.pullback f R).arrows g
⊢ (fun x x_1 h => ((fun T k x => Sieve.pullback k S) x x_1 h).arrows) Z (g ≫ f) a (𝟙 Z) ∧ 𝟙 Z ≫ g ≫ f = g ≫ f

Proof state:
case h.mp.intro.intro.intro.intro.intro
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
W : C
k : Z ⟶ W
l : W ⟶ X
hl : R.arrows l
left✝ : ((fun T k x => Sieve.pullback k S) W l hl).arrows k
comm : k ≫ l = g ≫ f
⊢ (Sieve.pullback f R).arrows g

Tactic:
rw [pullback_apply, ← comm]

Result:
case h.mp.intro.intro.intro.intro.intro
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
W : C
k : Z ⟶ W
l : W ⟶ X
hl : R.arrows l
left✝ : ((fun T k x => Sieve.pullback k S) W l hl).arrows k
comm : k ≫ l = g ≫ f
⊢ R.arrows (k ≫ l)

Proof state:
case h.mp
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

Tactic:
rintro ⟨W, k, l, hl, _, comm⟩

Result:
case h.mp.intro.intro.intro.intro.intro
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
W : C
k : Z ⟶ W
l : W ⟶ X
hl : R.arrows l
left✝ : ((fun T k x => Sieve.pullback k S) W l hl).arrows k
comm : k ≫ l = g ≫ f
⊢ (Sieve.pullback f R).arrows g

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
⊢ (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows

Tactic:
rintro Z f ⟨W, f, g, hg, hf : S _, rfl⟩

Result:
case intro.intro.intro.intro.intro
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
Z W : C
f : Z ⟶ W
g : W ⟶ X
hg : R.arrows g
hf : S.arrows (f ≫ g)
⊢ f ≫ g ∈ S.arrows

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
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSeparatedFor P (Sieve.pullback (g ≫ f) S).arrows

Tactic:
apply (hS (R.downward_closed hf _)).isSeparatedFor

Result:
no goals

Proof state:
case h.mpr
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
a : (Sieve.pullback f R).arrows g
⊢ (fun x x_1 h => ((fun T k x => Sieve.pullback k S) x x_1 h).arrows) Z (g ≫ f) a (𝟙 Z) ∧ 𝟙 Z ≫ g ≫ f = g ≫ f

Tactic:
simp [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
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows

Tactic:
rw [← pullback_comp]

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 ≫ f) S).arrows