theorem
Array.unique.mem_of_mem_unqiue
{α : Type u_1}
{a : α}
[DecidableEq α]
[LE α]
(as : Array α)
:
@[simp]
@[simp]
theorem
Array.nodup_unique
{α : Type u_1}
[DecidableEq α]
[LE α]
[LT α]
[Std.IsPreorder α]
[Std.LawfulOrderLT α]
[Std.Antisymm fun (x1 x2 : α) => x1 ≤ x2]
(as : Array α)
(h : List.Pairwise LE.le as.toList)
: