Theorem: Set.mem_subtypeOrderEmbedding_iff (Matroid/ForMathlib/SetSubtype.lean)

State before:
α : Type u_1
β : Type u_2
s✝ t r✝ s : Set α
x : α
r : Set ↑s
⊢ x ∈ s.subtypeOrderEmbedding r ↔ ∃ (hx : x ∈ s), ⟨x, hx⟩ ∈ r
Tactic:
simp [Set.subtypeOrderEmbedding]
State after:
no goals