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

Proof state:
case isFalse
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
h✝ : ¬stop ≤ xs.size
⊢ monotone fun x =>
    let any := fun stop h => Array.anyM.loop (f x) xs stop h start;
    any xs.size ⋯

Tactic:
apply monotone_anyM_loop

Result:
case isFalse.hmono
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
h✝ : ¬stop ≤ xs.size
⊢ monotone f

Proof state:
case isTrue
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
h✝ : stop ≤ xs.size
⊢ monotone fun x =>
    let any := fun stop h => Array.anyM.loop (f x) xs stop h start;
    any stop h✝

Tactic:
apply monotone_anyM_loop

Result:
case isTrue.hmono
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
h✝ : stop ≤ xs.size
⊢ monotone f

Proof state:
case isFalse.hmono
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
h✝ : ¬stop ≤ xs.size
⊢ monotone f

Tactic:
apply hmono

Result:
no goals

Proof state:
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x =>
    let any := fun stop h => Array.anyM.loop (f x) xs stop h start;
    if h : stop ≤ xs.size then any stop h else any xs.size ⋯

Tactic:
split

Result:
case isTrue
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
h✝ : stop ≤ xs.size
⊢ monotone fun x =>
    let any := fun stop h => Array.anyM.loop (f x) xs stop h start;
    any stop h✝

case isFalse
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
h✝ : ¬stop ≤ xs.size
⊢ monotone fun x =>
    let any := fun stop h => Array.anyM.loop (f x) xs stop h start;
    any xs.size ⋯

Proof state:
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x => Array.anyM (f x) xs start stop

Tactic:
unfold Array.anyM

Result:
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
⊢ monotone fun x =>
    let any := fun stop h => Array.anyM.loop (f x) xs stop h start;
    if h : stop ≤ xs.size then any stop h else any xs.size ⋯

Proof state:
case isTrue.hmono
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type u
f : γ → α → m Bool
xs : Array α
start stop : Nat
hmono : monotone f
h✝ : stop ≤ xs.size
⊢ monotone f

Tactic:
apply hmono

Result:
no goals