-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_filterAuxM
  {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type}
  (f : γ → α → m Bool) (xs acc : List α) (hmono : monotone f) :
    monotone (fun x => xs.filterAuxM (f x) acc)

Proof state:
case cons.hmono₁
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
hmono : monotone f
head✝ : α
tail✝ : List α
ih : ∀ (acc : List α), monotone fun x => List.filterAuxM (f x) tail✝ acc
acc : List α
⊢ monotone fun x => f x head✝

Tactic:
apply monotone_apply

Result:
case cons.hmono₁.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
hmono : monotone f
head✝ : α
tail✝ : List α
ih : ∀ (acc : List α), monotone fun x => List.filterAuxM (f x) tail✝ acc
acc : List α
⊢ monotone f

Proof state:
case cons.hmono₂.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
hmono : monotone f
head✝ : α
tail✝ : List α
ih : ∀ (acc : List α), monotone fun x => List.filterAuxM (f x) tail✝ acc
acc : List α
y : Bool
⊢ monotone fun x => List.filterAuxM (f x) tail✝ (bif y then head✝ :: acc else acc)

Tactic:
apply ih

Result:
no goals

Proof state:
case cons.hmono₂
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
hmono : monotone f
head✝ : α
tail✝ : List α
ih : ∀ (acc : List α), monotone fun x => List.filterAuxM (f x) tail✝ acc
acc : List α
⊢ monotone fun x b => List.filterAuxM (f x) tail✝ (bif b then head✝ :: acc else acc)

Tactic:
apply monotone_of_monotone_apply

Result:
case cons.hmono₂.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
hmono : monotone f
head✝ : α
tail✝ : List α
ih : ∀ (acc : List α), monotone fun x => List.filterAuxM (f x) tail✝ acc
acc : List α
⊢ ∀ (y : Bool), monotone fun x => List.filterAuxM (f x) tail✝ (bif y then head✝ :: acc else acc)

Proof state:
case cons.hmono₂.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
hmono : monotone f
head✝ : α
tail✝ : List α
ih : ∀ (acc : List α), monotone fun x => List.filterAuxM (f x) tail✝ acc
acc : List α
⊢ ∀ (y : Bool), monotone fun x => List.filterAuxM (f x) tail✝ (bif y then head✝ :: acc else acc)

Tactic:
intro y

Result:
case cons.hmono₂.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
hmono : monotone f
head✝ : α
tail✝ : List α
ih : ∀ (acc : List α), monotone fun x => List.filterAuxM (f x) tail✝ acc
acc : List α
y : Bool
⊢ monotone fun x => List.filterAuxM (f x) tail✝ (bif y then head✝ :: acc else acc)

Proof state:
case cons.hmono₁.h
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
hmono : monotone f
head✝ : α
tail✝ : List α
ih : ∀ (acc : List α), monotone fun x => List.filterAuxM (f x) tail✝ acc
acc : List α
⊢ monotone f

Tactic:
apply hmono

Result:
no goals

Proof state:
case cons
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
hmono : monotone f
head✝ : α
tail✝ : List α
ih : ∀ (acc : List α), monotone fun x => List.filterAuxM (f x) tail✝ acc
acc : List α
⊢ monotone fun x => List.filterAuxM (f x) (head✝ :: tail✝) acc

Tactic:
apply monotone_bind

Result:
case cons.hmono₁
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
hmono : monotone f
head✝ : α
tail✝ : List α
ih : ∀ (acc : List α), monotone fun x => List.filterAuxM (f x) tail✝ acc
acc : List α
⊢ monotone fun x => f x head✝

case cons.hmono₂
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
hmono : monotone f
head✝ : α
tail✝ : List α
ih : ∀ (acc : List α), monotone fun x => List.filterAuxM (f x) tail✝ acc
acc : List α
⊢ monotone fun x b => List.filterAuxM (f x) tail✝ (bif b then head✝ :: acc else acc)

Proof state:
case nil
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
hmono : monotone f
acc : List α
⊢ monotone fun x => List.filterAuxM (f x) [] acc

Tactic:
apply monotone_const

Result:
no goals