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

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