awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
head : α
tail : List α
ih : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ tail), c <+ insertionSort r tail
l₁ : List α
hr : Pairwise r (head :: l₁)
h : l₁ <+ tail
⊢ ∀ (a' : α), a' ∈ l₁ → r head a'

Tactic:
obtain ⟨hr, hp⟩ := pairwise_cons.mp hr

Premises used: List.pairwise_cons, Iff.mp
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
head : α
tail : List α
ih : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ tail), c <+ insertionSort r tail
l₁ : List α
hr : Pairwise r (head :: l₁)
h : l₁ <+ tail
hr₁ : ∀ (a' : α), a' ∈ l₁ → r head a'
⊢ Pairwise r l₁

Tactic:
obtain ⟨hr, hp⟩ := pairwise_cons.mp hr

Premises used: List.pairwise_cons, Iff.mp
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
head : α
tail : List α
ih : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ tail), c <+ insertionSort r tail
l₁ : List α
hr_1 : Pairwise r (head :: l₁)
h : l₁ <+ tail
hr : ∀ (a' : α), a' ∈ l₁ → r head a'
hp : Pairwise r l₁
⊢ head :: l₁ <+ insertionSort r (head :: tail)

Tactic:
cons_sublist_orderedInsert (ih hp h) hr

Premises used: List.cons_sublist_orderedInsert, List.foldr, List.insertionSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
head : α
tail : List α
ih : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ tail), c <+ insertionSort r tail
l₁ : List α
hr_1 : Pairwise r (head :: l₁)
h : l₁ <+ tail
hr : ∀ (a' : α), a' ∈ l₁ → r head a'
hp : Pairwise r l₁
⊢ head :: l₁ <+ insertionSort r (head :: tail)

Tactic:
exact cons_sublist_orderedInsert (ih hp h) hr

Premises used: List.cons_sublist_orderedInsert
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
head : α
tail : List α
ih : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ tail), c <+ insertionSort r tail
c : List α
hr : Pairwise r c
hc : c <+ head :: tail
cons : ∀ (h : c <+ tail), c <+ insertionSort r (head :: tail)
cons₁ : ∀ {l₁ : List α} (hr : Pairwise r (head :: l₁)) (h : l₁ <+ tail), head :: l₁ <+ insertionSort r (head :: tail)
⊢ c <+ insertionSort r (head :: tail)

Tactic:
cases hc with
    | cons  _ h => exact ih hr h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
      exact cons_sublist_orderedInsert (ih hp h) hr

Premises used: List.cons, List.pairwise_cons, Iff.mp
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l c : List α
hr : Pairwise r c
hc : c <+ l
nil : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ []), c <+ insertionSort r []
cons :
  ∀ (head : α) (tail : List α) (ih : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ tail), c <+ insertionSort r tail)
    {c : List α} (hr : Pairwise r c) (hc : c <+ head :: tail), c <+ insertionSort r (head :: tail)
⊢ c <+ insertionSort r l

Tactic:
induction l generalizing c with
  | nil         => grind
  | cons _ _ ih =>
    cases hc with
    | cons  _ h => exact ih hr h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
      exact cons_sublist_orderedInsert (ih hp h) hr

Premises used: List.cons, List.pairwise_cons, Iff.mp, List.nil
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
l : List α
hab : r a b
h : [a, b] <+ l
⊢ [a, b] <+ insertionSort r l

Tactic:
sublist_insertionSort (pairwise_pair.mpr hab) h

Premises used: Iff.mpr, List.sublist_insertionSort, List.pairwise_pair
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
l c : List α
hs : Pairwise r c
hc : c <+~ l
obtain : ∀ (d : List α) (hc : d ~ c) (hd : d <+ l), c <+ insertionSort r l
⊢ c <+ insertionSort r l

Tactic:
obtain ⟨d, hc, hd⟩ := hc
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
hd : d <+ []
⊢ c <+ insertionSort r []

Tactic:
grind [nil_perm]

Premises used: List.nil_perm
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail : List α
ih : ∀ {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ tail), c <+ insertionSort r tail
c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
h : d <+ tail
⊢ c <+ insertionSort r (a :: tail)

Tactic:
ih hs _ hc h |>.trans (sublist_orderedInsert ..)

Premises used: List.sublist_orderedInsert, List.Sublist.trans
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail : List α
ih : ∀ {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ tail), c <+ insertionSort r tail
c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
h : d <+ tail
⊢ c <+ insertionSort r (a :: tail)

