awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : s.max' H ∈ l
⊢ ∃ (i : Fin l.length), l.get i = s.max' 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 : (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 : s.max' H ∈ l
a :
  ∀ (i : Fin l.length) (hi : l.get i = s.max' H),
    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
⊢ 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

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

Premises used: List.mem_iff_get, Finset.max', Iff.mp
-- 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 : s.max' H ∈ l
i : Fin l.length
hi : l.get i = s.max' H
a :
  l.get i ≤
    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 ≤
    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

Tactic:
rw [← hi]
-- 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 : s.max' H ∈ l
i : Fin l.length
hi : l.get i = s.max' H
⊢ l.get i ≤
    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

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

Premises used: Fin.prop, Finset.pairwise_sort, LE.le, Nat.le_sub_one_of_lt, List.Pairwise.rel_get_of_le
-- 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 : s.max' H ∈ l
i : Fin l.length
hi : l.get i = s.max' H
⊢ l.get i ≤
    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

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

Premises used: Finset.pairwise_sort, LE.le, List.Pairwise.rel_get_of_le
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
s : Finset α
h : (s.sort fun (a b : α) ↦ a ≤ b).length - 1 < (s.sort fun (a b : α) ↦ a ≤ b).length
⊢ #s - 1 < #s

Tactic:
rw [length_sort] at h

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

Tactic:
card_pos.1 (lt_of_le_of_lt bot_le h)

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

Tactic:
exact card_pos.1 (lt_of_le_of_lt bot_le h)

Premises used: lt_of_le_of_lt, Iff.mp, Finset.card_pos, bot_le
-- 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
⊢ 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' ⋯

Tactic:
sorted_last_eq_max'_aux _ h _

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

Tactic:
simpa using Nat.sub_lt (card_pos.mpr h) Nat.zero_lt_one

Premises used: Iff.mpr, Nat.sub_lt, Finset.card_pos, Nat.zero_lt_one
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ (s.sort fun (a b : α) ↦ a ≤ b).length - 1 < (s.sort fun (a b : α) ↦ a ≤ b).length

Tactic:
simpa using Nat.sub_lt (card_pos.mpr h) Nat.zero_lt_one

Premises used: Iff.mpr, Nat.sub_lt, Finset.card_pos, Nat.zero_lt_one
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ {x : α | x ∈ s.sort fun (x1 x2 : α) ↦ x1 ≤ x2} = (↑s : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ Eq (α := α) ((↑((s.orderIsoOfFin h : (a : Fin k) → ↥s) i) : α) : α) ((s.orderEmbOfFin h : (a : Fin k) → α) i : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
x : ↥s
⊢ (↑(((OrderIso.symm (s.orderIsoOfFin h) : ↥s ≃o Fin k) : (a : ↥s) → Fin k) x) : ℕ) =
    List.idxOf (↑x : α) (s.sort fun (a b : α) ↦ a ≤ b)

Tactic:
rfl

Premises used: Set.Mem, setOf, Multiset.Mem, List.idxOf, rfl
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
rw : (↑i : ℕ) < k
⊢ (↑i : ℕ) < (s.sort fun (a b : α) ↦ a ≤ b).length

Tactic:
rw [length_sort, h]

Premises used: Finset.length_sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ (↑i : ℕ) < k

Tactic:
i.2

Premises used: Fin.isLt
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ (↑i : ℕ) < k

Tactic:
exact i.2

Premises used: Fin.isLt
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ (s.orderEmbOfFin h : (a : Fin k) → α) i =
    getElem (valid := fun (xs : List α) (i : Fin k) ↦ (↑i : ℕ) < xs.length) (s.sort fun (a b : α) ↦ a ≤ b) i ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ Membership.mem (α := α) s ((s.orderEmbOfFin h : (a : Fin k) → α) i : α)

Tactic:
(s.orderIsoOfFin h i).2

Premises used: Finset.orderIsoOfFin, Set.Mem, setOf, DFunLike.coe, Subtype.property
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ Set.range (ι := Fin k) (⇑(s.orderEmbOfFin h) : (a : Fin k) → α) = (↑s : Set α)

Tactic:
simp only [orderEmbOfFin, Set.range_comp ((↑) : _ → α) (s.orderIsoOfFin h),
  RelEmbedding.coe_trans, Set.image_univ, Finset.orderEmbOfFin, RelIso.range_eq,
    OrderEmbedding.coe_subtype, OrderIso.coe_toOrderEmbedding,
    Subtype.range_coe_subtype, Finset.setOf_mem]

Premises used: Set.range_comp, Set.image_univ, Finset.orderIsoOfFin, Finset.orderEmbOfFin, OrderIso.coe_toOrderEmbedding, Finset.setOf_mem, Subtype.range_coe_subtype, RelEmbedding.coe_trans, OrderEmbedding.coe_subtype, RelIso.range_eq, DFunLike.coe
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
a : (↑(image (α := Fin k) (⇑(s.orderEmbOfFin h) : (a : Fin k) → α) univ) : Set α) = (↑s : Set α)
⊢ image (α := Fin k) (⇑(s.orderEmbOfFin h) : (a : Fin k) → α) univ = s

Tactic:
apply Finset.coe_injective

Premises used: Finset.coe_injective
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ (↑(image (α := Fin k) (⇑(s.orderEmbOfFin h) : (a : Fin k) → α) univ) : Set α) = (↑s : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ map
      (RelEmbedding.toEmbedding (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2)
        (s.orderEmbOfFin h))
      univ =
    s

Tactic:
simp [map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ k = (s.sort fun (a b : α) ↦ a ≤ b).length

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
obtain :
  ∀ (h : #s = (s.sort fun (a b : α) ↦ a ≤ b).length),
    List.map (α := Fin (s.sort fun (a b : α) ↦ a ≤ b).length)
        (⇑(s.orderEmbOfFin h) : (a : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) → α)
        (List.finRange (s.sort fun (a b : α) ↦ a ≤ b).length) =
      s.sort fun (a b : α) ↦ a ≤ b
⊢ List.map (⇑(s.orderEmbOfFin h) : (a : Fin k) → α) (List.finRange k) = s.sort fun (a b : α) ↦ a ≤ b

Tactic:
obtain rfl : k = s.sort.length := by simp [h]

Premises used: Finset.sort, List.length, rfl
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : #s = (s.sort fun (a b : α) ↦ a ≤ b).length
⊢ List.map (α := Fin (s.sort fun (a b : α) ↦ a ≤ b).length)
      (⇑(s.orderEmbOfFin h) : (a : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) → α)
      (List.finRange (s.sort fun (a b : α) ↦ a ≤ b).length) =
    s.sort fun (a b : α) ↦ a ≤ b

Tactic:
List.map_getElem_finRange s.sort

Premises used: List.map_getElem_finRange, Finset.sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : #s = (s.sort fun (a b : α) ↦ a ≤ b).length
⊢ List.map (α := Fin (s.sort fun (a b : α) ↦ a ≤ b).length)
      (⇑(s.orderEmbOfFin h) : (a : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) → α)
      (List.finRange (s.sort fun (a b : α) ↦ a ≤ b).length) =
    s.sort fun (a b : α) ↦ a ≤ b

Tactic:
exact List.map_getElem_finRange s.sort

Premises used: List.map_getElem_finRange, Finset.sort
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
hz : 0 < k
⊢ (s.orderEmbOfFin h : (a : Fin k) → α) (⟨0, hz⟩ : Fin k) = s.min' ⋯

Tactic:
simp only [orderEmbOfFin_apply, Fin.getElem_fin, sorted_zero_eq_min']

Premises used: Finset.sorted_zero_eq_min', Finset.orderEmbOfFin_apply, Fin.getElem_fin
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
hz : 0 < k
⊢ (s.orderEmbOfFin h : (a : Fin k) → α) (⟨k - 1, ⋯⟩ : Fin k) = s.max' ⋯

Tactic:
simp [orderEmbOfFin_apply, max'_eq_sorted_last, h]

Premises used: Finset.max'_eq_sorted_last, Finset.orderEmbOfFin_apply
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
a : α
i : Fin 1
rw : (orderEmbOfFin {a} ⋯ : (a : Fin 1) → α) (⟨0, Nat.zero_lt_one⟩ : Fin 1) = a
rw₁ : min' {a} ⋯ = a
rw₂ rw₃ : a = a
⊢ (orderEmbOfFin {a} ⋯ : (a : Fin 1) → α) i = a

Tactic:
rw [Subsingleton.elim i ⟨0, Nat.zero_lt_one⟩, orderEmbOfFin_zero _ Nat.zero_lt_one,
    min'_singleton]

Premises used: Fin.mk, Finset.orderEmbOfFin_zero, Finset.min'_singleton, Subsingleton.elim, OfNat.ofNat, Nat.zero_lt_one
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
rw : image f univ = s
⊢ f = (⇑(s.orderEmbOfFin h) : (a : Fin k) → α)

Tactic:
rw [← hmono.range_inj (s.orderEmbOfFin h).strictMono, range_orderEmbOfFin, ← Set.image_univ,
    ← coe_univ, ← coe_image, coe_inj]

Premises used: Set.image_univ, Finset.orderEmbOfFin, Finset.coe_univ, OrderEmbedding.strictMono, Finset.coe_inj, Finset.coe_image, Finset.range_orderEmbOfFin, StrictMono.range_inj
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ image f univ = s

Tactic:
eq_of_subset_of_card_le (fun x hx => ?_) ?_

Premises used: Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
refine_1 : ∀ (x : α) (hx : x ∈ image f univ), x ∈ s
refine_2 : #s ≤ #(image f univ)
⊢ image f univ = s

Tactic:
refine eq_of_subset_of_card_le (fun x hx => ?_) ?_

Premises used: Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : α
hx : x ∈ image f univ
refine_1 : ∀ (x : Fin k), Membership.mem (γ := Finset (Fin k)) univ x → ∀ (hx : f x ∈ image f univ), f x ∈ s
⊢ x ∈ s

Tactic:
rcases mem_image.1 hx with ⟨x, _, rfl⟩

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : Fin k
left : Membership.mem (γ := Finset (Fin k)) univ x
hx : f x ∈ image f univ
⊢ f x ∈ s

Tactic:
hfs x
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : Fin k
left : Membership.mem (γ := Finset (Fin k)) univ x
hx : f x ∈ image f univ
⊢ f x ∈ s

Tactic:
exact hfs x
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
refine_2 : k ≤ #(image f univ)
refine_2₁ : k ≤ card (α := Fin k) univ
refine_2₂ : k ≤ Fintype.card (Fin k)
refine_2₃ refine_2₄ : k ≤ k
⊢ #s ≤ #(image f univ)

Tactic:
rw [h, card_image_of_injective _ hmono.injective, card_univ, Fintype.card_fin]

Premises used: Finset.card_univ, Fintype.card_fin, Finset.card_image_of_injective, StrictMono.injective
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k ↪o α
hfs : ∀ (x : Fin k), Membership.mem (α := α) s ((f : (a : Fin k) → α) x : α)
⊢ f = s.orderEmbOfFin h

Tactic:
RelEmbedding.ext <| funext_iff.1 <| orderEmbOfFin_unique h hfs f.strictMono

Premises used: Finset.orderEmbOfFin_unique, funext_iff, OrderEmbedding.strictMono, RelEmbedding.ext, Iff.mp
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
k l : ℕ
s : Finset α
i : Fin k
j : Fin l
h : #s = k
h' : #s = l
substs :
  ∀ {i j : Fin #s},
    Eq (α := α) ((s.orderEmbOfFin ⋯ : (a : Fin #s) → α) i : α) ((s.orderEmbOfFin ⋯ : (a : Fin #s) → α) j : α) ↔
      (↑i : ℕ) = (↑j : ℕ)
⊢ Eq (α := α) ((s.orderEmbOfFin h : (a : Fin k) → α) i : α) ((s.orderEmbOfFin h' : (a : Fin l) → α) j : α) ↔
    (↑i : ℕ) = (↑j : ℕ)

Tactic:
substs k l
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
i j : Fin #s
⊢ Eq (α := α) ((s.orderEmbOfFin ⋯ : (a : Fin #s) → α) i : α) ((s.orderEmbOfFin ⋯ : (a : Fin #s) → α) j : α) ↔
    (↑i : ℕ) = (↑j : ℕ)

Tactic:
(s.orderEmbOfFin rfl).eq_iff_eq.trans Fin.ext_iff

Premises used: Fin.ext_iff, Finset.orderEmbOfFin, Iff.trans, rfl, OrderEmbedding.eq_iff_eq
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
i j : Fin #s
⊢ Eq (α := α) ((s.orderEmbOfFin ⋯ : (a : Fin #s) → α) i : α) ((s.orderEmbOfFin ⋯ : (a : Fin #s) → α) j : α) ↔
    (↑i : ℕ) = (↑j : ℕ)

Tactic:
exact (s.orderEmbOfFin rfl).eq_iff_eq.trans Fin.ext_iff

Premises used: Fin.ext_iff, Finset.orderEmbOfFin, Iff.trans, rfl, OrderEmbedding.eq_iff_eq
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : k ≤ #s
a : Fin k
⊢ Membership.mem (α := α) s ((s.orderEmbOfCardLe h : (a : Fin k) → α) a : α)

Tactic:
simp only [orderEmbOfCardLe, RelEmbedding.coe_trans, Finset.orderEmbOfFin_mem,
    Function.comp_apply]

Premises used: RelEmbedding.coe_trans, Function.comp_apply, Finset.orderEmbOfCardLe, Finset.orderEmbOfFin_mem
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
⊢ k = n

Tactic:
simp_all [card_compl]

Premises used: Finset.card_compl
-- Module: Mathlib.Data.Finset.Sort
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
a :
  Eq (α := (a : Fin k) → Fin (n + 1))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (orderEmbOfFin {i}ᶜ h))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
        fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb))
⊢ orderEmbOfFin {i}ᶜ h =
    RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
      fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb

Tactic:
apply DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Data.Finset.Sort
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
a :
  Eq (α := (a : Fin k) → Fin (n + 1))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
        fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (orderEmbOfFin {i}ᶜ h))
⊢ Eq (α := (a : Fin k) → Fin (n + 1))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (orderEmbOfFin {i}ᶜ h))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
        fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb))

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Finset.Sort
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
⊢ i.succAbove ∘ Fin.cast ⋯ = (⇑(orderEmbOfFin {i}ᶜ h) : (a : Fin k) → Fin (n + 1))

Tactic:
orderEmbOfFin_unique _ (fun x ↦ ?_) ((Fin.strictMono_succAbove _).comp (Fin.cast_strictMono _))

Premises used: Finset.orderEmbOfFin_unique, Fin.strictMono_succAbove, Fin.cast_strictMono, StrictMono.comp
-- Module: Mathlib.Data.Finset.Sort
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
a : ∀ (x : Fin k), Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ ((i.succAbove ∘ Fin.cast ⋯) x)
a₁ : k = n
⊢ Eq (α := (a : Fin k) → Fin (n + 1))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
        fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (orderEmbOfFin {i}ᶜ h))

Tactic:
convert!
    orderEmbOfFin_unique _ (fun x ↦ ?_) ((Fin.strictMono_succAbove _).comp (Fin.cast_strictMono _))

Premises used: Finset.orderEmbOfFin_unique, Fin.strictMono_succAbove, Fin.cast_strictMono, StrictMono.comp
-- Module: Mathlib.Data.Finset.Sort
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
x : Fin k
⊢ Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ ((i.succAbove ∘ Fin.cast ⋯) x)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sort
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
⊢ k = n

Tactic:
simp [← h, card_compl]

Premises used: Finset.card_compl
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
n : ℕ
i : Fin (n + 1)
⊢ card (α := Fin (n + 1)) {i}ᶜ = n

Tactic:
simp [card_compl]

Premises used: Finset.card_compl
-- Module: Mathlib.Data.Finset.Sort
Goal:
n : ℕ
i : Fin (n + 1)
⊢ orderEmbOfFin {i}ᶜ ⋯ = i.succAboveOrderEmb

Tactic:
orderEmbOfFin_compl_singleton _

Premises used: Fin.succAbove, Fin.succAboveOrderEmb, RelEmbedding.ofMapRelIff, OrderEmbedding.ofStrictMono, Function.Embedding.trans, OrderEmbedding.ofMapLEIff, Finset.orderEmbOfFin_compl_singleton, ite
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
j : Fin k
⊢ card (α := Fin (n + 1)) {i}ᶜ = n

Tactic:
simp [card_compl]

Premises used: Finset.card_compl
-- Module: Mathlib.Data.Finset.Sort
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
j : Fin k
rw :
  (RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
          fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb :
        (a : Fin k) → Fin (n + 1))
      j =
    i.succAbove (Fin.cast ⋯ j)
⊢ (orderEmbOfFin {i}ᶜ h : (a : Fin k) → Fin (n + 1)) j = i.succAbove (Fin.cast ⋯ j)

Tactic:
rw [orderEmbOfFin_compl_singleton]

Premises used: Finset.orderEmbOfFin_compl_singleton
-- Module: Mathlib.Data.Finset.Sort
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
j : Fin k
⊢ (RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
          fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb :
        (a : Fin k) → Fin (n + 1))
      j =
    i.succAbove (Fin.cast ⋯ j)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sort
Goal:
n : ℕ
⊢ ∀ (a : Fin n),
    Membership.mem (γ := List (Fin n)) (Finset.sort Finset.univ fun (a b : Fin n) ↦ a ≤ b) a ↔ a ∈ List.finRange n

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
hα : Finite α
β : Type u_2
inst_1 : LinearOrder β
hβ : Infinite β
haveI : ∀ (this : Fintype α), Nonempty (α ↪o β)
⊢ Nonempty (α ↪o β)

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
hα : Finite α
β : Type u_2
inst_1 : LinearOrder β
hβ : Infinite β
this : Fintype α
obtain : ∀ (s : Finset β) (hs : s.card = Fintype.card α), Nonempty (α ↪o β)
⊢ Nonempty (α ↪o β)

Tactic:
obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq β (Fintype.card α)

Premises used: Infinite.exists_subset_card_eq, Fintype.card
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
hα : Finite α
β : Type u_2
inst_1 : LinearOrder β
hβ : Infinite β
this : Fintype α
s : Finset β
hs : s.card = Fintype.card α
⊢ Nonempty (α ↪o β)

Tactic:
⟨((Fintype.orderIsoFinOfCardEq α rfl).symm.toOrderEmbedding).trans (s.orderEmbOfFin hs)⟩

Premises used: Finset.orderEmbOfFin, OrderIso.toOrderEmbedding, Fintype.orderIsoFinOfCardEq, Nonempty.intro, OrderIso.symm, RelEmbedding.trans, rfl
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
hα : Finite α
β : Type u_2
inst_1 : LinearOrder β
hβ : Infinite β
this : Fintype α
s : Finset β
hs : s.card = Fintype.card α
⊢ Nonempty (α ↪o β)

Tactic:
exact ⟨((Fintype.orderIsoFinOfCardEq α rfl).symm.toOrderEmbedding).trans (s.orderEmbOfFin hs)⟩
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Finite α
motive : α → Prop
h : ∀ (j : α), (∀ k < j, motive k) → motive j
i : α
⊢ motive i

Tactic:
WellFoundedLT.induction _ h

Premises used: WellFoundedLT.induction
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f : α ↪o β
⊢ Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
rfl