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

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

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