[GOAL]
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
⊢ Set.Nonempty (partialSections F H)
[PROOFSTEP]
classical
cases isEmpty_or_nonempty J
· exact ⟨isEmptyElim, fun {j} => IsEmpty.elim' inferInstance j.1⟩
haveI : IsCofiltered J := ⟨⟩
use fun j : J => if hj : j ∈ G then F.map (IsCofiltered.infTo G H hj) (h (IsCofiltered.inf G H)).some else (h _).some
rintro ⟨X, Y, hX, hY, f⟩ hf
dsimp only
rwa [dif_pos hX, dif_pos hY, ← comp_app, ← F.map_comp, @IsCofiltered.infTo_commutes _ _ _ G H]
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
⊢ Set.Nonempty (partialSections F H)
[PROOFSTEP]
cases isEmpty_or_nonempty J
[GOAL]
case inl
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
h✝ : IsEmpty J
⊢ Set.Nonempty (partialSections F H)
[PROOFSTEP]
exact ⟨isEmptyElim, fun {j} => IsEmpty.elim' inferInstance j.1⟩
[GOAL]
case inr
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
h✝ : Nonempty J
⊢ Set.Nonempty (partialSections F H)
[PROOFSTEP]
haveI : IsCofiltered J := ⟨⟩
[GOAL]
case inr
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
⊢ Set.Nonempty (partialSections F H)
[PROOFSTEP]
use fun j : J => if hj : j ∈ G then F.map (IsCofiltered.infTo G H hj) (h (IsCofiltered.inf G H)).some else (h _).some
[GOAL]
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
⊢ (fun j =>
      if hj : j ∈ G then
        ↑(F.map (IsCofiltered.infTo G H hj)) (Nonempty.some (_ : Nonempty ↑(F.obj (IsCofiltered.inf G H))))
      else Nonempty.some (_ : Nonempty ↑(F.obj j))) ∈
    partialSections F H
[PROOFSTEP]
rintro ⟨X, Y, hX, hY, f⟩ hf
[GOAL]
case h.mk.mk.mk.mk
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
X Y : J
hX : X ∈ G
hY : Y ∈ G
f : X ⟶ Y
hf : { fst := X, snd := { fst := Y, snd := { fst := hX, snd := { fst := hY, snd := f } } } } ∈ H
⊢ ↑(F.map { fst := X, snd := { fst := Y, snd := { fst := hX, snd := { fst := hY, snd := f } } } }.snd.snd.snd.snd)
      ((fun j =>
          if hj : j ∈ G then
            ↑(F.map (IsCofiltered.infTo G H hj)) (Nonempty.some (_ : Nonempty ↑(F.obj (IsCofiltered.inf G H))))
          else Nonempty.some (_ : Nonempty ↑(F.obj j)))
        { fst := X, snd := { fst := Y, snd := { fst := hX, snd := { fst := hY, snd := f } } } }.fst) =
    (fun j =>
        if hj : j ∈ G then
          ↑(F.map (IsCofiltered.infTo G H hj)) (Nonempty.some (_ : Nonempty ↑(F.obj (IsCofiltered.inf G H))))
        else Nonempty.some (_ : Nonempty ↑(F.obj j)))
      { fst := X, snd := { fst := Y, snd := { fst := hX, snd := { fst := hY, snd := f } } } }.snd.fst
[PROOFSTEP]
dsimp only
[GOAL]
case h.mk.mk.mk.mk
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
X Y : J
hX : X ∈ G
hY : Y ∈ G
f : X ⟶ Y
hf : { fst := X, snd := { fst := Y, snd := { fst := hX, snd := { fst := hY, snd := f } } } } ∈ H
⊢ ↑(F.map f)
      (if hj : X ∈ G then
        ↑(F.map (IsCofiltered.infTo G H hj)) (Nonempty.some (_ : Nonempty ↑(F.obj (IsCofiltered.inf G H))))
      else Nonempty.some (_ : Nonempty ↑(F.obj X))) =
    if hj : Y ∈ G then
      ↑(F.map (IsCofiltered.infTo G H hj)) (Nonempty.some (_ : Nonempty ↑(F.obj (IsCofiltered.inf G H))))
    else Nonempty.some (_ : Nonempty ↑(F.obj Y))
[PROOFSTEP]
rwa [dif_pos hX, dif_pos hY, ← comp_app, ← F.map_comp, @IsCofiltered.infTo_commutes _ _ _ G H]
[GOAL]
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
⊢ Directed Superset fun G => partialSections F G.snd
[PROOFSTEP]
classical
intro A B
let ιA : FiniteDiagramArrow A.1 → FiniteDiagramArrow (A.1 ⊔ B.1) := fun f =>
  ⟨f.1, f.2.1, Finset.mem_union_left _ f.2.2.1, Finset.mem_union_left _ f.2.2.2.1, f.2.2.2.2⟩
let ιB : FiniteDiagramArrow B.1 → FiniteDiagramArrow (A.1 ⊔ B.1) := fun f =>
  ⟨f.1, f.2.1, Finset.mem_union_right _ f.2.2.1, Finset.mem_union_right _ f.2.2.2.1, f.2.2.2.2⟩
refine' ⟨⟨A.1 ⊔ B.1, A.2.image ιA ⊔ B.2.image ιB⟩, _, _⟩
· rintro u hu f hf
  have : ιA f ∈ A.2.image ιA ⊔ B.2.image ιB := by
    apply Finset.mem_union_left
    rw [Finset.mem_image]
    refine' ⟨f, hf, rfl⟩
  exact hu this
· rintro u hu f hf
  have : ιB f ∈ A.2.image ιA ⊔ B.2.image ιB :=
    by
    apply Finset.mem_union_right
    rw [Finset.mem_image]
    refine' ⟨f, hf, rfl⟩
  exact hu this
[GOAL]
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
⊢ Directed Superset fun G => partialSections F G.snd
[PROOFSTEP]
intro A B
[GOAL]
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
⊢ ∃ z,
    (fun G => partialSections F G.snd) A ⊇ (fun G => partialSections F G.snd) z ∧
      (fun G => partialSections F G.snd) B ⊇ (fun G => partialSections F G.snd) z
[PROOFSTEP]
let ιA : FiniteDiagramArrow A.1 → FiniteDiagramArrow (A.1 ⊔ B.1) := fun f =>
  ⟨f.1, f.2.1, Finset.mem_union_left _ f.2.2.1, Finset.mem_union_left _ f.2.2.2.1, f.2.2.2.2⟩
