-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_foldrM
    (f : γ → α → β → m β) (init : β) (xs : List α) (hmono : monotone f) :
    monotone (fun x => xs.foldrM (f x) (init := init))

Proof state:
case hmono.h.h.h.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
s : β
a : α
⊢ monotone f

Tactic:
apply hmono

Result:
no goals

Proof state:
case hmono.h.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
s : β
⊢ ∀ (y : α), monotone fun x => f x y s

Tactic:
intro a

Result:
case hmono.h.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
s : β
a : α
⊢ monotone fun x => f x a s

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
⊢ monotone fun x => List.foldrM (f x) init xs

Tactic:
apply monotone_foldlM

Result:
case hmono
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
⊢ monotone fun x s a => f x a s

Proof state:
case hmono
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
⊢ monotone fun x s a => f x a s

Tactic:
apply monotone_of_monotone_apply

Result:
case hmono.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
⊢ ∀ (y : β), monotone fun x a => f x a y

Proof state:
case hmono.h.h.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
s : β
a : α
⊢ monotone fun x => f x a

Tactic:
apply monotone_apply (a := a)

Result:
case hmono.h.h.h.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
s : β
a : α
⊢ monotone f

Proof state:
case hmono.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
s : β
⊢ monotone fun x a => f x a s

Tactic:
apply monotone_of_monotone_apply

Result:
case hmono.h.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
s : β
⊢ ∀ (y : α), monotone fun x => f x y s

Proof state:
case hmono.h.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
s : β
a : α
⊢ monotone fun x => f x a s

Tactic:
apply monotone_apply (a := s)

Result:
case hmono.h.h.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
s : β
a : α
⊢ monotone fun x => f x a

Proof state:
case hmono.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
⊢ ∀ (y : β), monotone fun x a => f x a y

Tactic:
intro s

Result:
case hmono.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : List α
hmono : monotone f
s : β
⊢ monotone fun x a => f x a s