internlm/Lean-Github huggingface dataset:
Theorem: SizedArray.mem_iff_get
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i, x[↑i] = a) → ∃ i hi, x.val[i] = a
Tactic:
. exact fun ⟨i,hxi⟩ => ⟨i.1, x.size_eq.symm ▸ i.2, hxi⟩
Proof state after:
no goals
Theorem: SizedArray.mem_iff_get
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i hi, x.val[i] = a) → ∃ i, x[↑i] = a
Tactic:
exact fun ⟨i,hi,hxi⟩ => ⟨⟨i, x.size_eq.symm ▸ hi⟩, hxi⟩
Proof state after:
no goals
Theorem: SizedArray.mem_iff_get
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i, x[↑i] = a) → ∃ i hi, x.val[i] = a
Tactic:
exact fun ⟨i,hxi⟩ => ⟨i.1, x.size_eq.symm ▸ i.2, hxi⟩
Proof state after:
no goals
Theorem: SizedArray.get_set_ite
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
j : Nat
hj : j < n
⊢ (set x i v)[j] = if ↑i = j then v else x[j]
Tactic:
if hij : i.1 = j then
  cases hij; rw [if_pos rfl, get_set_eq]
else
  rw [get_set_ne (h:=hij), if_neg hij]
Proof state after:
no goals
Theorem: SizedArray.get_set_ite
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
j : Nat
hj : j < n
hij : ↑i = j
⊢ (set x i v)[j] = if ↑i = j then v else x[j]
Tactic:
cases hij
Proof state after:
case refl
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
hj : ↑i < n
⊢ (set x i v)[↑i] = if ↑i = ↑i then v else x[↑i]
Theorem: SizedArray.get_set_ite
Proof state before:
case refl
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
hj : ↑i < n
⊢ (set x i v)[↑i] = if ↑i = ↑i then v else x[↑i]
Tactic:
rw [if_pos rfl, get_set_eq]
Proof state after:
no goals
Theorem: SizedArray.get_set_ite
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
j : Nat
hj : j < n
hij : ¬↑i = j
⊢ (set x i v)[j] = if ↑i = j then v else x[j]
Tactic:
rw [get_set_ne (h:=hij), if_neg hij]
Proof state after:
no goals
Theorem: SizedArray.set_set_eq
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
a b : α
j : Nat
hj : j < n
⊢ (set (set x i a) i b)[j] = (set x i b)[j]
Tactic:
if hij : i.1 = j then
  cases hij; simp only [get_set_eq]
else
  simp only [get_set_ne (h:=hij)]
Proof state after:
no goals
Theorem: SizedArray.set_set_eq
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
a b : α
j : Nat
hj : j < n
hij : ↑i = j
⊢ (set (set x i a) i b)[j] = (set x i b)[j]
Tactic:
cases hij
Proof state after:
case refl
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
a b : α
hj : ↑i < n
⊢ (set (set x i a) i b)[↑i] = (set x i b)[↑i]
Theorem: SizedArray.set_set_eq
Proof state before:
case refl
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
a b : α
hj : ↑i < n
⊢ (set (set x i a) i b)[↑i] = (set x i b)[↑i]
Tactic:
simp only [get_set_eq]
Proof state after:
no goals
Theorem: SizedArray.set_set_eq
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
a b : α
j : Nat
hj : j < n
hij : ¬↑i = j
⊢ (set (set x i a) i b)[j] = (set x i b)[j]
Tactic:
simp only [get_set_ne (h:=hij)]
Proof state after:
no goals
Theorem: SizedArray.set_set_comm
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
⊢ (set (set x i a) j b)[k] = (set (set x j b) i a)[k]
Tactic:
simp only [get_set_ite]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]
Theorem: SizedArray.set_set_comm
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]
Tactic:
apply dite (j.1 = k) <;> apply dite (i.1 = k) <;> intro hik hjk
Proof state after:
case t.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case t.e
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case e.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case e.e
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]
Theorem: SizedArray.set_set_comm
Proof state before:
case t.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case t.e
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case e.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case e.e
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]
Tactic:
all_goals simp only [hik, hjk, if_pos, if_neg]
Proof state after:
case t.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ b = a
Theorem: SizedArray.set_set_comm
Proof state before:
case t.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ b = a
Tactic:
cases hjk
Proof state after:
case t.t.refl
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
hk : ↑j < n
hik : ↑i = ↑j
⊢ b = a
Theorem: SizedArray.set_set_comm
Proof state before:
case t.t.refl
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
hk : ↑j < n
hik : ↑i = ↑j
⊢ b = a
Tactic:
exact absurd (Fin.eq_of_val_eq hik) h
Proof state after:
no goals
Theorem: SizedArray.set_set_comm
Proof state before:
case e.e
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]
Tactic:
simp only [hik, hjk, if_pos, if_neg]
Proof state after:
no goals
Theorem: SizedArray.swap_eq
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ (swap x i j).val = (set (set x i x[↑j]) j x[↑i]).val
Tactic:
dsimp only [swap]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ Array.swap x.val (Fin.cast (_ : n = Array.size x.val) i) (Fin.cast (_ : n = Array.size x.val) j) =
    (set (set x i x[↑j]) j x[↑i]).val
