awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  ∀ (hl : ∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))),
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α) (x_2 : x_1 ∈ xs), r x_1 x ↔ s (f x_1) (f x)) ∧
      ∀ (x : α) (x_1 : x ∈ xs) (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
cons : ∀ (a : α), a ∈ insertionSort r xs → (r a x ↔ s (f a) (f x))
cons₁ : ∀ (a : α), a ∈ insertionSort r xs → (r x a ↔ s (f x) (f a))
⊢ map f (orderedInsert r x (insertionSort r xs)) = orderedInsert s (f x) (insertionSort s (map f xs))

Tactic:
rw [List.map_orderedInsert _ s, ih hl.2.2]

Premises used: And.right, List.map_orderedInsert
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  ∀ (hl : ∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))),
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α) (x_2 : x_1 ∈ xs), r x_1 x ↔ s (f x_1) (f x)) ∧
      ∀ (x : α) (x_1 : x ∈ xs) (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r a x ↔ s (f a) (f x))

Tactic:
simpa only [mem_insertionSort] using hl.2.1

Premises used: And.right, And.left, List.mem_insertionSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  ∀ (hl : ∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))),
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α) (x_2 : x_1 ∈ xs), r x_1 x ↔ s (f x_1) (f x)) ∧
      ∀ (x : α) (x_1 : x ∈ xs) (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r x a ↔ s (f x) (f a))

Tactic:
simpa only [mem_insertionSort] using hl.1.2

Premises used: And.right, And.left, List.mem_insertionSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
f : α → β
l : List α
hl : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → (r a b ↔ s (f a) (f b))
nil :
  ∀
    (hl :
      ∀ (a : α),
        Membership.mem (γ := List α) [] a → ∀ (b : α), Membership.mem (γ := List α) [] b → (r a b ↔ s (f a) (f b))),
    map f (insertionSort r []) = insertionSort s (map f [])
cons :
  ∀ (x : α) (xs : List α)
    (ih :
      ∀ (hl : ∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))),
        map f (insertionSort r xs) = insertionSort s (map f xs))
    (hl : ∀ (a : α), a ∈ x :: xs → ∀ (b : α), b ∈ x :: xs → (r a b ↔ s (f a) (f b))),
    map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))
⊢ map f (insertionSort r l) = insertionSort s (map f l)

Tactic:
induction l with
  | nil => simp
  | cons x xs ih =>
    simp_rw [List.forall_mem_cons, forall_and] at hl
    simp_rw [List.map, insertionSort_cons]
    rw [List.map_orderedInsert _ s, ih hl.2.2]
    · simpa only [mem_insertionSort] using hl.2.1
    · simpa only [mem_insertionSort] using hl.1.2

Premises used: List.map, List.insertionSort_cons, List.cons, List.forall_mem_cons, List.map_orderedInsert, forall_and, List.mem_insertionSort, List.nil
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
nil : Pairwise r [] → insertionSort r [] = []
cons :
  ∀ (head : α) (tail : List α),
    (Pairwise r tail → insertionSort r tail = tail) →
      Pairwise r (head :: tail) → insertionSort r (head :: tail) = head :: tail
⊢ Pairwise r l → insertionSort r l = l

Tactic:
induction l
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
⊢ Pairwise r [] → insertionSort r [] = []

Tactic:
grind [cases List]

Premises used: List
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
head : α
tail : List α
tail_ih : Pairwise r tail → insertionSort r tail = tail
⊢ Pairwise r (head :: tail) → insertionSort r (head :: tail) = head :: tail

Tactic:
grind [cases List]

Premises used: List
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
inst_2 : Std.Refl r
x : α
xs : List α
nil : (orderedInsert r x []).erase x = []
cons :
  ∀ (head : α) (tail : List α),
    (orderedInsert r x tail).erase x = tail → (orderedInsert r x (head :: tail)).erase x = head :: tail