Tactic:
exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)

Premises used: List.sublist_orderedInsert, List.Sublist.trans
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail : List α
ih : ∀ {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ tail), c <+ insertionSort r tail
c : List α
hs : Pairwise r c
l₁ : List α
hc : a :: l₁ ~ c
h : l₁ <+ tail
⊢ c.erase a <+ insertionSort r tail

Tactic:
specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h

Premises used: List.Pairwise.erase
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail c : List α
hs : Pairwise r c
l₁ : List α
hc : a :: l₁ ~ c
h : l₁ <+ tail
ih : c.erase a <+ insertionSort r tail
⊢ a ∈ c

Tactic:
have hm := hc.mem_iff.mp <| mem_cons_self ..
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail c : List α
hs : Pairwise r c
l₁ : List α
hc : a :: l₁ ~ c
h : l₁ <+ tail
ih : c.erase a <+ insertionSort r tail
hm : a ∈ c
⊢ orderedInsert r a (c.erase a) = c

Tactic:
have he := orderedInsert_erase _ _ hm hs
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail c : List α
hs : Pairwise r c
l₁ : List α
hc : a :: l₁ ~ c
h : l₁ <+ tail
ih : c.erase a <+ insertionSort r tail
hm : a ∈ c
he : orderedInsert r a (c.erase a) = c
⊢ c <+ insertionSort r (a :: tail)

Tactic:
he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)

Premises used: Eq.rec, List.Sublist.orderedInsert_sublist, List.pairwise_insertionSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail c : List α
hs : Pairwise r c
l₁ : List α
hc : a :: l₁ ~ c
h : l₁ <+ tail
ih : c.erase a <+ insertionSort r tail
hm : a ∈ c
he : orderedInsert r a (c.erase a) = c
⊢ c <+ insertionSort r (a :: tail)

Tactic:
exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a : α
tail : List α
ih : ∀ {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ tail), c <+ insertionSort r tail
c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
hd : d <+ a :: tail
cons : ∀ (h : d <+ tail), c <+ insertionSort r (a :: tail)
cons₁ : ∀ {l₁ : List α} (hc : a :: l₁ ~ c) (h : l₁ <+ tail), c <+ insertionSort r (a :: tail)
⊢ c <+ insertionSort r (a :: tail)

Tactic:
cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)

Premises used: List.cons
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
l c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
hd : d <+ l
nil : ∀ {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ []), c <+ insertionSort r []
cons :
  ∀ (a : α) (tail : List α)
    (ih : ∀ {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ tail), c <+ insertionSort r tail)
    {c : List α} (hs : Pairwise r c) (d : List α) (hc : d ~ c) (hd : d <+ a :: tail), c <+ insertionSort r (a :: tail)
⊢ c <+ insertionSort r l

Tactic:
induction l generalizing c d with
  | nil         => grind [nil_perm]
  | cons a _ ih =>
    cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)

Premises used: List.nil_perm, List.cons, List.nil
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
l c : List α
hs : Pairwise r c
hc : c <+~ l
obtain : ∀ (d : List α) (hc : d ~ c) (hd : d <+ l), c <+ insertionSort r l
⊢ c <+ insertionSort r l

Tactic:
classical
  obtain ⟨d, hc, hd⟩ := hc
  induction l generalizing c d with
  | nil         => grind [nil_perm]
  | cons a _ ih =>
    cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)

Premises used: List.nil_perm, List.cons, List.nil
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Antisymm r
inst_2 : Std.Total r
inst_3 : IsTrans α r
a b : α
l : List α
hab : r a b
h : [a, b] <+~ l
⊢ [a, b] <+ insertionSort r l

Tactic:
sublist_insertionSort' (pairwise_pair.mpr hab) h

Premises used: Iff.mpr, List.sublist_insertionSort', List.pairwise_pair
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
⊢ Eq (α := List ℕ) (mergeSort [5, 27, 221, 95, 17, 43, 7, 2, 98, 567, 23, 12] fun (m n : ℕ) ↦ decide (m / 10 ≤ n / 10))
    [5, 7, 2, 17, 12, 27, 23, 43, 95, 98, 221, 567]

Tactic:
simp [mergeSort]

Premises used: List.mergeSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Antisymm r
l₁ l₂ : List α
⊢ Pairwise r l₁ → Pairwise r l₂ → ∀ (hl : l₁ ~ l₂), l₁ = l₂

