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

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a a' : α
as : List α
h' : f a' a = true
h : Sorted f [a']
⊢ f a' (insert f a [])[0] = true
Tactic:
simpa [insert]
State after:
no goals

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a a' : α
as : List α
h' : f a' a = true
a'' : α
as' : List α
h : Sorted f (a' :: a'' :: as')
h'' : f a a'' = true
⊢ f a' (insert f a (a'' :: as'))[0] = true
Tactic:
simpa [insert, h'']
State after:
no goals

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a a' : α
as : List α
h' : f a' a = true
a'' : α
as' : List α
h : Sorted f (a' :: a'' :: as')
h'' : f a a'' = false
⊢ f a' (insert f a (a'' :: as'))[0] = true
Tactic:
simp [insert, h'']
State after:
α : Type
f : α → α → Bool
r : α → α → Prop
a a' : α
as : List α
h' : f a' a = true
a'' : α
as' : List α
h : Sorted f (a' :: a'' :: as')
h'' : f a a'' = false
⊢ f a' a'' = true

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a a' : α
as : List α
h' : f a' a = true
a'' : α
as' : List α
h : Sorted f (a' :: a'' :: as')
h'' : f a a'' = false
⊢ f a' a'' = true
Tactic:
apply ordered_of_sorted f h
State after:
no goals