Theorem: Array.anyPairM_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
start stop : Nat
⊢ anyPairM (cons a x) p (start + 1) (stop + 1) = anyPairM x p start stop
Tactic:
dsimp [anyPairM]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
start stop : Nat
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then
      anyPairM.loop (cons a x) p (stop + 1) h (start + 1) (start + 1 + 1) (_ : start + 1 < Nat.succ (start + 1))
    else
      anyPairM.loop (cons a x) p (Nat.succ (size x)) (_ : Nat.le (size (cons a x)) (size (cons a x))) (start + 1)
        (start + 1 + 1) (_ : start + 1 < Nat.succ (start + 1))) =
    if h : stop ≤ size x then anyPairM.loop x p stop h start (start + 1) (_ : start < Nat.succ start)
    else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) start (start + 1) (_ : start < Nat.succ start)

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
start stop : Nat
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then
      anyPairM.loop (cons a x) p (stop + 1) h (start + 1) (start + 1 + 1) (_ : start + 1 < Nat.succ (start + 1))
    else
      anyPairM.loop (cons a x) p (Nat.succ (size x)) (_ : Nat.le (size (cons a x)) (size (cons a x))) (start + 1)
        (start + 1 + 1) (_ : start + 1 < Nat.succ (start + 1))) =
    if h : stop ≤ size x then anyPairM.loop x p stop h start (start + 1) (_ : start < Nat.succ start)
    else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) start (start + 1) (_ : start < Nat.succ start)
Tactic:
if h : stop ≤ x.size then
  rewrite [dif_pos (Nat.succ_le_succ h), dif_pos h]
  exact anyPairM_loop_cons_succ a x p h start.lt_succ_self
else
  rewrite [dif_neg fun h' => h (Nat.le_of_succ_le_succ h'), dif_neg h]
  exact anyPairM_loop_cons_succ a x p .refl start.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
start stop : Nat
h : stop ≤ size x
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then
      anyPairM.loop (cons a x) p (stop + 1) h (start + 1) (start + 1 + 1) (_ : start + 1 < Nat.succ (start + 1))
    else
      anyPairM.loop (cons a x) p (Nat.succ (size x)) (_ : Nat.le (size (cons a x)) (size (cons a x))) (start + 1)
        (start + 1 + 1) (_ : start + 1 < Nat.succ (start + 1))) =
    if h : stop ≤ size x then anyPairM.loop x p stop h start (start + 1) (_ : start < Nat.succ start)
    else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) start (start + 1) (_ : start < Nat.succ start)
Tactic:
rewrite [dif_pos (Nat.succ_le_succ h), dif_pos h]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
start stop : Nat
h : stop ≤ size x
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (size x)) (start + 1) (start + 1 + 1)
      (_ : start + 1 < Nat.succ (start + 1)) =
    anyPairM.loop x p stop h start (start + 1) (_ : start < Nat.succ start)

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
start stop : Nat
h : stop ≤ size x
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (size x)) (start + 1) (start + 1 + 1)
      (_ : start + 1 < Nat.succ (start + 1)) =
    anyPairM.loop x p stop h start (start + 1) (_ : start < Nat.succ start)
Tactic:
exact anyPairM_loop_cons_succ a x p h start.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
start stop : Nat
h : ¬stop ≤ size x
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then
      anyPairM.loop (cons a x) p (stop + 1) h (start + 1) (start + 1 + 1) (_ : start + 1 < Nat.succ (start + 1))
    else
      anyPairM.loop (cons a x) p (Nat.succ (size x)) (_ : Nat.le (size (cons a x)) (size (cons a x))) (start + 1)
        (start + 1 + 1) (_ : start + 1 < Nat.succ (start + 1))) =
    if h : stop ≤ size x then anyPairM.loop x p stop h start (start + 1) (_ : start < Nat.succ start)
    else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) start (start + 1) (_ : start < Nat.succ start)
Tactic:
rewrite [dif_neg fun h' => h (Nat.le_of_succ_le_succ h'), dif_neg h]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
start stop : Nat
h : ¬stop ≤ size x
⊢ anyPairM.loop (cons a x) p (Nat.succ (size x)) (_ : Nat.le (size (cons a x)) (size (cons a x))) (start + 1)
      (start + 1 + 1) (_ : start + 1 < Nat.succ (start + 1)) =
    anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) start (start + 1) (_ : start < Nat.succ start)

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
start stop : Nat
h : ¬stop ≤ size x
⊢ anyPairM.loop (cons a x) p (Nat.succ (size x)) (_ : Nat.le (size (cons a x)) (size (cons a x))) (start + 1)
      (start + 1 + 1) (_ : start + 1 < Nat.succ (start + 1)) =
    anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) start (start + 1) (_ : start < Nat.succ start)
Tactic:
exact anyPairM_loop_cons_succ a x p .refl start.lt_succ_self
State after:
no goals