internlm/Lean-Github huggingface dataset:
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro.intro.left.inj.hf
B : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : Profinite
π : X ⟶ B
πsurj : Function.Surjective ↑π
y : Equalizer.FirstObj F (Presieve.singleton π)
h : Equalizer.Presieve.firstMap F (Presieve.singleton π) y = Equalizer.Presieve.secondMap F (Presieve.singleton π) y
hFecs :
  Function.Bijective
    (MapToEqualizer F π (pullback.fst π π) (pullback.snd π π) (_ : pullback.fst π π ≫ π = pullback.snd π π ≫ π))
fork_comp : Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom = F.map π.op
fmap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
smap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.snd π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
iy_mem :
  F.map (pullback.fst π π).op ((EqualizerFirstObjIso F π).hom y) =
    F.map (pullback.snd π π).op ((EqualizerFirstObjIso F π).hom y)
x : F.obj B.op
hx :
  (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) x = (EqualizerFirstObjIso F π).hom y ∧
    ∀ (y_1 : F.obj B.op),
      (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) y_1 =
          (EqualizerFirstObjIso F π).hom y →
        y_1 = x
⊢ IsIso (EqualizerFirstObjIso F π).hom
Tactic:
exact inferInstance
Proof state after:
no goals
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro.intro.right
B : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : Profinite
π : X ⟶ B
πsurj : Function.Surjective ↑π
y : Equalizer.FirstObj F (Presieve.singleton π)
h : Equalizer.Presieve.firstMap F (Presieve.singleton π) y = Equalizer.Presieve.secondMap F (Presieve.singleton π) y
hFecs :
  Function.Bijective
    (MapToEqualizer F π (pullback.fst π π) (pullback.snd π π) (_ : pullback.fst π π ≫ π = pullback.snd π π ≫ π))
fork_comp : Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom = F.map π.op
fmap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
smap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.snd π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
iy_mem :
  F.map (pullback.fst π π).op ((EqualizerFirstObjIso F π).hom y) =
    F.map (pullback.snd π π).op ((EqualizerFirstObjIso F π).hom y)
x : F.obj B.op
hx :
  (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) x = (EqualizerFirstObjIso F π).hom y ∧
    ∀ (y_1 : F.obj B.op),
      (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) y_1 =
          (EqualizerFirstObjIso F π).hom y →
        y_1 = x
⊢ ∀ (y_1 : F.obj B.op), Equalizer.forkMap F (Presieve.singleton π) y_1 = y → y_1 = x
Tactic:
intro z hz
Proof state after:
case inr.intro.intro.intro.intro.right
B : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : Profinite
π : X ⟶ B
πsurj : Function.Surjective ↑π
y : Equalizer.FirstObj F (Presieve.singleton π)
h : Equalizer.Presieve.firstMap F (Presieve.singleton π) y = Equalizer.Presieve.secondMap F (Presieve.singleton π) y
hFecs :
  Function.Bijective
    (MapToEqualizer F π (pullback.fst π π) (pullback.snd π π) (_ : pullback.fst π π ≫ π = pullback.snd π π ≫ π))
fork_comp : Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom = F.map π.op
fmap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
smap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.snd π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
iy_mem :
  F.map (pullback.fst π π).op ((EqualizerFirstObjIso F π).hom y) =
    F.map (pullback.snd π π).op ((EqualizerFirstObjIso F π).hom y)
x : F.obj B.op
hx :
  (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) x = (EqualizerFirstObjIso F π).hom y ∧
    ∀ (y_1 : F.obj B.op),
      (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) y_1 =
          (EqualizerFirstObjIso F π).hom y →
        y_1 = x
z : F.obj B.op
hz : Equalizer.forkMap F (Presieve.singleton π) z = y
⊢ z = x
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro.intro.right
B : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : Profinite
π : X ⟶ B
πsurj : Function.Surjective ↑π
y : Equalizer.FirstObj F (Presieve.singleton π)
h : Equalizer.Presieve.firstMap F (Presieve.singleton π) y = Equalizer.Presieve.secondMap F (Presieve.singleton π) y
hFecs :
  Function.Bijective
    (MapToEqualizer F π (pullback.fst π π) (pullback.snd π π) (_ : pullback.fst π π ≫ π = pullback.snd π π ≫ π))
fork_comp : Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom = F.map π.op
fmap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
smap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.snd π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
iy_mem :
  F.map (pullback.fst π π).op ((EqualizerFirstObjIso F π).hom y) =
    F.map (pullback.snd π π).op ((EqualizerFirstObjIso F π).hom y)
x : F.obj B.op
hx :
  (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) x = (EqualizerFirstObjIso F π).hom y ∧
    ∀ (y_1 : F.obj B.op),
      (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) y_1 =
          (EqualizerFirstObjIso F π).hom y →
        y_1 = x
