-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_foldrM_fold
    (f : γ → α → β → m β) (xs : Array α) (stop i : Nat) (h : i ≤ xs.size) (b : β)
    (hmono : monotone f) : monotone (fun x => Array.foldrM.fold (f x) xs stop i h b)

Proof state:
case case3.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 β
xs : Array α
stop i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝² : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
h✝¹ : i✝.succ ≤ xs.size
h✝ : ¬(i✝.succ == stop) = true
ih : ∀ (__do_lift : β), monotone fun x => Array.foldrM.fold (f x) xs stop i✝ ⋯ __do_lift
⊢ monotone fun x => f x xs[i✝] b✝

Tactic:
apply monotone_apply

Result:
case case3.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 β
xs : Array α
stop i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝² : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
h✝¹ : i✝.succ ≤ xs.size
h✝ : ¬(i✝.succ == stop) = true
ih : ∀ (__do_lift : β), monotone fun x => Array.foldrM.fold (f x) xs stop i✝ ⋯ __do_lift
⊢ monotone fun x => f x xs[i✝]

Proof state:
case case3.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 β
xs : Array α
stop i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝² : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
h✝¹ : i✝.succ ≤ xs.size
h✝ : ¬(i✝.succ == stop) = true
ih : ∀ (__do_lift : β), monotone fun x => Array.foldrM.fold (f x) xs stop i✝ ⋯ __do_lift
⊢ monotone fun x => f x xs[i✝]

Tactic:
apply monotone_apply

Result:
case case3.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 β
xs : Array α
stop i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝² : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
h✝¹ : i✝.succ ≤ xs.size
h✝ : ¬(i✝.succ == stop) = true
ih : ∀ (__do_lift : β), monotone fun x => Array.foldrM.fold (f x) xs stop i✝ ⋯ __do_lift
⊢ monotone f

Proof state:
case case3
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
xs : Array α
stop i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝² : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
h✝¹ : i✝.succ ≤ xs.size
h✝ : ¬(i✝.succ == stop) = true
ih : ∀ (__do_lift : β), monotone fun x => Array.foldrM.fold (f x) xs stop i✝ ⋯ __do_lift
⊢ monotone fun x => do
    let __do_lift ← f x xs[i✝] b✝
    Array.foldrM.fold (f x) xs stop i✝ ⋯ __do_lift

Tactic:
apply monotone_bind

Result:
case case3.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 β
xs : Array α
stop i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝² : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
h✝¹ : i✝.succ ≤ xs.size
h✝ : ¬(i✝.succ == stop) = true
ih : ∀ (__do_lift : β), monotone fun x => Array.foldrM.fold (f x) xs stop i✝ ⋯ __do_lift
⊢ monotone fun x => f x xs[i✝] b✝

case case3.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 β
xs : Array α
stop i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝² : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
h✝¹ : i✝.succ ≤ xs.size
h✝ : ¬(i✝.succ == stop) = true
ih : ∀ (__do_lift : β), monotone fun x => Array.foldrM.fold (f x) xs stop i✝ ⋯ __do_lift
⊢ monotone fun x __do_lift => Array.foldrM.fold (f x) xs stop i✝ ⋯ __do_lift

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 β
xs : Array α
stop i : Nat
hmono : monotone f
b✝ : β
x✝ h✝¹ : 0 ≤ xs.size
h✝ : ¬(0 == stop) = true
⊢ monotone fun x =>
    if (0 == stop) = true then pure b✝
    else
      match 0, x✝ with
      | 0, x => pure b✝
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f x xs[i] b✝
        Array.foldrM.fold (f x) xs stop i ⋯ __do_lift

Tactic:
simp only [↓reduceIte, *]

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 β
xs : Array α
stop i : Nat
hmono : monotone f
b✝ : β
x✝ h✝¹ : 0 ≤ xs.size
h✝ : ¬(0 == stop) = true
⊢ monotone fun x => if false = true then pure b✝ else pure b✝

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 β
xs : Array α
stop i : Nat
hmono : monotone f
t✝ : Nat
h✝¹ : t✝ ≤ xs.size
b✝ : β
h✝ : (t✝ == stop) = true
⊢ monotone fun x => pure b✝

Tactic:
apply monotone_const

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 β
xs : Array α
stop i : Nat
hmono : monotone f
b✝ : β
x✝ h✝¹ : 0 ≤ xs.size
h✝ : ¬(0 == stop) = true
⊢ monotone fun x => if false = true then pure b✝ else pure b✝

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case case3
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
xs : Array α
stop i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝² : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
h✝¹ : i✝.succ ≤ xs.size
h✝ : ¬(i✝.succ == stop) = true
ih : ∀ (__do_lift : β), monotone fun x => Array.foldrM.fold (f x) xs stop i✝ ⋯ __do_lift
⊢ monotone fun x => Array.foldrM.fold (f x) xs stop i✝.succ h✝² b✝

Tactic:
unfold Array.foldrM.fold

Result:
case case3
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
xs : Array α
stop i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝² : i✝ + 1 ≤ xs.size
this✝ : i✝ < xs.size
h✝¹ : i✝.succ ≤ xs.size
h✝ : ¬(i✝.succ == stop) = true
ih : ∀ (__do_lift : β), monotone fun x => Array.foldrM.fold (f x) xs stop i✝ ⋯ __do_lift
⊢ monotone fun x =>
    if (i✝.succ == stop) = true then pure b✝
    else
      match i✝.succ, h✝² with
      | 0, x => pure b✝
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f x xs[i] b✝
        Array.foldrM.fold (f x) xs stop i ⋯ __do_lift