[GOAL]
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
⊢ ∃ z,
    (fun G => partialSections F G.snd) A ⊇ (fun G => partialSections F G.snd) z ∧
      (fun G => partialSections F G.snd) B ⊇ (fun G => partialSections F G.snd) z
[PROOFSTEP]
let ιB : FiniteDiagramArrow B.1 → FiniteDiagramArrow (A.1 ⊔ B.1) := fun f =>
  ⟨f.1, f.2.1, Finset.mem_union_right _ f.2.2.1, Finset.mem_union_right _ f.2.2.2.1, f.2.2.2.2⟩
[GOAL]
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
⊢ ∃ z,
    (fun G => partialSections F G.snd) A ⊇ (fun G => partialSections F G.snd) z ∧
      (fun G => partialSections F G.snd) B ⊇ (fun G => partialSections F G.snd) z
[PROOFSTEP]
refine' ⟨⟨A.1 ⊔ B.1, A.2.image ιA ⊔ B.2.image ιB⟩, _, _⟩
[GOAL]
case refine'_1
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
⊢ (fun G => partialSections F G.snd) A ⊇
    (fun G => partialSections F G.snd) { fst := A.fst ⊔ B.fst, snd := Finset.image ιA A.snd ⊔ Finset.image ιB B.snd }
[PROOFSTEP]
rintro u hu f hf
[GOAL]
case refine'_1
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
u : (j : J) → ↑(F.obj j)
hu :
  u ∈ (fun G => partialSections F G.snd) { fst := A.fst ⊔ B.fst, snd := Finset.image ιA A.snd ⊔ Finset.image ιB B.snd }
f : TopCat.FiniteDiagramArrow A.fst
hf : f ∈ A.snd
⊢ ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst
[PROOFSTEP]
have : ιA f ∈ A.2.image ιA ⊔ B.2.image ιB := by
  apply Finset.mem_union_left
  rw [Finset.mem_image]
  refine' ⟨f, hf, rfl⟩
[GOAL]
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
u : (j : J) → ↑(F.obj j)
hu :
  u ∈ (fun G => partialSections F G.snd) { fst := A.fst ⊔ B.fst, snd := Finset.image ιA A.snd ⊔ Finset.image ιB B.snd }
f : TopCat.FiniteDiagramArrow A.fst
hf : f ∈ A.snd
⊢ ιA f ∈ Finset.image ιA A.snd ⊔ Finset.image ιB B.snd
[PROOFSTEP]
apply Finset.mem_union_left
[GOAL]
case h
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
u : (j : J) → ↑(F.obj j)
hu :
  u ∈ (fun G => partialSections F G.snd) { fst := A.fst ⊔ B.fst, snd := Finset.image ιA A.snd ⊔ Finset.image ιB B.snd }
f : TopCat.FiniteDiagramArrow A.fst
hf : f ∈ A.snd
⊢ ιA f ∈ Finset.image ιA A.snd
[PROOFSTEP]
rw [Finset.mem_image]
[GOAL]
case h
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
u : (j : J) → ↑(F.obj j)
hu :
  u ∈ (fun G => partialSections F G.snd) { fst := A.fst ⊔ B.fst, snd := Finset.image ιA A.snd ⊔ Finset.image ιB B.snd }
f : TopCat.FiniteDiagramArrow A.fst
hf : f ∈ A.snd
⊢ ∃ a, a ∈ A.snd ∧ ιA a = ιA f
[PROOFSTEP]
refine' ⟨f, hf, rfl⟩
[GOAL]
case refine'_1
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
u : (j : J) → ↑(F.obj j)
hu :
  u ∈ (fun G => partialSections F G.snd) { fst := A.fst ⊔ B.fst, snd := Finset.image ιA A.snd ⊔ Finset.image ιB B.snd }
f : TopCat.FiniteDiagramArrow A.fst
hf : f ∈ A.snd
this : ιA f ∈ Finset.image ιA A.snd ⊔ Finset.image ιB B.snd
⊢ ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst
[PROOFSTEP]
exact hu this
[GOAL]
case refine'_2
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
⊢ (fun G => partialSections F G.snd) B ⊇
    (fun G => partialSections F G.snd) { fst := A.fst ⊔ B.fst, snd := Finset.image ιA A.snd ⊔ Finset.image ιB B.snd }
[PROOFSTEP]
rintro u hu f hf
[GOAL]
case refine'_2
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
u : (j : J) → ↑(F.obj j)
hu :
  u ∈ (fun G => partialSections F G.snd) { fst := A.fst ⊔ B.fst, snd := Finset.image ιA A.snd ⊔ Finset.image ιB B.snd }
f : TopCat.FiniteDiagramArrow B.fst
hf : f ∈ B.snd
⊢ ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst
[PROOFSTEP]
have : ιB f ∈ A.2.image ιA ⊔ B.2.image ιB := by
  apply Finset.mem_union_right
  rw [Finset.mem_image]
  refine' ⟨f, hf, rfl⟩
[GOAL]
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
u : (j : J) → ↑(F.obj j)
hu :
  u ∈ (fun G => partialSections F G.snd) { fst := A.fst ⊔ B.fst, snd := Finset.image ιA A.snd ⊔ Finset.image ιB B.snd }
f : TopCat.FiniteDiagramArrow B.fst
hf : f ∈ B.snd
⊢ ιB f ∈ Finset.image ιA A.snd ⊔ Finset.image ιB B.snd
[PROOFSTEP]
apply Finset.mem_union_right
[GOAL]
case h
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
u : (j : J) → ↑(F.obj j)
hu :
  u ∈ (fun G => partialSections F G.snd) { fst := A.fst ⊔ B.fst, snd := Finset.image ιA A.snd ⊔ Finset.image ιB B.snd }
f : TopCat.FiniteDiagramArrow B.fst
hf : f ∈ B.snd
⊢ ιB f ∈ Finset.image ιB B.snd
[PROOFSTEP]
rw [Finset.mem_image]
[GOAL]
case h
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
u : (j : J) → ↑(F.obj j)
hu :
  u ∈ (fun G => partialSections F G.snd) { fst := A.fst ⊔ B.fst, snd := Finset.image ιA A.snd ⊔ Finset.image ιB B.snd }
