-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Monadic.lean
theorem satisfiesM_foldrM [Monad m] [LawfulMonad m] {f : α → β → m β} (h₀ : motive b)
    (h₁ : ∀ (a : α) (_ : a ∈ l) (b) (_ : motive b), SatisfiesM motive (f a b)) :
    SatisfiesM motive (List.foldrM f b l)

Proof state:
case cons.hx
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
motive : β → Prop
b : β
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
h₀ : motive b
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)) → SatisfiesM motive (foldrM f b tl)
h₁ : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)
⊢ SatisfiesM (fun a => SatisfiesM motive (f hd a)) (foldrM f b tl)

Tactic:
let ⟨q, qh⟩ := ih (fun a am b hb => h₁ a (mem_cons_of_mem hd am) b hb)

Result:
case cons.hx
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
motive : β → Prop
b : β
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
h₀ : motive b
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)) → SatisfiesM motive (foldrM f b tl)
h₁ : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)
q : m { a // motive a }
qh : Subtype.val <$> q = foldrM f b tl
⊢ SatisfiesM (fun a => SatisfiesM motive (f hd a)) (foldrM f b tl)

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
motive : β → Prop
b : β
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
h₀ : motive b
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)) → SatisfiesM motive (foldrM f b tl)
h₁ : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)
⊢ SatisfiesM motive (foldrM f b (hd :: tl))

Tactic:
simp only [foldrM_cons]

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
motive : β → Prop
b : β
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
h₀ : motive b
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)) → SatisfiesM motive (foldrM f b tl)
h₁ : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)
⊢ SatisfiesM motive (foldrM f b tl >>= f hd)

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
motive : β → Prop
b : β
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
h₀ : motive b
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)) → SatisfiesM motive (foldrM f b tl)
h₁ : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)
⊢ SatisfiesM motive (foldrM f b tl >>= f hd)

Tactic:
apply SatisfiesM.bind_pre

Result:
case cons.hx
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
motive : β → Prop
b : β
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
h₀ : motive b
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)) → SatisfiesM motive (foldrM f b tl)
h₁ : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)
⊢ SatisfiesM (fun a => SatisfiesM motive (f hd a)) (foldrM f b tl)

Proof state:
case cons.hx
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
motive : β → Prop
b : β
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
h₀ : motive b
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)) → SatisfiesM motive (foldrM f b tl)
h₁ : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)
q : m { a // motive a }
qh : Subtype.val <$> q = foldrM f b tl
⊢ SatisfiesM (fun a => SatisfiesM motive (f hd a)) (foldrM f b tl)

Tactic:
exact ⟨(fun ⟨b, bh⟩ => ⟨b, h₁ hd (mem_cons_self hd tl) b bh⟩) <$> q,
  by simpa using qh⟩

Result:
no goals

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
motive : β → Prop
b : β
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
h₀ : motive b
h₁ : ∀ (a : α), a ∈ [] → ∀ (b : β), motive b → SatisfiesM motive (f a b)
⊢ SatisfiesM motive (foldrM f b [])

Tactic:
exact SatisfiesM.pure h₀

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
motive : β → Prop
b : β
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
h₀ : motive b
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)) → SatisfiesM motive (foldrM f b tl)
h₁ : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), motive b → SatisfiesM motive (f a b)
q : m { a // motive a }
qh : Subtype.val <$> q = foldrM f b tl
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | ⟨b, bh⟩ => ⟨b, ⋯⟩) <$>
        q =
    foldrM f b tl

Tactic:
simpa using qh

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
motive : β → Prop
l : List α
b : β
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
h₀ : motive b
h₁ : ∀ (a : α), a ∈ l → ∀ (b : β), motive b → SatisfiesM motive (f a b)
⊢ SatisfiesM motive (foldrM f b l)

Tactic:
induction l with
| nil => exact SatisfiesM.pure h₀
| cons hd tl ih =>
  simp only [foldrM_cons]
  apply SatisfiesM.bind_pre
  let ⟨q, qh⟩ := ih (fun a am b hb => h₁ a (mem_cons_of_mem hd am) b hb)
  exact ⟨(fun ⟨b, bh⟩ => ⟨b, h₁ hd (mem_cons_self hd tl) b bh⟩) <$> q,
    by simpa using qh⟩

Result:
no goals