-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem SatisfiesM_anyM [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) (start stop)
    (hstart : start ≤ min stop as.size) (tru : Prop) (fal : Nat → Prop) (h0 : fal start)
    (hp : ∀ i : Fin as.size, i.1 < stop → fal i.1 →
      SatisfiesM (bif · then tru else fal (i + 1)) (p as[i])) :
    SatisfiesM
      (fun res => bif res then tru else fal (min stop as.size))
      (anyM p as start stop)

Proof state:
case isFalse
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop✝ : Nat
hstart : start ≤ min stop✝ as.size
tru : Prop
fal : Nat → Prop
h0✝ : fal start
hp✝ : ∀ (i : Fin as.size), ↑i < stop✝ → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
stop j : Nat
hj' : j ≤ stop
hstop : stop ≤ as.size
h0 : fal j
hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
h✝ : ¬j < stop
⊢ SatisfiesM (fun res => bif res then tru else fal stop) (pure false)

Tactic:
next hj => exact .pure <| Nat.le_antisymm hj' (Nat.ge_of_not_lt hj) ▸ h0

Result:
no goals

Proof state:
case isTrue
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop✝ : Nat
hstart : start ≤ min stop✝ as.size
tru : Prop
fal : Nat → Prop
h0✝ : fal start
hp✝ : ∀ (i : Fin as.size), ↑i < stop✝ → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
stop j : Nat
hj' : j ≤ stop
hstop : stop ≤ as.size
h0 : fal j
hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
h✝ : j < stop
⊢ SatisfiesM (fun res => bif res then tru else fal stop)
    (let_fun this := ⋯;
    do
    let __do_lift ← p as[j]
    if __do_lift = true then pure true else anyM.loop p as stop hstop (j + 1))

Tactic:
next hj =>
exact (hp ⟨j, Nat.lt_of_lt_of_le hj hstop⟩ hj h0).bind fun
  | true, h => .pure h
  | false, h => go hj hstop h hp

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
hstart : start ≤ min stop as.size
tru : Prop
fal : Nat → Prop
h0 : fal start
hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
⊢ SatisfiesM (fun res => bif res then tru else fal (min stop as.size)) (anyM.loop p as (min stop as.size) ⋯ start)

Tactic:
exact go hstart _ h0 fun i hi => hp i <| Nat.lt_of_lt_of_le hi <| Nat.min_le_left ..

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop✝ : Nat
hstart : start ≤ min stop✝ as.size
tru : Prop
fal : Nat → Prop
h0✝ : fal start
hp✝ : ∀ (i : Fin as.size), ↑i < stop✝ → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
stop j : Nat
hj' : j ≤ stop
hstop : stop ≤ as.size
h0 : fal j
hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
⊢ SatisfiesM (fun res => bif res then tru else fal stop) (anyM.loop p as stop hstop j)

Tactic:
unfold anyM.loop

Result:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop✝ : Nat
hstart : start ≤ min stop✝ as.size
tru : Prop
fal : Nat → Prop
h0✝ : fal start
hp✝ : ∀ (i : Fin as.size), ↑i < stop✝ → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
stop j : Nat
hj' : j ≤ stop
hstop : stop ≤ as.size
h0 : fal j
hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
⊢ SatisfiesM (fun res => bif res then tru else fal stop)
    (if hlt : j < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← p as[j]
      if __do_lift = true then pure true else anyM.loop p as stop hstop (j + 1)
    else pure false)

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop✝ : Nat
hstart : start ≤ min stop✝ as.size
tru : Prop
fal : Nat → Prop
h0✝ : fal start
hp✝ : ∀ (i : Fin as.size), ↑i < stop✝ → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
stop j : Nat
hj' : j ≤ stop
hstop : stop ≤ as.size
h0 : fal j
hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
⊢ SatisfiesM (fun res => bif res then tru else fal stop)
    (if hlt : j < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← p as[j]
      if __do_lift = true then pure true else anyM.loop p as stop hstop (j + 1)
    else pure false)

Tactic:
split

Result:
case isTrue
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop✝ : Nat
hstart : start ≤ min stop✝ as.size
tru : Prop
fal : Nat → Prop
h0✝ : fal start
hp✝ : ∀ (i : Fin as.size), ↑i < stop✝ → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
stop j : Nat
hj' : j ≤ stop
hstop : stop ≤ as.size
h0 : fal j
hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
h✝ : j < stop
⊢ SatisfiesM (fun res => bif res then tru else fal stop)
    (let_fun this := ⋯;
    do
    let __do_lift ← p as[j]
    if __do_lift = true then pure true else anyM.loop p as stop hstop (j + 1))

case isFalse
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop✝ : Nat
hstart : start ≤ min stop✝ as.size
tru : Prop
fal : Nat → Prop
h0✝ : fal start
hp✝ : ∀ (i : Fin as.size), ↑i < stop✝ → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
stop j : Nat
hj' : j ≤ stop
hstop : stop ≤ as.size
h0 : fal j
hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
h✝ : ¬j < stop
⊢ SatisfiesM (fun res => bif res then tru else fal stop) (pure false)

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
hstart : start ≤ min stop as.size
tru : Prop
fal : Nat → Prop
h0 : fal start
hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
⊢ SatisfiesM (fun res => bif res then tru else fal (min stop as.size)) (anyM p as start stop)

Tactic:
simp only [Array.anyM_eq_anyM_loop]

Result:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
hstart : start ≤ min stop as.size
tru : Prop
fal : Nat → Prop
h0 : fal start
hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
⊢ SatisfiesM (fun res => bif res then tru else fal (min stop as.size)) (anyM.loop p as (min stop as.size) ⋯ start)

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop✝ : Nat
hstart : start ≤ min stop✝ as.size
tru : Prop
fal : Nat → Prop
h0✝ : fal start
hp✝ : ∀ (i : Fin as.size), ↑i < stop✝ → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
stop j : Nat
hj' : j ≤ stop
hstop : stop ≤ as.size
h0 : fal j
hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
hj : ¬j < stop
⊢ SatisfiesM (fun res => bif res then tru else fal stop) (pure false)

Tactic:
exact .pure <| Nat.le_antisymm hj' (Nat.ge_of_not_lt hj) ▸ h0

Result:
no goals