Theorem: Array.anyM_loop_cons_succ (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
i : Nat
⊢ anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) = anyM.loop p x stop h i
Tactic:
unfold anyM.loop
State after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
i : Nat
⊢ (if hlt : i + 1 < stop + 1 then
      let_fun this := (_ : i + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[i + 1]
      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)) (i + 1 + 1)
    else pure false) =
    if hlt : i < stop then
      let_fun this := (_ : i < size x);
      do
      let __do_lift ← p x[i]
      if __do_lift = true then pure true else anyM.loop p x stop h (i + 1)
    else pure false

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
i : Nat
⊢ (if hlt : i + 1 < stop + 1 then
      let_fun this := (_ : i + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[i + 1]
      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)) (i + 1 + 1)
    else pure false) =
    if hlt : i < stop then
      let_fun this := (_ : i < size x);
      do
      let __do_lift ← p x[i]
      if __do_lift = true then pure true else anyM.loop p x stop h (i + 1)
    else pure false
Tactic:
if hlt : i < stop then
  rewrite [dif_pos hlt, dif_pos (Nat.succ_lt_succ hlt)]
  apply bind_congr; intro b
  match b with
  | true => rfl
  | false =>
    simp only [if_neg]
    exact anyM_loop_cons_succ p a x h (i+1)
else
  rw [dif_neg hlt, dif_neg (fun h => hlt <| Nat.lt_of_succ_lt_succ 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
i : Nat
hlt : i < stop
⊢ (if hlt : i + 1 < stop + 1 then
      let_fun this := (_ : i + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[i + 1]
      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)) (i + 1 + 1)
    else pure false) =
    if hlt : i < stop then
      let_fun this := (_ : i < size x);
      do
      let __do_lift ← p x[i]
      if __do_lift = true then pure true else anyM.loop p x stop h (i + 1)
    else pure false
Tactic:
rewrite [dif_pos hlt, dif_pos (Nat.succ_lt_succ hlt)]
State after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
i : Nat
hlt : i < stop
⊢ (let_fun this := (_ : i + 1 < size (cons a x));
    do
    let __do_lift ← p (cons a x)[i + 1]
    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)) (i + 1 + 1)) =
    let_fun this := (_ : i < size x);
    do
    let __do_lift ← p x[i]
    if __do_lift = true then pure true else anyM.loop p x stop h (i + 1)

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
i : Nat
hlt : i < stop
⊢ (let_fun this := (_ : i + 1 < size (cons a x));
    do
    let __do_lift ← p (cons a x)[i + 1]
    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)) (i + 1 + 1)) =
    let_fun this := (_ : i < size x);
    do
    let __do_lift ← p x[i]
    if __do_lift = true then pure true else anyM.loop p x stop h (i + 1)
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
i : Nat
hlt : i < stop
⊢ ∀ (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)) (i + 1 + 1)) =
      if a_1 = true then pure true else anyM.loop p x stop h (i + 1)

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
i : Nat
hlt : i < stop
⊢ ∀ (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)) (i + 1 + 1)) =
      if a_1 = true then pure true else anyM.loop p x stop h (i + 1)
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
i : Nat
hlt : i < stop
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)) (i + 1 + 1)) =
    if b = true then pure true else anyM.loop p x stop h (i + 1)

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
i : Nat
hlt : i < stop
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)) (i + 1 + 1)) =
    if b = true then pure true else anyM.loop p x stop h (i + 1)
Tactic:
match b with
| true => rfl
| false =>
  simp only [if_neg]
  exact anyM_loop_cons_succ p a x h (i+1)
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
i : Nat
hlt : i < stop
b : Bool
⊢ (if true = true then pure true
    else anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1)) =
    if true = true then pure true else anyM.loop p x stop h (i + 1)
Tactic:
rfl
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
i : Nat
hlt : i < stop
b : Bool
⊢ (if false = true then pure true
    else anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1)) =
    if false = true then pure true else anyM.loop p x stop h (i + 1)
Tactic:
simp only [if_neg]
State after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
i : Nat
hlt : i < stop
b : Bool
⊢ anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) =
    anyM.loop p x stop h (i + 1)

State before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
i : Nat
hlt : i < stop
b : Bool
⊢ anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) =
    anyM.loop p x stop h (i + 1)
Tactic:
exact anyM_loop_cons_succ p a x h (i+1)
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
i : Nat
hlt : ¬i < stop
⊢ (if hlt : i + 1 < stop + 1 then
      let_fun this := (_ : i + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[i + 1]
      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)) (i + 1 + 1)
    else pure false) =
    if hlt : i < stop then
      let_fun this := (_ : i < size x);
      do
      let __do_lift ← p x[i]
      if __do_lift = true then pure true else anyM.loop p x stop h (i + 1)
    else pure false
Tactic:
rw [dif_neg hlt, dif_neg (fun h => hlt <| Nat.lt_of_succ_lt_succ h)]
State after:
no goals