case inl
J✝ : Type v
inst✝² : SmallCategory J✝
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)

case inr
J✝ : Type v
inst✝² : SmallCategory J✝
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)
J✝ : Type v
inst✝² : SmallCategory J✝
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)
cases (isEmpty_or_nonempty J)
no goals
case inl
J✝ : Type v
inst✝² : SmallCategory J✝
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)
exact ⟨isEmptyElim, fun {j} _ => IsEmpty.elim' inferInstance j.fst⟩
case inr
J✝ : Type v
inst✝² : SmallCategory J✝
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)
case inr
J✝ : Type v
inst✝² : SmallCategory J✝
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)
haveI : IsCofiltered J := ⟨⟩
case inr
J✝ : Type v
inst✝² : SmallCategory J✝
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
        (forget TopCat).map (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
case inr
J✝ : Type v
inst✝² : SmallCategory J✝
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)
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
case inr.mk.mk.mk.mk
J✝ : Type v
inst✝² : SmallCategory J✝
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
⊢ (forget TopCat).map
      (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
            (forget TopCat).map (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
          (forget TopCat).map (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
case inr
J✝ : Type v
inst✝² : SmallCategory J✝
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
        (forget TopCat).map (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
rintro ⟨X, Y, hX, hY, f⟩ hf
case inr.mk.mk.mk.mk
J✝ : Type v
inst✝² : SmallCategory J✝
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
⊢ (forget TopCat).map (F.map f)
      (if hj : X ∈ G then
        (forget TopCat).map (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
      (forget TopCat).map (F.map (IsCofiltered.infTo G H hj))
        (Nonempty.some (_ : Nonempty ↑(F.obj (IsCofiltered.inf G H))))
    else Nonempty.some (_ : Nonempty ↑(F.obj Y))
case inr.mk.mk.mk.mk
J✝ : Type v
inst✝² : SmallCategory J✝
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
⊢ (forget TopCat).map
      (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
            (forget TopCat).map (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
          (forget TopCat).map (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
dsimp only
no goals
case inr.mk.mk.mk.mk
J✝ : Type v
inst✝² : SmallCategory J✝
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
⊢ (forget TopCat).map (F.map f)
      (if hj : X ∈ G then
        (forget TopCat).map (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
      (forget TopCat).map (F.map (IsCofiltered.infTo G H hj))
        (Nonempty.some (_ : Nonempty ↑(F.obj (IsCofiltered.inf G H))))
    else Nonempty.some (_ : Nonempty ↑(F.obj Y))
rwa [dif_pos hX, dif_pos hY, ← comp_app, ← F.map_comp, @IsCofiltered.infTo_commutes _ _ _ G H]