[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 _)