Theorem: SizedArray.swap_eq
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ Array.swap x.val (Fin.cast (_ : n = Array.size x.val) i) (Fin.cast (_ : n = Array.size x.val) j) =
    (set (set x i x[↑j]) j x[↑i]).val
Tactic:
simp only [Array.swap_def]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ Array.set
      (Array.set x.val (Fin.cast (_ : n = Array.size x.val) i)
        (Array.get x.val (Fin.cast (_ : n = Array.size x.val) j)))
      { val := ↑(Fin.cast (_ : n = Array.size x.val) j),
        isLt :=
          (_ :
            ↑(Fin.cast (_ : n = Array.size x.val) j) <
              Array.size
                (Array.set x.val (Fin.cast (_ : n = Array.size x.val) i)
                  x.val[↑(Fin.cast (_ : n = Array.size x.val) j)])) }
      (Array.get x.val (Fin.cast (_ : n = Array.size x.val) i)) =
    (set (set x i x[↑j]) j x[↑i]).val
Theorem: SizedArray.swap_eq
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ Array.set
      (Array.set x.val (Fin.cast (_ : n = Array.size x.val) i)
        (Array.get x.val (Fin.cast (_ : n = Array.size x.val) j)))
      { val := ↑(Fin.cast (_ : n = Array.size x.val) j),
        isLt :=
          (_ :
            ↑(Fin.cast (_ : n = Array.size x.val) j) <
              Array.size
                (Array.set x.val (Fin.cast (_ : n = Array.size x.val) i)
                  x.val[↑(Fin.cast (_ : n = Array.size x.val) j)])) }
      (Array.get x.val (Fin.cast (_ : n = Array.size x.val) i)) =
    (set (set x i x[↑j]) j x[↑i]).val
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.swap_comm
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ swap x i j = swap x j i
Tactic:
iterate rewrite [swap_eq]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ set (set x i x[↑j]) j x[↑i] = set (set x j x[↑i]) i x[↑j]
Theorem: SizedArray.swap_comm
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ set (set x i x[↑j]) j x[↑i] = set (set x j x[↑i]) i x[↑j]
Tactic:
if hij : i = j then
  cases hij; rfl
else
  exact x.set_set_comm hij x[j.1] x[i.1]
