internlm/Lean-Github huggingface dataset:
Theorem: Array.anyPairM_empty
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
⊢ (if h : stop ≤ 0 then anyPairM.loop #[] p stop (_ : stop ≤ size #[]) start (start + 1) (_ : start < Nat.succ start)
    else anyPairM.loop #[] p 0 (_ : 0 ≤ size #[]) start (start + 1) (_ : start < Nat.succ start)) =
    pure false
Tactic:
if h : stop ≤ 0 then
  rewrite [dif_pos h]
  exact anyPairM_loop_empty p h start.lt_succ_self
else
  rewrite [dif_neg h]
  exact anyPairM_loop_empty p .refl start.lt_succ_self
Proof state after:
no goals
Theorem: Array.anyPairM_empty
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
h : stop ≤ 0
⊢ (if h : stop ≤ 0 then anyPairM.loop #[] p stop (_ : stop ≤ size #[]) start (start + 1) (_ : start < Nat.succ start)
    else anyPairM.loop #[] p 0 (_ : 0 ≤ size #[]) start (start + 1) (_ : start < Nat.succ start)) =
    pure false
Tactic:
rewrite [dif_pos h]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
h : stop ≤ 0
⊢ anyPairM.loop #[] p stop (_ : stop ≤ size #[]) start (start + 1) (_ : start < Nat.succ start) = pure false
Theorem: Array.anyPairM_empty
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
h : stop ≤ 0
⊢ anyPairM.loop #[] p stop (_ : stop ≤ size #[]) start (start + 1) (_ : start < Nat.succ start) = pure false
Tactic:
exact anyPairM_loop_empty p h start.lt_succ_self
Proof state after:
no goals
Theorem: Array.anyPairM_empty
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
h : ¬stop ≤ 0
⊢ (if h : stop ≤ 0 then anyPairM.loop #[] p stop (_ : stop ≤ size #[]) start (start + 1) (_ : start < Nat.succ start)
    else anyPairM.loop #[] p 0 (_ : 0 ≤ size #[]) start (start + 1) (_ : start < Nat.succ start)) =
    pure false
Tactic:
rewrite [dif_neg h]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
h : ¬stop ≤ 0
⊢ anyPairM.loop #[] p 0 (_ : 0 ≤ size #[]) start (start + 1) (_ : start < Nat.succ start) = pure false
Theorem: Array.anyPairM_empty
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
h : ¬stop ≤ 0
⊢ anyPairM.loop #[] p 0 (_ : 0 ≤ size #[]) start (start + 1) (_ : start < Nat.succ start) = pure false
Tactic:
exact anyPairM_loop_empty p .refl start.lt_succ_self
Proof state after:
no goals
Theorem: Array.anyPairM_cons_succ
Proof 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]
Proof 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)
Theorem: Array.anyPairM_cons_succ
Proof 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
Proof state after:
no goals
Theorem: Array.anyPairM_cons_succ
Proof 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]
Proof 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)
Theorem: Array.anyPairM_cons_succ
Proof 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
Proof state after:
no goals
Theorem: Array.anyPairM_cons_succ
Proof 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]
Proof 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)
Theorem: Array.anyPairM_cons_succ
Proof 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
Proof state after:
no goals
Theorem: Array.anyPairM_cons_zero
Proof 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]
Proof 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)
Theorem: Array.anyPairM_cons_zero
Proof 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]
Proof state after:
no goals
Theorem: Array.anyPairM_cons_zero
Proof 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]
Proof 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)
Theorem: Array.anyPairM_cons_zero
Proof 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
Proof state after:
no goals
Theorem: Array.anyPairM_cons_zero
Proof 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]
Proof 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)
Theorem: Array.anyPairM_cons_zero
Proof 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
Proof 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)
Theorem: Array.anyPairM_cons_zero
Proof 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
Proof 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)
Theorem: Array.anyPairM_cons_zero
Proof 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
Proof 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
Theorem: Array.anyPairM_cons_zero
Proof 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]
Proof 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
Theorem: Array.anyPairM_cons_zero
Proof 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]
Proof state after:
no goals
Theorem: Array.anyPair_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ anyPair (cons a x) p 0 (stop + 1) = (any x (p a) 0 stop || anyPair x p 0 stop)
Tactic:
apply Eq.trans <| anyPairM_cons_zero (m:=Id) a x p
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (do
      let b ← anyM (p a) x 0 stop
      if b = true then pure true else anyPairM x p 0 stop) =
    (any x (p a) 0 stop || anyPair x p 0 stop)
Theorem: Array.anyPair_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (do
      let b ← anyM (p a) x 0 stop
      if b = true then pure true else anyPairM x p 0 stop) =
    (any x (p a) 0 stop || anyPair x p 0 stop)
