-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_allM
    {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type u}
    (f : γ → α → m Bool) (xs : Array α) (start stop : Nat) (hmono : monotone f) :
    monotone (fun x => xs.allM (f x) start stop)

Proof state:
case hmono₁.hmono.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
y : α
⊢ monotone fun x => do
    let __do_lift ← f x y
    pure !__do_lift

Tactic:
apply monotone_bind

Result:
case hmono₁.hmono.h.hmono₁
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
y : α
⊢ monotone fun x => f x y

case hmono₁.hmono.h.hmono₂
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
y : α
⊢ monotone fun x __do_lift => pure !__do_lift

Proof state:
case hmono₁.hmono.h.hmono₁
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
y : α
⊢ monotone fun x => f x y

Tactic:
apply monotone_apply

Result:
case hmono₁.hmono.h.hmono₁.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
y : α
⊢ monotone f

Proof state:
case hmono₁.hmono
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x v => do
    let __do_lift ← f x v
    pure !__do_lift

Tactic:
apply monotone_of_monotone_apply

Result:
case hmono₁.hmono.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ ∀ (y : α),
    monotone fun x => do
      let __do_lift ← f x y
      pure !__do_lift

Proof state:
case hmono₁
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x =>
    Array.anyM
      (fun v => do
        let __do_lift ← f x v
        pure !__do_lift)
      xs start stop

Tactic:
apply monotone_anyM

Result:
case hmono₁.hmono
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x v => do
    let __do_lift ← f x v
    pure !__do_lift

Proof state:
case hmono₁.hmono.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ ∀ (y : α),
    monotone fun x => do
      let __do_lift ← f x y
      pure !__do_lift

Tactic:
intro y

Result:
case hmono₁.hmono.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
y : α
⊢ monotone fun x => do
    let __do_lift ← f x y
    pure !__do_lift

Proof state:
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x => Array.allM (f x) xs start stop

Tactic:
unfold Array.allM

Result:
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x => do
    let __do_lift ←
      Array.anyM
          (fun v => do
            let __do_lift ← f x v
            pure !__do_lift)
          xs start stop
    pure !__do_lift

Proof state:
case hmono₂
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x __do_lift => pure !__do_lift

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case hmono₁.hmono.h.hmono₂
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
y : α
⊢ monotone fun x __do_lift => pure !__do_lift

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case hmono₁.hmono.h.hmono₁.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
y : α
⊢ monotone f

Tactic:
apply hmono

Result:
no goals

Proof state:
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x => do
    let __do_lift ←
      Array.anyM
          (fun v => do
            let __do_lift ← f x v
            pure !__do_lift)
          xs start stop
    pure !__do_lift

Tactic:
apply monotone_bind

Result:
case hmono₁
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x =>
    Array.anyM
      (fun v => do
        let __do_lift ← f x v
        pure !__do_lift)
      xs start stop

case hmono₂
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x __do_lift => pure !__do_lift