f : TopCat.FiniteDiagramArrow B.fst
hf : f ∈ B.snd
⊢ ∃ a, a ∈ B.snd ∧ ιB a = ιB f
[PROOFSTEP]
refine' ⟨f, hf, rfl⟩
[GOAL]
case refine'_2
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : TopCat.FiniteDiagram J
ιA : TopCat.FiniteDiagramArrow A.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f =>
    { fst := f.fst,
      snd :=
        { fst := f.snd.fst,
          snd :=
            { fst := (_ : f.fst ∈ A.fst ∪ B.fst),
              snd := { fst := (_ : f.snd.fst ∈ A.fst ∪ B.fst), snd := f.snd.snd.snd.snd } } } }
u : (j : J) → ↑(F.obj j)
hu :
  u ∈ (fun G => partialSections F G.snd) { fst := A.fst ⊔ B.fst, snd := Finset.image ιA A.snd ⊔ Finset.image ιB B.snd }
f : TopCat.FiniteDiagramArrow B.fst
hf : f ∈ B.snd
this : ιB f ∈ Finset.image ιA A.snd ⊔ Finset.image ιB B.snd
⊢ ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst
[PROOFSTEP]
exact hu this
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
⊢ IsClosed (partialSections F H)
[PROOFSTEP]
have : partialSections F H = ⋂ (f : FiniteDiagramArrow G) (_ : f ∈ H), {u | F.map f.2.2.2.2 (u f.1) = u f.2.1} :=
  by
  ext1
  simp only [Set.mem_iInter, Set.mem_setOf_eq]
  rfl
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
⊢ partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H), {u | ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
[PROOFSTEP]
ext1
[GOAL]
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
x✝ : (j : J) → ↑(F.obj j)
⊢ x✝ ∈ partialSections F H ↔
    x✝ ∈ ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H), {u | ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
[PROOFSTEP]
simp only [Set.mem_iInter, Set.mem_setOf_eq]
[GOAL]
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
x✝ : (j : J) → ↑(F.obj j)
⊢ x✝ ∈ partialSections F H ↔
    ∀ (i : TopCat.FiniteDiagramArrow G), i ∈ H → ↑(F.map i.snd.snd.snd.snd) (x✝ i.fst) = x✝ i.snd.fst
[PROOFSTEP]
rfl
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H), {u | ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
⊢ IsClosed (partialSections F H)
[PROOFSTEP]
rw [this]
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H), {u | ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
⊢ IsClosed (⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H), {u | ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst})
[PROOFSTEP]
apply isClosed_biInter
[GOAL]
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H), {u | ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
⊢ ∀ (i : TopCat.FiniteDiagramArrow G),
    (i ∈ fun i => i ∈ H.val) → IsClosed {u | ↑(F.map i.snd.snd.snd.snd) (u i.fst) = u i.snd.fst}
[PROOFSTEP]
intro f
  _
    -- Porting note: can't see through forget
[GOAL]
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H), {u | ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ fun i => i ∈ H.val
⊢ IsClosed {u | ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
[PROOFSTEP]
have : T2Space ((forget TopCat).obj (F.obj f.snd.fst)) := inferInstanceAs (T2Space (F.obj f.snd.fst))
[GOAL]
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this✝ :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H), {u | ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ fun i => i ∈ H.val
this : T2Space ((forget TopCat).obj (F.obj f.snd.fst))
⊢ IsClosed {u | ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
[PROOFSTEP]
apply isClosed_eq
[GOAL]
case h.hf
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this✝ :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H), {u | ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ fun i => i ∈ H.val
this : T2Space ((forget TopCat).obj (F.obj f.snd.fst))
⊢ Continuous fun x => ↑(F.map f.snd.snd.snd.snd) (x f.fst)
[PROOFSTEP]
exact (F.map f.snd.snd.snd.snd).continuous.comp (continuous_apply f.fst)
[GOAL]
case h.hg
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this✝ :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H), {u | ↑(F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ fun i => i ∈ H.val
this : T2Space ((forget TopCat).obj (F.obj f.snd.fst))
⊢ Continuous fun x => x f.snd.fst
[PROOFSTEP]
continuity
[GOAL]
J : Type u
inst✝⁴ : SmallCategory J
F✝ : J ⥤ TopCat
F : J ⥤ TopCatMax
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
⊢ Nonempty ↑(limitCone F).pt
[PROOFSTEP]
classical
obtain ⟨u, hu⟩ :=
  IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed (fun G => partialSections F _)
    (partialSections.directed F) (fun G => partialSections.nonempty F _)
    (fun G => IsClosed.isCompact (partialSections.closed F _)) fun G => partialSections.closed F _
use u
intro X Y f
let G : FiniteDiagram J :=
  ⟨{ X, Y },
    {⟨X, Y, by simp only [true_or_iff, eq_self_iff_true, Finset.mem_insert], by
        simp only [eq_self_iff_true, or_true_iff, Finset.mem_insert, Finset.mem_singleton], f⟩}⟩
exact hu _ ⟨G, rfl⟩ (Finset.mem_singleton_self _)
[GOAL]
J : Type u
inst✝⁴ : SmallCategory J
F✝ : J ⥤ TopCat
F : J ⥤ TopCatMax
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
⊢ Nonempty ↑(limitCone F).pt
[PROOFSTEP]
obtain ⟨u, hu⟩ :=
  IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed (fun G => partialSections F _)
    (partialSections.directed F) (fun G => partialSections.nonempty F _)
    (fun G => IsClosed.isCompact (partialSections.closed F _)) fun G => partialSections.closed F _
[GOAL]
case intro
J : Type u
inst✝⁴ : SmallCategory J
F✝ : J ⥤ TopCat
F : J ⥤ TopCatMax
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ (i : TopCat.FiniteDiagram J), partialSections F i.snd
⊢ Nonempty ↑(limitCone F).pt
[PROOFSTEP]
use u
[GOAL]
case property
J : Type u
inst✝⁴ : SmallCategory J
F✝ : J ⥤ TopCat
F : J ⥤ TopCatMax
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ (i : TopCat.FiniteDiagram J), partialSections F i.snd
⊢ u ∈ {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j}
[PROOFSTEP]
intro X Y f
[GOAL]
case property
J : Type u
inst✝⁴ : SmallCategory J
F✝ : J ⥤ TopCat
F : J ⥤ TopCatMax
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ (i : TopCat.FiniteDiagram J), partialSections F i.snd
X Y : J
f : X ⟶ Y
⊢ ↑(F.map f) (u X) = u Y
[PROOFSTEP]
let G : FiniteDiagram J :=
  ⟨{ X, Y },
    {⟨X, Y, by simp only [true_or_iff, eq_self_iff_true, Finset.mem_insert], by
        simp only [eq_self_iff_true, or_true_iff, Finset.mem_insert, Finset.mem_singleton], f⟩}⟩
[GOAL]
J : Type u
inst✝⁴ : SmallCategory J
F✝ : J ⥤ TopCat
F : J ⥤ TopCatMax
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ (i : TopCat.FiniteDiagram J), partialSections F i.snd
X Y : J
f : X ⟶ Y
⊢ X ∈ {X, Y}
[PROOFSTEP]
simp only [true_or_iff, eq_self_iff_true, Finset.mem_insert]
[GOAL]
J : Type u
inst✝⁴ : SmallCategory J
F✝ : J ⥤ TopCat
F : J ⥤ TopCatMax
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ (i : TopCat.FiniteDiagram J), partialSections F i.snd
X Y : J
f : X ⟶ Y
⊢ Y ∈ {X, Y}
[PROOFSTEP]
simp only [eq_self_iff_true, or_true_iff, Finset.mem_insert, Finset.mem_singleton]
[GOAL]
case property
J : Type u
inst✝⁴ : SmallCategory J
F✝ : J ⥤ TopCat
F : J ⥤ TopCatMax
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ (i : TopCat.FiniteDiagram J), partialSections F i.snd
X Y : J
f : X ⟶ Y
G : TopCat.FiniteDiagram J :=
  { fst := {X, Y},
    snd :=
      {{ fst := X,
          snd := { fst := Y, snd := { fst := (_ : X ∈ {X, Y}), snd := { fst := (_ : Y ∈ {X, Y}), snd := f } } } }} }
⊢ ↑(F.map f) (u X) = u Y
[PROOFSTEP]
exact hu _ ⟨G, rfl⟩ (Finset.mem_singleton_self _)


[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
x✝ : OpenNhds x
⊢ x✝ ≤ x✝
[PROOFSTEP]
dsimp [LE.le]
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
x✝ : OpenNhds x
⊢ x✝.obj ≤ x✝.obj
[PROOFSTEP]
exact le_rfl
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
x✝² x✝¹ x✝ : OpenNhds x
⊢ x✝² ≤ x✝¹ → x✝¹ ≤ x✝ → x✝² ≤ x✝
[PROOFSTEP]
dsimp [LE.le]
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
x✝² x✝¹ x✝ : OpenNhds x
⊢ x✝².obj ≤ x✝¹.obj → x✝¹.obj ≤ x✝.obj → x✝².obj ≤ x✝.obj
[PROOFSTEP]
exact le_trans
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
x✝ : OpenNhds x
⊢ x✝ ≤ ⊤
[PROOFSTEP]
dsimp [LE.le]
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
x✝ : OpenNhds x
⊢ x✝.obj ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : (OpenNhds x)ᵒᵖ
⊢ (map (𝟙 X) x).obj U.unop = U.unop
[PROOFSTEP]
simp
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : (OpenNhds x)ᵒᵖ
⊢ (map (𝟙 X) x).op.obj U = U
[PROOFSTEP]
simp
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (inclusion (↑f x) ⋙ Opens.map f).obj U ≅ (map f x ⋙ inclusion x).obj U
[PROOFSTEP]
constructor
[GOAL]
case hom_inv_id
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ autoParam (?hom ≫ ?inv = 𝟙 ((inclusion (↑f x) ⋙ Opens.map f).obj U)) _auto✝
case inv_hom_id
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ autoParam (?inv ≫ ?hom = 𝟙 ((map f x ⋙ inclusion x).obj U)) _auto✝
case hom
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (inclusion (↑f x) ⋙ Opens.map f).obj U ⟶ (map f x ⋙ inclusion x).obj U
case inv
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (map f x ⋙ inclusion x).obj U ⟶ (inclusion (↑f x) ⋙ Opens.map f).obj U
[PROOFSTEP]
rfl
[GOAL]
case inv_hom_id
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ autoParam (?inv ≫ ?hom = 𝟙 ((map f x ⋙ inclusion x).obj U)) _auto✝
case hom
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (inclusion (↑f x) ⋙ Opens.map f).obj U ⟶ (map f x ⋙ inclusion x).obj U
case inv
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (map f x ⋙ inclusion x).obj U ⟶ (inclusion (↑f x) ⋙ Opens.map f).obj U
[PROOFSTEP]
rfl
[GOAL]
case hom
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (inclusion (↑f x) ⋙ Opens.map f).obj U ⟶ (map f x ⋙ inclusion x).obj U
case inv
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (map f x ⋙ inclusion x).obj U ⟶ (inclusion (↑f x) ⋙ Opens.map f).obj U
[PROOFSTEP]
exact 𝟙 _
[GOAL]
case inv
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (map f x ⋙ inclusion x).obj U ⟶ (inclusion (↑f x) ⋙ Opens.map f).obj U
[PROOFSTEP]
exact 𝟙 _


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : SpectralMap α β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : SpectralMap α β
toFun✝ : α → β
spectral'✝ : IsSpectralMap toFun✝
h : { toFun := toFun✝, spectral' := spectral'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, spectral' := spectral'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
toFun✝¹ : α → β
spectral'✝¹ : IsSpectralMap toFun✝¹
toFun✝ : α → β
spectral'✝ : IsSpectralMap toFun✝
h : { toFun := toFun✝¹, spectral' := spectral'✝¹ }.toFun = { toFun := toFun✝, spectral' := spectral'✝ }.toFun
⊢ { toFun := toFun✝¹, spectral' := spectral'✝¹ } = { toFun := toFun✝, spectral' := spectral'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : SpectralMap β γ
g : SpectralMap α β
⊢ ↑f ∘ ↑g = ↑↑f ∘ ↑↑g
[PROOFSTEP]
rfl
  -- porting note: removed `simp` from this and added lemma above to address `simpNF` lint
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : SpectralMap β γ
g : SpectralMap α β
⊢ ↑(comp f g) = ContinuousMap.comp ↑f ↑g
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : SpectralMap β γ
f₁ f₂ : SpectralMap α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]


[GOAL]
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace Z
proj : Z → B
inst✝ : Nonempty F
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ Function.Surjective proj
[PROOFSTEP]
obtain ⟨e, rfl⟩ := h.proj_eq
[GOAL]
case intro
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty F
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ↑e)
⊢ Function.Surjective (Prod.fst ∘ ↑e)
[PROOFSTEP]
exact Prod.fst_surjective.comp e.surjective
[GOAL]
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
proj : Z → B
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ Continuous proj
[PROOFSTEP]
obtain ⟨e, rfl⟩ := h.proj_eq
[GOAL]
case intro
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ↑e)
⊢ Continuous (Prod.fst ∘ ↑e)
[PROOFSTEP]
exact continuous_fst.comp e.continuous
[GOAL]
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
proj : Z → B
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ IsOpenMap proj
[PROOFSTEP]
obtain ⟨e, rfl⟩ := h.proj_eq
[GOAL]
case intro
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ↑e)
⊢ IsOpenMap (Prod.fst ∘ ↑e)
[PROOFSTEP]
exact isOpenMap_fst.comp e.isOpenMap


[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ↑f
⊢ IsIso f
[PROOFSTEP]
let E := Equiv.ofBijective _ bij
[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ↑f
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective (↑f) bij
⊢ IsIso f
[PROOFSTEP]
have hE : Continuous E.symm := by
  rw [continuous_iff_isClosed]
  intro S hS
  rw [← E.image_eq_preimage]
  exact isClosedMap f S hS
[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ↑f
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective (↑f) bij
⊢ Continuous ↑E.symm
[PROOFSTEP]
rw [continuous_iff_isClosed]
[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ↑f
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective (↑f) bij
⊢ ∀ (s : Set ((forget CompHaus).obj X)), IsClosed s → IsClosed (↑E.symm ⁻¹' s)
[PROOFSTEP]
intro S hS
[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ↑f
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective (↑f) bij
S : Set ((forget CompHaus).obj X)
hS : IsClosed S
⊢ IsClosed (↑E.symm ⁻¹' S)
[PROOFSTEP]
rw [← E.image_eq_preimage]
[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ↑f
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective (↑f) bij
S : Set ((forget CompHaus).obj X)
hS : IsClosed S
⊢ IsClosed (↑E '' S)
[PROOFSTEP]
exact isClosedMap f S hS
[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ↑f
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective (↑f) bij
hE : Continuous ↑E.symm
⊢ IsIso f
[PROOFSTEP]
refine' ⟨⟨⟨E.symm, hE⟩, _, _⟩⟩
[GOAL]
case refine'_1
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ↑f
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective (↑f) bij
hE : Continuous ↑E.symm
⊢ f ≫ ContinuousMap.mk ↑E.symm = 𝟙 X
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.w
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ↑f
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective (↑f) bij
hE : Continuous ↑E.symm
x : (forget CompHaus).obj X
⊢ ↑(f ≫ ContinuousMap.mk ↑E.symm) x = ↑(𝟙 X) x
[PROOFSTEP]
apply E.symm_apply_apply
[GOAL]
case refine'_2
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ↑f
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective (↑f) bij
hE : Continuous ↑E.symm
⊢ ContinuousMap.mk ↑E.symm ≫ f = 𝟙 Y
[PROOFSTEP]
ext x
[GOAL]
case refine'_2.w
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ↑f
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective (↑f) bij
hE : Continuous ↑E.symm
x : (forget CompHaus).obj Y
⊢ ↑(ContinuousMap.mk ↑E.symm ≫ f) x = ↑(𝟙 Y) x
[PROOFSTEP]
apply E.apply_symm_apply
[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ ContinuousMap.mk ↑f ≫ ContinuousMap.mk ↑(Homeomorph.symm f) = 𝟙 X
[PROOFSTEP]
ext x
[GOAL]
case w
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : ↑X.toTop ≃ₜ ↑Y.toTop
x : (forget CompHaus).obj X
⊢ ↑(ContinuousMap.mk ↑f ≫ ContinuousMap.mk ↑(Homeomorph.symm f)) x = ↑(𝟙 X) x
[PROOFSTEP]
exact f.symm_apply_apply x
[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ ContinuousMap.mk ↑(Homeomorph.symm f) ≫ ContinuousMap.mk ↑f = 𝟙 Y
[PROOFSTEP]
ext x
[GOAL]
case w
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : ↑X.toTop ≃ₜ ↑Y.toTop
x : (forget CompHaus).obj Y
⊢ ↑(ContinuousMap.mk ↑(Homeomorph.symm f) ≫ ContinuousMap.mk ↑f) x = ↑(𝟙 Y) x
[PROOFSTEP]
exact f.apply_symm_apply x
[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ≅ Y
x : ↑X.toTop
⊢ ↑f.inv (↑f.hom x) = x
[PROOFSTEP]
simp
[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ≅ Y
x : ↑Y.toTop
⊢ ↑f.hom (↑f.inv x) = x
[PROOFSTEP]
simp
[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ≅ Y
⊢ isoOfHomeo (homeoOfIso f) = f
[PROOFSTEP]
ext
[GOAL]
case w.w
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ≅ Y
x✝ : (forget CompHaus).obj X
⊢ ↑(isoOfHomeo (homeoOfIso f)).hom x✝ = ↑f.hom x✝
[PROOFSTEP]
rfl
[GOAL]
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ homeoOfIso (isoOfHomeo f) = f
[PROOFSTEP]
ext
[GOAL]
case H
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : ↑X.toTop ≃ₜ ↑Y.toTop
x✝ : ↑X.toTop
⊢ ↑(homeoOfIso (isoOfHomeo f)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {A B : CompHaus} (f : A ⟶ B) [inst : IsIso ((forget CompHaus).map f)], IsIso f
[PROOFSTEP]
intro A B f hf
[GOAL]
A B : CompHaus
f : A ⟶ B
hf : IsIso ((forget CompHaus).map f)
⊢ IsIso f
[PROOFSTEP]
exact CompHaus.isIso_of_bijective _ ((isIso_iff_bijective f).mp hf)
[GOAL]
X : TopCat
Y : CompHaus
⊢ Function.LeftInverse (fun f => ContinuousMap.mk (stoneCechExtend (_ : Continuous f.toFun))) fun f =>
    ContinuousMap.mk (↑f ∘ stoneCechUnit)
[PROOFSTEP]
rintro
  ⟨f : StoneCech X ⟶ Y, hf : Continuous f⟩
      -- Porting note: `ext` fails.
[GOAL]
case mk
X : TopCat
Y : CompHaus
f : StoneCech ↑X ⟶ ↑Y.toTop
hf : Continuous f
⊢ (fun f => ContinuousMap.mk (stoneCechExtend (_ : Continuous f.toFun)))
      ((fun f => ContinuousMap.mk (↑f ∘ stoneCechUnit)) (ContinuousMap.mk f)) =
    ContinuousMap.mk f
[PROOFSTEP]
apply ContinuousMap.ext
[GOAL]
case mk.h
X : TopCat
Y : CompHaus
f : StoneCech ↑X ⟶ ↑Y.toTop
hf : Continuous f
⊢ ∀ (a : ↑(stoneCechObj X).toTop),
    ↑((fun f => ContinuousMap.mk (stoneCechExtend (_ : Continuous f.toFun)))
            ((fun f => ContinuousMap.mk (↑f ∘ stoneCechUnit)) (ContinuousMap.mk f)))
        a =
      ↑(ContinuousMap.mk f) a
[PROOFSTEP]
intro (x : StoneCech X)
[GOAL]
case mk.h
X : TopCat
Y : CompHaus
f : StoneCech ↑X ⟶ ↑Y.toTop
hf : Continuous f
x : StoneCech ↑X
⊢ ↑((fun f => ContinuousMap.mk (stoneCechExtend (_ : Continuous f.toFun)))
          ((fun f => ContinuousMap.mk (↑f ∘ stoneCechUnit)) (ContinuousMap.mk f)))
      x =
    ↑(ContinuousMap.mk f) x
[PROOFSTEP]
refine' congr_fun _ x
[GOAL]
case mk.h
X : TopCat
Y : CompHaus
f : StoneCech ↑X ⟶ ↑Y.toTop
hf : Continuous f
x : StoneCech ↑X
⊢ ↑((fun f => ContinuousMap.mk (stoneCechExtend (_ : Continuous f.toFun)))
        ((fun f => ContinuousMap.mk (↑f ∘ stoneCechUnit)) (ContinuousMap.mk f))) =
    ↑(ContinuousMap.mk f)
[PROOFSTEP]
apply Continuous.ext_on denseRange_stoneCechUnit (continuous_stoneCechExtend _) hf
[GOAL]
case mk.h
X : TopCat
Y : CompHaus
f : StoneCech ↑X ⟶ ↑Y.toTop
hf : Continuous f
x : StoneCech ↑X
⊢ Set.EqOn (stoneCechExtend ?m.48961) f (Set.range stoneCechUnit)
X : TopCat
Y : CompHaus
f : StoneCech ↑X ⟶ ↑Y.toTop
hf : Continuous f
x : StoneCech ↑X
⊢ Continuous ((fun f => ContinuousMap.mk (↑f ∘ stoneCechUnit)) (ContinuousMap.mk f)).toFun
[PROOFSTEP]
rintro _ ⟨y, rfl⟩
[GOAL]
case mk.h.intro
X : TopCat
Y : CompHaus
f : StoneCech ↑X ⟶ ↑Y.toTop
hf : Continuous f
x : StoneCech ↑X
y : ↑X
⊢ stoneCechExtend ?m.48961 (stoneCechUnit y) = f (stoneCechUnit y)
X : TopCat
Y : CompHaus
f : StoneCech ↑X ⟶ ↑Y.toTop
hf : Continuous f
x : StoneCech ↑X
⊢ Continuous ((fun f => ContinuousMap.mk (↑f ∘ stoneCechUnit)) (ContinuousMap.mk f)).toFun
[PROOFSTEP]
apply congr_fun (stoneCechExtend_extends (hf.comp _)) y
[GOAL]
X : TopCat
Y : CompHaus
f : StoneCech ↑X ⟶ ↑Y.toTop
hf : Continuous f
x : StoneCech ↑X
⊢ Continuous fun x => stoneCechUnit x
[PROOFSTEP]
apply continuous_stoneCechUnit
[GOAL]
X : TopCat
Y : CompHaus
⊢ Function.RightInverse (fun f => ContinuousMap.mk (stoneCechExtend (_ : Continuous f.toFun))) fun f =>
    ContinuousMap.mk (↑f ∘ stoneCechUnit)
[PROOFSTEP]
rintro
  ⟨f : (X : Type _) ⟶ Y, hf : Continuous f⟩
      -- Porting note: `ext` fails.
[GOAL]
case mk
X : TopCat
Y : CompHaus
f : ↑X ⟶ ↑Y.toTop
hf : Continuous f
⊢ (fun f => ContinuousMap.mk (↑f ∘ stoneCechUnit))
      ((fun f => ContinuousMap.mk (stoneCechExtend (_ : Continuous f.toFun))) (ContinuousMap.mk f)) =
    ContinuousMap.mk f
[PROOFSTEP]
apply ContinuousMap.ext
[GOAL]
case mk.h
X : TopCat
Y : CompHaus
f : ↑X ⟶ ↑Y.toTop
hf : Continuous f
⊢ ∀ (a : ↑X),
    ↑((fun f => ContinuousMap.mk (↑f ∘ stoneCechUnit))
            ((fun f => ContinuousMap.mk (stoneCechExtend (_ : Continuous f.toFun))) (ContinuousMap.mk f)))
        a =
      ↑(ContinuousMap.mk f) a
[PROOFSTEP]
intro
[GOAL]
case mk.h
X : TopCat
Y : CompHaus
f : ↑X ⟶ ↑Y.toTop
hf : Continuous f
a✝ : ↑X
⊢ ↑((fun f => ContinuousMap.mk (↑f ∘ stoneCechUnit))
          ((fun f => ContinuousMap.mk (stoneCechExtend (_ : Continuous f.toFun))) (ContinuousMap.mk f)))
      a✝ =
    ↑(ContinuousMap.mk f) a✝
[PROOFSTEP]
exact congr_fun (stoneCechExtend_extends hf) _
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
⊢ CompactSpace ↑(TopCat.limitCone FF).pt
[PROOFSTEP]
show CompactSpace {u : ∀ j, F.obj j | ∀ {i j : J} (f : i ⟶ j), (F.map f) (u i) = u j}
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
⊢ CompactSpace ↑{u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j}
[PROOFSTEP]
rw [← isCompact_iff_compactSpace]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
⊢ IsCompact {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j}
[PROOFSTEP]
apply IsClosed.isCompact
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
⊢ IsClosed {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j}
[PROOFSTEP]
have :
  {u : ∀ j, F.obj j | ∀ {i j : J} (f : i ⟶ j), F.map f (u i) = u j} =
    ⋂ (i : J) (j : J) (f : i ⟶ j), {u | F.map f (u i) = u j} :=
  by
  ext1
  simp only [Set.mem_iInter, Set.mem_setOf_eq]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
⊢ {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j} = ⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j}
[PROOFSTEP]
ext1
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
x✝ : (j : J) → ↑(F.obj j).toTop
⊢ x✝ ∈ {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j} ↔
    x✝ ∈ ⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j}
[PROOFSTEP]
simp only [Set.mem_iInter, Set.mem_setOf_eq]
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j} = ⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j}
⊢ IsClosed {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j}
[PROOFSTEP]
rw [this]
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j} = ⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j}
⊢ IsClosed (⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j})
[PROOFSTEP]
apply isClosed_iInter
[GOAL]
case h.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j} = ⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j}
⊢ ∀ (i : J), IsClosed (⋂ (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j})
[PROOFSTEP]
intro i
[GOAL]
case h.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j} = ⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j}
i : J
⊢ IsClosed (⋂ (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j})
[PROOFSTEP]
apply isClosed_iInter
[GOAL]
case h.h.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j} = ⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j}
i : J
⊢ ∀ (i_1 : J), IsClosed (⋂ (f : i ⟶ i_1), {u | ↑(F.map f) (u i) = u i_1})
[PROOFSTEP]
intro j
[GOAL]
case h.h.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j} = ⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j}
i j : J
⊢ IsClosed (⋂ (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j})
[PROOFSTEP]
apply isClosed_iInter
[GOAL]
case h.h.h.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j} = ⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j}
i j : J
⊢ ∀ (i_1 : i ⟶ j), IsClosed {u | ↑(F.map i_1) (u i) = u j}
[PROOFSTEP]
intro f
[GOAL]
case h.h.h.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j} = ⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j}
i j : J
f : i ⟶ j
⊢ IsClosed {u | ↑(F.map f) (u i) = u j}
[PROOFSTEP]
apply isClosed_eq
[GOAL]
case h.h.h.h.hf
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j} = ⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j}
i j : J
f : i ⟶ j
⊢ Continuous fun x => ↑(F.map f) (x i)
[PROOFSTEP]
exact (ContinuousMap.continuous (F.map f)).comp (continuous_apply i)
[GOAL]
case h.h.h.h.hg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j} = ⋂ (i : J) (j : J) (f : i ⟶ j), {u | ↑(F.map f) (u i) = u j}
i j : J
f : i ⟶ j
⊢ Continuous fun x => x j
[PROOFSTEP]
exact continuous_apply j
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj (mk (TopCat.limitCone FF).pt)).map f ≫ (fun j => NatTrans.app (TopCat.limitCone FF).π j) Y =
      (fun j => NatTrans.app (TopCat.limitCone FF).π j) X ≫ F.map f