⊢ (orderedInsert r x xs).erase x = xs

Tactic:
induction xs
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
inst_2 : Std.Refl r
x : α
⊢ (orderedInsert r x []).erase x = []

Tactic:
grind [Std.Refl]

Premises used: Std.Refl
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
inst_2 : Std.Refl r
x head : α
tail : List α
tail_ih : (orderedInsert r x tail).erase x = tail
⊢ (orderedInsert r x (head :: tail)).erase x = head :: tail

Tactic:
grind [Std.Refl]

Premises used: Std.Refl
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
x : α
xs : List α
hx : ¬x ∈ xs
nil : ∀ (hx : ¬Membership.mem (γ := List α) [] x), (orderedInsert r x []).erase x = []
cons :
  ∀ (head : α) (tail : List α),
    (∀ (hx : ¬x ∈ tail), (orderedInsert r x tail).erase x = tail) →
      ∀ (hx : ¬x ∈ head :: tail), (orderedInsert r x (head :: tail)).erase x = head :: tail
⊢ (orderedInsert r x xs).erase x = xs

Tactic:
induction xs
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
x : α
hx : ¬Membership.mem (γ := List α) [] x
⊢ (orderedInsert r x []).erase x = []

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
x head : α
tail : List α
tail_ih : ∀ (hx : ¬x ∈ tail), (orderedInsert r x tail).erase x = tail
hx : ¬x ∈ head :: tail
⊢ (orderedInsert r x (head :: tail)).erase x = head :: tail

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
inst_2 : Std.Antisymm r
x : α
hx : Membership.mem (γ := List α) [] x
hxs : Pairwise r []
⊢ orderedInsert r x (List.erase [] x) = []

Tactic:
grind +splitIndPred
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
inst_2 : Std.Antisymm r
x head : α
tail : List α
tail_ih : ∀ (hx : x ∈ tail) (hxs : Pairwise r tail), orderedInsert r x (tail.erase x) = tail
hx : x ∈ head :: tail
hxs : Pairwise r (head :: tail)
⊢ orderedInsert r x ((head :: tail).erase x) = head :: tail

Tactic:
grind +splitIndPred
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
inst_2 : Std.Antisymm r
x : α
xs : List α
hx : x ∈ xs
hxs : Pairwise r xs
nil : ∀ (hx : Membership.mem (γ := List α) [] x) (hxs : Pairwise r []), orderedInsert r x (List.erase [] x) = []
cons :
  ∀ (head : α) (tail : List α),
    (∀ (hx : x ∈ tail) (hxs : Pairwise r tail), orderedInsert r x (tail.erase x) = tail) →
      ∀ (hx : x ∈ head :: tail) (hxs : Pairwise r (head :: tail)),
        orderedInsert r x ((head :: tail).erase x) = head :: tail
⊢ orderedInsert r x (xs.erase x) = xs

Tactic:
induction xs with grind +splitIndPred
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
x : α
xs : List α
nil : [] <+ orderedInsert r x []
cons : ∀ (head : α) (tail : List α), tail <+ orderedInsert r x tail → head :: tail <+ orderedInsert r x (head :: tail)
⊢ xs <+ orderedInsert r x xs

