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

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
x : Array α
p : α → Bool
⊢ any x p 0 (size x) = List.any x.data p
Tactic:
induction x using cons_induction with
| empty => rfl
| cons a x IH =>
  conv => lhs; simp only [any_cons]
  conv => rhs; simp only [data_cons, List.any_cons]
  rw [IH]
State after:
no goals

State before:
case empty
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
⊢ any #[] p 0 (size #[]) = List.any #[].data p
Tactic:
rfl
State after:
no goals

State before:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
a : α
x : Array α
IH : any x p 0 (size x) = List.any x.data p
⊢ any (cons a x) p 0 (size (cons a x)) = List.any (cons a x).data p
Tactic:
conv => lhs; simp only [any_cons]
State after:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
a : α
x : Array α
IH : any x p 0 (size x) = List.any x.data p
⊢ (p a || any x p 0 (size x)) = List.any (cons a x).data p

State before:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
a : α
x : Array α
IH : any x p 0 (size x) = List.any x.data p
⊢ (p a || any x p 0 (size x)) = List.any (cons a x).data p
Tactic:
conv => rhs; simp only [data_cons, List.any_cons]
State after:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
a : α
x : Array α
IH : any x p 0 (size x) = List.any x.data p
⊢ (p a || any x p 0 (size x)) = (p a || List.any x.data p)

State before:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
a : α
x : Array α
IH : any x p 0 (size x) = List.any x.data p
⊢ (p a || any x p 0 (size x)) = (p a || List.any x.data p)
Tactic:
rw [IH]
State after:
no goals