J✝ : Type v
inst✝¹ : SmallCategory J✝
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
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
⊢ Directed Superset fun G => partialSections F G.snd
intro A B
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
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⟩
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
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⟩
case refine'_1
J✝ : Type v
inst✝¹ : SmallCategory J✝
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 }

case refine'_2
J✝ : Type v
inst✝¹ : SmallCategory J✝
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 }
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
refine' ⟨⟨A.1 ⊔ B.1, A.2.image ιA ⊔ B.2.image ιB⟩, _, _⟩
case refine'_1
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
⊢ (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst
case refine'_1
J✝ : Type v
inst✝¹ : SmallCategory J✝
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 }
rintro u hu f hf
case refine'_1
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
⊢ (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst
case refine'_1
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
⊢ (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst
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⟩
no goals
case refine'_1
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
⊢ (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst
exact hu this
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
apply Finset.mem_union_left
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
rw [Finset.mem_image]
no goals
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
refine' ⟨f, hf, rfl⟩
case refine'_2
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
⊢ (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst
case refine'_2
J✝ : Type v
inst✝¹ : SmallCategory J✝
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 }
rintro u hu f hf
case refine'_2
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
⊢ (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst
case refine'_2
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
⊢ (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst
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⟩
no goals
case refine'_2
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
⊢ (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst
exact hu this
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
apply Finset.mem_union_right
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
rw [Finset.mem_image]
no goals
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
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
refine' ⟨f, hf, rfl⟩