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

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
⊢ anyM p #[] start stop = pure false
Tactic:
dsimp [anyM]
State after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
⊢ (if h : stop ≤ 0 then anyM.loop p #[] stop h start else anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start) =
    pure false

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
⊢ (if h : stop ≤ 0 then anyM.loop p #[] stop h start else anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start) =
    pure false
Tactic:
if h : stop ≤ 0 then
  rewrite [dif_pos h]
  exact anyM_loop_empty p h start
else
  rewrite [dif_neg h]
  exact anyM_loop_empty p .refl start
State after:
no goals

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
h : stop ≤ 0
⊢ (if h : stop ≤ 0 then anyM.loop p #[] stop h start else anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start) =
    pure false
Tactic:
rewrite [dif_pos h]
State after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
h : stop ≤ 0
⊢ anyM.loop p #[] stop h start = pure false

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
h : stop ≤ 0
⊢ anyM.loop p #[] stop h start = pure false
Tactic:
exact anyM_loop_empty p h start
State after:
no goals

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
h : ¬stop ≤ 0
⊢ (if h : stop ≤ 0 then anyM.loop p #[] stop h start else anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start) =
    pure false
Tactic:
rewrite [dif_neg h]
State after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
h : ¬stop ≤ 0
⊢ anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start = pure false

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
h : ¬stop ≤ 0
⊢ anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start = pure false
Tactic:
exact anyM_loop_empty p .refl start
State after:
no goals