-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Konig (goal)
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
intro intro₁ :
  ∀ (A B : FiniteDiagram J),
    ∃ (z : FiniteDiagram J),
      Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            A)
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            z) ∧
        Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            B)
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            z)
intro₂ intro₃ :
  ∀ (A B : FiniteDiagram J),
    ∃ (z : FiniteDiagram J),
      Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            A)
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            z) ∧
        Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            B)
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            z)
⊢ Directed (α := Set ((j : J) → (↑(F.obj j) : Type v))) Superset fun (G : FiniteDiagram J) ↦
    partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))
have refine_1 : ∀ (A B : FiniteDiagram J),
  let ιA :
    FiniteDiagramArrow (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) →
      FiniteDiagramArrow
        (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
          B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) :=
    fun (f : FiniteDiagramArrow (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) ↦
    PSigma.mk (β := fun (X : J) ↦
      (Y : J) ×'
        (_ :
          X ∈
            A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
              B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
          (_ :
            Y ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (X ⟶ Y))
      (f.fst (β := fun (X : J) ↦
        (Y : J) ×'
          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)))
      (PSigma.mk (β := fun (Y : J) ↦
        (_ :
          f.fst (β := fun (X : J) ↦
              (Y : J) ×'
                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
            A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
              B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
          (_ :
            Y ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (f.fst (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
              Y))
        (f.snd (β := fun (X : J) ↦
              (Y : J) ×'
                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
          (β := fun (Y : J) ↦
          (_ :
            f.fst (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                Y)))
        (PSigma.mk (β :=
          fun
            (x :
              f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
          (_ :
            f.snd (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                (β := fun (Y : J) ↦
                (_ :
                  f.fst (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                    A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                      Y)) ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (f.fst (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
              f.snd (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                (β := fun (Y : J) ↦
                (_ :
                  f.fst (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                    A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                      Y))))
          sorry
          (PSigma.mk (β :=
            fun
              (x :
                f.snd (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                    (β := fun (Y : J) ↦
                    (_ :
                      f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                        A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                          Y)) ∈
                  A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                    B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
            f.fst (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
              f.snd (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                (β := fun (Y : J) ↦
                (_ :
                  f.fst (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                    A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                      Y)))
            sorry
            (f.snd (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).snd
                      (β := fun (Y : J) ↦
                      (_ :
                        f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                          A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ⟶
                            Y)).snd
                  (β :=
                  fun
                    (x :
                      f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                        A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
                  (_ :
                    f.snd (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (X ⟶ Y)).fst
                        (β := fun (Y : J) ↦
                        (_ :
                          f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ∈
                            A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ⟶
                              Y)) ∈
                      A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                      f.snd (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (X ⟶ Y)).fst
                        (β := fun (Y : J) ↦
                        (_ :
                          f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ∈
                            A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ⟶
                              Y)))).snd
              (β :=
              fun
                (x :
                  f.snd (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                      (β := fun (Y : J) ↦
                      (_ :
                        f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                          A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ⟶
                            Y)) ∈
                    A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
              f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y)))))));
  let ιB :
    FiniteDiagramArrow (B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) →
      FiniteDiagramArrow
        (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
          B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) :=
    fun (f : FiniteDiagramArrow (B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) ↦
    PSigma.mk (β := fun (X : J) ↦
      (Y : J) ×'
        (_ :
          X ∈
            A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
              B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
          (_ :
            Y ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (X ⟶ Y))
      (f.fst (β := fun (X : J) ↦
        (Y : J) ×'
          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)))
      (PSigma.mk (β := fun (Y : J) ↦
        (_ :
          f.fst (β := fun (X : J) ↦
              (Y : J) ×'
                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
            A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
              B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
          (_ :
            Y ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (f.fst (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
              Y))
        (f.snd (β := fun (X : J) ↦
              (Y : J) ×'
                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
          (β := fun (Y : J) ↦
          (_ :
            f.fst (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
              B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                Y)))
        (PSigma.mk (β :=
          fun
            (x :
              f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
          (_ :
            f.snd (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                (β := fun (Y : J) ↦
                (_ :
                  f.fst (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                    B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                      Y)) ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (f.fst (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
              f.snd (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                (β := fun (Y : J) ↦
                (_ :
                  f.fst (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                    B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                      Y))))
          sorry
          (PSigma.mk (β :=
            fun
              (x :
                f.snd (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                    (β := fun (Y : J) ↦
                    (_ :
                      f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                        B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                          Y)) ∈
                  A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                    B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
            f.fst (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
              f.snd (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                (β := fun (Y : J) ↦
                (_ :
                  f.fst (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                    B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                      Y)))
            sorry
            (f.snd (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).snd
                      (β := fun (Y : J) ↦
                      (_ :
                        f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                          B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ⟶
                            Y)).snd
                  (β :=
                  fun
                    (x :
                      f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                        B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
                  (_ :
                    f.snd (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (X ⟶ Y)).fst
                        (β := fun (Y : J) ↦
                        (_ :
                          f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ∈
                            B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ⟶
                              Y)) ∈
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                      f.snd (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (X ⟶ Y)).fst
                        (β := fun (Y : J) ↦
                        (_ :
                          f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ∈
                            B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ⟶
                              Y)))).snd
              (β :=
              fun
                (x :
                  f.snd (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                      (β := fun (Y : J) ↦
                      (_ :
                        f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                          B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ⟶
                            Y)) ∈
                    B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
              f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y)))))));
  Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
    ((fun (G : FiniteDiagram J) ↦ partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
      A)
    ((fun (G : FiniteDiagram J) ↦ partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
      (Sigma.mk (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))
        (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
          B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))
        (Finset.image ιA (A.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ⊔
          Finset.image ιB (B.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))))
Tactic: classical
  intro A B
  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⟩
  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⟩
  refine ⟨⟨A.1 ⊔ B.1, A.2.image ιA ⊔ B.2.image ιB⟩, ?_, ?_⟩
  · rintro u hu f hf
    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⟩
    exact hu this
  · rintro u hu f hf
    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⟩
    exact hu this