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

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1)
      (_ : 0 < Nat.succ j) =
    do
    let b ← anyM (p a) x j stop
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
conv => lhs; unfold anyPairM.loop
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : 0 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      if 0 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
          (_ : 0 + 1 < Nat.succ (0 + 1))
      else pure false) =
    do
    let b ← anyM (p a) x j stop
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : 0 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      if 0 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
          (_ : 0 + 1 < Nat.succ (0 + 1))
      else pure false) =
    do
    let b ← anyM (p a) x j stop
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
conv => rhs; dsimp [anyM]; rewrite [dif_pos h]; unfold anyM.loop
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : 0 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      if 0 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
          (_ : 0 + 1 < Nat.succ (0 + 1))
      else pure false) =
    do
    let b ←
      if hlt : j < stop then
          let_fun this := (_ : j < size x);
          do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : 0 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      if 0 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
          (_ : 0 + 1 < Nat.succ (0 + 1))
      else pure false) =
    do
    let b ←
      if hlt : j < stop then
          let_fun this := (_ : j < size x);
          do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [if_pos stop.zero_lt_succ]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ (if h_1 : j + 1 < stop + 1 then do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
        (_ : 0 + 1 < Nat.succ (0 + 1))) =
    do
    let b ←
      if h_1 : j < stop then do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ (if h_1 : j + 1 < stop + 1 then do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
        (_ : 0 + 1 < Nat.succ (0 + 1))) =
    do
    let b ←
      if h_1 : j < stop then do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
if hj : j < stop then
  simp only [dif_pos (Nat.succ_lt_succ hj), dif_pos hj]
  simp only [getElem_cons_zero, getElem_cons_succ, bind_assoc]
  apply bind_congr; intro b
  match b with
  | true => simp only [ite_true, pure_bind]
  | false =>
    simp only [ite_false]
    rewrite [anyPairM_loop_cons_zero a x p h (j+1)]
    conv => lhs; lhs; dsimp [anyM]; rw [dif_pos h]
else
  simp only [dif_neg (fun h' => hj (Nat.lt_of_succ_lt_succ h')), dif_neg hj]
  rewrite [anyPairM_loop_cons_succ a x p h Nat.zero_lt_one]
  simp only [pure_bind, ite_false]
State after:
no goals

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ (if h_1 : j + 1 < stop + 1 then do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
        (_ : 0 + 1 < Nat.succ (0 + 1))) =
    do
    let b ←
      if h_1 : j < stop then do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [dif_pos (Nat.succ_lt_succ hj), dif_pos hj]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ (do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))) =
    do
    let b ←
      do
        let __do_lift ← p a x[j]
        if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ (do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))) =
    do
    let b ←
      do
        let __do_lift ← p a x[j]
        if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [getElem_cons_zero, getElem_cons_succ, bind_assoc]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ (do
      let __do_lift ← p a x[j]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))) =
    do
    let x_1 ← p a x[j]
    let b ← if x_1 = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ (do
      let __do_lift ← p a x[j]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))) =
    do
    let x_1 ← p a x[j]
    let b ← if x_1 = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
apply bind_congr
State after:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ ∀ (a_1 : Bool),
    (if a_1 = true then pure true
      else
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
          (_ : 0 < Nat.succ (j + 1))) =
      do
      let b ← if a_1 = true then pure true else anyM.loop (p a) x stop h (j + 1)
      if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one

State before:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ ∀ (a_1 : Bool),
    (if a_1 = true then pure true
      else
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
          (_ : 0 < Nat.succ (j + 1))) =
      do
      let b ← if a_1 = true then pure true else anyM.loop (p a) x stop h (j + 1)
      if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
intro b
State after:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ (if b = true then pure true
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
        (_ : 0 < Nat.succ (j + 1))) =
    do
    let b ← if b = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one

State before:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ (if b = true then pure true
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
        (_ : 0 < Nat.succ (j + 1))) =
    do
    let b ← if b = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
match b with
| true => simp only [ite_true, pure_bind]
| false =>
  simp only [ite_false]
  rewrite [anyPairM_loop_cons_zero a x p h (j+1)]
  conv => lhs; lhs; dsimp [anyM]; rw [dif_pos h]
State after:
no goals

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ (if true = true then pure true
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
        (_ : 0 < Nat.succ (j + 1))) =
    do
    let b ← if true = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [ite_true, pure_bind]
State after:
no goals

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ (if false = true then pure true
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
        (_ : 0 < Nat.succ (j + 1))) =
    do
    let b ← if false = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [ite_false]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
      (_ : 0 < Nat.succ (j + 1)) =
    do
    let b ← anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
      (_ : 0 < Nat.succ (j + 1)) =
    do
    let b ← anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
rewrite [anyPairM_loop_cons_zero a x p h (j+1)]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ (do
      let b ← anyM (p a) x (j + 1) stop
      if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one) =
    do
    let b ← anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ (do
      let b ← anyM (p a) x (j + 1) stop
      if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one) =
    do
    let b ← anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
conv => lhs; lhs; dsimp [anyM]; rw [dif_pos h]
State after:
no goals

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : ¬j < stop
⊢ (if h_1 : j + 1 < stop + 1 then do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
        (_ : 0 + 1 < Nat.succ (0 + 1))) =
    do
    let b ←
      if h_1 : j < stop then do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [dif_neg (fun h' => hj (Nat.lt_of_succ_lt_succ h')), dif_neg hj]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : ¬j < stop
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
      (_ : 0 + 1 < Nat.succ (0 + 1)) =
    do
    let b ← pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : ¬j < stop
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
      (_ : 0 + 1 < Nat.succ (0 + 1)) =
    do
    let b ← pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
rewrite [anyPairM_loop_cons_succ a x p h Nat.zero_lt_one]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : ¬j < stop
⊢ anyPairM.loop x p stop h 0 1 Nat.zero_lt_one = do
    let b ← pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : ¬j < stop
⊢ anyPairM.loop x p stop h 0 1 Nat.zero_lt_one = do
    let b ← pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [pure_bind, ite_false]
State after:
no goals