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

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
⊢ anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 = do
    let b ← p a
    if b = true then pure true else anyM.loop p x stop h 0
Tactic:
conv =>
  lhs; unfold anyM.loop
  rw [dif_pos stop.zero_lt_succ]
  simp only [getElem_cons_zero]
State after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
⊢ (do
      let __do_lift ← p a
      if __do_lift = true then pure true
        else anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1)) =
    do
    let b ← p a
    if b = true then pure true else anyM.loop p x stop h 0

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

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

State before:
case h
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
b : Bool
⊢ (if b = true then pure true
    else anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1)) =
    if b = true then pure true else anyM.loop p x stop h 0
Tactic:
rw [anyM_loop_cons_succ p a x h 0]
State after:
no goals