-- 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
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 ∧
      ∀ (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 ∧
          ∀ (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
            x.Compatible → ∃ t, x.IsAmalgamation t
⊢ IsSeparatedFor P (Sieve.pullback f S).arrows ∧
    ∀ (x : FamilyOfElements P (Sieve.pullback f S).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
choose H1 H1' using H1

Result:
case mpr.transitive
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
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 ∧
          ∀ (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
            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
⊢ IsSeparatedFor P (Sieve.pullback f S).arrows ∧
    ∀ (x : FamilyOfElements P (Sieve.pullback f S).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Proof state:
case mpr.transitive
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
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)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f R).arrows
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSheafFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f S).arrows

Tactic:
intro Y f

Result:
case mpr.transitive
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
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)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f R).arrows
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSheafFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (Sieve.pullback f S).arrows

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:
intro Y f

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

Proof state:
case mpr.of.intro.intro.H
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
⊢ T.FactorsThru (Sieve.pullback f (Sieve.generate S)).arrows

Tactic:
intro Z g hg

Result:
case mpr.of.intro.intro.H
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
Z : C
g : Z ⟶ Y
hg : T g
⊢ ∃ W i e, (Sieve.pullback f (Sieve.generate S)).arrows e ∧ i ≫ e = g