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

Proof state:
case case1
γ : 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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : x✝ < stop
this✝ : x✝ < xs.size
ih : monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)
⊢ monotone fun x => do
    let __do_lift ← f x xs[x✝]
    if __do_lift = true then pure true else Array.anyM.loop (f x) xs stop h (x✝ + 1)

Tactic:
apply monotone_bind

Result:
case case1.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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : x✝ < stop
this✝ : x✝ < xs.size
ih : monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)
⊢ monotone fun x => f x xs[x✝]

case case1.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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : x✝ < stop
this✝ : x✝ < xs.size
ih : monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)
⊢ monotone fun x __do_lift => if __do_lift = true then pure true else Array.anyM.loop (f x) xs stop h (x✝ + 1)

Proof state:
case case1
γ : 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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : x✝ < stop
this✝ : x✝ < xs.size
ih : monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)
⊢ monotone fun x =>
    if hlt : x✝ < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← f x xs[x✝]
      if __do_lift = true then pure true else Array.anyM.loop (f x) xs stop h (x✝ + 1)
    else pure false

Tactic:
simp only [↓reduceDIte, *]

Result:
case case1
γ : 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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : x✝ < stop
this✝ : x✝ < xs.size
ih : monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)
⊢ monotone fun x => do
    let __do_lift ← f x xs[x✝]
    if __do_lift = true then pure true else Array.anyM.loop (f x) xs stop h (x✝ + 1)

Proof state:
case case1.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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : x✝ < stop
this✝ : x✝ < xs.size
ih : monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)
⊢ monotone fun x => f x xs[x✝]

Tactic:
apply monotone_apply

Result:
case case1.hmono₁.h
γ : 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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : x✝ < stop
this✝ : x✝ < xs.size
ih : monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)
⊢ monotone f

Proof state:
case case1.hmono₂.h
γ : 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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : x✝ < stop
this✝ : x✝ < xs.size
ih : monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)
⊢ ∀ (y : Bool), monotone fun x => if y = true then pure true else Array.anyM.loop (f x) xs stop h (x✝ + 1)

Tactic:
intro y

Result:
case case1.hmono₂.h
γ : 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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : x✝ < stop
this✝ : x✝ < xs.size
ih : monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)
y : Bool
⊢ monotone fun x => if y = true then pure true else Array.anyM.loop (f x) xs stop h (x✝ + 1)

Proof state:
case case2
γ : 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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : ¬x✝ < stop
⊢ monotone fun x =>
    if hlt : x✝ < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← f x xs[x✝]
      if __do_lift = true then pure true else Array.anyM.loop (f x) xs stop h (x✝ + 1)
    else pure false

Tactic:
simp only [↓reduceDIte, *]

Result:
case case2
γ : 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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : ¬x✝ < stop
⊢ monotone fun x => pure false

Proof state:
case case1.hmono₂.h.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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝¹ : x✝ < stop
this✝ : x✝ < xs.size
ih : monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)
y : Bool
h✝ : ¬y = true
⊢ monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)

Tactic:
apply ih

Result:
no goals

Proof state:
case case1
γ : 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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : x✝ < stop
this✝ : x✝ < xs.size
ih : monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)
⊢ monotone fun x => Array.anyM.loop (f x) xs stop h x✝

Tactic:
unfold Array.anyM.loop

Result:
case case1
γ : 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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : x✝ < stop
this✝ : x✝ < xs.size
ih : monotone fun x => Array.anyM.loop (f x) xs stop h (x✝ + 1)
⊢ monotone fun x =>
    if hlt : x✝ < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← f x xs[x✝]
      if __do_lift = true then pure true else Array.anyM.loop (f x) xs stop h (x✝ + 1)
    else pure false

Proof state:
case case2
γ : 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 α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
x✝ : Nat
h✝ : ¬x✝ < stop
⊢ monotone fun x => pure false

Tactic:
apply monotone_const

Result:
no goals