-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_forIn'_loop {α : Type uu}
    (as : Array α) (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)) (i : Nat) (h : i ≤ as.size)
    (b : β) (hmono : monotone f) :
    monotone (fun x => Array.forIn'.loop as (f x) i h 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 γ
α : Type uu
as : Array α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝¹ : i✝ + 1 ≤ as.size
h'✝ : i✝ < as.size
this✝¹ : as.size - 1 < as.size
this✝ : as.size - 1 - i✝ < as.size
h✝ : i✝.succ ≤ as.size
ih : ∀ (b : β), monotone fun x => Array.forIn'.loop as (f x) i✝ ⋯ b
⊢ monotone fun x => f x as[as.size - 1 - i✝] ⋯

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 γ
α : Type uu
as : Array α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝¹ : i✝ + 1 ≤ as.size
h'✝ : i✝ < as.size
this✝¹ : as.size - 1 < as.size
this✝ : as.size - 1 - i✝ < as.size
h✝ : i✝.succ ≤ as.size
ih : ∀ (b : β), monotone fun x => Array.forIn'.loop as (f x) i✝ ⋯ b
⊢ monotone fun x => f x as[as.size - 1 - i✝]

Proof state:
case case2.hmono₂.h.yield
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : Array α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝¹ : i✝ + 1 ≤ as.size
h'✝ : i✝ < as.size
this✝¹ : as.size - 1 < as.size
this✝ : as.size - 1 - i✝ < as.size
h✝ : i✝.succ ≤ as.size
ih : ∀ (b : β), monotone fun x => Array.forIn'.loop as (f x) i✝ ⋯ b
a✝ : β
⊢ monotone fun x =>
    match ForInStep.yield a✝ with
    | ForInStep.done b => pure b
    | ForInStep.yield b => Array.forIn'.loop as (f x) i✝ ⋯ b

Tactic:
apply ih

Result:
no goals

Proof state:
case case2.hmono₂.h.done
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : Array α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝¹ : i✝ + 1 ≤ as.size
h'✝ : i✝ < as.size
this✝¹ : as.size - 1 < as.size
this✝ : as.size - 1 - i✝ < as.size
h✝ : i✝.succ ≤ as.size
ih : ∀ (b : β), monotone fun x => Array.forIn'.loop as (f x) i✝ ⋯ b
a✝ : β
⊢ monotone fun x =>
    match ForInStep.done a✝ with
    | ForInStep.done b => pure b
    | ForInStep.yield b => Array.forIn'.loop as (f x) i✝ ⋯ b

Tactic:
apply monotone_const

Result:
no goals

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 γ
α : Type uu
as : Array α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
i : Nat
hmono : monotone f
b✝ : β
i✝ : Nat
h✝¹ : i✝ + 1 ≤ as.size
h'✝ : i✝ < as.size
this✝¹ : as.size - 1 < as.size
this✝ : as.size - 1 - i✝ < as.size
h✝ : i✝.succ ≤ as.size
ih : ∀ (b : β), monotone fun x => Array.forIn'.loop as (f x) i✝ ⋯ b
y : ForInStep β
⊢ monotone fun x =>
    match y with
    | ForInStep.done b => pure b
    | ForInStep.yield b => Array.forIn'.loop as (f x) i✝ ⋯ b

Tactic:
cases y with
| done => apply monotone_const
| yield => apply ih

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 γ
α : Type uu
as : Array α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
i : Nat
hmono : monotone f
b✝ : β
x✝ h✝ : 0 ≤ as.size
⊢ monotone fun x => Array.forIn'.loop as (f x) 0 x✝ b✝

Tactic:
apply monotone_const

Result:
no goals