Set.subtype_mk_minimal_iff

lemma subtype_mk_minimal_iff (α : Type*) [Preorder α]    (s : Set α) (t : Set s) (x : α) (hx : x ∈ s) :    Minimal (· ∈ t) (⟨x, hx⟩ : s) ↔ Minimal (fun y ↦ ∃ h, y ∈ s ∧ ⟨y, h⟩ ∈ t) x := by  wlog hxt : (⟨x, hx⟩ : s) ∈ t  · have : ¬Minimal (· ∈ t) (⟨x, hx⟩ : s) := by contrapose! hxt; exact hxt.prop    simp_rw [this, false_iff, exists_and_left]; clear this; contrapose! hxt    have : x ∈ {y | y ∈ s ∧ ∃ (x : y ∈ s), ⟨y, x⟩ ∈ t} := hxt.prop    simp_all  simp +contextual [← OrderEmbedding.minimal_mem_image_iff    (f := ⟨Function.Embedding.subtype (· ∈ s), by simp⟩) hxt]