∀ {X : Type u_4} {inst : TopologicalSpace X} {toFun : ℕ → Set X} {isCompact' : ∀ (n : ℕ), IsCompact (toFun n)}
  {subset_interior_succ' : ∀ (n : ℕ), toFun n ⊆ interior (toFun (n + 1))} {iUnion_eq' : ⋃ n, toFun n = Set.univ}
  {toFun_1 : ℕ → Set X} {isCompact'_1 : ∀ (n : ℕ), IsCompact (toFun_1 n)}
  {subset_interior_succ'_1 : ∀ (n : ℕ), toFun_1 n ⊆ interior (toFun_1 (n + 1))}
  {iUnion_eq'_1 : ⋃ n, toFun_1 n = Set.univ},
  { toFun := toFun, isCompact' := isCompact', subset_interior_succ' := subset_interior_succ',
        iUnion_eq' := iUnion_eq' } =
      { toFun := toFun_1, isCompact' := isCompact'_1, subset_interior_succ' := subset_interior_succ'_1,
        iUnion_eq' := iUnion_eq'_1 } →
    toFun = toFun_1