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

Proof state:
case case1
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
i : Nat
x✝¹ x✝ : 0 ≤ xs.size
⊢ monotone fun x => pure none

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case case2.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
i i✝ : Nat
h✝ : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
x✝ : i✝.succ ≤ xs.size
ih : monotone fun x => Array.findSomeRevM?.find (f x) xs i✝ ⋯
⊢ monotone fun x r =>
    match r with
    | some val => pure r
    | none =>
      let_fun this := ⋯;
      Array.findSomeRevM?.find (f x) xs i✝ this

Tactic:
apply monotone_of_monotone_apply

Result:
case case2.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
i i✝ : Nat
h✝ : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
x✝ : i✝.succ ≤ xs.size
ih : monotone fun x => Array.findSomeRevM?.find (f x) xs i✝ ⋯
⊢ ∀ (y : Option β),
    monotone fun x =>
      match y with
      | some val => pure y
      | none =>
        let_fun this := ⋯;
        Array.findSomeRevM?.find (f x) xs i✝ this

Proof state:
case case2.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
i i✝ : Nat
h✝ : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
x✝ : i✝.succ ≤ xs.size
ih : monotone fun x => Array.findSomeRevM?.find (f x) xs i✝ ⋯
⊢ ∀ (y : Option β),
    monotone fun x =>
      match y with
      | some val => pure y
      | none =>
        let_fun this := ⋯;
        Array.findSomeRevM?.find (f x) xs i✝ this

Tactic:
intro y

Result:
case case2.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
i i✝ : Nat
h✝ : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
x✝ : i✝.succ ≤ xs.size
ih : monotone fun x => Array.findSomeRevM?.find (f x) xs i✝ ⋯
y : Option β
⊢ monotone fun x =>
    match y with
    | some val => pure y
    | none =>
      let_fun this := ⋯;
      Array.findSomeRevM?.find (f x) xs i✝ this

Proof state:
case case2.hmono₂.h.none
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
i i✝ : Nat
h✝ : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
x✝ : i✝.succ ≤ xs.size
ih : monotone fun x => Array.findSomeRevM?.find (f x) xs i✝ ⋯
⊢ monotone fun x =>
    match none with
    | some val => pure none
    | none =>
      let_fun this := ⋯;
      Array.findSomeRevM?.find (f x) xs i✝ this

Tactic:
apply ih

Result:
no goals

Proof state:
case case2
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
i i✝ : Nat
h✝ : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
x✝ : i✝.succ ≤ xs.size
ih : monotone fun x => Array.findSomeRevM?.find (f x) xs i✝ ⋯
⊢ monotone fun x => Array.findSomeRevM?.find (f x) xs i✝.succ h✝

Tactic:
unfold Array.findSomeRevM?.find

Result:
case case2
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
i i✝ : Nat
h✝ : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
x✝ : i✝.succ ≤ xs.size
ih : monotone fun x => Array.findSomeRevM?.find (f x) xs i✝ ⋯
⊢ monotone fun x =>
    let_fun this := ⋯;
    do
    let r ← f x xs[i✝]
    match r with
      | some val => pure r
      | none =>
        let_fun this := ⋯;
        Array.findSomeRevM?.find (f x) xs i✝ this

Proof state:
case case2.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
i i✝ : Nat
h✝ : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
x✝ : i✝.succ ≤ xs.size
ih : monotone fun x => Array.findSomeRevM?.find (f x) xs i✝ ⋯
⊢ monotone fun x => f x xs[i✝]

Tactic:
apply monotone_apply

Result:
case case2.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
i i✝ : Nat
h✝ : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
x✝ : i✝.succ ≤ xs.size
ih : monotone fun x => Array.findSomeRevM?.find (f x) xs i✝ ⋯
⊢ monotone f

Proof state:
case case2
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
i i✝ : Nat
h✝ : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
x✝ : i✝.succ ≤ xs.size
ih : monotone fun x => Array.findSomeRevM?.find (f x) xs i✝ ⋯
⊢ monotone fun x =>
    let_fun this := ⋯;
    do
    let r ← f x xs[i✝]
    match r with
      | some val => pure r
      | none =>
        let_fun this := ⋯;
        Array.findSomeRevM?.find (f x) xs i✝ this

Tactic:
apply monotone_bind

Result:
case case2.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
i i✝ : Nat
h✝ : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
x✝ : i✝.succ ≤ xs.size
ih : monotone fun x => Array.findSomeRevM?.find (f x) xs i✝ ⋯
⊢ monotone fun x => f x xs[i✝]

case case2.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
i i✝ : Nat
h✝ : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
x✝ : i✝.succ ≤ xs.size
ih : monotone fun x => Array.findSomeRevM?.find (f x) xs i✝ ⋯
⊢ monotone fun x r =>
    match r with
    | some val => pure r
    | none =>
      let_fun this := ⋯;
      Array.findSomeRevM?.find (f x) xs i✝ this

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 (Option β)
xs : Array α
hmono : monotone f
⊢ ∀ (i : Nat) (h : i ≤ xs.size), monotone fun x => Array.findSomeRevM?.find (f x) xs i h

Tactic:
intros i h

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 (Option β)
xs : Array α
hmono : monotone f
i : Nat
h : i ≤ xs.size
⊢ monotone fun x => Array.findSomeRevM?.find (f x) xs i h