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

State before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
h : Sorted r [a']
⊢ r a' (insert r a [])[0]
Tactic:
simp [insert]
State after:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
h : Sorted r [a']
⊢ r a' a

State before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
h : Sorted r [a']
⊢ r a' a
Tactic:
assumption
State after:
no goals

State before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
a'' : α
as' : List α
h : Sorted r (a' :: a'' :: as')
h'' : r a a''
⊢ r a' (insert r a (a'' :: as'))[0]
Tactic:
simpa [insert, h'']
State after:
no goals

State before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
a'' : α
as' : List α
h : Sorted r (a' :: a'' :: as')
h'' : ¬r a a''
⊢ r a' (insert r a (a'' :: as'))[0]
Tactic:
simp [insert, h'']
State after:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
a'' : α
as' : List α
h : Sorted r (a' :: a'' :: as')
h'' : ¬r a a''
⊢ r a' a''

State before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
a'' : α
as' : List α
h : Sorted r (a' :: a'' :: as')
h'' : ¬r a a''
⊢ r a' a''
Tactic:
apply ordered_of_sorted r h
State after:
no goals