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

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ Nodup (cons a x) ↔ ¬a ∈ x ∧ Nodup x
Tactic:
dsimp [Nodup]
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ anyPair (cons a x) BEq.beq 0 (Nat.succ (size x)) = false ↔ ¬a ∈ x ∧ anyPair x BEq.beq 0 (size x) = false

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ anyPair (cons a x) BEq.beq 0 (Nat.succ (size x)) = false ↔ ¬a ∈ x ∧ anyPair x BEq.beq 0 (size x) = false
Tactic:
conv =>
  pattern a ∉ x; change ¬(x.any (BEq.beq a) = true); rw [Bool.not_eq_true]
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ anyPair (cons a x) BEq.beq 0 (Nat.succ (size x)) = false ↔
    any x (BEq.beq a) 0 (size x) = false ∧ anyPair x BEq.beq 0 (size x) = false

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ anyPair (cons a x) BEq.beq 0 (Nat.succ (size x)) = false ↔
    any x (BEq.beq a) 0 (size x) = false ∧ anyPair x BEq.beq 0 (size x) = false
Tactic:
rewrite [anyPair_cons_zero]
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (any x (BEq.beq a) 0 (size x) || anyPair x BEq.beq 0 (size x)) = false ↔
    any x (BEq.beq a) 0 (size x) = false ∧ anyPair x BEq.beq 0 (size x) = false

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (any x (BEq.beq a) 0 (size x) || anyPair x BEq.beq 0 (size x)) = false ↔
    any x (BEq.beq a) 0 (size x) = false ∧ anyPair x BEq.beq 0 (size x) = false
Tactic:
match x.any (BEq.beq a) with
| true => simp only [Bool.true_or, false_and]
| false => simp only [Bool.false_or, true_and]
State after:
no goals

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (true || anyPair x BEq.beq 0 (size x)) = false ↔ true = false ∧ anyPair x BEq.beq 0 (size x) = false
Tactic:
simp only [Bool.true_or, false_and]
State after:
no goals

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (false || anyPair x BEq.beq 0 (size x)) = false ↔ false = false ∧ anyPair x BEq.beq 0 (size x) = false
Tactic:
simp only [Bool.false_or, true_and]
State after:
no goals