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

State before:
⊢ Sorted [3, 5]
Tactic:
apply Sorted.two_or_more
State after:
case hle

⊢ 3 ≤ 5

case hsorted

⊢ Sorted [5]

State before:
case hle

⊢ 3 ≤ 5

case hsorted

⊢ Sorted [5]
Tactic:
{ simp }
State after:
case hsorted

⊢ Sorted [5]

State before:
case hsorted

⊢ Sorted [5]
Tactic:
{ exact Sorted.single _ }
State after:
no goals

State before:
case hle

⊢ 3 ≤ 5
Tactic:
simp
State after:
no goals

State before:
case hsorted

⊢ Sorted [5]
Tactic:
exact Sorted.single _
State after:
no goals