Theorem: LoVe.Not_Sorted_17_13 (LoVe/Lectures/LoVe06_InductivePredicates_Demo.lean)

State before:
⊢ ¬Sorted [17, 13]
Tactic:
intro h
State after:
h : Sorted [17, 13]
⊢ False

State before:
h : Sorted [17, 13]
⊢ False
Tactic:
cases h with
| two_or_more _ _ hlet hsorted => simp at hlet
State after:
no goals

State before:
case two_or_more
hlet : 17 ≤ 13
hsorted : Sorted [13]
⊢ False
Tactic:
simp at hlet
State after:
no goals