Theorem: Profinite.final' (Profinite/ExplicitSheaves.lean)

State before:
A : Type (u + 2)
inst✝³ : Category A
G : A ⥤ Type (u + 1)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits G
inst✝ : ReflectsIsomorphisms G
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts (F ⋙ G)
hF' : EqualizerCondition (F ⋙ G)
⊢ Presheaf.IsSheaf (coherentTopology Profinite) F
Tactic:
rw [Presheaf.isSheaf_iff_isSheaf_forget (coherentTopology Profinite) F G,
  isSheaf_iff_isSheaf_of_type, ← extensiveRegular_generates_coherent, Presieve.isSheaf_coverage]
State after:
A : Type (u + 2)
inst✝³ : Category A
G : A ⥤ Type (u + 1)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits G
inst✝ : ReflectsIsomorphisms G
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts (F ⋙ G)
hF' : EqualizerCondition (F ⋙ G)
⊢ ∀ {X : Profinite} (R : Presieve X),
    R ∈
        Coverage.covering
          (ExtensiveRegularCoverage' Profinite
            (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
            (_ :
              ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X)
                {Y : Profinite} (f : Y ⟶ X) (x : IsIso (Sigma.desc π)),
                IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
          X →
      IsSheafFor (F ⋙ G) R

State before:
A : Type (u + 2)
inst✝³ : Category A
G : A ⥤ Type (u + 1)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits G
inst✝ : ReflectsIsomorphisms G
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts (F ⋙ G)
hF' : EqualizerCondition (F ⋙ G)
⊢ ∀ {X : Profinite} (R : Presieve X),
    R ∈
        Coverage.covering
          (ExtensiveRegularCoverage' Profinite
            (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
            (_ :
              ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X)
                {Y : Profinite} (f : Y ⟶ X) (x : IsIso (Sigma.desc π)),
                IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
          X →
      IsSheafFor (F ⋙ G) R
Tactic:
intro B S' hS
State after:
A : Type (u + 2)
inst✝³ : Category A
G : A ⥤ Type (u + 1)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits G
inst✝ : ReflectsIsomorphisms G
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts (F ⋙ G)
hF' : EqualizerCondition (F ⋙ G)
B : Profinite
S' : Presieve B
hS :
  S' ∈
    Coverage.covering
      (ExtensiveRegularCoverage' Profinite
        (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      B
⊢ IsSheafFor (F ⋙ G) S'

State before:
A : Type (u + 2)
inst✝³ : Category A
G : A ⥤ Type (u + 1)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits G
inst✝ : ReflectsIsomorphisms G
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts (F ⋙ G)
hF' : EqualizerCondition (F ⋙ G)
B : Profinite
S' : Presieve B
hS :
  S' ∈
    Coverage.covering
      (ExtensiveRegularCoverage' Profinite
        (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      B
⊢ IsSheafFor (F ⋙ G) S'
Tactic:
exact isSheafFor_of_Dagur hS hF hF'
State after:
no goals