-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Konig (goal)
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : ∀ (j : J), T2Space.{v} (↑(F.obj j) : Type v)
G : Finset J
H : Finset (FiniteDiagramArrow G)
x : (j : J) → (↑(F.obj j) : Type v)
⊢ x ∈ partialSections F H ↔
    Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type v)))
      (⋂ f ∈ H,
        {u : (j : J) → (↑(F.obj j) : Type v) |
          Eq (α :=
            (↑(F.obj
                  (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                    (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                      (_ : Y ∈ G) ×'
                        (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
              Type v))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                    (F.map
                      (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).snd (β :=
                                fun (Y : J) ↦
                                (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                  (_ : Y ∈ G) ×'
                                    (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                                      Y)).snd
                            (β :=
                            fun (x : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ↦
                            (_ :
                              f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                                  fun (Y : J) ↦
                                  (_ :
                                    f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                    (_ : Y ∈ G) ×'
                                      (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                                        Y)) ∈
                                G) ×'
                              (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                                f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                                  fun (Y : J) ↦
                                  (_ :
                                    f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                    (_ : Y ∈ G) ×'
                                      (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                                        Y)))).snd
                        (β :=
                        fun
                          (x :
                            f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                                fun (Y : J) ↦
                                (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                                  (_ : Y ∈ G) ×'
                                    (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)) ∈
                              G) ↦
                        f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                          f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                            fun (Y : J) ↦
                            (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                              (_ : Y ∈ G) ×'
                                (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y))))) :
                  (a : (↑(F.obj f.fst) : Type v)) → (↑(F.obj f.snd.fst) : Type v))
                (u (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)))) :
              (↑(F.obj
                    (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                      (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                        (_ : Y ∈ G) ×'
                          (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
                Type v))
            (u
                (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                  (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                    (_ : Y ∈ G) ×' (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y))) :
              (↑(F.obj
                    (f.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                      (_ : f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                        (_ : Y ∈ G) ×'
                          (f.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
                Type v))})
      x
have h : x ∈ partialSections F H ↔
  ∀ (i : FiniteDiagramArrow G) (i_1 : i ∈ H),
    Eq (α :=
      (↑(F.obj
            (i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
              (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                (_ : Y ∈ G) ×' (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
        Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              (F.map
                (i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).snd (β := fun (Y : J) ↦
                          (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                            (_ : Y ∈ G) ×'
                              (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)).snd
                      (β := fun (x : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ↦
                      (_ :
                        i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                            fun (Y : J) ↦
                            (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                              (_ : Y ∈ G) ×'
                                (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)) ∈
                          G) ×'
                        (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                          i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                            fun (Y : J) ↦
                            (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                              (_ : Y ∈ G) ×'
                                (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))).snd
                  (β :=
                  fun
                    (x :
                      i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β :=
                          fun (Y : J) ↦
                          (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                            (_ : Y ∈ G) ×'
                              (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)) ∈
                        G) ↦
                  i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶
                    i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                      (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                        (_ : Y ∈ G) ×'
                          (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y))))) :
            (a : (↑(F.obj i.fst) : Type v)) → (↑(F.obj i.snd.fst) : Type v))
          (x (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)))) :
        (↑(F.obj
              (i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                  (_ : Y ∈ G) ×' (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
          Type v))
      (x
          (i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
            (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
              (_ : Y ∈ G) ×' (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y))) :
        (↑(F.obj
              (i.snd (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)).fst (β := fun (Y : J) ↦
                (_ : i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ∈ G) ×'
                  (_ : Y ∈ G) ×' (i.fst (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) ⟶ Y)))) :
          Type v))
Tactic: simp only [Set.mem_iInter, Set.mem_setOf_eq]