-- Mathlib/Topology/Category/TopCat/Limits/Konig.lean
theorem partialSections.nonempty [IsCofilteredOrEmpty J] [h : ∀ j : J, Nonempty (F.obj j)]
    {G : Finset J} (H : Finset (FiniteDiagramArrow G)) : (partialSections F H).Nonempty

Proof state:
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 : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ (ConcreteCategory.hom (F.map ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩.snd.snd.snd.snd))
      ((fun j => if hj : j ∈ G then (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hj))) ⋯.some else ⋯.some)
        ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩.fst) =
    (fun j => if hj : j ∈ G then (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hj))) ⋯.some else ⋯.some)
      ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩.snd.fst

Tactic:
dsimp only

Result:
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 : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ (ConcreteCategory.hom (F.map f))
      (if hj : X ∈ G then (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hj))) ⋯.some else ⋯.some) =
    if hj : Y ∈ G then (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hj))) ⋯.some else ⋯.some

Proof state:
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
⊢ (partialSections F H).Nonempty

Tactic:
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

Result:
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 (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hj))) ⋯.some else ⋯.some) ∈
    partialSections F H

Proof state:
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)
⊢ (partialSections F H).Nonempty

Tactic:
cases isEmpty_or_nonempty J

Result:
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
⊢ (partialSections F H).Nonempty

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
⊢ (partialSections F H).Nonempty

Proof state:
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 : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ (ConcreteCategory.hom (F.map f))
      (if hj : X ∈ G then (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hj))) ⋯.some else ⋯.some) =
    if hj : Y ∈ G then (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hj))) ⋯.some else ⋯.some

Tactic:
rwa [dif_pos hX, dif_pos hY, ← comp_app, ← F.map_comp, @IsCofiltered.infTo_commutes _ _ _ G H]

Result:
no goals

Proof state:
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
⊢ (partialSections F H).Nonempty

Tactic:
haveI : IsCofiltered J := ⟨⟩

Result:
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
⊢ (partialSections F H).Nonempty

Proof state:
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
⊢ (partialSections F H).Nonempty

Tactic:
exact ⟨isEmptyElim, fun {j} => IsEmpty.elim' inferInstance j.1⟩

Result:
no goals

Proof state:
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 (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hj))) ⋯.some else ⋯.some) ∈
    partialSections F H

Tactic:
rintro ⟨X, Y, hX, hY, f⟩ hf

Result:
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 : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ (ConcreteCategory.hom (F.map ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩.snd.snd.snd.snd))
      ((fun j => if hj : j ∈ G then (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hj))) ⋯.some else ⋯.some)
        ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩.fst) =
    (fun j => if hj : j ∈ G then (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hj))) ⋯.some else ⋯.some)
      ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩.snd.fst