Theorem: Notes.sorted_of_insertSort (Notes4/IndPred2.lean)

State before:
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
l : List α
inst✝ : Asymmetric r
a : α
as : List α
⊢ Sorted r (insertSort r (a :: as))
Tactic:
dsimp [insertSort]
State after:
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
l : List α
inst✝ : Asymmetric r
a : α
as : List α
⊢ Sorted r (insert r a (insertSort r as))

State before:
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
l : List α
inst✝ : Asymmetric r
a : α
as : List α
⊢ Sorted r (insert r a (insertSort r as))
Tactic:
apply insert_sorted_of_sorted r <| sorted_of_insertSort as
State after:
no goals