awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
ι : Sort u_2
r : ℕ
f : ι → Set (Finset α)
⊢ (∀ ⦃x : Finset α⦄ (x_1 : ι) (h : x ∈ f x_1), #x = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → #x = r

Tactic:
exact forall_comm

Premises used: forall_comm
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
r : ℕ
f : (i : ι) → κ i → Set (Finset α)
⊢ Sized.{u_1} (α := α) r (⋃ (i : ι), ⋃ (j : κ i), f i j) ↔ ∀ (i : ι) (j : κ i), Sized r (f i j)

Tactic:
simp only [Set.sized_iUnion]

Premises used: Set.sized_iUnion
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
A : Set (Finset α)
r : ℕ
hA : Sized r A
⊢ IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) A

Tactic:
fun _s hs _t ht h hst => h <| Finset.eq_of_subset_of_card_le hst ((hA ht).trans (hA hs).symm).le

Premises used: Eq.le, Set.Pairwise, IsAntichain, Finset.eq_of_subset_of_card_le, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
A : Set (Finset α)
hA : Sized 0 A
⊢ A.Subsingleton

Tactic:
subsingleton_of_forall_eq ∅ fun _s hs => card_eq_zero.1 <| hA hs

Premises used: Set.subsingleton_of_forall_eq, Finset.card_eq_zero, Iff.mp, EmptyCollection.emptyCollection
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
A : Set (Finset α)
inst : Fintype α
hA : Sized (Fintype.card α) A
⊢ A.Subsingleton

Tactic:
subsingleton_of_forall_eq Finset.univ fun s hs => s.card_eq_iff_eq_univ.1 <| hA hs

Premises used: Finset.univ, Finset.card_eq_iff_eq_univ, Set.subsingleton_of_forall_eq, Iff.mp
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
A : Set (Finset α)
r : ℕ
hA : Sized r A
⊢ ∅ ∈ A ↔ A = {∅}

Tactic:
hA.isAntichain.bot_mem_iff

Premises used: Set.Mem, IsAntichain.bot_mem_iff, Set.Sized.isAntichain
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
A : Set (Finset α)
r : ℕ
inst : Fintype α
hA : Sized r A
⊢ Finset.univ ∈ A ↔ A = {Finset.univ}

Tactic:
hA.isAntichain.top_mem_iff

Premises used: Set.Mem, Set.Sized.isAntichain, IsAntichain.top_mem_iff
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
s : Finset α
r : ℕ
⊢ Sized r (↑(powersetCard r s) : Set (Finset α))

Tactic:
fun _t ht => (mem_powersetCard.1 ht).2

Premises used: Set.Sized, Finset.mem_powersetCard, And.right, Iff.mp
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
inst : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
A : Finset α
rw : A ∈ 𝒜 → #A = r ↔ A ∈ (↑𝒜 : Set (Finset α)) → #A = r
rw₁ rw₂ : A ∈ 𝒜 → #A = r ↔ A ∈ 𝒜 → #A = r
⊢ A ∈ 𝒜 → Membership.mem (γ := Finset (Finset α)) (powersetCard r univ) A ↔ A ∈ (↑𝒜 : Set (Finset α)) → #A = r

Tactic:
rw [mem_powersetCard_univ, mem_coe]

Premises used: Finset.mem_powersetCard_univ, Finset.mem_coe
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
inst : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
rw : #𝒜 ≤ card.{u_1} (α := Finset α) (powersetCard r univ)
⊢ #𝒜 ≤ (Fintype.card α).choose r

Tactic:
rw [Fintype.card, ← card_powersetCard]

Premises used: Fintype.card, Finset.card_powersetCard
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
inst : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
⊢ #𝒜 ≤ card.{u_1} (α := Finset α) (powersetCard r univ)

Tactic:
card_le_card (subset_powersetCard_univ_iff.mpr h𝒜)

Premises used: Iff.mpr, Finset.card_le_card, Finset.subset_powersetCard_univ_iff
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
inst : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
⊢ #𝒜 ≤ card.{u_1} (α := Finset α) (powersetCard r univ)

Tactic:
exact card_le_card (subset_powersetCard_univ_iff.mpr h𝒜)