z : F.obj B.op
hz : Equalizer.forkMap F (Presieve.singleton π) z = y
⊢ z = x
Tactic:
apply_fun (EqualizerFirstObjIso F π).hom at hz
Proof state after:
case inr.intro.intro.intro.intro.right
B : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : Profinite
π : X ⟶ B
πsurj : Function.Surjective ↑π
y : Equalizer.FirstObj F (Presieve.singleton π)
h : Equalizer.Presieve.firstMap F (Presieve.singleton π) y = Equalizer.Presieve.secondMap F (Presieve.singleton π) y
hFecs :
  Function.Bijective
    (MapToEqualizer F π (pullback.fst π π) (pullback.snd π π) (_ : pullback.fst π π ≫ π = pullback.snd π π ≫ π))
fork_comp : Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom = F.map π.op
fmap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
smap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.snd π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
iy_mem :
  F.map (pullback.fst π π).op ((EqualizerFirstObjIso F π).hom y) =
    F.map (pullback.snd π π).op ((EqualizerFirstObjIso F π).hom y)
x : F.obj B.op
hx :
  (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) x = (EqualizerFirstObjIso F π).hom y ∧
    ∀ (y_1 : F.obj B.op),
      (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) y_1 =
          (EqualizerFirstObjIso F π).hom y →
        y_1 = x
z : F.obj B.op
hz : (EqualizerFirstObjIso F π).hom (Equalizer.forkMap F (Presieve.singleton π) z) = (EqualizerFirstObjIso F π).hom y
⊢ z = x
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro.intro.right
B : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : Profinite
π : X ⟶ B
πsurj : Function.Surjective ↑π
y : Equalizer.FirstObj F (Presieve.singleton π)
h : Equalizer.Presieve.firstMap F (Presieve.singleton π) y = Equalizer.Presieve.secondMap F (Presieve.singleton π) y
hFecs :
  Function.Bijective
    (MapToEqualizer F π (pullback.fst π π) (pullback.snd π π) (_ : pullback.fst π π ≫ π = pullback.snd π π ≫ π))
fork_comp : Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom = F.map π.op
fmap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
smap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.snd π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
iy_mem :
  F.map (pullback.fst π π).op ((EqualizerFirstObjIso F π).hom y) =
    F.map (pullback.snd π π).op ((EqualizerFirstObjIso F π).hom y)
x : F.obj B.op
hx :
  (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) x = (EqualizerFirstObjIso F π).hom y ∧
    ∀ (y_1 : F.obj B.op),
      (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) y_1 =
          (EqualizerFirstObjIso F π).hom y →
        y_1 = x
z : F.obj B.op
hz : (EqualizerFirstObjIso F π).hom (Equalizer.forkMap F (Presieve.singleton π) z) = (EqualizerFirstObjIso F π).hom y
⊢ z = x
Tactic:
exact hx.2 z hz
Proof state after:
no goals
Theorem: Profinite.final
Proof 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]
Proof 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
Theorem: Profinite.final
Proof 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 _
Proof 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
Theorem: Profinite.final
Proof 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
Proof 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
Theorem: Profinite.final
Proof 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
Proof 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)
Theorem: Profinite.final
Proof 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 _ _⟩
Proof state after:
no goals
Theorem: Profinite.final
Proof 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
Proof state after:
no goals
Theorem: Profinite.final'
Proof 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]
Proof 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
Theorem: Profinite.final'
Proof 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
Proof 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'
Theorem: Profinite.final'
Proof 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'
Proof state after:
no goals
Theorem: equiv_reflects_mono
Proof state before:
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
⊢ Mono f
Tactic:
have h := e.functor.map_injective (X := X) (Y := Y)
Proof state after:
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
h : Function.Injective e.functor.map
⊢ Mono f
Theorem: equiv_reflects_mono
Proof state before:
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
h : Function.Injective e.functor.map
⊢ Mono f
Tactic:
cases' hef with hef
Proof state after:
case mk
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h : Function.Injective e.functor.map
hef : ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
⊢ Mono f
Theorem: equiv_reflects_mono
Proof state before:
case mk
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h : Function.Injective e.functor.map
hef : ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
⊢ Mono f
Tactic:
constructor
Proof state after:
case mk.right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h : Function.Injective e.functor.map
hef : ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Theorem: equiv_reflects_mono
Proof state before:
case mk.right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h : Function.Injective e.functor.map
hef : ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Tactic:
intros W φ ψ h
Proof state after:
case mk.right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h✝ : Function.Injective e.functor.map
hef : ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ φ = ψ
Theorem: equiv_reflects_mono
Proof state before:
case mk.right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h✝ : Function.Injective e.functor.map
hef : ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ φ = ψ
Tactic:
specialize @hef (e.functor.obj W) (e.functor.map φ) (e.functor.map ψ)
Proof state after:
case mk.right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h✝ : Function.Injective e.functor.map
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
hef : e.functor.map φ ≫ e.functor.map f = e.functor.map ψ ≫ e.functor.map f → e.functor.map φ = e.functor.map ψ
⊢ φ = ψ
Theorem: equiv_reflects_mono
Proof state before:
case mk.right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h✝ : Function.Injective e.functor.map
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
hef : e.functor.map φ ≫ e.functor.map f = e.functor.map ψ ≫ e.functor.map f → e.functor.map φ = e.functor.map ψ
⊢ φ = ψ
Tactic:
sorry
Proof state after:
no goals
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
rintro ⟨α, ⟨h, ⟨Y, ⟨π, hπ⟩⟩⟩⟩
Proof state after:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology C) X