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

State before:
A : Type (u + 2)
inst✝ : Category A
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
⊢ Presheaf.IsSheaf (coherentTopology Profinite) F
Tactic:
rw [← extensiveRegular_generates_coherent]
State after:
A : Type (u + 2)
inst✝ : Category A
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
⊢ Presheaf.IsSheaf
    (Coverage.toGrothendieck Profinite
      (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))))
    F

State before:
A : Type (u + 2)
inst✝ : Category A
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
⊢ Presheaf.IsSheaf
    (Coverage.toGrothendieck Profinite
      (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))))
    F
Tactic:
refine' fun E => (Presieve.isSheaf_coverage _ _).2 _
State after:
A : Type (u + 2)
inst✝ : Category A
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
⊢ ∀ {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 ⋙ coyoneda.obj E.op) R

State before:
A : Type (u + 2)
inst✝ : Category A
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
⊢ ∀ {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 ⋙ coyoneda.obj E.op) R
Tactic:
intro B S hS
State after:
A : Type (u + 2)
inst✝ : Category A
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
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 ⋙ coyoneda.obj E.op) S

State before:
A : Type (u + 2)
inst✝ : Category A
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
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 ⋙ coyoneda.obj E.op) S
Tactic:
apply isSheafFor_of_Dagur hS
State after:
case hFpfp
A : Type (u + 2)
inst✝ : Category A
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
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
⊢ PreservesFiniteProducts (F ⋙ coyoneda.obj E.op)

case hFecs
A : Type (u + 2)
inst✝ : Category A
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
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
⊢ EqualizerCondition (F ⋙ coyoneda.obj E.op)

State before:
case hFpfp
A : Type (u + 2)
inst✝ : Category A
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
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
⊢ PreservesFiniteProducts (F ⋙ coyoneda.obj E.op)
Tactic:
exact ⟨fun J inst => have := hF.1; compPreservesLimitsOfShape _ _⟩
State after:
no goals

State before:
case hFecs
A : Type (u + 2)
inst✝ : Category A
F : Profiniteᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
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
⊢ EqualizerCondition (F ⋙ coyoneda.obj E.op)
Tactic:
exact hF' E
State after:
no goals