Tactic:
eq_of_pairwise (fun _ _ _ _ => antisymm)

Premises used: antisymm, List.Perm.eq_of_pairwise
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Antisymm r
l₁ l₂ : List α
hp : l₁ <+~ l₂
hs₁ : Pairwise r l₁
hs₂ : Pairwise r l₂
let : ∀ (w : List α) (h : w ~ l₁) (h' : w <+ l₂), l₁ <+ l₂
⊢ l₁ <+ l₂

Tactic:
let ⟨_, h, h'⟩ := hp
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Antisymm r
l₁ l₂ : List α
hp : l₁ <+~ l₂
hs₁ : Pairwise r l₁
hs₂ : Pairwise r l₂
w : List α
h : w ~ l₁
h' : w <+ l₂
⊢ l₁ <+ l₂

Tactic:
Sublist.trans (h.eq_of_pairwise' (hs₂.sublist h') hs₁ ▸ Sublist.refl _) h'

Premises used: List.Sublist.trans
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Antisymm r
l₁ l₂ : List α
hp : l₁ <+~ l₂
hs₁ : Pairwise r l₁
hs₂ : Pairwise r l₂
w : List α
h : w ~ l₁
h' : w <+ l₂
⊢ l₁ <+ l₂

Tactic:
exact Sublist.trans (h.eq_of_pairwise' (hs₂.sublist h') hs₁ ▸ Sublist.refl _) h'

Premises used: List.Sublist.trans
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Antisymm r
inst_1 : Std.Irrefl r
l₁ l₂ : List α
h₁ : Pairwise r l₁
h₂ : Pairwise r l₂
hl₁₂ : l₁ ⊆ l₂
hl₁₂' : l₂ ⊆ l₁
⊢ l₁ = l₂

