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

State before:
EverythinProj_ExtrDisc : EverythingIsProjective ExtrDisc
X : ExtrDisc
S : Presieve X
hS :
  S ∈
    Coverage.covering
      (ExtensiveRegularCoverage ExtrDisc EverythinProj_ExtrDisc
        (_ :
          ∀ {α : 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)))
      X
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
hF : PreservesFiniteProducts F
⊢ IsSheafFor F S
Tactic:
cases' hS with hSIso hSSingle
State after:
case inl
EverythinProj_ExtrDisc : EverythingIsProjective ExtrDisc
X : ExtrDisc
S : Presieve X
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
hF : PreservesFiniteProducts F
hSIso : S ∈ ExtensiveSieve X
⊢ IsSheafFor F S

case inr
EverythinProj_ExtrDisc : EverythingIsProjective ExtrDisc
X : ExtrDisc
S : Presieve X
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
hF : PreservesFiniteProducts F
hSSingle : S ∈ RegularSieve X
⊢ IsSheafFor F S

State before:
case inl
EverythinProj_ExtrDisc : EverythingIsProjective ExtrDisc
X : ExtrDisc
S : Presieve X
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
hF : PreservesFiniteProducts F
hSIso : S ∈ ExtensiveSieve X
⊢ IsSheafFor F S
Tactic:
exact isSheafForExtensiveSieve hSIso hF
State after:
no goals

State before:
case inr
EverythinProj_ExtrDisc : EverythingIsProjective ExtrDisc
X : ExtrDisc
S : Presieve X
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
hF : PreservesFiniteProducts F
hSSingle : S ∈ RegularSieve X
⊢ IsSheafFor F S
Tactic:
exact isSheafForRegularSieve hSSingle F
State after:
no goals