chain_property_set_has_bound

lemma chain_property_set_has_bound (k : ℤ) :    ∀ c ⊆ property_set X k, IsChain (· ⊆ ·) c →      ∃ ub ∈ property_set X k, ∀ s ∈ c, s ⊆ ub := by  intro c hc hchain  use (⋃ s ∈ c,s) ∪ (if k = S then {o} else ∅)  by_cases h : c = ∅  · simpa [h] using property_set_nonempty X k  have h : ∃ z, z ∈ c := by    rw [Set.ext_iff] at h    push Not at h    simpa using h  have : (⋃ s ∈ c,s) ∪ (if k = S then ({o} : Set X) else ∅) = (⋃ s ∈ c,s) := by    ext x    constructor    · rintro (l | r)      · exact l      simp only [mem_ite_empty_right, mem_singleton_iff] at r      obtain ⟨z, hz⟩ := h      rw [r.right]      push _ ∈ _      use z, hz      specialize hc hz      dsimp only [property_set] at hc      rw [mem_setOf_eq] at hc      exact hc.right.right r.left    · exact fun hex ↦ Or.intro_left (x ∈ if k = ↑S then {o} else ∅) hex  simp_rw [this]  dsimp only [property_set] at hc ⊢  simp only [mem_setOf_eq, iUnion_subset_iff]  constructor  · constructor    · intro i hi      specialize hc hi      rw [mem_setOf_eq] at hc      exact hc.left    constructor    · intro x hx y hy      push _ ∈ _ at hx hy      obtain ⟨sx, hsx, hsx'⟩ := hx      obtain ⟨sy, hsy, hsy'⟩ := hy      obtain hxy | hyx := hchain.total hsx hsy      · exact (hc hsy).right.left (hxy hsx') hsy'      · exact (hc hsx).right.left hsx' (hyx hsy')    · obtain ⟨x,hx⟩ := h      intro hk      push _ ∈ _      exact ⟨x, hx, (hc hx).right.right hk⟩  · exact fun s a ↦ subset_iUnion₂_of_subset s a fun ⦃a⦄ a ↦ a