[PROOFSTEP]
intro _ _ f
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ ((Functor.const J).obj (mk (TopCat.limitCone FF).pt)).map f ≫ (fun j => NatTrans.app (TopCat.limitCone FF).π j) Y✝ =
    (fun j => NatTrans.app (TopCat.limitCone FF).π j) X✝ ≫ F.map f
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case w.mk
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
X✝ Y✝ : J
f : X✝ ⟶ Y✝
x : (j : J) → ↑(FF.obj j)
hx : x ∈ {u | ∀ {i j : J} (f : i ⟶ j), ↑(FF.map f) (u i) = u j}
⊢ ↑(((Functor.const J).obj (mk (TopCat.limitCone FF).pt)).map f ≫ (fun j => NatTrans.app (TopCat.limitCone FF).π j) Y✝)
      { val := x, property := hx } =
    ↑((fun j => NatTrans.app (TopCat.limitCone FF).π j) X✝ ≫ F.map f) { val := x, property := hx }
[PROOFSTEP]
simp only [comp_apply, Functor.const_obj_map, id_apply]
[GOAL]
case w.mk
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCatMax := F ⋙ compHausToTop
X✝ Y✝ : J
f : X✝ ⟶ Y✝
x : (j : J) → ↑(FF.obj j)
hx : x ∈ {u | ∀ {i j : J} (f : i ⟶ j), ↑(FF.map f) (u i) = u j}
⊢ ↑(NatTrans.app (TopCat.limitCone (F ⋙ compHausToTop)).π Y✝)
      (↑(𝟙 (mk (TopCat.limitCone (F ⋙ compHausToTop)).pt)) { val := x, property := hx }) =
    ↑(F.map f) (↑(NatTrans.app (TopCat.limitCone (F ⋙ compHausToTop)).π X✝) { val := x, property := hx })
