-- 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.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.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 f

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:
intro y

Result:
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

Proof state:
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 γ
α : 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✝] ⋯ b✝

Tactic:
apply monotone_apply

Result:
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✝] ⋯

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 γ
α : 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 => Array.forIn'.loop as (f x) i✝.succ h✝¹ b✝

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 γ
α : 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✝] ⋯ b✝

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 γ
α : 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 __do_lift =>
    match __do_lift with
    | ForInStep.done b => pure b
    | ForInStep.yield b => Array.forIn'.loop as (f x) i✝ ⋯ b

Proof state:
case case2.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 γ
α : 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 f

Tactic:
apply hmono

Result:
no goals

Proof state:
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 γ
α : 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 __do_lift =>
    match __do_lift with
    | ForInStep.done b => pure b
    | ForInStep.yield b => Array.forIn'.loop as (f x) i✝ ⋯ b

Tactic:
apply monotone_of_monotone_apply

Result:
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