case a
α : Type u_1
β : Type ?u.7886
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h ≤ min' s H

case a
α : Type u_1
β : Type ?u.7886
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
⊢ min' s H ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h
α : Type u_1
β : Type ?u.7886
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h = min' s H
apply le_antisymm
case a.intro
α : Type u_1
β : Type ?u.7886
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : min' s H ∈ l
i : Fin (List.length l)
hi : List.get l i = min' s H
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h ≤ min' s H
case a
α : Type u_1
β : Type ?u.7886
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : min' s H ∈ l
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h ≤ min' s H
obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this
case a.intro
α : Type u_1
β : Type ?u.7886
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : min' s H ∈ l
i : Fin (List.length l)
hi : List.get l i = min' s H
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h ≤ List.get l i
case a.intro
α : Type u_1
β : Type ?u.7886
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : min' s H ∈ l
i : Fin (List.length l)
hi : List.get l i = min' s H
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h ≤ min' s H
rw [← hi]
no goals
case a
α : Type u_1
β : Type ?u.7886
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : List.get l { val := 0, isLt := h } ∈ s
⊢ min' s H ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h
exact s.min'_le _ this