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

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 β
xs : Array α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ ∀ (y : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) y

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 β
xs : Array α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝.succ j✝ b✝

Tactic:
unfold Array.foldlM.loop

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 : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ monotone fun x =>
    if hlt : j✝ < stop then
      match i'✝.succ with
      | 0 => pure b✝
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f x b✝ xs[j✝]
        Array.foldlM.loop (f x) xs stop h i' (j✝ + 1) __do_lift
    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 : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
⊢ monotone fun x => 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 : Nat
h : stop ≤ xs.size
hmono : monotone f
t✝ j✝ : Nat
b✝ : β
h✝ : ¬j✝ < stop
⊢ monotone fun x => Array.foldlM.loop (f x) xs stop h t✝ j✝ b✝

Tactic:
simp only [Array.foldlM.loop, ↓reduceDIte, *]

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 : Nat
h : stop ≤ xs.size
hmono : monotone f
t✝ j✝ : Nat
b✝ : β
h✝ : ¬j✝ < stop
⊢ monotone fun x => pure b✝

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 : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ monotone fun x => do
    let __do_lift ← f x b✝ xs[j✝]
    Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift

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 β
xs : Array α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ monotone fun x => f x b✝ xs[j✝]

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 β
xs : Array α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ monotone fun x __do_lift => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift

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 : Nat
h : stop ≤ xs.size
hmono : monotone f
t✝ j✝ : Nat
b✝ : β
h✝ : ¬j✝ < stop
⊢ monotone fun x => pure b✝

Tactic:
apply monotone_const

Result:
no goals

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 : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
⊢ monotone fun x => Array.foldlM.loop (f x) xs stop h 0 j✝ b✝

Tactic:
simp only [Array.foldlM.loop, ↓reduceDIte, *]

Result:
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 : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
⊢ monotone fun x => pure b✝

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 β
xs : Array α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ monotone fun x => f x b✝

Tactic:
apply monotone_apply

Result:
case case2.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 : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ 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 β
xs : Array α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ monotone fun x =>
    if hlt : j✝ < stop then
      match i'✝.succ with
      | 0 => pure b✝
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f x b✝ xs[j✝]
        Array.foldlM.loop (f x) xs stop h i' (j✝ + 1) __do_lift
    else pure b✝

Tactic:
simp only [↓reduceDIte, *]

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 : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ monotone fun x => do
    let __do_lift ← f x b✝ xs[j✝]
    Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift