Theorem: Set.mem_toSubset' (Sard/ToSubset.lean)

State before:
X : Type u_1
s t : Set X
h : s ≤ t
x : ↑t
⊢ x ∈ s.toSubset' t h ↔ ↑x ∈ s
Tactic:
rw [toSubset', Set.range_inclusion, Set.mem_setOf_eq]
State after:
no goals