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

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 α
hmono : monotone f
⊢ ∀ (y : α),
    monotone fun x r =>
      let r := r.snd;
      let i := r;
      do
      let __do_lift ← f x y
      let __do_jp : Nat → PUnit → m (ForInStep (MProd (Option (Option Nat)) Nat)) := fun i y =>
        let i := i + 1;
        do
        pure PUnit.unit
        pure (ForInStep.yield ⟨none, i⟩)
      if __do_lift = true then pure (ForInStep.done ⟨some (some i), i⟩)
        else do
          let y ← pure PUnit.unit
          __do_jp i y

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 α
hmono : monotone f
y : α
⊢ monotone fun x r =>
    let r := r.snd;
    let i := r;
    do
    let __do_lift ← f x y
    let __do_jp : Nat → PUnit → m (ForInStep (MProd (Option (Option Nat)) Nat)) := fun i y =>
      let i := i + 1;
      do
      pure PUnit.unit
      pure (ForInStep.yield ⟨none, i⟩)
    if __do_lift = true then pure (ForInStep.done ⟨some (some i), i⟩)
      else do
        let y ← pure PUnit.unit
        __do_jp i y

Proof state:
case hmono₁.hmono.h.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 α
hmono : monotone f
y : α
r : MProd (Option (Option Nat)) Nat
⊢ monotone fun x __do_lift =>
    let __do_jp := fun i y =>
      let i := i + 1;
      do
      pure PUnit.unit
      pure (ForInStep.yield ⟨none, i⟩);
    if __do_lift = true then pure (ForInStep.done ⟨some (some r.snd), r.snd⟩)
    else do
      let y ← pure PUnit.unit
      __do_jp r.snd y

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case hmono₁.hmono.h.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 α
hmono : monotone f
y : α
⊢ ∀ (y_1 : MProd (Option (Option Nat)) Nat),
    monotone fun x =>
      let r := y_1.snd;
      let i := r;
      do
      let __do_lift ← f x y
      let __do_jp : Nat → PUnit → m (ForInStep (MProd (Option (Option Nat)) Nat)) := fun i y =>
        let i := i + 1;
        do
        pure PUnit.unit
        pure (ForInStep.yield ⟨none, i⟩)
      if __do_lift = true then pure (ForInStep.done ⟨some (some i), i⟩)
        else do
          let y ← pure PUnit.unit
          __do_jp i y

Tactic:
intro r

Result:
case hmono₁.hmono.h.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 α
hmono : monotone f
y : α
r : MProd (Option (Option Nat)) Nat
⊢ monotone fun x =>
    let r := r.snd;
    let i := r;
    do
    let __do_lift ← f x y
    let __do_jp : Nat → PUnit → m (ForInStep (MProd (Option (Option Nat)) Nat)) := fun i y =>
      let i := i + 1;
      do
      pure PUnit.unit
      pure (ForInStep.yield ⟨none, i⟩)
    if __do_lift = true then pure (ForInStep.done ⟨some (some i), i⟩)
      else do
        let y ← pure PUnit.unit
        __do_jp i y

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

Tactic:
apply monotone_apply

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

Proof state:
case hmono₁.hmono.h.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 α
hmono : monotone f
y : α
r : MProd (Option (Option Nat)) Nat
⊢ monotone fun x =>
    let r := r.snd;
    let i := r;
    do
    let __do_lift ← f x y
    let __do_jp : Nat → PUnit → m (ForInStep (MProd (Option (Option Nat)) Nat)) := fun i y =>
      let i := i + 1;
      do
      pure PUnit.unit
      pure (ForInStep.yield ⟨none, i⟩)
    if __do_lift = true then pure (ForInStep.done ⟨some (some i), i⟩)
      else do
        let y ← pure PUnit.unit
        __do_jp i y

Tactic:
apply monotone_bind

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

case hmono₁.hmono.h.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 α
hmono : monotone f
y : α
r : MProd (Option (Option Nat)) Nat
⊢ monotone fun x __do_lift =>
    let __do_jp := fun i y =>
      let i := i + 1;
      do
      pure PUnit.unit
      pure (ForInStep.yield ⟨none, i⟩);
    if __do_lift = true then pure (ForInStep.done ⟨some (some r.snd), r.snd⟩)
    else do
      let y ← pure PUnit.unit
      __do_jp r.snd y

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

Tactic:
apply hmono

Result:
no goals

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 α
hmono : monotone f
y : α
⊢ monotone fun x r =>
    let r := r.snd;
    let i := r;
    do
    let __do_lift ← f x y
    let __do_jp : Nat → PUnit → m (ForInStep (MProd (Option (Option Nat)) Nat)) := fun i y =>
      let i := i + 1;
      do
      pure PUnit.unit
      pure (ForInStep.yield ⟨none, i⟩)
    if __do_lift = true then pure (ForInStep.done ⟨some (some i), i⟩)
      else do
        let y ← pure PUnit.unit
        __do_jp i y

Tactic:
apply monotone_of_monotone_apply

Result:
case hmono₁.hmono.h.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 α
hmono : monotone f
y : α
⊢ ∀ (y_1 : MProd (Option (Option Nat)) Nat),
    monotone fun x =>
      let r := y_1.snd;
      let i := r;
      do
      let __do_lift ← f x y
      let __do_jp : Nat → PUnit → m (ForInStep (MProd (Option (Option Nat)) Nat)) := fun i y =>
        let i := i + 1;
        do
        pure PUnit.unit
        pure (ForInStep.yield ⟨none, i⟩)
      if __do_lift = true then pure (ForInStep.done ⟨some (some i), i⟩)
        else do
          let y ← pure PUnit.unit
          __do_jp i y