Theorem: Array.mem_cons (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ any (cons b x) (fun x => a == x) 0 (size (cons b x)) = true ↔ a = b ∨ a ∈ x
Tactic:
rewrite [any_cons]
State after:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ (a == b || any x (fun x => a == x) 0 (size x)) = true ↔ a = b ∨ a ∈ x

State before:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ (a == b || any x (fun x => a == x) 0 (size x)) = true ↔ a = b ∨ a ∈ x
Tactic:
simp only [Bool.or_eq_true, beq_iff_eq]
State after:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ a = b ∨ any x (fun x => a == x) 0 (size x) = true ↔ a = b ∨ a ∈ x

State before:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ a = b ∨ any x (fun x => a == x) 0 (size x) = true ↔ a = b ∨ a ∈ x
Tactic:
exact Iff.rfl
State after:
no goals