internlm/Lean-Github huggingface dataset:
Theorem: Array.swap_comm
Proof state before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]
Tactic:
apply dite (i.1 = k) <;> apply dite (j.1 = k) <;> intros hjk hik
Proof state after:
case t.t
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ↑j = k
hik : ↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case t.e
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ¬↑j = k
hik : ↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case e.t
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ↑j = k
hik : ¬↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case e.e
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ¬↑j = k
hik : ¬↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]
Theorem: Array.swap_comm
Proof state before:
case t.t
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ↑j = k
hik : ↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case t.e
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ¬↑j = k
hik : ↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case e.t
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ↑j = k
hik : ¬↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case e.e
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ¬↑j = k
hik : ¬↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]
Tactic:
all_goals simp only [hik, hjk, if_true, if_false]
Proof state after:
no goals
Theorem: Array.swap_comm
Proof state before:
α : Type u
x : Array α
i j : Fin (size x)
⊢ size (swap x i j) = size (swap x j i)
Tactic:
simp only [size_swap]
Proof state after:
no goals
Theorem: Array.swap_comm
Proof state before:
case e.e
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ¬↑j = k
hik : ¬↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]
Tactic:
simp only [hik, hjk, if_true, if_false]
Proof state after:
no goals
Theorem: Array.anyM_loop_empty
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
stop : Nat
h : stop ≤ 0
i : Nat
⊢ anyM.loop p #[] stop h i = pure false
Tactic:
cases h
Proof state after:
case refl
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
i : Nat
⊢ anyM.loop p #[] 0 (_ : Nat.le 0 0) i = pure false
Theorem: Array.anyM_loop_empty
Proof state before:
case refl
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
i : Nat
⊢ anyM.loop p #[] 0 (_ : Nat.le 0 0) i = pure false
Tactic:
unfold anyM.loop
Proof state after:
case refl
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
i : Nat
⊢ (if hlt : i < 0 then
      let_fun this := (_ : i < size #[]);
      do
      let __do_lift ← p #[][i]
      if __do_lift = true then pure true else anyM.loop p #[] 0 (_ : Nat.le 0 0) (i + 1)
    else pure false) =
    pure false
Theorem: Array.anyM_loop_empty
Proof state before:
case refl
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
i : Nat
⊢ (if hlt : i < 0 then
      let_fun this := (_ : i < size #[]);
      do
      let __do_lift ← p #[][i]
      if __do_lift = true then pure true else anyM.loop p #[] 0 (_ : Nat.le 0 0) (i + 1)
    else pure false) =
    pure false
Tactic:
rw [dif_neg i.not_lt_zero]
Proof state after:
no goals
Theorem: Array.anyM_loop_cons_succ
Proof 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
Proof 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
Theorem: Array.anyM_loop_cons_succ
Proof 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)]
Proof state after:
no goals
Theorem: Array.anyM_loop_cons_succ
Proof 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)]
Proof 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)
Theorem: Array.anyM_loop_cons_succ
Proof 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
Proof 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)
Theorem: Array.anyM_loop_cons_succ
Proof 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
Proof 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)
Theorem: Array.anyM_loop_cons_succ
Proof 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)
Proof state after:
no goals
Theorem: Array.anyM_loop_cons_succ
Proof 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
Proof state after:
no goals
Theorem: Array.anyM_loop_cons_succ
Proof 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]
Proof 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)
Theorem: Array.anyM_loop_cons_succ
Proof 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)
Proof state after:
no goals
Theorem: Array.anyM_loop_cons_succ
Proof 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)]
Proof state after:
no goals
Theorem: Array.anyM_loop_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
⊢ anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 = do
    let b ← p a
    if b = true then pure true else anyM.loop p x stop h 0
Tactic:
conv =>
  lhs; unfold anyM.loop
  rw [dif_pos stop.zero_lt_succ]
  simp only [getElem_cons_zero]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
⊢ (do
      let __do_lift ← p a
      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)) (0 + 1)) =
    do
    let b ← p a
    if b = true then pure true else anyM.loop p x stop h 0
Theorem: Array.anyM_loop_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
⊢ (do
      let __do_lift ← p a
      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)) (0 + 1)) =
    do
    let b ← p a
    if b = true then pure true else anyM.loop p x stop h 0
Tactic:
apply bind_congr
Proof 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
⊢ ∀ (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)) (0 + 1)) =
      if a_1 = true then pure true else anyM.loop p x stop h 0
Theorem: Array.anyM_loop_cons_zero
Proof 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
⊢ ∀ (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)) (0 + 1)) =
      if a_1 = true then pure true else anyM.loop p x stop h 0
Tactic:
intro b
Proof 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
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)) (0 + 1)) =
    if b = true then pure true else anyM.loop p x stop h 0
Theorem: Array.anyM_loop_cons_zero
Proof 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
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)) (0 + 1)) =
    if b = true then pure true else anyM.loop p x stop h 0