Tactic:
((subperm_of_subset h₁.nodup hl₁₂).antisymm
    (subperm_of_subset h₂.nodup hl₁₂')).eq_of_pairwise' h₁ h₂

Premises used: List.subperm_of_subset, List.Perm.eq_of_pairwise', List.Pairwise.nodup, List.Subperm.antisymm
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Antisymm r
inst_1 : Std.Irrefl r
l₁ l₂ : List α
h₁ : Pairwise r l₁
h₂ : Pairwise r l₂
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
⊢ l₁ ⊆ l₂

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Antisymm r
inst_1 : Std.Irrefl r
l₁ l₂ : List α
h₁ : Pairwise r l₁
h₂ : Pairwise r l₂
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
⊢ l₂ ⊆ l₁

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : (fun (x1 x2 : α) ↦ decide (r x1 x2)) a b = true
h₂ : (fun (x1 x2 : α) ↦ decide (r x1 x2)) b c = true
⊢ r a b

Tactic:
simpa using h₁
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : (fun (x1 x2 : α) ↦ decide (r x1 x2)) a b = true
h₂ : (fun (x1 x2 : α) ↦ decide (r x1 x2)) b c = true
⊢ r b c

Tactic:
simpa using h₂
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : (fun (x1 x2 : α) ↦ decide (r x1 x2)) a b = true
h₂ : (fun (x1 x2 : α) ↦ decide (r x1 x2)) b c = true
⊢ (fun (x1 x2 : α) ↦ decide (r x1 x2)) a c = true

Tactic:
simpa using _root_.trans (by simpa using h₁) (by simpa using h₂)

Premises used: trans
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b : α
⊢ ((fun (x1 x2 : α) ↦ decide (r x1 x2)) a b || (fun (x1 x2 : α) ↦ decide (r x1 x2)) b a) = true

Tactic:
simpa using Std.Total.total a b

Premises used: Std.Total.total
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise (fun (a b : α) ↦ (fun (x1 x2 : α) ↦ decide (r x1 x2)) a b = true) l

Tactic:
simpa using h
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise (fun (a b : α) ↦ (fun (x1 x2 : α) ↦ decide (r x1 x2)) a b = true) l'

Tactic:
simpa using h'
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise r (l.merge l' fun (x1 x2 : α) ↦ decide (r x1 x2))

Tactic:
simpa using pairwise_merge (le := (r · ·))
    (fun a b c h₁ h₂ => by simpa using _root_.trans (by simpa using h₁) (by simpa using h₂))
    (fun a b => by simpa using Std.Total.total a b)
    l l' (by simpa using h) (by simpa using h')

Premises used: List.pairwise_merge
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
l : List α
x x_1 x_2 : α
⊢ (fun (x1 x2 : α) ↦ decide (r x1 x2)) x x_1 = true →
    (fun (x1 x2 : α) ↦ decide (r x1 x2)) x_1 x_2 = true → (fun (x1 x2 : α) ↦ decide (r x1 x2)) x x_2 = true

Tactic:
simpa using trans_of r

Premises used: trans_of
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
l : List α
⊢ ∀ (a b : α), ((fun (x1 x2 : α) ↦ decide (r x1 x2)) a b || (fun (x1 x2 : α) ↦ decide (r x1 x2)) b a) = true

Tactic:
simpa using total_of r

Premises used: total_of
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
l : List α
⊢ Pairwise r (l.mergeSort fun (x1 x2 : α) ↦ decide (r x1 x2))

Tactic:
simpa using pairwise_mergeSort (le := (r · ·))
    (fun _ _ _ => by simpa using trans_of r)
    (by simpa using total_of r)
    l

Premises used: List.pairwise_mergeSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
inst_3 : Std.Antisymm r
l : List α
⊢ Pairwise r l → (l.mergeSort fun (x1 x2 : α) ↦ decide (r x1 x2)) = l

Tactic:
(mergeSort_perm _ _).eq_of_pairwise' (pairwise_mergeSort' _ l)

Premises used: List.Perm.eq_of_pairwise', List.pairwise_mergeSort', List.mergeSort_perm, Decidable.decide
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
inst_3 : Std.Antisymm r
l : List α
⊢ (l.mergeSort fun (x1 x2 : α) ↦ decide (r x1 x2)) = insertionSort r l

Tactic:
((mergeSort_perm l _).trans (perm_insertionSort r l).symm).eq_of_pairwise'
    (pairwise_mergeSort' r l) (pairwise_insertionSort r l)

Premises used: List.Perm.eq_of_pairwise', List.Perm.trans, List.pairwise_insertionSort, List.Perm.symm, List.pairwise_mergeSort', List.mergeSort_perm, List.perm_insertionSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedLE ↔ Monotone l.get

Tactic:
.rfl

Premises used: List.SortedLE, Iff.rfl
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedGE ↔ Antitone l.get

Tactic:
.rfl

Premises used: Iff.rfl, List.SortedGE
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedLT ↔ StrictMono l.get

Tactic:
.rfl

Premises used: List.SortedLT, Iff.rfl
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedGT ↔ StrictAnti l.get

Tactic:
.rfl

Premises used: Iff.rfl, List.SortedGT
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
simp :
  (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      (⟨i, h⟩ : Fin l.length) < ⟨i_1, h_1⟩ → l.get (⟨i, h⟩ : Fin l.length) ≤ l.get (⟨i_1, h_1⟩ : Fin l.length)) ↔
    Pairwise (fun (x1 x2 : α) ↦ x1 ≤ x2) l
⊢ l.SortedLE ↔ Pairwise (fun (x1 x2 : α) ↦ x1 ≤ x2) l

Tactic:
simp only [sortedLE_iff_monotone_get, monotone_iff_forall_lt, Fin.forall_iff]

Premises used: Fin.forall_iff, monotone_iff_forall_lt, List.sortedLE_iff_monotone_get
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      (⟨i, h⟩ : Fin l.length) < ⟨i_1, h_1⟩ → l.get (⟨i, h⟩ : Fin l.length) ≤ l.get (⟨i_1, h_1⟩ : Fin l.length)) ↔
    Pairwise (fun (x1 x2 : α) ↦ x1 ≤ x2) l

Tactic:
grind [pairwise_iff_getElem]

Premises used: List.pairwise_iff_getElem
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
simp :
  (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      (⟨i, h⟩ : Fin l.length) < ⟨i_1, h_1⟩ → l.get (⟨i_1, h_1⟩ : Fin l.length) ≤ l.get (⟨i, h⟩ : Fin l.length)) ↔
    Pairwise (fun (x1 x2 : α) ↦ x1 ≥ x2) l
⊢ l.SortedGE ↔ Pairwise (fun (x1 x2 : α) ↦ x1 ≥ x2) l

Tactic:
simp only [sortedGE_iff_antitone_get, antitone_iff_forall_lt, Fin.forall_iff]

Premises used: Fin.forall_iff, List.sortedGE_iff_antitone_get, antitone_iff_forall_lt
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      (⟨i, h⟩ : Fin l.length) < ⟨i_1, h_1⟩ → l.get (⟨i_1, h_1⟩ : Fin l.length) ≤ l.get (⟨i, h⟩ : Fin l.length)) ↔
    Pairwise (fun (x1 x2 : α) ↦ x1 ≥ x2) l

