-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_forIn'_loop {α : Type uu}
    (as : List α) (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)) (as' : List α) (b : β)
    (p : Exists (fun bs => bs ++ as' = as)) (hmono : monotone f) :
    monotone (fun x => List.forIn'.loop as (f x) as' b p)

Proof state:
case cons.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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
a✝ : β
⊢ monotone fun x =>
    match ForInStep.yield a✝ with
    | ForInStep.done b => pure b
    | ForInStep.yield b =>
      let_fun this := ⋯;
      List.forIn'.loop as (f x) as' b this

Tactic:
apply ih

Result:
no goals

Proof state:
case cons.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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ monotone fun x => f x a ⋯

Tactic:
apply monotone_apply

Result:
case cons.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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ monotone fun x => f x a

Proof state:
case cons.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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ monotone fun x => f x a ⋯ b

Tactic:
apply monotone_apply

Result:
case cons.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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ monotone fun x => f x a ⋯

Proof state:
case cons.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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
a✝ : β
⊢ monotone fun x =>
    match ForInStep.done a✝ with
    | ForInStep.done b => pure b
    | ForInStep.yield b =>
      let_fun this := ⋯;
      List.forIn'.loop as (f x) as' b this

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case cons.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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ monotone fun x __do_lift =>
    match __do_lift with
    | ForInStep.done b => pure b
    | ForInStep.yield b =>
      let_fun this := ⋯;
      List.forIn'.loop as (f x) as' b this

Tactic:
apply monotone_of_monotone_apply

Result:
case cons.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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ ∀ (y : ForInStep β),
    monotone fun x =>
      match y with
      | ForInStep.done b => pure b
      | ForInStep.yield b =>
        let_fun this := ⋯;
        List.forIn'.loop as (f x) as' b this

Proof state:
case cons.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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
y : ForInStep β
⊢ monotone fun x =>
    match y with
    | ForInStep.done b => pure b
    | ForInStep.yield b =>
      let_fun this := ⋯;
      List.forIn'.loop as (f x) as' b this

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

Result:
no goals

Proof state:
case cons.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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ monotone f

Tactic:
apply hmono

Result:
no goals

Proof state:
case cons
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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ monotone fun x => List.forIn'.loop as (f x) (a :: as') b p

Tactic:
apply monotone_bind

Result:
case cons.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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ monotone fun x => f x a ⋯ b

case cons.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 : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ monotone fun x __do_lift =>
    match __do_lift with
    | ForInStep.done b => pure b
    | ForInStep.yield b =>
      let_fun this := ⋯;
      List.forIn'.loop as (f x) as' b this