Theorem: ExtrDisc.final (ExtrDisc/ExplicitSheaves.lean)

State before:
A : Type (u + 2)
inst✝ : Category A
F : ExtrDiscᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) F
Tactic:
rw [← extensiveRegular_generates_coherent]
State after:
A : Type (u + 2)
inst✝ : Category A
F : ExtrDiscᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
⊢ Presheaf.IsSheaf
    (Coverage.toGrothendieck ExtrDisc
      (ExtensiveRegularCoverage ExtrDisc everything_proj
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
    F

State before:
A : Type (u + 2)
inst✝ : Category A
F : ExtrDiscᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
⊢ Presheaf.IsSheaf
    (Coverage.toGrothendieck ExtrDisc
      (ExtensiveRegularCoverage ExtrDisc everything_proj
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
    F
Tactic:
exact fun E => (Presieve.isSheaf_coverage _ _).2 <| fun S hS => isSheafFor_of_extensiveRegular hS
  ⟨fun J inst => have := hF.1; compPreservesLimitsOfShape _ _⟩
State after:
no goals