[PROOFSTEP]
exact (hx f).symm
[GOAL]
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f → Function.Surjective ↑f
[PROOFSTEP]
dsimp [Function.Surjective]
[GOAL]
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f → ∀ (b : (forget CompHaus).obj Y), ∃ a, ↑f a = b
[PROOFSTEP]
contrapose!
[GOAL]
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ (∃ b, ∀ (a : (forget CompHaus).obj X), ↑f a ≠ b) → ¬Epi f
[PROOFSTEP]
rintro ⟨y, hy⟩ hf
[GOAL]
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
⊢ False
[PROOFSTEP]
let C := Set.range f
[GOAL]
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
⊢ False
[PROOFSTEP]
have hC : IsClosed C := (isCompact_range f.continuous).isClosed
[GOAL]
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
⊢ False
[PROOFSTEP]
let D := ({ y } : Set Y)
[GOAL]
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
⊢ False
[PROOFSTEP]
have hD : IsClosed D := isClosed_singleton
[GOAL]
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
⊢ False
[PROOFSTEP]
have hCD : Disjoint C D := by
  rw [Set.disjoint_singleton_right]
  rintro ⟨y', hy'⟩
  exact hy y' hy'
[GOAL]
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
⊢ Disjoint C D
[PROOFSTEP]
rw [Set.disjoint_singleton_right]
[GOAL]
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
⊢ ¬y ∈ C
[PROOFSTEP]
rintro ⟨y', hy'⟩
[GOAL]
case intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
y' : (forget CompHaus).obj X
hy' : ↑f y' = y
⊢ False
[PROOFSTEP]
exact hy y' hy'
[GOAL]
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
⊢ False
[PROOFSTEP]
haveI : NormalSpace ((forget CompHaus).obj Y) := normalOfCompactT2
[GOAL]
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this : NormalSpace ((forget CompHaus).obj Y)
⊢ False
[PROOFSTEP]
obtain ⟨φ, hφ0, hφ1, hφ01⟩ := exists_continuous_zero_one_of_closed hC hD hCD
[GOAL]
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
⊢ False
[PROOFSTEP]
haveI : CompactSpace (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.compactSpace
[GOAL]
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this : CompactSpace (ULift ↑(Set.Icc 0 1))
⊢ False
[PROOFSTEP]
haveI : T2Space (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.t2Space
[GOAL]
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
⊢ False
[PROOFSTEP]
let Z := of (ULift.{u} <| Set.Icc (0 : ℝ) 1)
[GOAL]
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
⊢ False
[PROOFSTEP]
let g : Y ⟶ Z := ⟨fun y' => ⟨⟨φ y', hφ01 y'⟩⟩, continuous_uLift_up.comp (φ.continuous.subtype_mk fun y' => hφ01 y')⟩
[GOAL]
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
⊢ False
[PROOFSTEP]
let h : Y ⟶ Z := ⟨fun _ => ⟨⟨0, Set.left_mem_Icc.mpr zero_le_one⟩⟩, continuous_const⟩
[GOAL]
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
⊢ False
[PROOFSTEP]
have H : h = g := by
  rw [← cancel_epi f]
  ext x
  apply ULift.ext
  apply Subtype.ext
  dsimp
    -- Porting note: This `change` is not ideal.
          -- I think lean is having issues understanding when a `ContinuousMap` should be considered
          -- as a morphism.
          -- TODO(?): Make morphisms in `CompHaus` (and other topological categories)
          -- into a one-field-structure.
  change 0 = φ (f x)
  simp only [hφ0 (Set.mem_range_self x), Pi.zero_apply]
[GOAL]
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
⊢ h = g
[PROOFSTEP]
rw [← cancel_epi f]
[GOAL]
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
⊢ f ≫ h = f ≫ g
[PROOFSTEP]
ext x
[GOAL]
case w
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ ↑(f ≫ h) x = ↑(f ≫ g) x
[PROOFSTEP]
apply ULift.ext
[GOAL]
case w.h
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ (↑(f ≫ h) x).down = (↑(f ≫ g) x).down
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case w.h.a
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ ↑(↑(f ≫ h) x).down = ↑(↑(f ≫ g) x).down
[PROOFSTEP]
dsimp
  -- Porting note: This `change` is not ideal.
        -- I think lean is having issues understanding when a `ContinuousMap` should be considered
        -- as a morphism.
        -- TODO(?): Make morphisms in `CompHaus` (and other topological categories)
        -- into a one-field-structure.
[GOAL]
case w.h.a
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ ↑(↑(f ≫ ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }) x).down =
    ↑(↑(f ≫ ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }) x).down
