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

Proof state:
case hmono₁.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 a r =>
    let r := r.snd;
    do
    let __do_lift ← f x a
    match __do_lift with
      | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
      | x => do
        pure PUnit.unit
        pure (ForInStep.yield ⟨none, PUnit.unit⟩)

Tactic:
apply monotone_of_monotone_apply

Result:
case hmono₁.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 : α),
    monotone fun x r =>
      let r := r.snd;
      do
      let __do_lift ← f x y
      match __do_lift with
        | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
        | x => do
          pure PUnit.unit
          pure (ForInStep.yield ⟨none, PUnit.unit⟩)

Proof state:
case hmono₁.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 : α
r : MProd (Option (Option β)) PUnit
⊢ monotone fun x => f x y

Tactic:
apply monotone_apply

Result:
case hmono₁.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 : α
r : MProd (Option (Option β)) PUnit
⊢ monotone f

Proof state:
case hmono₁.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 : α
⊢ ∀ (y_1 : MProd (Option (Option β)) PUnit),
    monotone fun x =>
      let r := y_1.snd;
      do
      let __do_lift ← f x y
      match __do_lift with
        | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
        | x => do
          pure PUnit.unit
          pure (ForInStep.yield ⟨none, PUnit.unit⟩)

Tactic:
intro r

Result:
case hmono₁.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 : α
r : MProd (Option (Option β)) PUnit
⊢ monotone fun x =>
    let r := r.snd;
    do
    let __do_lift ← f x y
    match __do_lift with
      | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
      | x => do
        pure PUnit.unit
        pure (ForInStep.yield ⟨none, PUnit.unit⟩)

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 r =>
    let __do_jp := fun y => pure none;
    match r.fst with
    | none => do
      let y ← pure PUnit.unit
      __do_jp y
    | some a => pure a

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case hmono₁.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 : α
r : MProd (Option (Option β)) PUnit
⊢ monotone fun x __do_lift =>
    match __do_lift with
    | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
    | x => do
      pure PUnit.unit
      pure (ForInStep.yield ⟨none, PUnit.unit⟩)

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case hmono₁.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 : α
r : MProd (Option (Option β)) PUnit
⊢ monotone fun x =>
    let r := r.snd;
    do
    let __do_lift ← f x y
    match __do_lift with
      | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
      | x => do
        pure PUnit.unit
        pure (ForInStep.yield ⟨none, PUnit.unit⟩)

Tactic:
apply monotone_bind

Result:
case hmono₁.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 : α
r : MProd (Option (Option β)) PUnit
⊢ monotone fun x => f x y

case hmono₁.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 : α
r : MProd (Option (Option β)) PUnit
⊢ monotone fun x __do_lift =>
    match __do_lift with
    | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
    | x => do
      pure PUnit.unit
      pure (ForInStep.yield ⟨none, PUnit.unit⟩)

Proof state:
case hmono₁.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 : α
⊢ monotone fun x r =>
    let r := r.snd;
    do
    let __do_lift ← f x y
    match __do_lift with
      | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
      | x => do
        pure PUnit.unit
        pure (ForInStep.yield ⟨none, PUnit.unit⟩)

Tactic:
apply monotone_of_monotone_apply

Result:
case hmono₁.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 : α
⊢ ∀ (y_1 : MProd (Option (Option β)) PUnit),
    monotone fun x =>
      let r := y_1.snd;
      do
      let __do_lift ← f x y
      match __do_lift with
        | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
        | x => do
          pure PUnit.unit
          pure (ForInStep.yield ⟨none, PUnit.unit⟩)

Proof state:
case hmono₁.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 : α
r : MProd (Option (Option β)) PUnit
⊢ monotone f

Tactic:
apply hmono

Result:
no goals

Proof state:
case hmono₁.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 : α),
    monotone fun x r =>
      let r := r.snd;
      do
      let __do_lift ← f x y
      match __do_lift with
        | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
        | x => do
          pure PUnit.unit
          pure (ForInStep.yield ⟨none, PUnit.unit⟩)

Tactic:
intro y

Result:
case hmono₁.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 : α
⊢ monotone fun x r =>
    let r := r.snd;
    do
    let __do_lift ← f x y
    match __do_lift with
      | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
      | x => do
        pure PUnit.unit
        pure (ForInStep.yield ⟨none, PUnit.unit⟩)