Tactic:
rw [anyM_loop_cons_succ p a x h 0]
Proof state after:
no goals
Theorem: Array.anyM_empty
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
⊢ anyM p #[] start stop = pure false
Tactic:
dsimp [anyM]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
⊢ (if h : stop ≤ 0 then anyM.loop p #[] stop h start else anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start) =
    pure false
Theorem: Array.anyM_empty
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
⊢ (if h : stop ≤ 0 then anyM.loop p #[] stop h start else anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start) =
    pure false
Tactic:
if h : stop ≤ 0 then
  rewrite [dif_pos h]
  exact anyM_loop_empty p h start
else
  rewrite [dif_neg h]
  exact anyM_loop_empty p .refl start
Proof state after:
no goals
Theorem: Array.anyM_empty
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
h : stop ≤ 0
⊢ (if h : stop ≤ 0 then anyM.loop p #[] stop h start else anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start) =
    pure false
Tactic:
rewrite [dif_pos h]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
h : stop ≤ 0
⊢ anyM.loop p #[] stop h start = pure false
Theorem: Array.anyM_empty
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
h : stop ≤ 0
⊢ anyM.loop p #[] stop h start = pure false
Tactic:
exact anyM_loop_empty p h start
Proof state after:
no goals
Theorem: Array.anyM_empty
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
h : ¬stop ≤ 0
⊢ (if h : stop ≤ 0 then anyM.loop p #[] stop h start else anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start) =
    pure false
Tactic:
rewrite [dif_neg h]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
h : ¬stop ≤ 0
⊢ anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start = pure false
Theorem: Array.anyM_empty
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
h : ¬stop ≤ 0
⊢ anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start = pure false
Tactic:
exact anyM_loop_empty p .refl start
Proof state after:
no goals
Theorem: Array.anyM_cons_succ
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
start stop : Nat
⊢ anyM p (cons a x) (start + 1) (stop + 1) = anyM p x start stop
Tactic:
dsimp [anyM]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
start stop : Nat
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h (start + 1)
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) (start + 1)) =
    if h : stop ≤ size x then anyM.loop p x stop h start else anyM.loop p x (size x) (_ : size x ≤ size x) start
Theorem: Array.anyM_cons_succ
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
start stop : Nat
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h (start + 1)
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) (start + 1)) =
    if h : stop ≤ size x then anyM.loop p x stop h start else anyM.loop p x (size x) (_ : size x ≤ size x) start
Tactic:
if h : stop ≤ x.size then
  rewrite [dif_pos h, dif_pos (Nat.succ_le_succ h)]
  exact anyM_loop_cons_succ p a x h start
else
  rewrite [dif_neg h, dif_neg (fun h' => h <| Nat.le_of_succ_le_succ h')]
  exact anyM_loop_cons_succ p a x .refl start
Proof state after:
no goals
Theorem: Array.anyM_cons_succ
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
start stop : Nat
h : stop ≤ size x
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h (start + 1)
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) (start + 1)) =
    if h : stop ≤ size x then anyM.loop p x stop h start else anyM.loop p x (size x) (_ : size x ≤ size x) start
Tactic:
rewrite [dif_pos h, dif_pos (Nat.succ_le_succ h)]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
start stop : Nat
h : stop ≤ size x
⊢ anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (size x)) (start + 1) = anyM.loop p x stop h start
Theorem: Array.anyM_cons_succ
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
start stop : Nat
h : stop ≤ size x
⊢ anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (size x)) (start + 1) = anyM.loop p x stop h start
Tactic:
exact anyM_loop_cons_succ p a x h start
Proof state after:
no goals
Theorem: Array.anyM_cons_succ
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
start stop : Nat
h : ¬stop ≤ size x
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h (start + 1)
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) (start + 1)) =
    if h : stop ≤ size x then anyM.loop p x stop h start else anyM.loop p x (size x) (_ : size x ≤ size x) start
Tactic:
rewrite [dif_neg h, dif_neg (fun h' => h <| Nat.le_of_succ_le_succ h')]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
start stop : Nat
h : ¬stop ≤ size x
⊢ anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) (start + 1) =
    anyM.loop p x (size x) (_ : size x ≤ size x) start
Theorem: Array.anyM_cons_succ
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
start stop : Nat
h : ¬stop ≤ size x
⊢ anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) (start + 1) =
    anyM.loop p x (size x) (_ : size x ≤ size x) start
Tactic:
exact anyM_loop_cons_succ p a x .refl start
Proof state after:
no goals
Theorem: Array.anyM_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
⊢ anyM p (cons a x) 0 (stop + 1) = do
    let b ← p a
    if b = true then pure true else anyM p x 0 stop
Tactic:
dsimp [anyM]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h 0
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) 0) =
    do
    let b ← p a
    if b = true then pure true
      else if h : stop ≤ size x then anyM.loop p x stop h 0 else anyM.loop p x (size x) (_ : size x ≤ size x) 0
Theorem: Array.anyM_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h 0
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) 0) =
    do
    let b ← p a
    if b = true then pure true
      else if h : stop ≤ size x then anyM.loop p x stop h 0 else anyM.loop p x (size x) (_ : size x ≤ size x) 0
Tactic:
if h : stop ≤ x.size then
  simp only [dif_pos h, dif_pos (Nat.succ_le_succ h)]
  exact anyM_loop_cons_zero p a x h
else
  simp only [dif_neg h, dif_neg (fun h' => h <| Nat.le_of_succ_le_succ h')]
  exact anyM_loop_cons_zero p a x .refl
Proof state after:
no goals
Theorem: Array.anyM_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h 0
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) 0) =
    do
    let b ← p a
    if b = true then pure true
      else if h : stop ≤ size x then anyM.loop p x stop h 0 else anyM.loop p x (size x) (_ : size x ≤ size x) 0
Tactic:
simp only [dif_pos h, dif_pos (Nat.succ_le_succ h)]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
⊢ anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (size x)) 0 = do
    let b ← p a
    if b = true then pure true else anyM.loop p x stop h 0
Theorem: Array.anyM_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : stop ≤ size x
⊢ anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (size x)) 0 = do
    let b ← p a
    if b = true then pure true else anyM.loop p x stop h 0
Tactic:
exact anyM_loop_cons_zero p a x h
Proof state after:
no goals