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

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 (Option β)
xs : Array α
hmono : monotone f
y : Array β
⊢ monotone fun x a => do
    let __do_lift ← f x a
    match __do_lift with
      | some b => pure (y.push b)
      | none => pure y

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 (Option β)
xs : Array α
hmono : monotone f
y : Array β
⊢ ∀ (y_1 : α),
    monotone fun x => do
      let __do_lift ← f x y_1
      match __do_lift with
        | some b => pure (y.push b)
        | none => pure y

Proof state:
case hmono.h.h.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 (Option β)
xs : Array α
hmono : monotone f
y : Array β
z : α
⊢ monotone fun x __do_lift =>
    match __do_lift with
    | some b => pure (y.push b)
    | none => pure y

Tactic:
apply monotone_const

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 (Option β)
xs : Array α
hmono : monotone f
y : Array β
⊢ ∀ (y_1 : α),
    monotone fun x => do
      let __do_lift ← f x y_1
      match __do_lift with
        | some b => pure (y.push b)
        | none => pure y

Tactic:
intro z

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 (Option β)
xs : Array α
hmono : monotone f
y : Array β
z : α
⊢ monotone fun x => do
    let __do_lift ← f x z
    match __do_lift with
      | some b => pure (y.push b)
      | none => pure y

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 (Option β)
xs : Array α
hmono : monotone f
⊢ ∀ (y : Array β),
    monotone fun x a => do
      let __do_lift ← f x a
      match __do_lift with
        | some b => pure (y.push b)
        | none => pure y

Tactic:
intro y

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 (Option β)
xs : Array α
hmono : monotone f
y : Array β
⊢ monotone fun x a => do
    let __do_lift ← f x a
    match __do_lift with
      | some b => pure (y.push b)
      | none => pure y

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 (Option β)
xs : Array α
hmono : monotone f
⊢ monotone fun x bs a => do
    let __do_lift ← f x a
    match __do_lift with
      | some b => pure (bs.push b)
      | none => pure bs

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 (Option β)
xs : Array α
hmono : monotone f
⊢ ∀ (y : Array β),
    monotone fun x a => do
      let __do_lift ← f x a
      match __do_lift with
        | some b => pure (y.push b)
        | none => pure y

Proof state:
case hmono.h.h.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 (Option β)
xs : Array α
hmono : monotone f
y : Array β
z : α
⊢ monotone f

Tactic:
apply hmono

Result:
no goals

Proof state:
case hmono.h.h.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 (Option β)
xs : Array α
hmono : monotone f
y : Array β
z : α
⊢ monotone fun x => f x z

Tactic:
apply monotone_apply

Result:
case hmono.h.h.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 (Option β)
xs : Array α
hmono : monotone f
y : Array β
z : α
⊢ monotone f

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 (Option β)
xs : Array α
hmono : monotone f
y : Array β
z : α
⊢ monotone fun x => do
    let __do_lift ← f x z
    match __do_lift with
      | some b => pure (y.push b)
      | none => pure y

Tactic:
apply monotone_bind

Result:
case hmono.h.h.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 (Option β)
xs : Array α
hmono : monotone f
y : Array β
z : α
⊢ monotone fun x => f x z

case hmono.h.h.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 (Option β)
xs : Array α
hmono : monotone f
y : Array β
z : α
⊢ monotone fun x __do_lift =>
    match __do_lift with
    | some b => pure (y.push b)
    | none => pure y

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 (Option β)
xs : Array α
hmono : monotone f
⊢ monotone fun x => Array.filterMapM (f x) xs

Tactic:
unfold Array.filterMapM

Result:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m (Option β)
xs : Array α
hmono : monotone f
⊢ monotone fun x =>
    Array.foldlM
      (fun bs a => do
        let __do_lift ← f x a
        match __do_lift with
          | some b => pure (bs.push b)
          | none => pure bs)
      #[] xs

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 (Option β)
xs : Array α
hmono : monotone f
⊢ monotone fun x =>
    Array.foldlM
      (fun bs a => do
        let __do_lift ← f x a
        match __do_lift with
          | some b => pure (bs.push b)
          | none => pure bs)
      #[] 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 (Option β)
xs : Array α
hmono : monotone f
⊢ monotone fun x bs a => do
    let __do_lift ← f x a
    match __do_lift with
      | some b => pure (bs.push b)
      | none => pure bs