Theorem: List.nodup_range (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
n : Nat
⊢ Nodup (range n)
Tactic:
rewrite [range_eq_range']
State after:
α : Type u
β : Type v
n : Nat
⊢ Nodup (range' 0 n)

State before:
α : Type u
β : Type v
n : Nat
⊢ Nodup (range' 0 n)
Tactic:
apply nodup_range'
State after:
case hstep
α : Type u
β : Type v
n : Nat
⊢ 1 > 0

State before:
case hstep
α : Type u
β : Type v
n : Nat
⊢ 1 > 0
Tactic:
decide
State after:
no goals