-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem anyM_loop_cons [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat)
    (h : stop + 1 ≤ (a :: as).length) :
    anyM.loop p ⟨a :: as⟩ (stop + 1) h (start + 1) =
      anyM.loop p ⟨as⟩ stop (by simpa using h) start

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
⊢ (if hlt : start + 1 < stop + 1 then
      let_fun this := ⋯;
      do
      let __do_lift ← p { toList := a :: as }[start + 1]
      if __do_lift = true then pure true else anyM.loop p { toList := a :: as } (stop + 1) h (start + 1 + 1)
    else pure false) =
    anyM.loop p { toList := as } stop ⋯ start

Tactic:
conv => rhs; rw [anyM.loop]

Result:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
⊢ (if hlt : start + 1 < stop + 1 then
      let_fun this := ⋯;
      do
      let __do_lift ← p { toList := a :: as }[start + 1]
      if __do_lift = true then pure true else anyM.loop p { toList := a :: as } (stop + 1) h (start + 1 + 1)
    else pure false) =
    if hlt : start < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← p { toList := as }[start]
      if __do_lift = true then pure true else anyM.loop p { toList := as } stop ⋯ (start + 1)
    else pure false

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
⊢ anyM.loop p { toList := a :: as } (stop + 1) h (start + 1) = anyM.loop p { toList := as } stop ⋯ start

Tactic:
rw [anyM.loop]

Result:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
⊢ (if hlt : start + 1 < stop + 1 then
      let_fun this := ⋯;
      do
      let __do_lift ← p { toList := a :: as }[start + 1]
      if __do_lift = true then pure true else anyM.loop p { toList := a :: as } (stop + 1) h (start + 1 + 1)
    else pure false) =
    anyM.loop p { toList := as } stop ⋯ start

Proof state:
case isTrue
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
h'✝ : start + 1 < stop + 1
h' : start < stop
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← p { toList := a :: as }[start + 1]
    if __do_lift = true then pure true else anyM.loop p { toList := as } stop ⋯ (start + 1)) =
    let_fun this := ⋯;
    do
    let __do_lift ← p { toList := as }[start]
    if __do_lift = true then pure true else anyM.loop p { toList := as } stop ⋯ (start + 1)

Tactic:
simp

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
⊢ (if hlt : start + 1 < stop + 1 then
      let_fun this := ⋯;
      do
      let __do_lift ← p { toList := a :: as }[start + 1]
      if __do_lift = true then pure true else anyM.loop p { toList := a :: as } (stop + 1) h (start + 1 + 1)
    else pure false) =
    if hlt : start < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← p { toList := as }[start]
      if __do_lift = true then pure true else anyM.loop p { toList := as } stop ⋯ (start + 1)
    else pure false

Tactic:
split <;> rename_i h'

Result:
case isTrue
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
h' : start + 1 < stop + 1
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← p { toList := a :: as }[start + 1]
    if __do_lift = true then pure true else anyM.loop p { toList := a :: as } (stop + 1) h (start + 1 + 1)) =
    if hlt : start < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← p { toList := as }[start]
      if __do_lift = true then pure true else anyM.loop p { toList := as } stop ⋯ (start + 1)
    else pure false

case isFalse
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
h' : ¬start + 1 < stop + 1
⊢ pure false =
    if hlt : start < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← p { toList := as }[start]
      if __do_lift = true then pure true else anyM.loop p { toList := as } stop ⋯ (start + 1)
    else pure false

Proof state:
m : Type → Type ?u.51551
α : Type ?u.51562
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
⊢ stop ≤ { toList := as }.size

Tactic:
simpa using h

Result:
no goals

Proof state:
case isFalse.hnc
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
h' : ¬start + 1 < stop + 1
⊢ ¬start < stop

Tactic:
omega

Result:
no goals

Proof state:
case isTrue
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
h'✝ : start + 1 < stop + 1
h' : start < stop
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← p { toList := a :: as }[start + 1]
    if __do_lift = true then pure true else anyM.loop p { toList := a :: as } (stop + 1) h (start + 1 + 1)) =
    if hlt : start < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← p { toList := as }[start]
      if __do_lift = true then pure true else anyM.loop p { toList := as } stop ⋯ (start + 1)
    else pure false

Tactic:
rw [dif_pos h', anyM_loop_cons]

Result:
case isTrue
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
h'✝ : start + 1 < stop + 1
h' : start < stop
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← p { toList := a :: as }[start + 1]
    if __do_lift = true then pure true else anyM.loop p { toList := as } stop ⋯ (start + 1)) =
    let_fun this := ⋯;
    do
    let __do_lift ← p { toList := as }[start]
    if __do_lift = true then pure true else anyM.loop p { toList := as } stop ⋯ (start + 1)

Proof state:
case isTrue
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
h' : start + 1 < stop + 1
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← p { toList := a :: as }[start + 1]
    if __do_lift = true then pure true else anyM.loop p { toList := a :: as } (stop + 1) h (start + 1 + 1)) =
    if hlt : start < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← p { toList := as }[start]
      if __do_lift = true then pure true else anyM.loop p { toList := as } stop ⋯ (start + 1)
    else pure false

Tactic:
simp only [Nat.add_lt_add_iff_right] at h'

Result:
case isTrue
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
h'✝ : start + 1 < stop + 1
h' : start < stop
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← p { toList := a :: as }[start + 1]
    if __do_lift = true then pure true else anyM.loop p { toList := a :: as } (stop + 1) h (start + 1 + 1)) =
    if hlt : start < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← p { toList := as }[start]
      if __do_lift = true then pure true else anyM.loop p { toList := as } stop ⋯ (start + 1)
    else pure false

Proof state:
case isFalse
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
h' : ¬start + 1 < stop + 1
⊢ pure false =
    if hlt : start < stop then
      let_fun this := ⋯;
      do
      let __do_lift ← p { toList := as }[start]
      if __do_lift = true then pure true else anyM.loop p { toList := as } stop ⋯ (start + 1)
    else pure false

Tactic:
rw [dif_neg]

Result:
case isFalse.hnc
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
a : α
as : List α
stop start : Nat
h : stop + 1 ≤ (a :: as).length
h' : ¬start + 1 < stop + 1
⊢ ¬start < stop