Theorem: List.Sorted.toFinset_sort (RMT4/to_mathlib.lean)

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
α : Type u_4
inst✝ : LinearOrder α
l l1 l2 : List α
s : Finset α
hl : Sorted (fun x x_1 => x < x_1) l
⊢ ∀ (x : α), x ∈ Finset.sort (fun x x_1 => x ≤ x_1) (toFinset l) ↔ x ∈ l
Tactic:
simp
State after:
no goals