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

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
⊢ any (cons a x) p 0 (size (cons a x)) = (p a || any x p 0 (size x))
Tactic:
rewrite [size_cons]
State after:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
⊢ any (cons a x) p 0 (Nat.succ (size x)) = (p a || any x p 0 (size x))

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
⊢ any (cons a x) p 0 (Nat.succ (size x)) = (p a || any x p 0 (size x))
Tactic:
exact any_cons_zero a x p
State after:
no goals