-- Mathlib/Data/List/Sort.lean
theorem Sublist.orderedInsert_sublist [IsTrans α r] {as bs} (x) (hs : as <+ bs) (hb : bs.Sorted r) :
    orderedInsert r x as <+ orderedInsert r x bs

Proof state:
case pos
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : 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

Result:
no goals

Proof state:
case nil
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
bs : List α
x : α
hb : Sorted r bs
hs : [] <+ bs
⊢ orderedInsert r x [] <+ orderedInsert r x bs

Tactic:
simp

Result:
no goals

Proof state:
case cons.nil
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
hb : Sorted r []
hs : a :: as <+ []
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x []

Tactic:
contradiction

Result:
no goals

Proof state:
case pos
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Sorted r (a :: bs)
a✝ : as <+ bs
hr : r x a
⊢ x :: a :: as <+ x :: a :: bs

Tactic:
simp_all only [sorted_cons, cons_sublist_cons]

Result:
no goals

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬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 _)

Result:
no goals

Proof state:
case pos
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
⊢ a :: orderedInsert r x as <+ x :: b :: bs

Tactic:
have hba := pairwise_cons.mp hb |>.left _ (mem_of_cons_sublist ‹a :: as <+ bs›)

Result:
case pos
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
hba : r b a
⊢ a :: orderedInsert r x as <+ x :: b :: bs

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬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

Result:
no goals

Proof state:
case cons.cons
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted 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

Tactic:
cases hs <;> split_ifs with hr

Result:
case pos
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : r x b
⊢ x :: a :: as <+ x :: b :: bs

case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬r x b
⊢ x :: a :: as <+ b :: orderedInsert r x bs

case pos
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
⊢ a :: orderedInsert r x as <+ x :: b :: bs

case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

case pos
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Sorted r (a :: bs)
a✝ : as <+ bs
hr : r x a
⊢ x :: a :: as <+ x :: a :: bs

case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Sorted r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

Tactic:
have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons

Result:
case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
ih : orderedInsert r x (a :: as) <+ orderedInsert r x bs
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬r x b
ih : orderedInsert r x (a :: as) <+ orderedInsert r x bs
⊢ x :: a :: as <+ b :: orderedInsert r x bs

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

Result:
case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬r x b
ih : x :: a :: as <+ orderedInsert r x bs
⊢ x :: a :: as <+ b :: orderedInsert r x bs

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Sorted r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

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

Result:
no goals

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
ih : orderedInsert r x (a :: as) <+ orderedInsert r x bs
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

Tactic:
rw [orderedInsert, if_neg hr] at ih

Result:
case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
ih : a :: orderedInsert r x as <+ orderedInsert r x bs
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

Proof state:
case cons.cons
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
hs : a :: as <+ b :: bs
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x (b :: bs)

Tactic:
unfold orderedInsert

Result:
case cons.cons
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted 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

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬r x b
⊢ x :: a :: as <+ b :: orderedInsert r x bs

Tactic:
have ih := orderedInsert_sublist x ‹a :: as <+ bs›  hb.of_cons

Result:
case neg
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬r x b
ih : orderedInsert r x (a :: as) <+ orderedInsert r x bs
⊢ x :: a :: as <+ b :: orderedInsert r x bs

Proof state:
case pos
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Sorted r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : r x b
⊢ x :: a :: as <+ x :: b :: bs

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

Result:
no goals