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

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
stop : Nat
h : stop ≤ 0
i j : Nat
hij : i < j
⊢ anyPairM.loop #[] p stop h i j hij = pure false
Tactic:
cases Nat.eq_zero_of_le_zero h
State after:
case refl
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
i j : Nat
hij : i < j
h : 0 ≤ 0
⊢ anyPairM.loop #[] p 0 h i j hij = pure false

State before:
case refl
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
i j : Nat
hij : i < j
h : 0 ≤ 0
⊢ anyPairM.loop #[] p 0 h i j hij = pure false
Tactic:
unfold anyPairM.loop
State after:
case refl
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
i j : Nat
hij : i < j
h : 0 ≤ 0
⊢ (if hj : j < 0 then
      let_fun this := (_ : i < size #[]);
      let_fun this_1 := (_ : j < size #[]);
      do
      let __do_lift ← p #[][i] #[][j]
      if __do_lift = true then pure true else anyPairM.loop #[] p 0 h i (j + 1) (_ : i < Nat.succ j)
    else if i < 0 then anyPairM.loop #[] p 0 h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false) =
    pure false

State before:
case refl
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
i j : Nat
hij : i < j
h : 0 ≤ 0
⊢ (if hj : j < 0 then
      let_fun this := (_ : i < size #[]);
      let_fun this_1 := (_ : j < size #[]);
      do
      let __do_lift ← p #[][i] #[][j]
      if __do_lift = true then pure true else anyPairM.loop #[] p 0 h i (j + 1) (_ : i < Nat.succ j)
    else if i < 0 then anyPairM.loop #[] p 0 h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false) =
    pure false
Tactic:
rw [dif_neg j.not_lt_zero, if_neg i.not_lt_zero]
State after:
no goals