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

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

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

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