Theorem: Array.nodup_empty (Algdata/Data/Array/Basic.lean)

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
⊢ Nodup #[]
Tactic:
dsimp [Nodup]
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
⊢ anyPair #[] BEq.beq 0 (size #[]) = false

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
⊢ anyPair #[] BEq.beq 0 (size #[]) = false
Tactic:
exact anyPair_empty BEq.beq
State after:
no goals