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

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 (Array β)
xs : Array α
hmono : monotone f
y : Array β
⊢ ∀ (y_1 : α),
    monotone fun x => do
      let __do_lift ← f x y_1
      pure (y ++ __do_lift)

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 (Array β)
xs : Array α
hmono : monotone f
y : Array β
z : α
⊢ monotone fun x => do
    let __do_lift ← f x z
    pure (y ++ __do_lift)

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

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

Tactic:
apply hmono

Result:
no goals

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 (Array β)
xs : Array α
hmono : monotone f
⊢ ∀ (y : Array β),
    monotone fun x a => do
      let __do_lift ← f x a
      pure (y ++ __do_lift)

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 (Array β)
xs : Array α
hmono : monotone f
y : Array β
⊢ monotone fun x a => do
    let __do_lift ← f x a
    pure (y ++ __do_lift)

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

Tactic:
unfold Array.flatMapM

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

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 (Array β)
xs : Array α
hmono : monotone f
y : Array β
z : α
⊢ monotone fun x => do
    let __do_lift ← f x z
    pure (y ++ __do_lift)

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 (Array β)
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 (Array β)
xs : Array α
hmono : monotone f
y : Array β
z : α
⊢ monotone fun x __do_lift => pure (y ++ __do_lift)

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 (Array β)
xs : Array α
hmono : monotone f
⊢ monotone fun x bs a => do
    let __do_lift ← f x a
    pure (bs ++ __do_lift)

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 (Array β)
xs : Array α
hmono : monotone f
⊢ ∀ (y : Array β),
    monotone fun x a => do
      let __do_lift ← f x a
      pure (y ++ __do_lift)

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

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 (Array β)
xs : Array α
hmono : monotone f
y : Array β
⊢ monotone fun x a => do
    let __do_lift ← f x a
    pure (y ++ __do_lift)

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 (Array β)
xs : Array α
hmono : monotone f
y : Array β
⊢ ∀ (y_1 : α),
    monotone fun x => do
      let __do_lift ← f x y_1
      pure (y ++ __do_lift)

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 (Array β)
xs : Array α
hmono : monotone f
y : Array β
z : α
⊢ monotone fun x __do_lift => pure (y ++ __do_lift)

Tactic:
apply monotone_const

Result:
no goals