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

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

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : i + 1 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[i + 1] (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)) (i + 1) (j + 1 + 1)
            (_ : i + 1 < Nat.succ (j + 1))
    else
      if i + 1 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1)
          (i + 1 + 2) (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
      else pure false) =
    if hj : j < stop then
      let_fun this := (_ : i < size x);
      let_fun this_1 := (_ : j < size x);
      do
      let __do_lift ← p x[i] x[j]
      if __do_lift = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
    else if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Tactic:
if hj : j < stop then
  rewrite [dif_pos (Nat.succ_lt_succ hj), dif_pos hj]
  apply bind_congr; intro b
  match b with
  | true => rfl
  | false =>
    simp only [ite_false]
    exact anyPairM_loop_cons_succ a x p h (.step hij)
else
  rewrite [dif_neg (fun h' => hj (Nat.lt_of_succ_lt_succ h')), dif_neg hj]
  if hi : i < stop then
    rewrite [if_pos (Nat.succ_lt_succ hi), if_pos hi]
    exact anyPairM_loop_cons_succ a x p h (i+1).lt_succ_self
  else
    rw [if_neg (fun h' => hi (Nat.lt_of_succ_lt_succ h')), if_neg hi]
State after:
no goals

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : i + 1 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[i + 1] (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)) (i + 1) (j + 1 + 1)
            (_ : i + 1 < Nat.succ (j + 1))
    else
      if i + 1 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1)
          (i + 1 + 2) (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
      else pure false) =
    if hj : j < stop then
      let_fun this := (_ : i < size x);
      let_fun this_1 := (_ : j < size x);
      do
      let __do_lift ← p x[i] x[j]
      if __do_lift = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
    else if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Tactic:
rewrite [dif_pos (Nat.succ_lt_succ hj), dif_pos hj]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
⊢ (let_fun this := (_ : i + 1 < size (cons a x));
    let_fun this_1 := (_ : j + 1 < size (cons a x));
    do
    let __do_lift ← p (cons a x)[i + 1] (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)) (i + 1) (j + 1 + 1)
          (_ : i + 1 < Nat.succ (j + 1))) =
    let_fun this := (_ : i < size x);
    let_fun this_1 := (_ : j < size x);
    do
    let __do_lift ← p x[i] x[j]
    if __do_lift = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
⊢ (let_fun this := (_ : i + 1 < size (cons a x));
    let_fun this_1 := (_ : j + 1 < size (cons a x));
    do
    let __do_lift ← p (cons a x)[i + 1] (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)) (i + 1) (j + 1 + 1)
          (_ : i + 1 < Nat.succ (j + 1))) =
    let_fun this := (_ : i < size x);
    let_fun this_1 := (_ : j < size x);
    do
    let __do_lift ← p x[i] x[j]
    if __do_lift = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Tactic:
apply bind_congr
State after:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
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)) (i + 1) (j + 1 + 1)
          (_ : i + 1 < Nat.succ (j + 1))) =
      if a_1 = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)

State before:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
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)) (i + 1) (j + 1 + 1)
          (_ : i + 1 < Nat.succ (j + 1))) =
      if a_1 = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Tactic:
intro b
State after:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
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)) (i + 1) (j + 1 + 1)
        (_ : i + 1 < Nat.succ (j + 1))) =
    if b = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)

State before:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
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)) (i + 1) (j + 1 + 1)
        (_ : i + 1 < Nat.succ (j + 1))) =
    if b = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Tactic:
match b with
| true => rfl
| false =>
  simp only [ite_false]
  exact anyPairM_loop_cons_succ a x p h (.step hij)
State after:
no goals

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
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)) (i + 1) (j + 1 + 1)
        (_ : i + 1 < Nat.succ (j + 1))) =
    if true = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Tactic:
rfl
State after:
no goals

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
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)) (i + 1) (j + 1 + 1)
        (_ : i + 1 < Nat.succ (j + 1))) =
    if false = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Tactic:
simp only [ite_false]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
b : Bool
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
      (_ : i + 1 < Nat.succ (j + 1)) =
    anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
b : Bool
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
      (_ : i + 1 < Nat.succ (j + 1)) =
    anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Tactic:
exact anyPairM_loop_cons_succ a x p h (.step hij)
State after:
no goals

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : i + 1 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[i + 1] (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)) (i + 1) (j + 1 + 1)
            (_ : i + 1 < Nat.succ (j + 1))
    else
      if i + 1 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1)
          (i + 1 + 2) (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
      else pure false) =
    if hj : j < stop then
      let_fun this := (_ : i < size x);
      let_fun this_1 := (_ : j < size x);
      do
      let __do_lift ← p x[i] x[j]
      if __do_lift = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
    else if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Tactic:
rewrite [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
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
⊢ (if i + 1 < stop + 1 then
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
        (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
    else pure false) =
    if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
⊢ (if i + 1 < stop + 1 then
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
        (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
    else pure false) =
    if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Tactic:
if hi : i < stop then
  rewrite [if_pos (Nat.succ_lt_succ hi), if_pos hi]
  exact anyPairM_loop_cons_succ a x p h (i+1).lt_succ_self
else
  rw [if_neg (fun h' => hi (Nat.lt_of_succ_lt_succ h')), if_neg hi]
State after:
no goals

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
hi : i < stop
⊢ (if i + 1 < stop + 1 then
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
        (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
    else pure false) =
    if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Tactic:
rewrite [if_pos (Nat.succ_lt_succ hi), if_pos hi]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
hi : i < stop
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
      (_ : i + 1 + 1 < Nat.succ (i + 1 + 1)) =
    anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1))

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
hi : i < stop
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
      (_ : i + 1 + 1 < Nat.succ (i + 1 + 1)) =
    anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1))
Tactic:
exact anyPairM_loop_cons_succ a x p h (i+1).lt_succ_self
State after:
no goals

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
hi : ¬i < stop
⊢ (if i + 1 < stop + 1 then
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
        (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
    else pure false) =
    if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Tactic:
rw [if_neg (fun h' => hi (Nat.lt_of_succ_lt_succ h')), if_neg hi]
State after:
no goals