[PROOFSTEP]
change 0 = φ (f x)
[GOAL]
case w.h.a
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ 0 = ↑φ (↑f x)
[PROOFSTEP]
simp only [hφ0 (Set.mem_range_self x), Pi.zero_apply]
[GOAL]
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H : h = g
⊢ False
[PROOFSTEP]
apply_fun fun e => (e y).down.1 at H
[GOAL]
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H : ↑(↑h y).down = ↑(↑g y).down
⊢ False
[PROOFSTEP]
dsimp at H
[GOAL]
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H :
  ↑(↑(ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }) y).down =
    ↑(↑(ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }) y).down
⊢ False
[PROOFSTEP]
change 0 = φ y at H
[GOAL]
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H : 0 = ↑φ y
⊢ False
[PROOFSTEP]
simp only [hφ1 (Set.mem_singleton y), Pi.one_apply] at H
[GOAL]
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ↑f
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H : 0 = 1
⊢ False
[PROOFSTEP]
exact zero_ne_one H
[GOAL]
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Function.Surjective ↑f → Epi f
[PROOFSTEP]
rw [← CategoryTheory.epi_iff_surjective]
[GOAL]
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Epi ↑f → Epi f
[PROOFSTEP]
apply (forget CompHaus).epi_of_epi_map
[GOAL]
X Y : CompHaus
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ↑f
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Mono f → Function.Injective ↑f
[PROOFSTEP]
intro hf x₁ x₂ h
[GOAL]
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : ↑f x₁ = ↑f x₂
⊢ x₁ = x₂
[PROOFSTEP]
let g₁ : of PUnit ⟶ X := ⟨fun _ => x₁, continuous_const⟩
[GOAL]
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : ↑f x₁ = ↑f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
⊢ x₁ = x₂
[PROOFSTEP]
let g₂ : of PUnit ⟶ X := ⟨fun _ => x₂, continuous_const⟩
[GOAL]
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : ↑f x₁ = ↑f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
⊢ x₁ = x₂
[PROOFSTEP]
have : g₁ ≫ f = g₂ ≫ f := by
  ext
  exact h
