Theorem: Array.anyPairM_empty (Algdata/Data/Array/Basic.lean)

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

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
⊢ (if h : stop ≤ size #[] then anyPairM.loop #[] p stop h start (start + 1) (_ : start < Nat.succ start)
    else
      anyPairM.loop #[] p (size #[]) (_ : Nat.le (size #[]) (size #[])) start (start + 1)
        (_ : start < Nat.succ start)) =
    pure false
Tactic:
simp only [size_toArray, List.length_nil]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
⊢ (if h : stop ≤ 0 then anyPairM.loop #[] p stop (_ : stop ≤ size #[]) start (start + 1) (_ : start < Nat.succ start)
    else anyPairM.loop #[] p 0 (_ : 0 ≤ size #[]) start (start + 1) (_ : start < Nat.succ start)) =
    pure false

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

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

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
h : stop ≤ 0
⊢ anyPairM.loop #[] p stop (_ : stop ≤ size #[]) start (start + 1) (_ : start < Nat.succ start) = pure false
Tactic:
exact anyPairM_loop_empty p h start.lt_succ_self
State after:
no goals

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

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