-- Mathlib/Topology/Category/TopCat/Limits/Konig.lean
theorem partialSections.directed :
    Directed Superset fun G : FiniteDiagram J => partialSections F G.2

Proof state:
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 => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, 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

Tactic:
refine ⟨⟨A.1 ⊔ B.1, A.2.image ιA ⊔ B.2.image ιB⟩, ?_, ?_⟩

Result:
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 => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
⊢ (fun G => partialSections F G.snd) A ⊇
    (fun G => partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩

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 => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
⊢ (fun G => partialSections F G.snd) B ⊇
    (fun G => partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩

Proof state:
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 => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G => partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : TopCat.FiniteDiagramArrow B.fst
hf : f ∈ B.snd
⊢ (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst

Tactic:
have : ιB f ∈ A.2.image ιA ⊔ B.2.image ιB := by
  apply Finset.mem_union_right
  rw [Finset.mem_image]
  exact ⟨f, hf, rfl⟩

Result:
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 => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G => partialSections F G.snd) ⟨A.fst ⊔ B.fst, 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
⊢ (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst

Proof state:
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 => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, 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

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

Result:
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 => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, 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

Proof state:
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 => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G => partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : TopCat.FiniteDiagramArrow B.fst
hf : f ∈ B.snd
⊢ ∃ a ∈ B.snd, ιB a = ιB f

Tactic:
exact ⟨f, hf, rfl⟩

Result:
no goals

Proof state:
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 => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G => partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : TopCat.FiniteDiagramArrow A.fst
hf : f ∈ A.snd
⊢ ∃ a ∈ A.snd, ιA a = ιA f

Tactic:
exact ⟨f, hf, rfl⟩

Result:
no goals

Proof state:
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 => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G => partialSections F G.snd) ⟨A.fst ⊔ B.fst, 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

Tactic:
rw [Finset.mem_image]

Result:
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 => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : TopCat.FiniteDiagramArrow B.fst → TopCat.FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f => ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G => partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : TopCat.FiniteDiagramArrow B.fst
hf : f ∈ B.snd
⊢ ∃ a ∈ B.snd, ιB a = ιB f