Theorem: Array.anyPair_cons_zero (Algdata/Data/Array/Basic.lean)

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ anyPair (cons a x) p 0 (stop + 1) = (any x (p a) 0 stop || anyPair x p 0 stop)
Tactic:
apply Eq.trans <| anyPairM_cons_zero (m:=Id) a x p
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (do
      let b ← anyM (p a) x 0 stop
      if b = true then pure true else anyPairM x p 0 stop) =
    (any x (p a) 0 stop || anyPair x p 0 stop)

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (do
      let b ← anyM (p a) x 0 stop
      if b = true then pure true else anyPairM x p 0 stop) =
    (any x (p a) 0 stop || anyPair x p 0 stop)
Tactic:
conv =>
  lhs; change if any x (p a) 0 stop = true then true else anyPair x p 0 stop
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (if any x (p a) 0 stop = true then true else anyPair x p 0 stop) = (any x (p a) 0 stop || anyPair x p 0 stop)

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (if any x (p a) 0 stop = true then true else anyPair x p 0 stop) = (any x (p a) 0 stop || anyPair x p 0 stop)
Tactic:
match any x (p a) 0 stop 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
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (if true = true then true else anyPair x p 0 stop) = (true || anyPair x p 0 stop)
Tactic:
simp only [ite_true, Bool.true_or]
State after:
no goals

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