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

State before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a : α
as : List α
h : Sorted r (a :: as)
⊢ Sorted r as
Tactic:
match h with 
| single => apply nil  
| longer _ h'' => exact h''
State after:
no goals

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

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