Tactic:
grind [pairwise_iff_getElem]

Premises used: List.pairwise_iff_getElem
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
simp :
  (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      (⟨i, h⟩ : Fin l.length) < ⟨i_1, h_1⟩ → l.get (⟨i, h⟩ : Fin l.length) < l.get (⟨i_1, h_1⟩ : Fin l.length)) ↔
    Pairwise (fun (x1 x2 : α) ↦ x1 < x2) l
⊢ l.SortedLT ↔ Pairwise (fun (x1 x2 : α) ↦ x1 < x2) l

Tactic:
simp only [sortedLT_iff_strictMono_get, StrictMono, Fin.forall_iff]

Premises used: StrictMono, List.sortedLT_iff_strictMono_get, Fin.forall_iff
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      (⟨i, h⟩ : Fin l.length) < ⟨i_1, h_1⟩ → l.get (⟨i, h⟩ : Fin l.length) < l.get (⟨i_1, h_1⟩ : Fin l.length)) ↔
    Pairwise (fun (x1 x2 : α) ↦ x1 < x2) l

Tactic:
grind [pairwise_iff_getElem]

Premises used: List.pairwise_iff_getElem
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
simp :
  (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      (⟨i, h⟩ : Fin l.length) < ⟨i_1, h_1⟩ → l.get (⟨i_1, h_1⟩ : Fin l.length) < l.get (⟨i, h⟩ : Fin l.length)) ↔
    Pairwise (fun (x1 x2 : α) ↦ x1 > x2) l
⊢ l.SortedGT ↔ Pairwise (fun (x1 x2 : α) ↦ x1 > x2) l

Tactic:
simp only [sortedGT_iff_strictAnti_get, StrictAnti, Fin.forall_iff]

Premises used: List.sortedGT_iff_strictAnti_get, Fin.forall_iff, StrictAnti
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      (⟨i, h⟩ : Fin l.length) < ⟨i_1, h_1⟩ → l.get (⟨i_1, h_1⟩ : Fin l.length) < l.get (⟨i, h⟩ : Fin l.length)) ↔
    Pairwise (fun (x1 x2 : α) ↦ x1 > x2) l

Tactic:
grind [pairwise_iff_getElem]

Premises used: List.pairwise_iff_getElem
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedLE ↔ IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) l

Tactic:
sortedLE_iff_pairwise.trans isChain_iff_pairwise.symm

Premises used: List.sortedLE_iff_pairwise, Iff.trans, List.isChain_iff_pairwise, Iff.symm
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedGE ↔ IsChain (fun (x1 x2 : α) ↦ x1 ≥ x2) l

Tactic:
sortedGE_iff_pairwise.trans isChain_iff_pairwise.symm

Premises used: List.sortedGE_iff_pairwise, Iff.trans, List.isChain_iff_pairwise, Iff.symm
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedLT ↔ IsChain (fun (x1 x2 : α) ↦ x1 < x2) l

Tactic:
sortedLT_iff_pairwise.trans isChain_iff_pairwise.symm

Premises used: List.sortedLT_iff_pairwise, Iff.trans, List.isChain_iff_pairwise, Iff.symm
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedGT ↔ IsChain (fun (x1 x2 : α) ↦ x1 > x2) l

Tactic:
sortedGT_iff_pairwise.trans isChain_iff_pairwise.symm

Premises used: List.sortedGT_iff_pairwise, Iff.trans, List.isChain_iff_pairwise, Iff.symm
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedLE ↔
    ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄,
      i ≤ j →
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi ≤
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj

Tactic:
⟨fun h _ _ _ _ hij => h.monotone_get hij, fun h => Monotone.sortedLE <| fun _ _ => (h ·)⟩

Premises used: List.SortedLE.monotone_get, Monotone.sortedLE, Iff.intro
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedGE ↔
    ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄,
      j ≤ i →
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi ≤
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj

Tactic:
⟨fun h _ _ _ _ hij => h.antitone_get hij, fun h => Antitone.sortedGE <| fun _ _ => (h ·)⟩

Premises used: Antitone.sortedGE, Iff.intro, List.SortedGE.antitone_get