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

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

Tactic:
let ⟨q, qh⟩ := h₁ b h₀ hd (mem_cons_self hd tl)

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

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

Tactic:
simp only [foldlM_cons]

Result:
case cons
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
motive : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
hd : α
tl : List α
ih :
  ∀ {b : β},
    motive b →
      (∀ (b : β), motive b → ∀ (a : α), a ∈ tl → SatisfiesM motive (f b a)) → SatisfiesM motive (List.foldlM f b tl)
b : β
h₀ : motive b
h₁ : ∀ (b : β), motive b → ∀ (a : α), a ∈ hd :: tl → SatisfiesM motive (f b a)
⊢ SatisfiesM motive do
    let init ← f b hd
    List.foldlM f init tl

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

Tactic:
exact SatisfiesM.pure h₀

Result:
no goals

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

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

Result:
no goals

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

Tactic:
apply SatisfiesM.bind_pre

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

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

Tactic:
simpa using qh

Result:
no goals

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

Tactic:
exact ⟨(fun ⟨b, bh⟩ => ⟨b, ih bh (fun b bh a am => h₁ b bh a (mem_cons_of_mem hd am))⟩) <$> q,
  by simpa using qh⟩

Result:
no goals