Theorem: Array.anyM_loop_empty (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
stop : Nat
h : stop ≤ 0
i : Nat
⊢ anyM.loop p #[] stop h i = pure false
Tactic:
cases h
State after:
case refl
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
i : Nat
⊢ anyM.loop p #[] 0 (_ : Nat.le 0 0) i = pure false

State before:
case refl
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
i : Nat
⊢ anyM.loop p #[] 0 (_ : Nat.le 0 0) i = pure false
Tactic:
unfold anyM.loop
State after:
case refl
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
i : Nat
⊢ (if hlt : i < 0 then
      let_fun this := (_ : i < size #[]);
      do
      let __do_lift ← p #[][i]
      if __do_lift = true then pure true else anyM.loop p #[] 0 (_ : Nat.le 0 0) (i + 1)
    else pure false) =
    pure false

State before:
case refl
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
i : Nat
⊢ (if hlt : i < 0 then
      let_fun this := (_ : i < size #[]);
      do
      let __do_lift ← p #[][i]
      if __do_lift = true then pure true else anyM.loop p #[] 0 (_ : Nat.le 0 0) (i + 1)
    else pure false) =
    pure false
Tactic:
rw [dif_neg i.not_lt_zero]
State after:
no goals