-- Mathlib/Data/List/Sort.lean
theorem cons_sublist_orderedInsert {l c : List α} {a : α} (hl : c <+ l) (ha : ∀ a' ∈ c, a ≼ a') :
    a :: c <+ orderedInsert r a l

Proof state:
case neg.cons₂
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a head✝ : α
tail✝ : List α
hr : ¬r a head✝
l₁✝ : List α
ha : ∀ a' ∈ head✝ :: l₁✝, r a a'
ih : head✝ :: l₁✝ <+ tail✝ → a :: head✝ :: l₁✝ <+ orderedInsert r a tail✝
a✝ : l₁✝ <+ tail✝
⊢ a :: head✝ :: l₁✝ <+ head✝ :: orderedInsert r a tail✝

Tactic:
exact absurd (ha _ <| mem_cons_self ..) hr

Result:
no goals

Proof state:
case cons
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ a' ∈ c, r a a'
head✝ : α
tail✝ : List α
ih : c <+ tail✝ → a :: c <+ orderedInsert r a tail✝
hl : c <+ head✝ :: tail✝
⊢ a :: c <+ if r a head✝ then a :: head✝ :: tail✝ else head✝ :: orderedInsert r a tail✝

Tactic:
split_ifs with hr

Result:
case pos
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ a' ∈ c, r a a'
head✝ : α
tail✝ : List α
ih : c <+ tail✝ → a :: c <+ orderedInsert r a tail✝
hl : c <+ head✝ :: tail✝
hr : r a head✝
⊢ a :: c <+ a :: head✝ :: tail✝

case neg
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ a' ∈ c, r a a'
head✝ : α
tail✝ : List α
ih : c <+ tail✝ → a :: c <+ orderedInsert r a tail✝
hl : c <+ head✝ :: tail✝
hr : ¬r a head✝
⊢ a :: c <+ head✝ :: orderedInsert r a tail✝

Proof state:
case neg.cons
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ a' ∈ c, r a a'
head✝ : α
tail✝ : List α
ih : c <+ tail✝ → a :: c <+ orderedInsert r a tail✝
hr : ¬r a head✝
h : c <+ tail✝
⊢ a :: c <+ head✝ :: orderedInsert r a tail✝

Tactic:
exact .cons _ <| ih h

Result:
no goals

Proof state:
case nil
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ a' ∈ c, r a a'
hl : c <+ []
⊢ a :: c <+ orderedInsert r a []

Tactic:
simp_all only [sublist_nil, orderedInsert, Sublist.refl]

Result:
no goals

Proof state:
case cons
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ a' ∈ c, r a a'
head✝ : α
tail✝ : List α
ih : c <+ tail✝ → a :: c <+ orderedInsert r a tail✝
hl : c <+ head✝ :: tail✝
⊢ a :: c <+ orderedInsert r a (head✝ :: tail✝)

Tactic:
unfold orderedInsert

Result:
case cons
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ a' ∈ c, r a a'
head✝ : α
tail✝ : List α
ih : c <+ tail✝ → a :: c <+ orderedInsert r a tail✝
hl : c <+ head✝ :: tail✝
⊢ a :: c <+ if r a head✝ then a :: head✝ :: tail✝ else head✝ :: orderedInsert r a tail✝

Proof state:
case pos
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ a' ∈ c, r a a'
head✝ : α
tail✝ : List α
ih : c <+ tail✝ → a :: c <+ orderedInsert r a tail✝
hl : c <+ head✝ :: tail✝
hr : r a head✝
⊢ a :: c <+ a :: head✝ :: tail✝

Tactic:
exact .cons₂ _ hl

Result:
no goals

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ a' ∈ c, r a a'
head✝ : α
tail✝ : List α
ih : c <+ tail✝ → a :: c <+ orderedInsert r a tail✝
hl : c <+ head✝ :: tail✝
hr : ¬r a head✝
⊢ a :: c <+ head✝ :: orderedInsert r a tail✝

Tactic:
cases hl with
| cons _ h => exact .cons _ <| ih h
| cons₂    => exact absurd (ha _ <| mem_cons_self ..) hr

Result:
no goals