-- 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_1
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
⊢ IsSeparatedFor P (Sieve.pullback f S).arrows

Tactic:
intro x t₁ t₂ h₁ h₂

Result:
case mpr.transitive.refine_1
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
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂

Proof state:
case mpr.top
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
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X✝), IsSheafFor P (Sieve.pullback f ⊤).arrows

Tactic:
intros

Result:
case mpr.top
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✝ Y✝ : C
f✝ : Y✝ ⟶ X✝
⊢ IsSheafFor P (Sieve.pullback f✝ ⊤).arrows

Proof state:
case a
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) ⋯
Z : C
g : Z ⟶ Y
Y₁ Y₂ ZZ : C
g₁ : ZZ ⟶ Y₁
g₂ : ZZ ⟶ Y₂
f₁ : Y₁ ⟶ Z
f₂ : Y₂ ⟶ Z
h₁ : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows f₁
h₂ : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ g₁ ≫ f₁ ≫ g = g₂ ≫ f₂ ≫ g

Tactic:
rw [reassoc_of% h]

Result:
no goals

Proof state:
case mpr.transitive.refine_2
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, x.IsAmalgamation t

Tactic:
obtain ⟨t, ht⟩ := H1' f q hq

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