Theorem: PartialEquiv.ofSetEquiv_apply_mem (Matroid/ForMathlib/PartialEquiv.lean)

State before:
α : Type u_1
β : Type u_2
inst✝³ : Nonempty α
inst✝² : Nonempty β
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
⊢ ↑(PartialEquiv.ofSetEquiv e) x = ↑(e ⟨x, hx⟩)
Tactic:
simp [hx]
State after:
no goals