Theorem: Array.anyM_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
⊢ anyM p (cons a x) 0 (stop + 1) = do
    let b ← p a
    if b = true then pure true else anyM p x 0 stop
Tactic:
dsimp [anyM]
State after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h 0
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) 0) =
    do
    let b ← p a
    if b = true then pure true
      else if h : stop ≤ size x then anyM.loop p x stop h 0 else anyM.loop p x (size x) (_ : size x ≤ size x) 0

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h 0
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) 0) =
    do
    let b ← p a
    if b = true then pure true
      else if h : stop ≤ size x then anyM.loop p x stop h 0 else anyM.loop p x (size x) (_ : size x ≤ size x) 0
Tactic:
if h : stop ≤ x.size then
  simp only [dif_pos h, dif_pos (Nat.succ_le_succ h)]
  exact anyM_loop_cons_zero p a x h
else
  simp only [dif_neg h, dif_neg (fun h' => h <| Nat.le_of_succ_le_succ h')]
  exact anyM_loop_cons_zero p a x .refl
State after:
no goals

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h 0
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) 0) =
    do
    let b ← p a
    if b = true then pure true
      else if h : stop ≤ size x then anyM.loop p x stop h 0 else anyM.loop p x (size x) (_ : size x ≤ size x) 0
Tactic:
simp only [dif_pos h, dif_pos (Nat.succ_le_succ h)]
State after:
α : 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 (size x)) 0 = 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
⊢ anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (size x)) 0 = do
    let b ← p a
    if b = true then pure true else anyM.loop p x stop h 0
Tactic:
exact anyM_loop_cons_zero p a x h
State after:
no goals

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : ¬stop ≤ size x
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h 0
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) 0) =
    do
    let b ← p a
    if b = true then pure true
      else if h : stop ≤ size x then anyM.loop p x stop h 0 else anyM.loop p x (size x) (_ : size x ≤ size x) 0
Tactic:
simp only [dif_neg h, dif_neg (fun h' => h <| Nat.le_of_succ_le_succ h')]
State after:
α : 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) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) 0 = do
    let b ← p a
    if b = true then pure true else anyM.loop p x (size x) (_ : size x ≤ size x) 0

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) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) 0 = do
    let b ← p a
    if b = true then pure true else anyM.loop p x (size x) (_ : size x ≤ size x) 0
Tactic:
exact anyM_loop_cons_zero p a x .refl
State after:
no goals