-- Mathlib/Data/List/Sort.lean
theorem sublist_insertionSort' {l c : List α} (hs : c.Sorted r) (hc : c <+~ l) :
    c <+ insertionSort r l

Proof state:
case intro.intro.cons.cons₂
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
tail✝ c : List α
hs : Sorted r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
ih : c.erase a <+ insertionSort r tail✝
hm : a ∈ c
⊢ c <+ insertionSort r (a :: tail✝)

Tactic:
have he := orderedInsert_erase _ _ hm hs

Result:
case intro.intro.cons.cons₂
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
tail✝ c : List α
hs : Sorted 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✝)

Proof state:
case intro.intro.nil
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
c : List α
hs : Sorted r c
d : List α
hc : d ~ c
hd : d <+ []
⊢ c <+ insertionSort r []

Tactic:
simp_all only [sublist_nil, insertionSort, nil_perm]

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
l c : List α
hs : Sorted r c
hc : c <+~ l
⊢ c <+ insertionSort r l

Tactic:
classical
obtain ⟨d, hc, hd⟩ := hc
induction l generalizing c d with
| nil         => simp_all only [sublist_nil, insertionSort, nil_perm]
| cons a _ ih =>
  cases hd with
  | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
  | 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 (sorted_insertionSort ..)

Result:
no goals

Proof state:
case intro.intro
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
l c : List α
hs : Sorted r c
d : List α
hc : d ~ c
hd : d <+ l
⊢ c <+ insertionSort r l

Tactic:
induction l generalizing c d with
| nil         => simp_all only [sublist_nil, insertionSort, nil_perm]
| cons a _ ih =>
  cases hd with
  | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
  | 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 (sorted_insertionSort ..)

Result:
no goals

Proof state:
case intro.intro.cons.cons
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
tail✝ : List α
ih : ∀ {c : List α}, Sorted r c → ∀ (d : List α), d ~ c → d <+ tail✝ → c <+ insertionSort r tail✝
c : List α
hs : Sorted r c
d : List α
hc : d ~ c
h : d <+ tail✝
⊢ c <+ insertionSort r (a :: tail✝)

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

Result:
no goals

Proof state:
case intro.intro.cons.cons₂
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
tail✝ c : List α
hs : Sorted 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 (sorted_insertionSort ..)

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
l c : List α
hs : Sorted r c
hc : c <+~ l
⊢ c <+ insertionSort r l

Tactic:
obtain ⟨d, hc, hd⟩ := hc

Result:
case intro.intro
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
l c : List α
hs : Sorted r c
d : List α
hc : d ~ c
hd : d <+ l
⊢ c <+ insertionSort r l

Proof state:
case intro.intro.cons.cons₂
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
tail✝ c : List α
hs : Sorted r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
ih : c.erase a <+ insertionSort r tail✝
⊢ c <+ insertionSort r (a :: tail✝)

Tactic:
have hm := hc.mem_iff.mp <| mem_cons_self ..

Result:
case intro.intro.cons.cons₂
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
tail✝ c : List α
hs : Sorted r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
ih : c.erase a <+ insertionSort r tail✝
hm : a ∈ c
⊢ c <+ insertionSort r (a :: tail✝)

Proof state:
case intro.intro.cons.cons₂
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
tail✝ : List α
ih : ∀ {c : List α}, Sorted r c → ∀ (d : List α), d ~ c → d <+ tail✝ → c <+ insertionSort r tail✝
c : List α
hs : Sorted r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
⊢ c <+ insertionSort r (a :: tail✝)

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

Result:
case intro.intro.cons.cons₂
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
tail✝ c : List α
hs : Sorted r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
ih : c.erase a <+ insertionSort r tail✝
⊢ c <+ insertionSort r (a :: tail✝)

Proof state:
case intro.intro.cons
α : Type u
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
tail✝ : List α
ih : ∀ {c : List α}, Sorted r c → ∀ (d : List α), d ~ c → d <+ tail✝ → c <+ insertionSort r tail✝
c : List α
hs : Sorted r c
d : List α
hc : d ~ c
hd : d <+ a :: tail✝
⊢ c <+ insertionSort r (a :: tail✝)

Tactic:
cases hd with
| cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
| 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 (sorted_insertionSort ..)

Result:
no goals