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

Proof state:
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⟩

Tactic:
rintro u hu f hf

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⟩⟩⟩⟩
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
⊢ (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
⊢ ∃ 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 ι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⟩

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⟩⟩⟩⟩
⊢ ∃ 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 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⟩⟩⟩⟩
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
this : ιA 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

Tactic:
exact hu this

Result:
no goals

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⟩⟩⟩⟩
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 ιA A.snd ⊔ Finset.image ιB B.snd

Tactic:
apply Finset.mem_union_right

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
⊢ ιB f ∈ Finset.image ιB B.snd

Proof state:
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
⊢ Directed Superset fun G => partialSections F G.snd

Tactic:
intro A B

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

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⟩⟩⟩⟩
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 f ∈ Finset.image ιA A.snd ⊔ Finset.image ιB B.snd

Tactic:
apply Finset.mem_union_left

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 A.fst
hf : f ∈ A.snd
⊢ ιA f ∈ Finset.image ιA A.snd

Proof state:
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⟩⟩⟩⟩
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
⊢ (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst

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

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⟩⟩⟩⟩
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
this : ιA 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