Tactic:
conv =>
  lhs; change if any x (p a) 0 stop = true then true else anyPair x p 0 stop
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (if any x (p a) 0 stop = true then true else anyPair x p 0 stop) = (any x (p a) 0 stop || anyPair x p 0 stop)
Theorem: Array.anyPair_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (if any x (p a) 0 stop = true then true else anyPair x p 0 stop) = (any x (p a) 0 stop || anyPair x p 0 stop)
Tactic:
match any x (p a) 0 stop with
| true => simp only [ite_true, Bool.true_or]
| false => simp only [ite_false, Bool.false_or]
Proof state after:
no goals
Theorem: Array.anyPair_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (if true = true then true else anyPair x p 0 stop) = (true || anyPair x p 0 stop)
Tactic:
simp only [ite_true, Bool.true_or]
Proof state after:
no goals
Theorem: Array.anyPair_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (if false = true then true else anyPair x p 0 stop) = (false || anyPair x p 0 stop)
Tactic:
simp only [ite_false, Bool.false_or]
Proof state after:
no goals
Theorem: Array.nodup_empty
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
⊢ Nodup #[]
Tactic:
dsimp [Nodup]
Proof state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
⊢ anyPair #[] BEq.beq 0 (size #[]) = false
Theorem: Array.nodup_empty
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
⊢ anyPair #[] BEq.beq 0 (size #[]) = false
Tactic:
exact anyPair_empty BEq.beq
Proof state after:
no goals
Theorem: Array.nodup_cons
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ Nodup (cons a x) ↔ ¬a ∈ x ∧ Nodup x
Tactic:
dsimp [Nodup]
Proof state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ anyPair (cons a x) BEq.beq 0 (Nat.succ (size x)) = false ↔ ¬a ∈ x ∧ anyPair x BEq.beq 0 (size x) = false
Theorem: Array.nodup_cons
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ anyPair (cons a x) BEq.beq 0 (Nat.succ (size x)) = false ↔ ¬a ∈ x ∧ anyPair x BEq.beq 0 (size x) = false
Tactic:
conv =>
  pattern a ∉ x; change ¬(x.any (BEq.beq a) = true); rw [Bool.not_eq_true]
Proof state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ anyPair (cons a x) BEq.beq 0 (Nat.succ (size x)) = false ↔
    any x (BEq.beq a) 0 (size x) = false ∧ anyPair x BEq.beq 0 (size x) = false
Theorem: Array.nodup_cons
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ anyPair (cons a x) BEq.beq 0 (Nat.succ (size x)) = false ↔
    any x (BEq.beq a) 0 (size x) = false ∧ anyPair x BEq.beq 0 (size x) = false
Tactic:
rewrite [anyPair_cons_zero]
Proof state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (any x (BEq.beq a) 0 (size x) || anyPair x BEq.beq 0 (size x)) = false ↔
    any x (BEq.beq a) 0 (size x) = false ∧ anyPair x BEq.beq 0 (size x) = false
Theorem: Array.nodup_cons
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (any x (BEq.beq a) 0 (size x) || anyPair x BEq.beq 0 (size x)) = false ↔
    any x (BEq.beq a) 0 (size x) = false ∧ anyPair x BEq.beq 0 (size x) = false
Tactic:
match x.any (BEq.beq a) with
| true => simp only [Bool.true_or, false_and]
| false => simp only [Bool.false_or, true_and]
Proof state after:
no goals
Theorem: Array.nodup_cons
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (true || anyPair x BEq.beq 0 (size x)) = false ↔ true = false ∧ anyPair x BEq.beq 0 (size x) = false
Tactic:
simp only [Bool.true_or, false_and]
Proof state after:
no goals
Theorem: Array.nodup_cons
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (false || anyPair x BEq.beq 0 (size x)) = false ↔ false = false ∧ anyPair x BEq.beq 0 (size x) = false
Tactic:
simp only [Bool.false_or, true_and]
Proof state after:
no goals
Theorem: List.get_congr
Proof state before:
α : Type u
β : Type v
γ : Type w
x y : List α
i : Fin (length x)
j✝ : Fin (length y)
j : Fin (length x)
h : ↑i = ↑j
⊢ get x i = get x j
Tactic:
rw [Fin.eq_of_val_eq h]
Proof state after:
no goals
Theorem: List.get_concat_length
Proof state before:
α : Type u
β : Type v
γ : Type w
l : List α
a : α
h : length l < length (l ++ [a])
⊢ get (l ++ [a]) { val := length l, isLt := h } = a
Tactic:
apply Option.some.inj
Proof state after:
case x
α : Type u
β : Type v
γ : Type w
l : List α
a : α
h : length l < length (l ++ [a])
⊢ some (get (l ++ [a]) { val := length l, isLt := h }) = some a
Theorem: List.get_concat_length
Proof state before:
case x
α : Type u
β : Type v
γ : Type w
l : List α
a : α
h : length l < length (l ++ [a])
⊢ some (get (l ++ [a]) { val := length l, isLt := h }) = some a
Tactic:
rw [←get?_eq_get, get?_concat_length]
Proof state after:
no goals
Theorem: List.get_take
Proof state before:
α : Type u
β : Type v
γ : Type w
l : List α
n i : Nat
hi₁ : i < length (take n l)
hi₂ : i < length l
⊢ get (take n l) { val := i, isLt := hi₁ } = get l { val := i, isLt := hi₂ }
Tactic:
rw [get_of_eq (l.take_append_drop n).symm, get_append_left]
Proof state after:
no goals
Theorem: List.dropLast_concat_getLast
Proof state before:
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ dropLast as ++ [getLast as h] = as
Tactic:
rw [as.dropLast_eq_take, as.singleton_getLast_eq_drop]
Proof state after:
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ take (length as - 1) as ++ drop (length as - 1) as = as
Theorem: List.dropLast_concat_getLast
Proof state before:
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ take (length as - 1) as ++ drop (length as - 1) as = as
Tactic:
exact as.take_append_drop (as.length - 1)
Proof state after:
no goals
Theorem: List.dropLast_concat_getLast'
Proof state before:
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ concat (dropLast as) (getLast as h) = as
Tactic:
rw [List.concat_eq_append]
Proof state after:
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ dropLast as ++ [getLast as h] = as
Theorem: List.dropLast_concat_getLast'
Proof state before:
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ dropLast as ++ [getLast as h] = as
Tactic:
exact as.dropLast_concat_getLast h
Proof state after:
no goals