Proof state after:
no goals
Theorem: SizedArray.swap_comm
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ set (set x i x[↑j]) j x[↑i] = swap x j i
Tactic:
rewrite [swap_eq]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ set (set x i x[↑j]) j x[↑i] = set (set x j x[↑i]) i x[↑j]
Theorem: SizedArray.swap_comm
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
hij : i = j
⊢ set (set x i x[↑j]) j x[↑i] = set (set x j x[↑i]) i x[↑j]
Tactic:
cases hij
Proof state after:
case refl
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
⊢ set (set x i x[↑i]) i x[↑i] = set (set x i x[↑i]) i x[↑i]
Theorem: SizedArray.swap_comm
Proof state before:
case refl
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
⊢ set (set x i x[↑i]) i x[↑i] = set (set x i x[↑i]) i x[↑i]
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.swap_comm
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
hij : ¬i = j
⊢ set (set x i x[↑j]) j x[↑i] = set (set x j x[↑i]) i x[↑j]
Tactic:
exact x.set_set_comm hij x[j.1] x[i.1]
Proof state after:
no goals
Theorem: SizedArray.get_swap_second
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ (swap x i j)[↑j] = x[↑i]
Tactic:
rw [swap_eq, get_set_eq]
Proof state after:
no goals
Theorem: SizedArray.get_swap_first
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ (swap x i j)[↑i] = x[↑j]
Tactic:
rw [swap_comm, get_swap_second]
Proof state after:
no goals
Theorem: SizedArray.get_swap
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
k : Nat
hk : k < n
⊢ (swap x i j)[k] = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
rw [swap_eq, get_set_ite, get_set_ite]
Proof state after:
no goals
Theorem: SizedArray.get_replicate
Proof state before:
α : Type u
n✝ : Nat
a : α
i✝ n i : Nat
h : i + 1 < n + 1
⊢ (replicate (n + 1) a)[i + 1] = a
Tactic:
simp only [replicate_succ_eq_cons, get_cons_succ (hi₁:=h) (hi₂:=Nat.lt_of_succ_lt_succ h)]
Proof state after:
α : Type u
n✝ : Nat
a : α
i✝ n i : Nat
h : i + 1 < n + 1
⊢ (replicate n a)[i] = a
Theorem: SizedArray.get_replicate
Proof state before:
α : Type u
n✝ : Nat
a : α
i✝ n i : Nat
h : i + 1 < n + 1
⊢ (replicate n a)[i] = a
Tactic:
exact get_replicate (a:=a) (i:=i) (h:=Nat.lt_of_succ_lt_succ h)
Proof state after:
no goals
Theorem: SizedArray.replicate_succ_eq_push
Proof state before:
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
⊢ (replicate (n + 1) a)[i] = (push (replicate n a) a)[i]
Tactic:
simp only [get_replicate, get_push]
Proof state after:
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
⊢ a = if h : i < n then a else a
Theorem: SizedArray.replicate_succ_eq_push
Proof state before:
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
⊢ a = if h : i < n then a else a
Tactic:
apply dite (i < n) <;> (intro h; simp only [h]; rfl)
Proof state after:
no goals
Theorem: SizedArray.replicate_succ_eq_push
Proof state before:
case e
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
⊢ ¬i < n → a = if h : i < n then a else a
Tactic:
intro h
Proof state after:
case e
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
h : ¬i < n
⊢ a = if h : i < n then a else a
Theorem: SizedArray.replicate_succ_eq_push
Proof state before:
case e
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
h : ¬i < n
⊢ a = if h : i < n then a else a
Tactic:
simp only [h]
Proof state after:
case e
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
h : ¬i < n
⊢ a = if h : False then a else a
Theorem: SizedArray.replicate_succ_eq_push
Proof state before:
case e
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
h : ¬i < n
⊢ a = if h : False then a else a
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.foldlMIdx_empty
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ foldlMIdx f init empty = pure init
Tactic:
unfold foldlMIdx
Proof state after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ foldlMIdx.loop f empty 0 (_ : 0 ≤ 0) init = pure init
Theorem: SizedArray.foldlMIdx_empty
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ foldlMIdx.loop f empty 0 (_ : 0 ≤ 0) init = pure init
Tactic:
unfold foldlMIdx.loop
Proof state after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (if h : 0 = 0 then pure (h ▸ init)
    else
      let_fun this := (_ : 0 < 0);
      do
      let __do_lift ← f 0 init empty[0]
      foldlMIdx.loop f empty (0 + 1) this __do_lift) =
    pure init
Theorem: SizedArray.foldlMIdx_empty
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (if h : 0 = 0 then pure (h ▸ init)
    else
      let_fun this := (_ : 0 < 0);
      do
      let __do_lift ← f 0 init empty[0]
      foldlMIdx.loop f empty (0 + 1) this __do_lift) =
    pure init
Tactic:
exact dif_pos rfl
Proof state after:
no goals
Theorem: SizedArray.foldlMIdx.loop_cons_succ
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
⊢ loop f (cons a x) (i + 1) h₁ b = loop (fun i b => f (i + 1) b) x i h₂ b
Tactic:
unfold loop
Proof state after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift
Theorem: SizedArray.foldlMIdx.loop_cons_succ
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift
Tactic:
if h : i = n then
  cases h; rw [dif_pos rfl, dif_pos rfl]
