Univ prop Dedekind Mac Neille Completion

theorem univ_prop_DedekindMacNeilleCompletion{α : Type*} [PartialOrder α] {β : Type*} [CompleteLattice β] (f : α ↪o β) :∃ f' : DedekindMacNeilleCompletion α ↪o β, f = f' ∘ coe' := by  let g := fun x : DedekindMacNeilleCompletion α ↦ sSup <| lowerBounds <| upperBounds <| f '' x.val  have : ∀ (A B : DedekindMacNeilleCompletion α), g A ≤ g B ↔ A ≤ B := by    refine fun A B ↦ ⟨?_,?_⟩    · intro h      by_contra!      rcases (Set.not_subset.1 this) with ⟨a, haA, haB⟩      have : ∃ u ∈ upperBounds B, ¬ a ≤ u := by        by_contra!        exact haB ((ClosureOperator.IsClosed.closure_eq B.property) ▸ this)      refine (fun w ↦ this.choose_spec.2 (f.map_rel_iff'.1 w)) ?_      have h₁ : f a ≤ g A := le_sSup fun u hu ↦ hu (Exists.intro a ⟨haA, rfl⟩)      have h₂ : g B ≤ f (this.choose) := by        refine sSup_le fun y hy ↦ hy ?_        simp only [upperBounds, Set.mem_image, forall_exists_index, and_imp,          forall_apply_eq_imp_iff₂, Set.mem_setOf_eq, OrderEmbedding.le_iff_le]        exact this.choose_spec.1.out      exact le_trans h₁ <| le_trans h h₂    · intro h      simp only [upperBounds, Set.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,        sSup_le_iff, g]      exact fun y hy ↦ hy.out fun w hw ↦ le_sSup fun ⦃a⦄ a ↦ a w (h hw)  refine ⟨⟨⟨g,fun x y h ↦ le_antisymm ((this x y).1 <| (le_antisymm_iff.1 h).1)    ((this y x).1 <| (le_antisymm_iff.1 h).2)⟩,?_⟩,?_⟩  · simp only [Function.Embedding.coeFn_mk, Subtype.forall, Subtype.mk_le_mk, Set.le_eq_subset, g]    exact fun x hx y hy ↦ this ⟨x, hx⟩ ⟨y, hy⟩  · refine funext fun x ↦ ?_    simp only [RelEmbedding.coe_mk, Function.Embedding.coeFn_mk, coe', Function.comp_apply, g]    refine le_antisymm (le_sSup fun a ha ↦ ha.out <|      Set.mem_image_of_mem f Set.self_mem_Iic) <| sSup_le fun _ hb ↦ hb ?_    simp only [upperBounds, Set.mem_image, Set.mem_Iic, forall_exists_index, and_imp,      forall_apply_eq_imp_iff₂, Set.mem_setOf_eq, OrderEmbedding.le_iff_le, imp_self, implies_true]