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

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
⊢ monotone fun x => List.allM (f x) []

Tactic:
apply monotone_const

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 : monotone fun x => List.allM (f x) tail✝
⊢ monotone fun x __do_lift =>
    match __do_lift with
    | true => List.allM (f x) tail✝
    | false => pure false

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 : monotone fun x => List.allM (f x) tail✝
⊢ ∀ (y : Bool),
    monotone fun x =>
      match y with
      | true => List.allM (f x) tail✝
      | false => pure false

Proof state:
case cons.hmono₂.h.true
γ : 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 : monotone fun x => List.allM (f x) tail✝
⊢ monotone fun x =>
    match true with
    | true => List.allM (f x) tail✝
    | false => pure false

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 : monotone fun x => List.allM (f x) tail✝
⊢ 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 : monotone fun x => List.allM (f x) tail✝
⊢ monotone f

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 : monotone fun x => List.allM (f x) tail✝
⊢ monotone fun x => List.allM (f x) (head✝ :: tail✝)

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 : monotone fun x => List.allM (f x) tail✝
⊢ 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 : monotone fun x => List.allM (f x) tail✝
⊢ monotone fun x __do_lift =>
    match __do_lift with
    | true => List.allM (f x) tail✝
    | false => pure false

Proof state:
case cons.hmono₂.h.false
γ : 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 : monotone fun x => List.allM (f x) tail✝
⊢ monotone fun x =>
    match false with
    | true => List.allM (f x) tail✝
    | false => pure false

Tactic:
apply monotone_const

Result:
no goals

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 : monotone fun x => List.allM (f x) tail✝
y : Bool
⊢ monotone fun x =>
    match y with
    | true => List.allM (f x) tail✝
    | false => pure false

Tactic:
cases y

Result:
case cons.hmono₂.h.false
γ : 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 : monotone fun x => List.allM (f x) tail✝
⊢ monotone fun x =>
    match false with
    | true => List.allM (f x) tail✝
    | false => pure false

case cons.hmono₂.h.true
γ : 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 : monotone fun x => List.allM (f x) tail✝
⊢ monotone fun x =>
    match true with
    | true => List.allM (f x) tail✝
    | false => pure false

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 : monotone fun x => List.allM (f x) tail✝
⊢ ∀ (y : Bool),
    monotone fun x =>
      match y with
      | true => List.allM (f x) tail✝
      | false => pure false

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 : monotone fun x => List.allM (f x) tail✝
y : Bool
⊢ monotone fun x =>
    match y with
    | true => List.allM (f x) tail✝
    | false => pure false

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 : monotone fun x => List.allM (f x) tail✝
⊢ monotone f

Tactic:
apply hmono

Result:
no goals