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

Proof state:
case cons.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 β
hmono : monotone f
head✝ : α
xs : List α
⊢ monotone fun x __do_lift => List.mapM.loop (f x) xs [__do_lift]

Tactic:
apply monotone_of_monotone_apply

Result:
case cons.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 β
hmono : monotone f
head✝ : α
xs : List α
⊢ ∀ (y : β), monotone fun x => List.mapM.loop (f x) xs [y]

Proof state:
case cons.hmono₂.h.cons.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 β
hmono : monotone f
head✝¹ : α
y : β
head✝ : α
tail✝ : List α
ih : ∀ (ys : List β), monotone fun x => List.mapM.loop (f x) tail✝ ys
ys : List β
⊢ monotone f

Tactic:
apply hmono

Result:
no goals

Proof state:
case cons.hmono₂.h.cons.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 β
hmono : monotone f
head✝¹ : α
y✝ : β
head✝ : α
tail✝ : List α
ih : ∀ (ys : List β), monotone fun x => List.mapM.loop (f x) tail✝ ys
ys : List β
y : β
⊢ monotone fun x => List.mapM.loop (f x) tail✝ (y :: ys)

Tactic:
apply ih

Result:
no goals

Proof state:
case cons.hmono₂.h.cons
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m β
hmono : monotone f
head✝¹ : α
y : β
head✝ : α
tail✝ : List α
ih : ∀ (ys : List β), monotone fun x => List.mapM.loop (f x) tail✝ ys
ys : List β
⊢ monotone fun x => List.mapM.loop (f x) (head✝ :: tail✝) ys

Tactic:
apply monotone_bind

Result:
case cons.hmono₂.h.cons.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 β
hmono : monotone f
head✝¹ : α
y : β
head✝ : α
tail✝ : List α
ih : ∀ (ys : List β), monotone fun x => List.mapM.loop (f x) tail✝ ys
ys : List β
⊢ monotone fun x => f x head✝

case cons.hmono₂.h.cons.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 β
hmono : monotone f
head✝¹ : α
y : β
head✝ : α
tail✝ : List α
ih : ∀ (ys : List β), monotone fun x => List.mapM.loop (f x) tail✝ ys
ys : List β
⊢ monotone fun x __do_lift => List.mapM.loop (f x) tail✝ (__do_lift :: ys)

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

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case cons.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 β
hmono : monotone f
head✝ : α
xs : List α
⊢ ∀ (y : β), monotone fun x => List.mapM.loop (f x) xs [y]

Tactic:
intro y

Result:
case cons.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 β
hmono : monotone f
head✝ : α
xs : List α
y : β
⊢ monotone fun x => List.mapM.loop (f x) xs [y]

Proof state:
case cons.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 β
hmono : monotone f
head✝ : α
xs : List α
⊢ monotone f

Tactic:
apply hmono

Result:
no goals

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

Tactic:
apply monotone_bind

Result:
case cons.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 β
hmono : monotone f
head✝ : α
xs : List α
⊢ monotone fun x => f x head✝

case cons.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 β
hmono : monotone f
head✝ : α
xs : List α
⊢ monotone fun x __do_lift => List.mapM.loop (f x) xs [__do_lift]

Proof state:
case cons.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 β
hmono : monotone f
head✝ : α
xs : List α
y : β
⊢ monotone fun x => List.mapM.loop (f x) xs [y]

Tactic:
generalize [y] = ys

Result:
case cons.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 β
hmono : monotone f
head✝ : α
xs : List α
y : β
ys : List β
⊢ monotone fun x => List.mapM.loop (f x) xs ys

Proof state:
case cons.hmono₂.h.cons.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 β
hmono : monotone f
head✝¹ : α
y : β
head✝ : α
tail✝ : List α
ih : ∀ (ys : List β), monotone fun x => List.mapM.loop (f x) tail✝ ys
ys : List β
⊢ ∀ (y : β), monotone fun x => List.mapM.loop (f x) tail✝ (y :: ys)

Tactic:
intro y

Result:
case cons.hmono₂.h.cons.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 β
hmono : monotone f
head✝¹ : α
y✝ : β
head✝ : α
tail✝ : List α
ih : ∀ (ys : List β), monotone fun x => List.mapM.loop (f x) tail✝ ys
ys : List β
y : β
⊢ monotone fun x => List.mapM.loop (f x) tail✝ (y :: ys)

Proof state:
case cons.hmono₂.h.cons.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 β
hmono : monotone f
head✝¹ : α
y : β
head✝ : α
tail✝ : List α
ih : ∀ (ys : List β), monotone fun x => List.mapM.loop (f x) tail✝ ys
ys : List β
⊢ monotone fun x => f x head✝

Tactic:
apply monotone_apply

Result:
case cons.hmono₂.h.cons.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 β
hmono : monotone f
head✝¹ : α
y : β
head✝ : α
tail✝ : List α
ih : ∀ (ys : List β), monotone fun x => List.mapM.loop (f x) tail✝ ys
ys : List β
⊢ monotone f

Proof state:
case cons.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 β
hmono : monotone f
head✝ : α
xs : List α
⊢ monotone fun x => f x head✝

Tactic:
apply monotone_apply

Result:
case cons.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 β
hmono : monotone f
head✝ : α
xs : List α
⊢ monotone f