Premises used: Iff.mpr, Finset.card_le_card, Finset.subset_powersetCard_univ_iff
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
𝒜 : Finset (Finset α)
A : Finset α
r : ℕ
⊢ A ∈ 𝒜 # r ↔ A ∈ 𝒜 ∧ #A = r

Tactic:
mem_filter

Premises used: Set.Mem, setOf, Finset.mem_filter
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
𝒜 : Finset (Finset α)
r : ℕ
⊢ 𝒜 # r ⊆ 𝒜

Tactic:
filter_subset _ _

Premises used: Set.Mem, setOf, Finset.filter_subset
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
𝒜 : Finset (Finset α)
r : ℕ
⊢ Set.Sized r (↑(𝒜 # r) : Set (Finset α))

Tactic:
fun _ => And.right ∘ mem_slice.mp

Premises used: Set.Sized, Function.comp, And.right, Iff.mp, Finset.mem_slice
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
𝒜 : Finset (Finset α)
A : Finset α
r₁ r₂ : ℕ
h₁ : A ∈ 𝒜 # r₁
h₂ : A ∈ 𝒜 # r₂
⊢ r₁ = r₂

Tactic:
(sized_slice h₁).symm.trans <| sized_slice h₂

Premises used: Finset.sized_slice, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
𝒜 : Finset (Finset α)
A₁ A₂ : Finset α
r₁ r₂ : ℕ
h₁ : A₁ ∈ 𝒜 # r₁
h₂ : A₂ ∈ 𝒜 # r₂
⊢ r₁ ≠ r₂ → A₁ ≠ A₂

Tactic:
mt fun h => (sized_slice h₁).symm.trans ((congr_arg card h).trans (sized_slice h₂))

Premises used: Finset.sized_slice, mt, congr_arg, Finset.card, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
𝒜 : Finset (Finset α)
⊢ Set.PairwiseDisjoint Set.univ 𝒜.slice

Tactic:
fun _ _ _ _ hmn =>
  disjoint_filter.2 fun _s _hs hm hn => hmn <| hm.symm.trans hn

Premises used: Iff.mpr, Finset.slice, Set.PairwiseDisjoint, Finset.disjoint_filter, Set.Pairwise, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
𝒜 : Finset (Finset α)
inst : Fintype α
inst_1 : DecidableEq α
⊢ (Iic (Fintype.card α)).biUnion 𝒜.slice = 𝒜

Tactic:
Subset.antisymm (biUnion_subset.2 fun _r _ => slice_subset) fun s hs =>
    mem_biUnion.2 ⟨#s, mem_Iic.2 <| s.card_le_univ, mem_slice.2 <| ⟨hs, rfl⟩⟩

Premises used: Iff.mpr, Finset.slice_subset, Finset.mem_Iic, Finset.card_le_univ, And.intro, Exists.intro, Finset.card, Finset.biUnion_subset, Finset.mem_slice, Finset.Subset.antisymm, Finset.mem_biUnion, rfl
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
𝒜 : Finset (Finset α)
inst : Fintype α
this : DecidableEq α := Classical.decEq α
rw : (↑(Iic (Fintype.card α)) : Set ℕ).PairwiseDisjoint 𝒜.slice
⊢ ∑ r ∈ Iic (Fintype.card α), #(𝒜 # r) = #𝒜

Tactic:
rw [← card_biUnion, biUnion_slice]

Premises used: Finset.biUnion_slice, Finset.card_biUnion
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
𝒜 : Finset (Finset α)
inst : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ (↑(Iic (Fintype.card α)) : Set ℕ).PairwiseDisjoint 𝒜.slice

Tactic:
Finset.pairwiseDisjoint_slice.subset (Set.subset_univ _)

Premises used: Set.subset_univ, Set.PairwiseDisjoint.subset, Finset.pairwiseDisjoint_slice
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
𝒜 : Finset (Finset α)
inst : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ (↑(Iic (Fintype.card α)) : Set ℕ).PairwiseDisjoint 𝒜.slice

Tactic:
exact Finset.pairwiseDisjoint_slice.subset (Set.subset_univ _)

Premises used: Set.subset_univ, Set.PairwiseDisjoint.subset, Finset.pairwiseDisjoint_slice
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ s.val.sort r = s.sort r

Tactic:
rfl

Premises used: Finset.sort, rfl
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ List.Pairwise r (s.sort r)

Tactic:
Multiset.pairwise_sort _ _

Premises used: Multiset.pairwise_sort, Finset.sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ (↑(s.sort r) : Multiset α) = s.val

Tactic:
Multiset.sort_eq _ _

Premises used: Multiset.sort_eq, Finset.sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
rw : s.val.Nodup
⊢ (↑(s.sort r) : Multiset α).Nodup

Tactic:
rw [sort_eq]

Premises used: Finset.sort_eq
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ s.val.Nodup

Tactic:
s.2

Premises used: Finset.nodup
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ s.val.Nodup

Tactic:
exact s.2

Premises used: Finset.nodup
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
inst_4 : DecidableEq α
⊢ (s.sort r).toFinset = s

Tactic:
List.toFinset_eq (s.sort_nodup r) ▸ eq_of_veq (s.sort_eq r)

Premises used: Finset.eq_of_veq, Finset.sort_eq, Eq.rec, Finset.sort_nodup, List.toFinset_eq
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ sort ∅ r = []

Tactic:
Multiset.sort_zero r

Premises used: Multiset.sort_zero, Finset.sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
a : α
⊢ sort {a} r = [a]

Tactic:
Multiset.sort_singleton a r

Premises used: Multiset.sort_singleton, Finset.sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
r' : β → β → Prop
inst_4 : DecidableRel r'
inst_5 : IsTrans β r'
inst_6 : Std.Antisymm r'
inst_7 : Std.Total r'
hs : ∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' ((f : (a : α) → β) a) ((f : (a : α) → β) b)
⊢ List.map (⇑f : (a : α) → β) (s.sort r) = (map f s).sort r'

Tactic:
Multiset.map_sort _ _ _ _ hs

Premises used: Multiset.map_sort, Multiset.map, Finset.sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
inst : LinearOrder α
inst_1 : LinearOrder β
hf : StrictMonoOn.{u_1, u_2} (β := β) (⇑f : (a : α) → β) (↑s : Set α)
⊢ List.map (⇑f : (a : α) → β) (s.sort fun (a b : α) ↦ a ≤ b) = (map f s).sort fun (a b : β) ↦ a ≤ b

Tactic:
Finset.map_sort _ _ _ _ fun _a ha _b hb => (hf.le_iff_le ha hb).symm

Premises used: StrictMonoOn.le_iff_le, Finset.map_sort, Iff.symm
-- Module: Mathlib.Data.Finset.Sort
Goal:
n : ℕ
⊢ ((range n).sort fun (a b : ℕ) ↦ a ≤ b) = List.range n

Tactic:
Multiset.sort_range n

Premises used: Multiset.ofList, Multiset.range, Finset.sort, Multiset.sort_range
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
rw : (↑(s.sort r) : Multiset α) = (↑s.toList : Multiset α)
⊢ s.sort r ~ s.toList

Tactic:
rw [← Multiset.coe_eq_coe]

Premises used: Multiset.coe_eq_coe
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ (↑(s.sort r) : Multiset α) = (↑s.toList : Multiset α)

Tactic:
simp only [coe_toList, sort_eq]

Premises used: Finset.sort_eq, Finset.coe_toList
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
inst_4 : DecidableEq α
l : List α
hl : l.Nodup
⊢ l.toFinset.sort r = l ↔ List.Pairwise r l

Tactic:
⟨?_, ((sort_perm_toList _ r).trans (List.toFinset_toList hl)).eq_of_pairwise'
    (pairwise_sort _ _)⟩

Premises used: Finset.pairwise_sort, List.toFinset_toList, List.Perm.eq_of_pairwise', List.toFinset, List.Perm.trans, Iff.intro, Finset.sort_perm_toList
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
inst_4 : DecidableEq α
l : List α
hl : l.Nodup
refine : l.toFinset.sort r = l → List.Pairwise r l
⊢ l.toFinset.sort r = l ↔ List.Pairwise r l

Tactic:
refine ⟨?_, ((sort_perm_toList _ r).trans (List.toFinset_toList hl)).eq_of_pairwise'
    (pairwise_sort _ _)⟩
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
inst_4 : DecidableEq α
l : List α
hl : l.Nodup
h : l.toFinset.sort r = l
rw : List.Pairwise r (l.toFinset.sort r)
⊢ List.Pairwise r l

Tactic:
rw [← h]
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
inst_4 : DecidableEq α
l : List α
hl : l.Nodup
h : l.toFinset.sort r = l
⊢ List.Pairwise r (l.toFinset.sort r)

Tactic:
pairwise_sort _ r

Premises used: Finset.pairwise_sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
inst_4 : DecidableEq α
l : List α
hl : l.Nodup
h : l.toFinset.sort r = l
⊢ List.Pairwise r (l.toFinset.sort r)

Tactic:
exact pairwise_sort _ r

Premises used: Finset.pairwise_sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
m : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
h : m.Nodup
⊢ { val := m, nodup := h : Finset α }.sort r = m.sort r

Tactic:
rfl

Premises used: Finset.sort, rfl
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
a : α
⊢ a ∈ s.sort r ↔ a ∈ s

Tactic:
Multiset.mem_sort _

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.mem_sort, Finset.sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ (s.sort r).length = #s

Tactic:
Multiset.length_sort _

Premises used: Multiset.length_sort, Finset.card, Finset.sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
rw : (cons a s h₂).val.sort r = a :: s.sort r
rw₁ : (a ::ₘ s.val).sort r = a :: s.sort r
rw₂ : a :: s.val.sort r = a :: s.sort r
rw₃ rw₄ : a :: s.sort r = a :: s.sort r
⊢ (cons a s h₂).sort r = a :: s.sort r

Tactic:
rw [sort, cons_val, Multiset.sort_cons a _ r h₁, sort_val]

Premises used: Multiset.sort_cons, Finset.cons_val, Finset.sort, Finset.sort_val
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
inst_4 : DecidableEq α
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
rw : (cons a s h₂).sort r = a :: s.sort r
rw₁ rw₂ : a :: s.sort r = a :: s.sort r
⊢ (insert a s).sort r = a :: s.sort r

Tactic:
rw [← cons_eq_insert _ _ h₂, sort_cons r h₁]

Premises used: Finset.sort_cons, Finset.cons_eq_insert
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
⊢ (s.sort fun (a b : α) ↦ a ≤ b).SortedLT

Tactic:
(pairwise_sort _ _).sortedLE.sortedLT_of_nodup (sort_nodup _ _)

Premises used: Finset.pairwise_sort, Finset.sort_nodup, List.Pairwise.sortedLE, List.SortedLE.sortedLT_of_nodup
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
⊢ (s.sort fun (x1 x2 : α) ↦ x1 ≥ x2).SortedGT

Tactic:
(pairwise_sort _ _).sortedGE.sortedGT_of_nodup (sort_nodup _ _)

Premises used: List.Pairwise.sortedGE, Finset.pairwise_sort, Finset.sort_nodup, List.SortedGE.sortedGT_of_nodup
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
a : (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ s.min' H
a₁ : s.min' H ≤ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length)
⊢ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) = s.min' H

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
⊢ s.min' H ∈ l

Tactic:
have : s.min' H ∈ l := (s.mem_sort (· ≤ ·)).mpr (s.min'_mem H)
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
this : s.min' H ∈ l
⊢ ∃ (i : Fin l.length), l.get i = s.min' H

Tactic:
List.mem_iff_get.1 this

Premises used: List.mem_iff_get, Iff.mp
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
this : s.min' H ∈ l
a :
  ∀ (i : Fin l.length) (hi : l.get i = s.min' H),
    (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ s.min' H
⊢ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ s.min' H

Tactic:
obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this

Premises used: Finset.min', List.mem_iff_get, Iff.mp
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
this : s.min' H ∈ l
i : Fin l.length
hi : l.get i = s.min' H
a : (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ l.get i
⊢ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ s.min' H

Tactic:
rw [← hi]
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
this : s.min' H ∈ l
i : Fin l.length
hi : l.get i = s.min' H
⊢ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ l.get i

Tactic:
(s.pairwise_sort (· ≤ ·)).rel_get_of_le (Nat.zero_le i)

Premises used: Nat.zero_le, Finset.pairwise_sort, LE.le, Fin.val, List.Pairwise.rel_get_of_le
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
this : s.min' H ∈ l
i : Fin l.length
hi : l.get i = s.min' H
⊢ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ l.get i

Tactic:
exact (s.pairwise_sort (· ≤ ·)).rel_get_of_le (Nat.zero_le i)

Premises used: Finset.pairwise_sort, LE.le, List.Pairwise.rel_get_of_le
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
⊢ l.get (⟨0, h⟩ : Fin l.length) ∈ s

Tactic:
have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l _)
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
this : l.get (⟨0, h⟩ : Fin l.length) ∈ s
⊢ s.min' H ≤ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length)

Tactic:
s.min'_le _ this

Premises used: Finset.min'_le
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
this : l.get (⟨0, h⟩ : Fin l.length) ∈ s
⊢ s.min' H ≤ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length)

Tactic:
exact s.min'_le _ this

Premises used: Finset.min'_le
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : 0 < #s), 0 < #s
⊢ 0 < #s

Tactic:
rwa [length_sort] at h

Premises used: Finset.length_sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.sort fun (a b : α) ↦ a ≤ b) 0 h = s.min' ⋯

Tactic:
sorted_zero_eq_min'_aux _ _ _

Premises used: Finset.sorted_zero_eq_min'_aux
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
s : Finset α
h : s.Nonempty
rw : 0 < #s
⊢ 0 < (s.sort fun (a b : α) ↦ a ≤ b).length

Tactic:
rw [length_sort]

Premises used: Finset.length_sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ 0 < #s

Tactic:
card_pos.2 h

Premises used: Iff.mpr, Finset.card_pos
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ 0 < #s

Tactic:
exact card_pos.2 h

Premises used: Iff.mpr, Finset.card_pos
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ s.min' h = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.sort fun (a b : α) ↦ a ≤ b) 0 ⋯

Tactic:
(sorted_zero_eq_min'_aux _ _ _).symm

Premises used: Finset.sorted_zero_eq_min'_aux, Eq.symm
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : (s.sort fun (a b : α) ↦ a ≤ b).length - 1 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
a :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.sort fun (a b : α) ↦ a ≤ b)
      ((s.sort fun (a b : α) ↦ a ≤ b).length - 1) h ≤
    s.max' H
a₁ :
  s.max' H ≤
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.sort fun (a b : α) ↦ a ≤ b)
      ((s.sort fun (a b : α) ↦ a ≤ b).length - 1) h
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.sort fun (a b : α) ↦ a ≤ b)
      ((s.sort fun (a b : α) ↦ a ≤ b).length - 1) h =
    s.max' H

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : (s.sort fun (a b : α) ↦ a ≤ b).length - 1 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
⊢ l.get (⟨(s.sort fun (a b : α) ↦ a ≤ b).length - 1, h⟩ : Fin l.length) ∈ s

