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

Proof state:
case 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 PUnit
xs : Array α
start stop : Nat
hmono : monotone f
y : α
⊢ PUnit → monotone fun x => f x y

Tactic:
intro z

Result:
case 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 PUnit
xs : Array α
start stop : Nat
hmono : monotone f
y : α
z : PUnit
⊢ monotone fun x => f x y

Proof state:
case 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 PUnit
xs : Array α
start stop : Nat
hmono : monotone f
⊢ ∀ (y : α), monotone fun x x_1 => f x y

Tactic:
intro y

Result:
case 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 PUnit
xs : Array α
start stop : Nat
hmono : monotone f
y : α
⊢ monotone fun x x_1 => f x y

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

Tactic:
apply monotone_foldrM

Result:
case 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 PUnit
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x a x_1 => f x a

Proof state:
case 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 PUnit
xs : Array α
start stop : Nat
hmono : monotone f
y : α
⊢ monotone fun x x_1 => f x y

Tactic:
apply monotone_of_monotone_apply

Result:
case 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 PUnit
xs : Array α
start stop : Nat
hmono : monotone f
y : α
⊢ PUnit → monotone fun x => f x y

Proof state:
case hmono.h.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 PUnit
xs : Array α
start stop : Nat
hmono : monotone f
y : α
z : PUnit
⊢ monotone f

Tactic:
apply hmono

Result:
no goals

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

Tactic:
unfold Array.forRevM

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

Proof state:
case 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 PUnit
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x a x_1 => f x a

Tactic:
apply monotone_of_monotone_apply

Result:
case 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 PUnit
xs : Array α
start stop : Nat
hmono : monotone f
⊢ ∀ (y : α), monotone fun x x_1 => f x y

Proof state:
case 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 PUnit
xs : Array α
start stop : Nat
hmono : monotone f
y : α
z : PUnit
⊢ monotone fun x => f x y

Tactic:
apply monotone_apply

Result:
case hmono.h.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 PUnit
xs : Array α
start stop : Nat
hmono : monotone f
y : α
z : PUnit
⊢ monotone f