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

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ any (cons a x) p 0 (stop + 1) = (p a || any x p 0 stop)
Tactic:
dsimp [any, Id.run]
State after:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ anyM p (cons a x) 0 (stop + 1) = (p a || anyM p x 0 stop)

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ anyM p (cons a x) 0 (stop + 1) = (p a || anyM p x 0 stop)
Tactic:
rewrite [anyM_cons_zero (m:=Id) p a x]
State after:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (do
      let b ← p a
      if b = true then pure true else anyM p x 0 stop) =
    (p a || anyM p x 0 stop)

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (do
      let b ← p a
      if b = true then pure true else anyM p x 0 stop) =
    (p a || anyM p x 0 stop)
Tactic:
dsimp
State after:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (if p a = true then true else anyM p x 0 stop) = (p a || anyM p x 0 stop)

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (if p a = true then true else anyM p x 0 stop) = (p a || anyM p x 0 stop)
Tactic:
match p a with
| true => simp only [ite_true, Bool.true_or]
| false => simp only [ite_false, Bool.false_or]
State after:
no goals

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (if true = true then true else anyM p x 0 stop) = (true || anyM p x 0 stop)
Tactic:
simp only [ite_true, Bool.true_or]
State after:
no goals

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (if false = true then true else anyM p x 0 stop) = (false || anyM p x 0 stop)
Tactic:
simp only [ite_false, Bool.false_or]
State after:
no goals