else
  have : i < n := Nat.lt_of_le_of_ne h₂ h
  simp only [dif_neg (Nat.ne_of_lt this), dif_neg (Nat.ne_of_lt (Nat.succ_lt_succ this))]
  rw [get_cons_succ]
  exact bind_congr λ b => foldlMIdx.loop_cons_succ f a x (i+1) (Nat.succ_lt_succ this) this b
Proof state after:
no goals
Theorem: SizedArray.foldlMIdx.loop_cons_succ
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : i = n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift
Tactic:
cases h
Proof state after:
case refl
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
h₁ : n + 1 ≤ n + 1
h₂ : n ≤ n
b : β (n + 1)
⊢ (if h : n + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : n + 1 < n + 1);
      do
      let __do_lift ← f (n + 1) b (cons a x)[n + 1]
      loop f (cons a x) (n + 1 + 1) this __do_lift) =
    if h : n = n then pure (h ▸ b)
    else
      let_fun this := (_ : n < n);
      do
      let __do_lift ← f (n + 1) b x[n]
      loop (fun i b => f (i + 1) b) x (n + 1) this __do_lift
Theorem: SizedArray.foldlMIdx.loop_cons_succ
Proof state before:
case refl
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
h₁ : n + 1 ≤ n + 1
h₂ : n ≤ n
b : β (n + 1)
⊢ (if h : n + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : n + 1 < n + 1);
      do
      let __do_lift ← f (n + 1) b (cons a x)[n + 1]
      loop f (cons a x) (n + 1 + 1) this __do_lift) =
    if h : n = n then pure (h ▸ b)
    else
      let_fun this := (_ : n < n);
      do
      let __do_lift ← f (n + 1) b x[n]
      loop (fun i b => f (i + 1) b) x (n + 1) this __do_lift
Tactic:
rw [dif_pos rfl, dif_pos rfl]
Proof state after:
no goals
Theorem: SizedArray.foldlMIdx.loop_cons_succ
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift
Tactic:
have : i < n := Nat.lt_of_le_of_ne h₂ h
Proof state after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift
Theorem: SizedArray.foldlMIdx.loop_cons_succ
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift
Tactic:
simp only [dif_neg (Nat.ne_of_lt this), dif_neg (Nat.ne_of_lt (Nat.succ_lt_succ this))]
Proof state after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) __do_lift) =
    do
    let __do_lift ← f (i + 1) b x[i]
    loop (fun i b => f (i + 1) b) x (i + 1) (_ : i < n) __do_lift
Theorem: SizedArray.foldlMIdx.loop_cons_succ
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) __do_lift) =
    do
    let __do_lift ← f (i + 1) b x[i]
    loop (fun i b => f (i + 1) b) x (i + 1) (_ : i < n) __do_lift
Tactic:
rw [get_cons_succ]
Proof state after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (do
      let __do_lift ← f (i + 1) b x[i]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) __do_lift) =
    do
    let __do_lift ← f (i + 1) b x[i]
    loop (fun i b => f (i + 1) b) x (i + 1) (_ : i < n) __do_lift

case hi₂
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ i < n
Theorem: SizedArray.foldlMIdx.loop_cons_succ
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (do
      let __do_lift ← f (i + 1) b x[i]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) __do_lift) =
    do
    let __do_lift ← f (i + 1) b x[i]
    loop (fun i b => f (i + 1) b) x (i + 1) (_ : i < n) __do_lift

case hi₂
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ i < n
Tactic:
exact bind_congr λ b => foldlMIdx.loop_cons_succ f a x (i+1) (Nat.succ_lt_succ this) this b
Proof state after:
no goals
Theorem: SizedArray.foldlMIdx_cons
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ foldlMIdx f init (cons a x) = do
    let b ← f 0 init a
    foldlMIdx (fun i b => f (Nat.succ i) b) b x
Tactic:
unfold foldlMIdx
Proof state after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ foldlMIdx.loop f (cons a x) 0 (_ : 0 ≤ n + 1) init = do
    let b ← f 0 init a
    foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b