awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Sort (hypothesis)
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 : ∀ (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))
have 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))
Tactic: simp_rw [List.forall_mem_cons, forall_and] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))
have cons : map f (orderedInsert r x (insertionSort r xs)) = orderedInsert s (f x) (insertionSort s (map f xs))
Tactic: simp_rw [List.map, insertionSort_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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))
⊢ map f (orderedInsert r x (insertionSort r xs)) = orderedInsert s (f x) (insertionSort s (map f xs))
have cons : ∀ (a : α), a ∈ insertionSort r xs → (r a x ↔ s (f a) (f x))
Tactic: rw [List.map_orderedInsert _ s, ih hl.2.2]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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))
⊢ map f (orderedInsert r x (insertionSort r xs)) = orderedInsert s (f x) (insertionSort s (map f xs))
have cons₁ : ∀ (a : α), a ∈ insertionSort r xs → (r x a ↔ s (f x) (f a))
Tactic: rw [List.map_orderedInsert _ s, ih hl.2.2]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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))
⊢ map f (insertionSort r l) = insertionSort s (map f l)
have 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 [])
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
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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 [])
⊢ map f (insertionSort r l) = insertionSort s (map f l)
have 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))
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
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
⊢ Pairwise r l → insertionSort r l = l
have nil : Pairwise r [] → insertionSort r [] = []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
nil : Pairwise r [] → insertionSort r [] = []
⊢ Pairwise r l → insertionSort r l = l
have cons : ∀ (head : α) (tail : List α),
  (Pairwise r tail → insertionSort r tail = tail) →
    Pairwise r (head :: tail) → insertionSort r (head :: tail) = head :: tail
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
inst_2 : Std.Refl r
x : α
xs : List α
⊢ (orderedInsert r x xs).erase x = xs
have nil : (orderedInsert r x []).erase x = []
Tactic: induction xs
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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 = []
⊢ (orderedInsert r x xs).erase x = xs
have cons : ∀ (head : α) (tail : List α),
  (orderedInsert r x tail).erase x = tail → (orderedInsert r x (head :: tail)).erase x = head :: tail
