ConditionallyCompleteLattice.le_biSup

lemma ConditionallyCompleteLattice.le_biSup {α : Type*} [ConditionallyCompleteLinearOrder α]    {ι : Type*} {f : ι → α} {s : Set ι} {a : α} (hfs : BddAbove (f '' s)) (ha : ∃ i ∈ s, f i = a) :    a ≤ ⨆ i ∈ s, f i := by  apply le_csSup  · --TODO: improve this    rw [bddAbove_def] at *    rcases hfs with ⟨x, hx⟩    use (max x (sSup ∅))    intro y hy    simp only [Set.mem_range] at hy    rcases hy with ⟨z, hz⟩    rw [iSup] at hz    by_cases h : z ∈ s    · have : (@Set.range α (z ∈ s) fun _ ↦ f z) = {f z} := by        rw [Set.eq_singleton_iff_unique_mem]        exact ⟨Set.mem_range_self h, fun x hx ↦ hx.2.symm⟩      rw [this, csSup_singleton _] at hz      have : f z ≤ x := by        simp only [Set.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hx        exact hx z h      rw [hz] at this      exact le_max_of_le_left this    have : (@Set.range α (z ∈ s) fun _ ↦ f z) = ∅ := by simpa    rw [this] at hz    exact hz ▸ le_max_right x y  rw [Set.mem_range]  rcases ha with ⟨i, hi, fia⟩  use i  rw [iSup]  convert csSup_singleton _  rw [Set.eq_singleton_iff_unique_mem]  refine ⟨⟨hi, fia⟩, fun x hx ↦ ?_⟩  simp only [Set.mem_range, exists_prop] at hx  rwa [hx.2] at fia