[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ Nodup ↑(sort r s)
[PROOFSTEP]
rw [sort_eq]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ Nodup s.val
[PROOFSTEP]
exact s.2
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ sort r s ~ toList s
[PROOFSTEP]
rw [← Multiset.coe_eq_coe]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ ↑(sort r s) = ↑(toList s)
[PROOFSTEP]
simp only [coe_toList, sort_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h = min' s H
[PROOFSTEP]
let l := s.sort (· ≤ ·)
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have : s.min' H ∈ l := (Finset.mem_sort (α := α) (· ≤ ·)).mpr (s.min'_mem H)
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this
[GOAL]
case a.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [← hi]
[GOAL]
case a.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact (s.sort_sorted (· ≤ ·)).rel_nthLe_of_le _ _ (Nat.zero_le i)
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l 0 h)
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact s.min'_le _ this
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
⊢ 0 < card s
[PROOFSTEP]
rwa [length_sort] at h 
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : Finset.Nonempty s
⊢ 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
[PROOFSTEP]
rw [length_sort]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : Finset.Nonempty s
⊢ 0 < card s
[PROOFSTEP]
exact card_pos.2 h
[GOAL]
α : Type u_1
β : Type u_2
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
⊢ 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
[PROOFSTEP]
let l := s.sort (· ≤ ·)
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have : l.get ⟨(s.sort (· ≤ ·)).length - 1, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l _ h)
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact s.le_max' _ this
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have : s.max' H ∈ l := (Finset.mem_sort (α := α) (· ≤ ·)).mpr (s.max'_mem H)
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
obtain ⟨i, hi⟩ : ∃ i, l.get i = s.max' H := List.mem_iff_get.1 this
[GOAL]
case a.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [← hi]
[GOAL]
case a.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact (s.sort_sorted (· ≤ ·)).rel_nthLe_of_le _ _ (Nat.le_pred_of_lt i.prop)
[GOAL]
α : Type u_1
β : Type u_2
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)
⊢ Finset.Nonempty s
[PROOFSTEP]
rw [length_sort] at h 
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : card s - 1 < card s
⊢ Finset.Nonempty s
[PROOFSTEP]
exact card_pos.1 (lt_of_le_of_lt bot_le h)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : Finset.Nonempty s
⊢ List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
[PROOFSTEP]
simpa using Nat.sub_lt (card_pos.mpr h) zero_lt_one
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
i : Fin k
⊢ ↑i < List.length (sort (fun x x_1 => x ≤ x_1) s)
[PROOFSTEP]
rw [length_sort, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
i : Fin k
⊢ ↑i < k
[PROOFSTEP]
exact i.2
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
⊢ Set.range ↑(orderEmbOfFin s h) = ↑s
[PROOFSTEP]
simp only [orderEmbOfFin, Set.range_comp ((↑) : _ → α) (s.orderIsoOfFin h), RelEmbedding.coe_trans, Set.image_univ,
  Finset.orderEmbOfFin, RelIso.range_eq, OrderEmbedding.subtype_apply, OrderIso.coe_toOrderEmbedding, eq_self_iff_true,
  Subtype.range_coe_subtype, Finset.setOf_mem, Finset.coe_inj]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
hz : 0 < k
⊢ ↑(orderEmbOfFin s h) { val := 0, isLt := hz } = min' s (_ : Finset.Nonempty s)
[PROOFSTEP]
simp only [orderEmbOfFin_apply, Fin.val_mk, sorted_zero_eq_min']
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
hz : 0 < k
⊢ ↑(orderEmbOfFin s h) { val := k - 1, isLt := (_ : k - 1 < k) } = max' s (_ : Finset.Nonempty s)
[PROOFSTEP]
simp [orderEmbOfFin_apply, max'_eq_sorted_last, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a : α
i : Fin 1
⊢ ↑(orderEmbOfFin {a} (_ : card {a} = 1)) i = a
[PROOFSTEP]
rw [Subsingleton.elim i ⟨0, zero_lt_one⟩, orderEmbOfFin_zero _ zero_lt_one, min'_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ f = ↑(orderEmbOfFin s h)
[PROOFSTEP]
apply Fin.strictMono_unique hmono (s.orderEmbOfFin h).strictMono
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ Set.range f = Set.range ↑(orderEmbOfFin s h)
[PROOFSTEP]
rw [range_orderEmbOfFin, ← Set.image_univ, ← coe_univ, ← coe_image, coe_inj]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ image f univ = s
[PROOFSTEP]
refine' eq_of_subset_of_card_le (fun x hx => _) _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : α
hx : x ∈ image f univ
⊢ x ∈ s
[PROOFSTEP]
rcases mem_image.1 hx with ⟨x, _, rfl⟩
[GOAL]
case refine'_1.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : Fin k
left✝ : x ∈ univ
hx : f x ∈ image f univ
⊢ f x ∈ s
[PROOFSTEP]
exact hfs x
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ card s ≤ card (image f univ)
[PROOFSTEP]
rw [h, card_image_of_injective _ hmono.injective, card_univ, Fintype.card_fin]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
k l : ℕ
s : Finset α
i : Fin k
j : Fin l
h : card s = k
h' : card s = l
⊢ ↑(orderEmbOfFin s h) i = ↑(orderEmbOfFin s h') j ↔ ↑i = ↑j
[PROOFSTEP]
substs k l
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
i j : Fin (card s)
⊢ ↑(orderEmbOfFin s (_ : card s = card s)) i = ↑(orderEmbOfFin s (_ : card s = card s)) j ↔ ↑i = ↑j
[PROOFSTEP]
exact (s.orderEmbOfFin rfl).eq_iff_eq.trans Fin.ext_iff
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : k ≤ card s
a : Fin k
⊢ ↑(orderEmbOfCardLe s h) a ∈ s
[PROOFSTEP]
simp only [orderEmbOfCardLe, RelEmbedding.coe_trans, Finset.orderEmbOfFin_mem, Function.comp_apply]