Tactic:
induction xs
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
x : α
⊢ [] <+ orderedInsert r x []

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
x head : α
tail : List α
tail_ih : tail <+ orderedInsert r x tail
⊢ head :: tail <+ orderedInsert r x (head :: tail)

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l c : List α
a : α
hl : c <+ l
ha : ∀ (a' : α), a' ∈ c → r a a'
nil : ∀ (hl : c <+ []), a :: c <+ orderedInsert r a []
cons :
  ∀ (head : α) (tail : List α),
    (∀ (hl : c <+ tail), a :: c <+ orderedInsert r a tail) →
      ∀ (hl : c <+ head :: tail), a :: c <+ orderedInsert r a (head :: tail)
⊢ a :: c <+ orderedInsert r a l

Tactic:
induction l
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
c : List α
a : α
ha : ∀ (a' : α), a' ∈ c → r a a'
hl : c <+ []
⊢ a :: c <+ orderedInsert r a []

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
c : List α
a : α
ha : ∀ (a' : α), a' ∈ c → r a a'
head : α
tail : List α
tail_ih : ∀ (hl : c <+ tail), a :: c <+ orderedInsert r a tail
hl : c <+ head :: tail
⊢ a :: c <+ orderedInsert r a (head :: tail)

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
bs : List α
x : α
hb : Pairwise r bs
hs : [] <+ bs
⊢ orderedInsert r x [] <+ orderedInsert r x bs

Tactic:
simp
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
hb : Pairwise r []
hs : a :: as <+ []
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x []

Tactic:
contradiction
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
hs : a :: as <+ b :: bs
cons :
  a :: as <+ bs →
    (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
      if r x b then x :: b :: bs else b :: orderedInsert r x bs
cons₁ :
  ∀ (hb : Pairwise r (a :: bs)),
    as <+ bs →
      (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
        if r x a then x :: a :: bs else a :: orderedInsert r x bs
⊢ (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
    if r x b then x :: b :: bs else b :: orderedInsert r x bs

Tactic:
cases hs
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
pos : ∀ (hr : r x a), r x b → x :: a :: as <+ x :: b :: bs
neg : ∀ (hr : r x a), ¬r x b → x :: a :: as <+ b :: orderedInsert r x bs
pos₁ : ∀ (hr : ¬r x a), r x b → a :: orderedInsert r x as <+ x :: b :: bs
neg₁ : ∀ (hr : ¬r x a), ¬r x b → a :: orderedInsert r x as <+ b :: orderedInsert r x bs
⊢ (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
    if r x b then x :: b :: bs else b :: orderedInsert r x bs

Tactic:
split_ifs with hr
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
h : as <+ bs
pos : ∀ (hr : r x a), x :: a :: as <+ x :: a :: bs
neg : ∀ (hr : ¬r x a), a :: orderedInsert r x as <+ a :: orderedInsert r x bs
⊢ (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
    if r x a then x :: a :: bs else a :: orderedInsert r x bs

Tactic:
split_ifs with hr
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : r x a
h_1 : r x b
⊢ x :: a :: as <+ x :: b :: bs

Tactic:
.cons_cons _ <| .cons _ ‹a :: as <+ bs›

Premises used: List.Sublist.cons_cons, List.Sublist.cons
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : r x a
h_1 : r x b
⊢ x :: a :: as <+ x :: b :: bs

Tactic:
exact .cons_cons _ <| .cons _ ‹a :: as <+ bs›
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : r x a
h_1 : ¬r x b
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x bs

Tactic:
have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : r x a
h_1 : ¬r x b
ih : orderedInsert r x (a :: as) <+ orderedInsert r x bs
⊢ x :: a :: as <+ orderedInsert r x bs

Tactic:
simp only [hr, orderedInsert_cons, ite_true] at ih

Premises used: List.orderedInsert_cons, ite_true
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : r x a
h_1 : ¬r x b
ih : x :: a :: as <+ orderedInsert r x bs
⊢ x :: a :: as <+ b :: orderedInsert r x bs

Tactic:
.trans ih <| .cons _ (.refl _)

Premises used: List.Sublist.trans, List.Sublist.refl, List.Sublist.cons
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : r x a
h_1 : ¬r x b
ih : x :: a :: as <+ orderedInsert r x bs
⊢ x :: a :: as <+ b :: orderedInsert r x bs

Tactic:
exact .trans ih <| .cons _ (.refl _)
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : ¬r x a
h_1 : r x b
⊢ r b a

Tactic:
have hba := pairwise_cons.mp hb |>.left _ (mem_of_cons_sublist ‹a :: as <+ bs›)
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : ¬r x a
h_1 : r x b
hba : r b a
⊢ a :: orderedInsert r x as <+ x :: b :: bs

Tactic:
absurd (trans_of _ ‹r x b› hba) hr

Premises used: absurd, trans_of
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : ¬r x a
h_1 : r x b
hba : r b a
⊢ a :: orderedInsert r x as <+ x :: b :: bs

Tactic:
exact absurd (trans_of _ ‹r x b› hba) hr

Premises used: absurd, trans_of
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : ¬r x a
h_1 : ¬r x b
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x bs

Tactic:
have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : ¬r x a
h_1 : ¬r x b
ih : orderedInsert r x (a :: as) <+ orderedInsert r x bs
⊢ a :: orderedInsert r x as <+ orderedInsert r x bs

Tactic:
rw [orderedInsert_cons, if_neg hr] at ih

Premises used: List.orderedInsert_cons, if_neg
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : ¬r x a
h_1 : ¬r x b
ih : a :: orderedInsert r x as <+ orderedInsert r x bs
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

Tactic:
.cons _ ih

Premises used: List.Sublist.cons
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
h : a :: as <+ bs
hr : ¬r x a
h_1 : ¬r x b
ih : a :: orderedInsert r x as <+ orderedInsert r x bs
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

Tactic:
exact .cons _ ih
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
h : as <+ bs
hr : r x a
⊢ x :: a :: as <+ x :: a :: bs

Tactic:
simp_all
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
h : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

Tactic:
.cons_cons _ <| orderedInsert_sublist x ‹as <+ bs› hb.of_cons

Premises used: List.Sublist.cons_cons, List.Pairwise.of_cons
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
h : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

Tactic:
exact .cons_cons _ <| orderedInsert_sublist x ‹as <+ bs› hb.of_cons

Premises used: List.Pairwise.of_cons
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
bs : List α
x : α
hb : Pairwise r bs
a : α
as : List α
hs : a :: as <+ bs
cons : ∀ (hb : Pairwise r []) (hs : a :: as <+ []), orderedInsert r x (a :: as) <+ orderedInsert r x []
cons₁ :
  ∀ (b : α) (bs : List α) (hb : Pairwise r (b :: bs)) (hs : a :: as <+ b :: bs),
    orderedInsert r x (a :: as) <+ orderedInsert r x (b :: bs)
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x bs

Tactic:
cases bs with
    | nil => contradiction
    | cons b bs =>
      unfold orderedInsert
      cases hs <;> split_ifs with hr
      · exact .cons_cons _ <| .cons _ ‹a :: as <+ bs›
      · have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        simp only [hr, orderedInsert_cons, ite_true] at ih
        exact .trans ih <| .cons _ (.refl _)
      · have hba := pairwise_cons.mp hb |>.left _ (mem_of_cons_sublist ‹a :: as <+ bs›)
        exact absurd (trans_of _ ‹r x b› hba) hr
      · have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        rw [orderedInsert_cons, if_neg hr] at ih
        exact .cons _ ih
      · simp_all
      · exact .cons_cons _ <| orderedInsert_sublist x ‹as <+ bs› hb.of_cons

Premises used: List.orderedInsert_cons, List.orderedInsert, ite_true, List.Sublist.cons, List.Pairwise.of_cons, List.nil
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
as bs : List α
x : α
hs : as <+ bs
hb : Pairwise r bs
nil : ∀ (hs : [] <+ bs), orderedInsert r x [] <+ orderedInsert r x bs
cons : ∀ (a : α) (as : List α) (hs : a :: as <+ bs), orderedInsert r x (a :: as) <+ orderedInsert r x bs
⊢ orderedInsert r x as <+ orderedInsert r x bs

Tactic:
cases as with
  | nil => simp
  | cons a as =>
    cases bs with
    | nil => contradiction
    | cons b bs =>
      unfold orderedInsert
      cases hs <;> split_ifs with hr
      · exact .cons_cons _ <| .cons _ ‹a :: as <+ bs›
      · have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        simp only [hr, orderedInsert_cons, ite_true] at ih
        exact .trans ih <| .cons _ (.refl _)
      · have hba := pairwise_cons.mp hb |>.left _ (mem_of_cons_sublist ‹a :: as <+ bs›)
        exact absurd (trans_of _ ‹r x b› hba) hr
      · have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        rw [orderedInsert_cons, if_neg hr] at ih
        exact .cons _ ih
      · simp_all
      · exact .cons_cons _ <| orderedInsert_sublist x ‹as <+ bs› hb.of_cons

Premises used: List.orderedInsert_cons, List.orderedInsert, ite_true, List.Sublist.cons, List.Pairwise.of_cons, List.nil
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
pos : ∀ (h' : r a b), Pairwise r (List.orderedInsert r a (b :: l))
neg : ∀ (h' : ¬r a b), Pairwise r (List.orderedInsert r a (b :: l))
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
by_cases h' : a ≼ b
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : r a b
⊢ Pairwise r (List.orderedInsert r a (b :: 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
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
this : ∀ (b' : α), b' ∈ List.orderedInsert r a l → r b b'
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
simpa [orderedInsert_cons, h', h.of_cons.orderedInsert a l]

Premises used: List.orderedInsert_cons, List.Pairwise.of_cons
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
neg : ∀ (b' : α), b' ∈ List.orderedInsert r a l → r b b'
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
suffices ∀ b' : α, b' ∈ List.orderedInsert r a l → r b b' by
        simpa [orderedInsert_cons, h', h.of_cons.orderedInsert a l]
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
b' : α
bm : b' ∈ List.orderedInsert r a l
neg : ∀ (h' : ¬r b' b) (bm : b' ∈ List.orderedInsert r b' l), r b b'
neg₁ : ∀ (bm : b' ∈ l), r b b'
⊢ r b b'

Tactic:
rcases (mem_orderedInsert r).mp bm with rfl | bm

Premises used: List.mem_orderedInsert, Iff.mp, rfl
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
b : α
l : List α
h : Pairwise r (b :: l)
b' : α
h' : ¬r b' b
bm : b' ∈ List.orderedInsert r b' l
⊢ r b b'

Tactic:
(total_of r _ _).resolve_left h'

Premises used: Or.resolve_left, 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
b : α
l : List α
h : Pairwise r (b :: l)
b' : α
h' : ¬r b' b
bm : b' ∈ List.orderedInsert r b' l
⊢ r b b'

Tactic:
exact (total_of r _ _).resolve_left h'

Premises used: Or.resolve_left, 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
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
b' : α
bm_1 : b' ∈ List.orderedInsert r a l
bm : b' ∈ l
⊢ r b b'

Tactic:
rel_of_pairwise_cons h bm

Premises used: List.rel_of_pairwise_cons
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : Std.Total r
inst_2 : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
b' : α
bm_1 : b' ∈ List.orderedInsert r a l
bm : b' ∈ l
⊢ r b b'

Tactic:
exact rel_of_pairwise_cons h bm

Premises used: List.rel_of_pairwise_cons
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
c : List α
hr : Pairwise r c
hc : c <+ []
⊢ c <+ insertionSort r []

Tactic:
grind
-- 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
h : c <+ tail
⊢ c <+ insertionSort r (head :: tail)

Tactic:
ih hr 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
head : α
tail : List α
ih : ∀ {c : List α} (hr : Pairwise r c) (hc : c <+ tail), c <+ insertionSort r tail
c : List α
hr : Pairwise r c
h : c <+ tail
⊢ c <+ insertionSort r (head :: tail)

Tactic:
exact ih hr h |>.trans (sublist_orderedInsert ..)

Premises used: List.sublist_orderedInsert, List.Sublist.trans