Tactic:
have : l.get ⟨s.sort.length - 1, h⟩ ∈ s :=
      (s.mem_sort (· ≤ ·)).1 (List.get_mem l _)
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : (s.sort fun (a b : α) ↦ a ≤ b).length - 1 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
this : l.get (⟨(s.sort fun (a b : α) ↦ a ≤ b).length - 1, h⟩ : Fin l.length) ∈ s
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.sort fun (a b : α) ↦ a ≤ b)
      ((s.sort fun (a b : α) ↦ a ≤ b).length - 1) h ≤
    s.max' H

Tactic:
s.le_max' _ this

Premises used: Finset.le_max'
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : (s.sort fun (a b : α) ↦ a ≤ b).length - 1 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
this : l.get (⟨(s.sort fun (a b : α) ↦ a ≤ b).length - 1, h⟩ : Fin l.length) ∈ s
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.sort fun (a b : α) ↦ a ≤ b)
      ((s.sort fun (a b : α) ↦ a ≤ b).length - 1) h ≤
    s.max' H

Tactic:
exact s.le_max' _ this

Premises used: Finset.le_max'
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : (s.sort fun (a b : α) ↦ a ≤ b).length - 1 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
⊢ s.max' H ∈ l

Tactic:
have : s.max' H ∈ l := (s.mem_sort (· ≤ ·)).mpr (s.max'_mem H)