-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
    allM p as = (! ·) <$> anyM ((! ·) <$> p ·) as

Proof state:
case cons.e_a.h
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih : allM p as = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) as
b : Bool
⊢ (match b with
    | true => allM p as
    | false => pure false) =
    (fun x => !x) <$>
      match !b with
      | true => pure true
      | false => anyM (fun x => (fun x => !x) <$> p x) as

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : List α
⊢ allM p as = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) as

Tactic:
induction as with
| nil => simp
| cons a as ih =>
  simp only [allM, anyM, bind_map_left, _root_.map_bind]
  congr
  funext b
  split <;> simp_all

Result:
no goals

Proof state:
case cons
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih : allM p as = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) as
⊢ allM p (a :: as) = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) (a :: as)

Tactic:
simp only [allM, anyM, bind_map_left, _root_.map_bind]

Result:
case cons
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih : allM p as = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) as
⊢ (do
      let __do_lift ← p a
      match __do_lift with
        | true => allM p as
        | false => pure false) =
    do
    let a ← p a
    (fun x => !x) <$>
        match !a with
        | true => pure true
        | false => anyM (fun x => (fun x => !x) <$> p x) as

Proof state:
case cons
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih : allM p as = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) as
⊢ (do
      let __do_lift ← p a
      match __do_lift with
        | true => allM p as
        | false => pure false) =
    do
    let a ← p a
    (fun x => !x) <$>
        match !a with
        | true => pure true
        | false => anyM (fun x => (fun x => !x) <$> p x) as

Tactic:
congr

Result:
case cons.e_a
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih : allM p as = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) as
⊢ (fun __do_lift =>
      match __do_lift with
      | true => allM p as
      | false => pure false) =
    fun a =>
    (fun x => !x) <$>
      match !a with
      | true => pure true
      | false => anyM (fun x => (fun x => !x) <$> p x) as

Proof state:
case nil
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
⊢ allM p [] = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) []

Tactic:
simp

Result:
no goals

Proof state:
case cons.e_a
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih : allM p as = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) as
⊢ (fun __do_lift =>
      match __do_lift with
      | true => allM p as
      | false => pure false) =
    fun a =>
    (fun x => !x) <$>
      match !a with
      | true => pure true
      | false => anyM (fun x => (fun x => !x) <$> p x) as

Tactic:
funext b

Result:
case cons.e_a.h
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih : allM p as = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) as
b : Bool
⊢ (match b with
    | true => allM p as
    | false => pure false) =
    (fun x => !x) <$>
      match !b with
      | true => pure true
      | false => anyM (fun x => (fun x => !x) <$> p x) as