-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Konig (goal)
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty.{v + 1} (↑(F.obj j) : Type v)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h_1 : Nonempty J
this : IsCofiltered J
X Y : J
hX : X ∈ G
hY : Y ∈ G
f : X ⟶ Y
hf :
  PSigma.mk (β := fun (X : J) ↦ (Y : J) ×' (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : J) ↦ (_ : X ∈ G) ×' (_ : Y ∈ G) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ G) ↦ (_ : Y ∈ G) ×' (X ⟶ Y)) hX
          (PSigma.mk (β := fun (x : Y ∈ G) ↦ X ⟶ Y) hY f))) ∈
    H
h₁ :
  Eq (α := (↑(F.obj Y) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (F.map f) :
          (a : (↑(F.obj X) : Type v)) → (↑(F.obj Y) : Type v))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
                F.obj (IsCofiltered.inf G H)) (F.map (IsCofiltered.infTo G H hX)) :
              (a : (↑(F.obj (IsCofiltered.inf G H)) : Type v)) → (↑(F.obj X) : Type v))
            (Nonempty.some ⋯) :
          (↑(F.obj X) : Type v)) :
      (↑(F.obj Y) : Type v))
    (if hj : Y ∈ G then
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
              F.obj (IsCofiltered.inf G H)) (F.map (IsCofiltered.infTo G H hj)) :
            (a : (↑(F.obj (IsCofiltered.inf G H)) : Type v)) → (↑(F.obj Y) : Type v))
          (Nonempty.some ⋯)
      else ⋯.some :
      (↑(F.obj Y) : Type v))
⊢ Eq (α := (↑(F.obj Y) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (F.map f) :
          (a : (↑(F.obj X) : Type v)) → (↑(F.obj Y) : Type v))
        (if hj : X ∈ G then
          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
                F.obj (IsCofiltered.inf G H)) (F.map (IsCofiltered.infTo G H hj)) :
              (a : (↑(F.obj (IsCofiltered.inf G H)) : Type v)) → (↑(F.obj X) : Type v))
            (Nonempty.some ⋯)
        else ⋯.some) :
      (↑(F.obj Y) : Type v))
    (if hj : Y ∈ G then
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
              F.obj (IsCofiltered.inf G H)) (F.map (IsCofiltered.infTo G H hj)) :
            (a : (↑(F.obj (IsCofiltered.inf G H)) : Type v)) → (↑(F.obj Y) : Type v))
          (Nonempty.some ⋯)
      else ⋯.some :
      (↑(F.obj Y) : Type v))
have h₂ : Eq (α := (↑(F.obj Y) : Type v))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (F.map f) :
        (a : (↑(F.obj X) : Type v)) → (↑(F.obj Y) : Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
              F.obj (IsCofiltered.inf G H)) (F.map (IsCofiltered.infTo G H hX)) :
            (a : (↑(F.obj (IsCofiltered.inf G H)) : Type v)) → (↑(F.obj X) : Type v))
          (Nonempty.some sorry) :
        (↑(F.obj X) : Type v)) :
    (↑(F.obj Y) : Type v))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
          F.obj (IsCofiltered.inf G H)) (F.map (IsCofiltered.infTo G H hY)) :
        (a : (↑(F.obj (IsCofiltered.inf G H)) : Type v)) → (↑(F.obj Y) : Type v))
      (Nonempty.some sorry) :
    (↑(F.obj Y) : Type v))
Tactic: rwa [dif_pos hX, dif_pos hY, ← comp_app, ← F.map_comp, @IsCofiltered.infTo_commutes _ _ _ G H]