Tactic: induction xs
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
x : α
xs : List α
hx : ¬x ∈ xs
⊢ (orderedInsert r x xs).erase x = xs
have nil : ∀ (hx : ¬Membership.mem (γ := List α) [] x), (orderedInsert r x []).erase x = []
Tactic: induction xs
Cleared hypotheses: xs, hx
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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 = []
⊢ (orderedInsert r x xs).erase x = xs
have 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
Tactic: induction xs
Cleared hypotheses: xs, hx
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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
⊢ orderedInsert r x (xs.erase x) = xs
have nil : ∀ (hx : Membership.mem (γ := List α) [] x) (hxs : Pairwise r []), orderedInsert r x (List.erase [] x) = []
Tactic: induction xs with grind +splitIndPred
Cleared hypotheses: xs, hx, hxs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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) = []
⊢ orderedInsert r x (xs.erase x) = xs
have 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
Tactic: induction xs with grind +splitIndPred
Cleared hypotheses: xs, hx, hxs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
x : α
xs : List α
⊢ xs <+ orderedInsert r x xs
have nil : [] <+ orderedInsert r x []
Tactic: induction xs
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
x : α
xs : List α
nil : [] <+ orderedInsert r x []
⊢ xs <+ orderedInsert r x xs
have cons : ∀ (head : α) (tail : List α), tail <+ orderedInsert r x tail → head :: tail <+ orderedInsert r x (head :: tail)
Tactic: induction xs
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l c : List α
a : α
hl : c <+ l
ha : ∀ (a' : α), a' ∈ c → r a a'
⊢ a :: c <+ orderedInsert r a l
have nil : ∀ (hl : c <+ []), a :: c <+ orderedInsert r a []
Tactic: induction l
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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 []
⊢ a :: c <+ orderedInsert r a l
have cons : ∀ (head : α) (tail : List α),
  (∀ (hl : c <+ tail), a :: c <+ orderedInsert r a tail) →
    ∀ (hl : c <+ head :: tail), a :: c <+ orderedInsert r a (head :: tail)
Tactic: induction l
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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
⊢ (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
have 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
Tactic: cases hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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
⊢ (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
have 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
Tactic: cases hs
Cleared hypotheses: b, hb, hs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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
⊢ (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
have pos : ∀ (hr : r x a), r x b → x :: a :: as <+ x :: b :: bs
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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
⊢ (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
have neg : ∀ (hr : r x a), ¬r x b → x :: a :: as <+ b :: orderedInsert r x bs
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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
⊢ (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
have pos₁ : ∀ (hr : ¬r x a), r x b → a :: orderedInsert r x as <+ x :: b :: bs
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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
⊢ (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
have neg₁ : ∀ (hr : ¬r x a), ¬r x b → a :: orderedInsert r x as <+ b :: orderedInsert r x bs
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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
⊢ (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
have pos : ∀ (hr : r x a), x :: a :: as <+ x :: a :: bs
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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
⊢ (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
have neg : ∀ (hr : ¬r x a), a :: orderedInsert r x as <+ a :: orderedInsert r x bs
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Data.List.Sort (hypothesis)
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 <+ b :: orderedInsert r x bs
have ih : orderedInsert r x (a :: as) <+ orderedInsert r x bs
Tactic: have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
-- Lean 4 proof step from Mathlib.Data.List.Sort (hypothesis)
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 <+ b :: orderedInsert r x bs
have ih₁ : x :: a :: as <+ orderedInsert r x bs
Tactic: simp only [hr, orderedInsert_cons, ite_true] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.List.Sort (hypothesis)
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
⊢ a :: orderedInsert r x as <+ x :: b :: bs
have hba : r b a
Tactic: have hba := pairwise_cons.mp hb |>.left _ (mem_of_cons_sublist ‹a :: as <+ bs›)
-- Lean 4 proof step from Mathlib.Data.List.Sort (hypothesis)
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
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs
have ih : orderedInsert r x (a :: as) <+ orderedInsert r x bs
Tactic: have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
-- Lean 4 proof step from Mathlib.Data.List.Sort (hypothesis)
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 <+ b :: orderedInsert r x bs
have ih₁ : a :: orderedInsert r x as <+ orderedInsert r x bs
Tactic: rw [orderedInsert_cons, if_neg hr] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x bs
have cons : ∀ (hb : Pairwise r []) (hs : a :: as <+ []), orderedInsert r x (a :: as) <+ orderedInsert r x []
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
Cleared hypotheses: bs, hb, hs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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 []
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x bs
have cons₁ : ∀ (b : α) (bs : List α) (hb : Pairwise r (b :: bs)) (hs : a :: as <+ b :: bs),
  orderedInsert r x (a :: as) <+ orderedInsert r x (b :: 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
Cleared hypotheses: bs, hb, hs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
as bs : List α
x : α
hs : as <+ bs
hb : Pairwise r bs
⊢ orderedInsert r x as <+ orderedInsert r x bs
have nil : ∀ (hs : [] <+ bs), orderedInsert r x [] <+ 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
Cleared hypotheses: as, hs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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
⊢ orderedInsert r x as <+ orderedInsert r x bs
have cons : ∀ (a : α) (as : List α) (hs : a :: as <+ bs), orderedInsert r x (a :: 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
Cleared hypotheses: as, hs
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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)
⊢ Pairwise r (List.orderedInsert r a (b :: l))
have pos : ∀ (h' : r a b), Pairwise r (List.orderedInsert r a (b :: l))
Tactic: by_cases h' : a ≼ b
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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))
⊢ Pairwise r (List.orderedInsert r a (b :: l))
have neg : ∀ (h' : ¬r a b), Pairwise r (List.orderedInsert r a (b :: l))
Tactic: by_cases h' : a ≼ b
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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))
have neg : ∀ (b' : α), b' ∈ List.orderedInsert r a l → r b b'
Tactic: suffices ∀ b' : α, b' ∈ List.orderedInsert r a l → r b b' by
        simpa [orderedInsert_cons, h', h.of_cons.orderedInsert a l]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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
⊢ r b b'
have neg : ∀ (h' : ¬r b' b) (bm : b' ∈ List.orderedInsert r b' l), r b b'
Tactic: rcases (mem_orderedInsert r).mp bm with rfl | bm
Cleared hypotheses: a, h', bm
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
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'
⊢ r b b'
have neg₁ : ∀ (bm : b' ∈ l), r b b'
Tactic: rcases (mem_orderedInsert r).mp bm with rfl | bm
-- Lean 4 proof step from Mathlib.Data.List.Sort (hypothesis)
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
⊢ head :: l₁ <+ insertionSort r (head :: tail)
have hr₁ : ∀ (a' : α), a' ∈ l₁ → r head a'
Tactic: obtain ⟨hr, hp⟩ := pairwise_cons.mp hr