-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem anyM_toList [Monad m] (p : α → m Bool) (as : Array α) :
    as.toList.anyM p = as.anyM p :=
  match as with
  | ⟨[]⟩  => rfl
  | ⟨a :: as⟩ => by
    simp only [List.anyM, anyM, size_toArray, List.length_cons, Nat.le_refl, ↓reduceDIte]
    rw [anyM.loop, dif_pos (by omega)]
    congr 1
    funext b
    split
    · simp
    · simp only [Bool.false_eq_true, ↓reduceIte]
      rw [anyM_loop_cons]
      simpa [anyM] using anyM_toList p ⟨as⟩

Proof state:
case e_a
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
⊢ (fun __do_lift =>
      match __do_lift with
      | true => pure true
      | false => List.anyM p as) =
    fun __do_lift => if __do_lift = true then pure true else anyM.loop p { toList := a :: as } (as.length + 1) ⋯ (0 + 1)

Tactic:
funext b

Result:
case e_a.h
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
b : Bool
⊢ (match b with
    | true => pure true
    | false => List.anyM p as) =
    if b = true then pure true else anyM.loop p { toList := a :: as } (as.length + 1) ⋯ (0 + 1)

Proof state:
case e_a.h.h_2
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
__do_lift✝ : Bool
⊢ List.anyM p as = anyM.loop p { toList := a :: as } (as.length + 1) ⋯ (0 + 1)

Tactic:
rw [anyM_loop_cons]

Result:
case e_a.h.h_2
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
__do_lift✝ : Bool
⊢ List.anyM p as = anyM.loop p { toList := as } as.length ⋯ 0

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
⊢ (do
      let __do_lift ← p a
      match __do_lift with
        | true => pure true
        | false => List.anyM p as) =
    let_fun this := ⋯;
    do
    let __do_lift ← p { toList := a :: as }[0]
    if __do_lift = true then pure true else anyM.loop p { toList := a :: as } (as.length + 1) ⋯ (0 + 1)

Tactic:
congr 1

Result:
case e_a
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
⊢ (fun __do_lift =>
      match __do_lift with
      | true => pure true
      | false => List.anyM p as) =
    fun __do_lift => if __do_lift = true then pure true else anyM.loop p { toList := a :: as } (as.length + 1) ⋯ (0 + 1)

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
⊢ (do
      let __do_lift ← p a
      match __do_lift with
        | true => pure true
        | false => List.anyM p as) =
    anyM.loop p { toList := a :: as } (as.length + 1) ⋯ 0

Tactic:
rw [anyM.loop, dif_pos (by omega)]

Result:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
⊢ (do
      let __do_lift ← p a
      match __do_lift with
        | true => pure true
        | false => List.anyM p as) =
    let_fun this := ⋯;
    do
    let __do_lift ← p { toList := a :: as }[0]
    if __do_lift = true then pure true else anyM.loop p { toList := a :: as } (as.length + 1) ⋯ (0 + 1)

Proof state:
case e_a.h
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
b : Bool
⊢ (match b with
    | true => pure true
    | false => List.anyM p as) =
    if b = true then pure true else anyM.loop p { toList := a :: as } (as.length + 1) ⋯ (0 + 1)

Tactic:
split

Result:
case e_a.h.h_1
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
__do_lift✝ : Bool
⊢ pure true = if true = true then pure true else anyM.loop p { toList := a :: as } (as.length + 1) ⋯ (0 + 1)

case e_a.h.h_2
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
__do_lift✝ : Bool
⊢ List.anyM p as = if false = true then pure true else anyM.loop p { toList := a :: as } (as.length + 1) ⋯ (0 + 1)

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
⊢ List.anyM p { toList := a :: as }.toList = anyM p { toList := a :: as }

Tactic:
simp only [List.anyM, anyM, size_toArray, List.length_cons, Nat.le_refl, ↓reduceDIte]

Result:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
⊢ (do
      let __do_lift ← p a
      match __do_lift with
        | true => pure true
        | false => List.anyM p as) =
    anyM.loop p { toList := a :: as } (as.length + 1) ⋯ 0

Proof state:
case e_a.h.h_2
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
__do_lift✝ : Bool
⊢ List.anyM p as = if false = true then pure true else anyM.loop p { toList := a :: as } (as.length + 1) ⋯ (0 + 1)

Tactic:
simp only [Bool.false_eq_true, ↓reduceIte]

Result:
case e_a.h.h_2
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
__do_lift✝ : Bool
⊢ List.anyM p as = anyM.loop p { toList := a :: as } (as.length + 1) ⋯ (0 + 1)

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
⊢ 0 < as.length + 1

Tactic:
omega

Result:
no goals

Proof state:
case e_a.h.h_1
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
__do_lift✝ : Bool
⊢ pure true = if true = true then pure true else anyM.loop p { toList := a :: as } (as.length + 1) ⋯ (0 + 1)

Tactic:
simp

Result:
no goals

Proof state:
case e_a.h.h_2
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as✝ : Array α
a : α
as : List α
__do_lift✝ : Bool
⊢ List.anyM p as = anyM.loop p { toList := as } as.length ⋯ 0

Tactic:
simpa [anyM] using anyM_toList p ⟨as⟩

Result:
no goals