[GOAL]
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : ↑f x₁ = ↑f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
⊢ g₁ ≫ f = g₂ ≫ f
[PROOFSTEP]
ext
[GOAL]
case w
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : ↑f x₁ = ↑f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
x✝ : (forget CompHaus).obj (of PUnit)
⊢ ↑(g₁ ≫ f) x✝ = ↑(g₂ ≫ f) x✝
[PROOFSTEP]
exact h
[GOAL]
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : ↑f x₁ = ↑f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
this : g₁ ≫ f = g₂ ≫ f
⊢ x₁ = x₂
[PROOFSTEP]
rw [cancel_mono] at this
[GOAL]
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : ↑f x₁ = ↑f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
this : g₁ = g₂
⊢ x₁ = x₂
[PROOFSTEP]
apply_fun fun e => e PUnit.unit at this
[GOAL]
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : ↑f x₁ = ↑f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
this : ↑g₁ PUnit.unit = ↑g₂ PUnit.unit
⊢ x₁ = x₂
[PROOFSTEP]
exact this
[GOAL]
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Function.Injective ↑f → Mono f
[PROOFSTEP]
rw [← CategoryTheory.mono_iff_injective]
[GOAL]
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Mono ↑f → Mono f
[PROOFSTEP]
apply (forget CompHaus).mono_of_mono_map