-- Mathlib/CategoryTheory/Sites/Coverage.lean
theorem isSheaf_coverage (K : Coverage C) (P : Cᵒᵖ ⥤ Type*) :
    Presieve.IsSheaf (toGrothendieck _ K) P ↔
    (∀ {X : C} (R : Presieve X), R ∈ K X → Presieve.IsSheafFor P R)

Proof state:
case mpr.transitive.refine_2.intro
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : K.Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C},
    ∀ R ∈ K.covering X, IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), (y g).IsAmalgamation (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : q.Compatible
t : P.obj (Opposite.op Y)
ht : q.IsAmalgamation t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ y (gg ≫ g) ggg ?mpr.transitive.refine_2.intro.h = P.map (ggg ≫ gg).op (x g hg)

case mpr.transitive.refine_2.intro.h
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : K.Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C},
    ∀ R ∈ K.covering X, IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), (y g).IsAmalgamation (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : q.Compatible
t : P.obj (Opposite.op Y)
ht : q.IsAmalgamation t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ (Sieve.pullback (𝟙 ZZ) (Sieve.pullback ((gg ≫ g) ≫ f) S)).arrows ggg

Tactic:
on_goal 2 => simpa using hggg

Result:
case mpr.transitive.refine_2.intro
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : K.Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C},
    ∀ R ∈ K.covering X, IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), (y g).IsAmalgamation (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : q.Compatible
t : P.obj (Opposite.op Y)
ht : q.IsAmalgamation t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ y (gg ≫ g) ggg ⋯ = P.map (ggg ≫ gg).op (x g hg)

Proof state:
case mpr.of
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.covering X
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows

Tactic:
obtain ⟨T, hT1, hT2⟩ := K.pullback f S hS

Result:
case mpr.of.intro.intro
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.covering X
Y : C
f : Y ⟶ X
T : Presieve Y
hT1 : T ∈ K.covering Y
hT2 : T.FactorsThruAlong S f
⊢ IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows