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

Proof state:
case hmono
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : Array α
hmono : monotone f
⊢ monotone fun x a => do
    let __do_lift ← f x a
    pure (if __do_lift = true then some a else none)

Tactic:
apply monotone_of_monotone_apply

Result:
case hmono.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : Array α
hmono : monotone f
⊢ ∀ (y : α),
    monotone fun x => do
      let __do_lift ← f x y
      pure (if __do_lift = true then some y else none)

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

Tactic:
apply monotone_apply

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

Proof state:
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : Array α
hmono : monotone f
⊢ monotone fun x =>
    Array.findSomeRevM?
      (fun a => do
        let __do_lift ← f x a
        pure (if __do_lift = true then some a else none))
      xs

Tactic:
apply monotone_findSomeRevM?

Result:
case hmono
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : Array α
hmono : monotone f
⊢ monotone fun x a => do
    let __do_lift ← f x a
    pure (if __do_lift = true then some a else none)

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

Tactic:
unfold Array.findRevM?

Result:
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : Array α
hmono : monotone f
⊢ monotone fun x =>
    Array.findSomeRevM?
      (fun a => do
        let __do_lift ← f x a
        pure (if __do_lift = true then some a else none))
      xs

Proof state:
case hmono.h.hmono₂
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : Array α
hmono : monotone f
y : α
⊢ monotone fun x __do_lift => pure (if __do_lift = true then some y else none)

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case hmono.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : Array α
hmono : monotone f
⊢ ∀ (y : α),
    monotone fun x => do
      let __do_lift ← f x y
      pure (if __do_lift = true then some y else none)

Tactic:
intro y

Result:
case hmono.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : Array α
hmono : monotone f
y : α
⊢ monotone fun x => do
    let __do_lift ← f x y
    pure (if __do_lift = true then some y else none)

Proof state:
case hmono.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : Array α
hmono : monotone f
y : α
⊢ monotone fun x => do
    let __do_lift ← f x y
    pure (if __do_lift = true then some y else none)

Tactic:
apply monotone_bind

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

case hmono.h.hmono₂
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : Array α
hmono : monotone f
y : α
⊢ monotone fun x __do_lift => pure (if __do_lift = true then some y else none)

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

Tactic:
apply hmono

Result:
no goals