-- Mathlib/CategoryTheory/Sites/Coherent/CoherentSheaves.lean
lemma isSheaf_coherent (P : Cᵒᵖ ⥤ Type w) :
    Presieve.IsSheaf (coherentTopology C) P ↔
    (∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → (X a ⟶ B)),
      EffectiveEpiFamily X π → (Presieve.ofArrows X π).IsSheafFor P)

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ (∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)) →
    Presieve.IsSheaf (coherentTopology C) P

Tactic:
intro h

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
⊢ Presieve.IsSheaf (coherentTopology C) P

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
⊢ ∀ {X : C}, ∀ R ∈ (coherentCoverage C).covering X, Presieve.IsSheafFor P R

Tactic:
rintro B S ⟨α, _, X, π, rfl, hS⟩

Result:
case mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
B : C
α : Type
w✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
hS : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
α : Type
inst✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
simp only [coherentTopology, Presieve.isSheaf_coverage] at hP

Result:
case mp
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
B : C
α : Type
inst✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP : ∀ {X : C}, ∀ R ∈ (coherentCoverage C).covering X, Presieve.IsSheafFor P R
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)

Proof state:
case mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
B : C
α : Type
w✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
hS : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
exact h _ _ _ _ hS

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ Presieve.IsSheaf (coherentTopology C) P ↔
    ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ Presieve.IsSheaf (coherentTopology C) P →
    ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ (∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)) →
    Presieve.IsSheaf (coherentTopology C) P

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ Presieve.IsSheaf (coherentTopology C) P →
    ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
intro hP B α _ X π h

Result:
case mp
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
α : Type
inst✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
B : C
α : Type
inst✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP : ∀ {X : C}, ∀ R ∈ (coherentCoverage C).covering X, Presieve.IsSheafFor P R
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
apply hP

Result:
case mp.a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
B : C
α : Type
inst✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP : ∀ {X : C}, ∀ R ∈ (coherentCoverage C).covering X, Presieve.IsSheafFor P R
⊢ Presieve.ofArrows X π ∈ (coherentCoverage C).covering B

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
⊢ Presieve.IsSheaf (coherentTopology C) P

Tactic:
simp only [coherentTopology, Presieve.isSheaf_coverage]

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
⊢ ∀ {X : C}, ∀ R ∈ (coherentCoverage C).covering X, Presieve.IsSheafFor P R

Proof state:
case mp.a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
B : C
α : Type
inst✝ : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP : ∀ {X : C}, ∀ R ∈ (coherentCoverage C).covering X, Presieve.IsSheafFor P R
⊢ Presieve.ofArrows X π ∈ (coherentCoverage C).covering B

Tactic:
exact ⟨α, inferInstance, X, π, rfl, h⟩

Result:
no goals