internlm/Lean-Github huggingface dataset:
Theorem: CompHaus.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro.intro.left.inj.hf
B : CompHaus
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : CompHaus
π : 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: CompHaus.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro.intro.right
B : CompHaus
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : CompHaus
π : 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 : CompHaus
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : CompHaus
π : 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: CompHaus.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro.intro.right
B : CompHaus
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : CompHaus
π : 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 : CompHaus
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : CompHaus
π : 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: CompHaus.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro.intro.right
B : CompHaus
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : CompHaus
π : 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: CompHaus.final
Proof state before:
A : Type (u + 2)
inst✝ : Category A
F : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
⊢ Presheaf.IsSheaf (coherentTopology CompHaus) F
Tactic:
rw [← extensiveRegular_generates_coherent]
Proof state after:
A : Type (u + 2)
inst✝ : Category A
F : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
⊢ Presheaf.IsSheaf
    (Coverage.toGrothendieck CompHaus
      (ExtensiveRegularCoverage' CompHaus
        (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
    F
Theorem: CompHaus.final
Proof state before:
A : Type (u + 2)
inst✝ : Category A
F : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
⊢ Presheaf.IsSheaf
    (Coverage.toGrothendieck CompHaus
      (ExtensiveRegularCoverage' CompHaus
        (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
            (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 : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
⊢ ∀ {X : CompHaus} (R : Presieve X),
    R ∈
        Coverage.covering
          (ExtensiveRegularCoverage' CompHaus
            (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
            (_ :
              ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
                (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: CompHaus.final
Proof state before:
A : Type (u + 2)
inst✝ : Category A
F : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
⊢ ∀ {X : CompHaus} (R : Presieve X),
    R ∈
        Coverage.covering
          (ExtensiveRegularCoverage' CompHaus
            (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
            (_ :
              ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
                (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 : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
B : CompHaus
S : Presieve B
hS :
  S ∈
    Coverage.covering
      (ExtensiveRegularCoverage' CompHaus
        (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
            (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: CompHaus.final
Proof state before:
A : Type (u + 2)
inst✝ : Category A
F : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
B : CompHaus
S : Presieve B
hS :
  S ∈
    Coverage.covering
      (ExtensiveRegularCoverage' CompHaus
        (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
            (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 : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
B : CompHaus
S : Presieve B
hS :
  S ∈
    Coverage.covering
      (ExtensiveRegularCoverage' CompHaus
        (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
            (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 : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
B : CompHaus
S : Presieve B
hS :
  S ∈
    Coverage.covering
      (ExtensiveRegularCoverage' CompHaus
        (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      B
⊢ EqualizerCondition (F ⋙ coyoneda.obj E.op)
Theorem: CompHaus.final
Proof state before:
case hFpfp
A : Type (u + 2)
inst✝ : Category A
F : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
B : CompHaus
S : Presieve B
hS :
  S ∈
    Coverage.covering
      (ExtensiveRegularCoverage' CompHaus
        (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
            (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: CompHaus.final
Proof state before:
case hFecs
A : Type (u + 2)
inst✝ : Category A
F : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj E.op)
E : A
B : CompHaus
S : Presieve B
hS :
  S ∈
    Coverage.covering
      (ExtensiveRegularCoverage' CompHaus
        (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
            (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: CompHaus.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 : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts (F ⋙ G)
hF' : EqualizerCondition (F ⋙ G)
⊢ Presheaf.IsSheaf (coherentTopology CompHaus) F
Tactic:
rw [Presheaf.isSheaf_iff_isSheaf_forget (coherentTopology CompHaus) 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 : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts (F ⋙ G)
hF' : EqualizerCondition (F ⋙ G)
⊢ ∀ {X : CompHaus} (R : Presieve X),
    R ∈
        Coverage.covering
          (ExtensiveRegularCoverage' CompHaus
            (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
            (_ :
              ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
                (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
          X →
      IsSheafFor (F ⋙ G) R
Theorem: CompHaus.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 : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts (F ⋙ G)
hF' : EqualizerCondition (F ⋙ G)
⊢ ∀ {X : CompHaus} (R : Presieve X),
    R ∈
        Coverage.covering
          (ExtensiveRegularCoverage' CompHaus
            (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
            (_ :
              ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
                (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 : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts (F ⋙ G)
hF' : EqualizerCondition (F ⋙ G)
B : CompHaus
S' : Presieve B
hS :
  S' ∈
    Coverage.covering
      (ExtensiveRegularCoverage' CompHaus
        (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      B
⊢ IsSheafFor (F ⋙ G) S'
Theorem: CompHaus.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 : CompHausᵒᵖ ⥤ A
hF : PreservesFiniteProducts (F ⋙ G)
hF' : EqualizerCondition (F ⋙ G)
B : CompHaus
S' : Presieve B
hS :
  S' ∈
    Coverage.covering
      (ExtensiveRegularCoverage' CompHaus
        (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
            (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: TopCat.isOpen_iso
Proof state before:
X Y : TopCat
U : Set ↑X
f : X ≅ Y
h : IsOpen U
⊢ IsOpen (↑f.hom '' U)
Tactic:
let ff := TopCat.homeoOfIso f
Proof state after:
X Y : TopCat
U : Set ↑X
f : X ≅ Y
h : IsOpen U
ff : ↑X ≃ₜ ↑Y := homeoOfIso f
⊢ IsOpen (↑f.hom '' U)
Theorem: TopCat.isOpen_iso
Proof state before:
X Y : TopCat
U : Set ↑X
f : X ≅ Y
h : IsOpen U
ff : ↑X ≃ₜ ↑Y := homeoOfIso f
⊢ IsOpen (↑f.hom '' U)
Tactic:
rw [← Homeomorph.isOpen_image ff] at h
Proof state after:
X Y : TopCat
U : Set ↑X
f : X ≅ Y
ff : ↑X ≃ₜ ↑Y := homeoOfIso f
h : IsOpen (↑ff '' U)
⊢ IsOpen (↑f.hom '' U)
Theorem: TopCat.isOpen_iso
Proof state before:
X Y : TopCat
U : Set ↑X
f : X ≅ Y
ff : ↑X ≃ₜ ↑Y := homeoOfIso f
h : IsOpen (↑ff '' U)
⊢ IsOpen (↑f.hom '' U)
Tactic:
assumption
Proof state after:
no goals
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
⊢ TotallyDisconnectedSpace ↑Y
Tactic:
have surj' : Function.Surjective f.hom
Proof state after:
case surj'
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
⊢ Function.Surjective ↑f.hom

X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
⊢ TotallyDisconnectedSpace ↑Y
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
⊢ TotallyDisconnectedSpace ↑Y
Tactic:
have inj' : Function.Injective f.hom
Proof state after:
case inj'
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
⊢ Function.Injective ↑f.hom

X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
⊢ TotallyDisconnectedSpace ↑Y
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
⊢ TotallyDisconnectedSpace ↑Y
Tactic:
constructor
Proof state after:
case isTotallyDisconnected_univ
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
⊢ IsTotallyDisconnected Set.univ
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
⊢ IsTotallyDisconnected Set.univ
Tactic:
unfold _root_.IsTotallyDisconnected
Proof state after:
case isTotallyDisconnected_univ
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
⊢ ∀ (t : Set ↑Y), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
⊢ ∀ (t : Set ↑Y), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
Tactic:
intro t _ ht₂
Proof state after:
case isTotallyDisconnected_univ
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
⊢ Set.Subsingleton t
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
⊢ Set.Subsingleton t
Tactic:
apply Set.subsingleton_of_preimage surj'
Proof state after:
case isTotallyDisconnected_univ.hs
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
⊢ Set.Subsingleton (↑f.hom ⁻¹' t)