case a
α : Type u_1
β : Type ?u.15918
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < 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) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h ≤ max' s H

case a
α : Type u_1
β : Type ?u.15918
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < 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
⊢ max' s H ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h
α : Type u_1
β : Type ?u.15918
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < 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) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h = max' s H
apply le_antisymm
no goals
case a
α : Type u_1
β : Type ?u.15918
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < 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 := List.length (sort (fun x x_1 => x ≤ x_1) s) - 1, isLt := h } ∈ s
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h ≤ max' s H
exact s.le_max' _ this
case a.intro
α : Type u_1
β : Type ?u.15918
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < 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 : max' s H ∈ l
i : Fin (List.length l)
hi : List.get l i = max' s H
⊢ max' s H ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h
case a
α : Type u_1
β : Type ?u.15918
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < 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 : max' s H ∈ l
⊢ max' s H ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h
obtain ⟨i, hi⟩ : ∃ i, l.get i = s.max' H := List.mem_iff_get.1 this
case a.intro
α : Type u_1
β : Type ?u.15918
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < 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 : max' s H ∈ l
i : Fin (List.length l)
hi : List.get l i = max' s H
⊢ List.get l i ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h
case a.intro
α : Type u_1
β : Type ?u.15918
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < 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 : max' s H ∈ l
i : Fin (List.length l)
hi : List.get l i = max' s H
⊢ max' s H ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h
rw [← hi]