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

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
x : Array α
a : α
p : α → Bool
⊢ any (push x a) p 0 (size (push x a)) = (any x p 0 (size x) || p a)
Tactic:
induction x using cons_induction with
| empty =>
  simp only [push_empty_eq_cons, any_cons, any_empty, Bool.or_false, Bool.false_or]
| cons b x IH =>
  simp only [push_cons_eq_cons_push, any_cons, IH]
  exact Eq.symm <| Bool.or_assoc (p b) (x.any p) (p a)
State after:
no goals

State before:
case empty
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
p : α → Bool
⊢ any (push #[] a) p 0 (size (push #[] a)) = (any #[] p 0 (size #[]) || p a)
Tactic:
simp only [push_empty_eq_cons, any_cons, any_empty, Bool.or_false, Bool.false_or]
State after:
no goals

State before:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
p : α → Bool
b : α
x : Array α
IH : any (push x a) p 0 (size (push x a)) = (any x p 0 (size x) || p a)
⊢ any (push (cons b x) a) p 0 (size (push (cons b x) a)) = (any (cons b x) p 0 (size (cons b x)) || p a)
Tactic:
simp only [push_cons_eq_cons_push, any_cons, IH]
State after:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
p : α → Bool
b : α
x : Array α
IH : any (push x a) p 0 (size (push x a)) = (any x p 0 (size x) || p a)
⊢ (p b || (any x p 0 (size x) || p a)) = (p b || any x p 0 (size x) || p a)

State before:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
p : α → Bool
b : α
x : Array α
IH : any (push x a) p 0 (size (push x a)) = (any x p 0 (size x) || p a)
⊢ (p b || (any x p 0 (size x) || p a)) = (p b || any x p 0 (size x) || p a)
Tactic:
exact Eq.symm <| Bool.or_assoc (p b) (x.any p) (p a)
State after:
no goals