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

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
⊢ anyPairM (cons a x) p 0 (stop + 1) = do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true else anyPairM x p 0 stop
Tactic:
dsimp [anyPairM]
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyPairM.loop (cons a x) p (stop + 1) h 0 (0 + 1) (_ : 0 < Nat.succ 0)
    else
      anyPairM.loop (cons a x) p (Nat.succ (size x)) (_ : Nat.le (size (cons a x)) (size (cons a x))) 0 (0 + 1)
        (_ : 0 < Nat.succ 0)) =
    do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true
      else
        if h : stop ≤ size x then anyPairM.loop x p stop h 0 (0 + 1) (_ : 0 < Nat.succ 0)
        else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) 0 (0 + 1) (_ : 0 < Nat.succ 0)

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

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyPairM.loop (cons a x) p (stop + 1) h 0 (0 + 1) (_ : 0 < Nat.succ 0)
    else
      anyPairM.loop (cons a x) p (Nat.succ (size x)) (_ : Nat.le (size (cons a x)) (size (cons a x))) 0 (0 + 1)
        (_ : 0 < Nat.succ 0)) =
    do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true
      else
        if h : stop ≤ size x then anyPairM.loop x p stop h 0 (0 + 1) (_ : 0 < Nat.succ 0)
        else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) 0 (0 + 1) (_ : 0 < Nat.succ 0)
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
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (size x)) 0 (0 + 1) (_ : 0 < Nat.succ 0) = do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true else anyPairM.loop x p stop h 0 (0 + 1) (_ : 0 < Nat.succ 0)

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (size x)) 0 (0 + 1) (_ : 0 < Nat.succ 0) = do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true else anyPairM.loop x p stop h 0 (0 + 1) (_ : 0 < Nat.succ 0)
Tactic:
exact anyPairM_loop_cons_zero a x p h 0
State after:
no goals

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : ¬stop ≤ size x
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyPairM.loop (cons a x) p (stop + 1) h 0 (0 + 1) (_ : 0 < Nat.succ 0)
    else
      anyPairM.loop (cons a x) p (Nat.succ (size x)) (_ : Nat.le (size (cons a x)) (size (cons a x))) 0 (0 + 1)
        (_ : 0 < Nat.succ 0)) =
    do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true
      else
        if h : stop ≤ size x then anyPairM.loop x p stop h 0 (0 + 1) (_ : 0 < Nat.succ 0)
        else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) 0 (0 + 1) (_ : 0 < Nat.succ 0)
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
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
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))) 0 (0 + 1)
      (_ : 0 < Nat.succ 0) =
    do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true
      else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) 0 (0 + 1) (_ : 0 < Nat.succ 0)

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
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))) 0 (0 + 1)
      (_ : 0 < Nat.succ 0) =
    do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true
      else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) 0 (0 + 1) (_ : 0 < Nat.succ 0)
Tactic:
apply Eq.trans <| anyPairM_loop_cons_zero a x p .refl 0
State after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : ¬stop ≤ size x
⊢ (do
      let b ← anyM (p a) x 0 (size x)
      if b = true then pure true else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) 0 1 Nat.zero_lt_one) =
    do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true
      else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) 0 (0 + 1) (_ : 0 < Nat.succ 0)

State before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : ¬stop ≤ size x
⊢ (do
      let b ← anyM (p a) x 0 (size x)
      if b = true then pure true else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) 0 1 Nat.zero_lt_one) =
    do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true
      else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) 0 (0 + 1) (_ : 0 < Nat.succ 0)
Tactic:
apply congrFun
State after:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : ¬stop ≤ size x
⊢ bind (anyM (p a) x 0 (size x)) = bind (anyM (p a) x 0 stop)

State before:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : ¬stop ≤ size x
⊢ bind (anyM (p a) x 0 (size x)) = bind (anyM (p a) x 0 stop)
Tactic:
apply congrArg
State after:
case h.h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : ¬stop ≤ size x
⊢ anyM (p a) x 0 (size x) = anyM (p a) x 0 stop

State before:
case h.h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : ¬stop ≤ size x
⊢ anyM (p a) x 0 (size x) = anyM (p a) x 0 stop
Tactic:
dsimp [anyM]
State after:
case h.h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : ¬stop ≤ size x
⊢ (if h : size x ≤ size x then anyM.loop (p a) x (size x) h 0 else anyM.loop (p a) x (size x) (_ : size x ≤ size x) 0) =
    if h : stop ≤ size x then anyM.loop (p a) x stop h 0 else anyM.loop (p a) x (size x) (_ : size x ≤ size x) 0

State before:
case h.h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : ¬stop ≤ size x
⊢ (if h : size x ≤ size x then anyM.loop (p a) x (size x) h 0 else anyM.loop (p a) x (size x) (_ : size x ≤ size x) 0) =
    if h : stop ≤ size x then anyM.loop (p a) x stop h 0 else anyM.loop (p a) x (size x) (_ : size x ≤ size x) 0
Tactic:
simp only [dif_pos x.size.le_refl, dif_neg h]
State after:
no goals