-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_foldrM
    (f : γ → α → β → m β) (init : β) (xs : Array α) (start stop : Nat) (hmono : monotone f) :
    monotone (fun x => xs.foldrM (f x) init start stop)

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 β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x => Array.foldrM (f x) init xs start stop

Tactic:
unfold Array.foldrM

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 β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x =>
    if h : start ≤ xs.size then if stop < start then Array.foldrM.fold (f x) xs stop start h init else pure init
    else if stop < xs.size then Array.foldrM.fold (f x) xs stop xs.size ⋯ init else pure init

Proof state:
case isTrue
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
h✝ : start ≤ xs.size
⊢ monotone fun x => if stop < start then Array.foldrM.fold (f x) xs stop start h✝ init else pure init

Tactic:
split

Result:
case isTrue.isTrue
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
h✝¹ : start ≤ xs.size
h✝ : stop < start
⊢ monotone fun x => Array.foldrM.fold (f x) xs stop start h✝¹ init

case isTrue.isFalse
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
h✝¹ : start ≤ xs.size
h✝ : ¬stop < start
⊢ monotone fun x => pure init

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 β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x =>
    if h : start ≤ xs.size then if stop < start then Array.foldrM.fold (f x) xs stop start h init else pure init
    else if stop < xs.size then Array.foldrM.fold (f x) xs stop xs.size ⋯ init else pure init

Tactic:
split

Result:
case isTrue
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
h✝ : start ≤ xs.size
⊢ monotone fun x => if stop < start then Array.foldrM.fold (f x) xs stop start h✝ init else pure init

case isFalse
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
h✝ : ¬start ≤ xs.size
⊢ monotone fun x => if stop < xs.size then Array.foldrM.fold (f x) xs stop xs.size ⋯ init else pure init

Proof state:
case isFalse
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
h✝ : ¬start ≤ xs.size
⊢ monotone fun x => if stop < xs.size then Array.foldrM.fold (f x) xs stop xs.size ⋯ init else pure init

Tactic:
split

Result:
case isFalse.isTrue
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
h✝¹ : ¬start ≤ xs.size
h✝ : stop < xs.size
⊢ monotone fun x => Array.foldrM.fold (f x) xs stop xs.size ⋯ init

case isFalse.isFalse
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
h✝¹ : ¬start ≤ xs.size
h✝ : ¬stop < xs.size
⊢ monotone fun x => pure init

Proof state:
case isTrue.isFalse
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
h✝¹ : start ≤ xs.size
h✝ : ¬stop < start
⊢ monotone fun x => pure init

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case isTrue.isTrue
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
h✝¹ : start ≤ xs.size
h✝ : stop < start
⊢ monotone fun x => Array.foldrM.fold (f x) xs stop start h✝¹ init

Tactic:
apply monotone_foldrM_fold (hmono := hmono)

Result:
no goals

Proof state:
case isFalse.isTrue
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
h✝¹ : ¬start ≤ xs.size
h✝ : stop < xs.size
⊢ monotone fun x => Array.foldrM.fold (f x) xs stop xs.size ⋯ init

Tactic:
apply monotone_foldrM_fold (hmono := hmono)

Result:
no goals

Proof state:
case isFalse.isFalse
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → β → m β
init : β
xs : Array α
start stop : Nat
hmono : monotone f
h✝¹ : ¬start ≤ xs.size
h✝ : ¬stop < xs.size
⊢ monotone fun x => pure init

Tactic:
apply monotone_const

Result:
no goals