internlm/Lean-Github huggingface dataset:
Theorem: Array.get_set_of_eq
Proof state before:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i = j
hj' : j < as.size
⊢ (as.set i x)[j] = x
Tactic:
rw [as.get_set i j hj']
Proof state after:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i = j
hj' : j < as.size
⊢ (if ↑i = j then x else as[j]) = x
Theorem: Array.get_set_of_eq
Proof state before:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i = j
hj' : j < as.size
⊢ (if ↑i = j then x else as[j]) = x
Tactic:
rw [if_pos h]
Proof state after:
no goals
Theorem: Array.get_set_of_ne
Proof state before:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
⊢ ↑i ≠ j → (as.set i x)[j] = as[j]
Tactic:
intro h
Proof state after:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
⊢ (as.set i x)[j] = as[j]
Theorem: Array.get_set_of_ne
Proof state before:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
⊢ (as.set i x)[j] = as[j]
Tactic:
have hj' : j < as.size := as.size_set i x ▸ hj
Proof state after:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
hj' : j < as.size
⊢ (as.set i x)[j] = as[j]
Theorem: Array.get_set_of_ne
Proof state before:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
hj' : j < as.size
⊢ (as.set i x)[j] = as[j]
Tactic:
rw [as.get_set i j hj']
Proof state after:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
hj' : j < as.size
⊢ (if ↑i = j then x else as[j]) = as[j]
Theorem: Array.get_set_of_ne
Proof state before:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
hj' : j < as.size
⊢ (if ↑i = j then x else as[j]) = as[j]
Tactic:
rw [if_neg h]
Proof state after:
no goals
Theorem: Array.get_pop
Proof state before:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop[i] = as[i]
Tactic:
rw [←as.get_eq_getElem ⟨i, get_pop.aux as hi⟩]
Proof state after:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop[i] = as.get ⟨i, ⋯⟩
Theorem: Array.get_pop
Proof state before:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop[i] = as.get ⟨i, ⋯⟩
Tactic:
rw [←as.pop.get_eq_getElem ⟨i, hi⟩]
Proof state after:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop.get ⟨i, hi⟩ = as.get ⟨i, ⋯⟩
Theorem: Array.get_pop
Proof state before:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop.get ⟨i, hi⟩ = as.get ⟨i, ⋯⟩
Tactic:
rw [get, get]
Proof state after:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop.data.get ⟨i, hi⟩ = as.data.get ⟨i, ⋯⟩
Theorem: Array.get_pop
Proof state before:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop.data.get ⟨i, hi⟩ = as.data.get ⟨i, ⋯⟩
Tactic:
unfold pop
Proof state after:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ { data := as.data.dropLast }.data.get ⟨i, hi⟩ = as.data.get ⟨i, ⋯⟩
Theorem: Array.get_pop
Proof state before:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ { data := as.data.dropLast }.data.get ⟨i, hi⟩ = as.data.get ⟨i, ⋯⟩
Tactic:
rw [List.get_dropLast]
Proof state after:
no goals
Theorem: Array.get_swap_fst
Proof state before:
α : Type ?u.1585
as : Array α
i j : Fin as.size
⊢ ↑i < (as.swap i j).size
Tactic:
simp [i.isLt]
Proof state after:
no goals
Theorem: Array.get_swap_fst
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (as.swap i j)[↑i] = as[↑j]
Tactic:
simp only [swap]
Proof state after:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ((as.set i (as.get j)).set (⋯ ▸ j) (as.get i))[↑i] = as[↑j]
Theorem: Array.get_swap_fst
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ((as.set i (as.get j)).set (⋯ ▸ j) (as.get i))[↑i] = as[↑j]
Tactic:
rw [get_set]
Proof state after:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (if ↑(⋯ ▸ j) = ↑i then as.get i else (as.set i (as.get j))[↑i]) = as[↑j]

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size
Theorem: Array.get_swap_fst
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (if ↑(⋯ ▸ j) = ↑i then as.get i else (as.set i (as.get j))[↑i]) = as[↑j]

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ↑(⋯ ▸ j) = ↑i
⊢ as.get i = as[↑j]

case isFalse
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ¬↑(⋯ ▸ j) = ↑i
⊢ (as.set i (as.get j))[↑i] = as[↑j]

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size
Theorem: Array.get_swap_fst
Proof state before:
case isTrue
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ↑(⋯ ▸ j) = ↑i
⊢ as.get i = as[↑j]

case isFalse
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ¬↑(⋯ ▸ j) = ↑i
⊢ (as.set i (as.get j))[↑i] = as[↑j]

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size
Tactic:
next heq =>
  have : j.val = i.val := by
    rw [←heq]
    apply Fin.val_eq_val_of_heq
    rw [size_set]
    elim_casts
    reflexivity
  simp [get_eq_getElem, this]
Proof state after:
case isFalse
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ¬↑(⋯ ▸ j) = ↑i
⊢ (as.set i (as.get j))[↑i] = as[↑j]

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size
Theorem: Array.get_swap_fst
Proof state before:
case isFalse
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ¬↑(⋯ ▸ j) = ↑i
⊢ (as.set i (as.get j))[↑i] = as[↑j]

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size
Tactic:
next =>
  rw [get_set_eq, get_eq_getElem]
Proof state after:
no goals
Theorem: Array.get_swap_fst
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ as.get i = as[↑j]
Tactic:
have : j.val = i.val := by
  rw [←heq]
  apply Fin.val_eq_val_of_heq
  rw [size_set]
  elim_casts
  reflexivity
Proof state after:
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
this : ↑j = ↑i
⊢ as.get i = as[↑j]
Theorem: Array.get_swap_fst
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
this : ↑j = ↑i
⊢ as.get i = as[↑j]
Tactic:
simp [get_eq_getElem, this]
Proof state after:
no goals
Theorem: Array.get_swap_fst
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ ↑j = ↑i
Tactic:
rw [←heq]
Proof state after:
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ ↑j = ↑(⋯ ▸ j)
Theorem: Array.get_swap_fst
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ ↑j = ↑(⋯ ▸ j)
Tactic:
apply Fin.val_eq_val_of_heq
Proof state after:
case a
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ as.size = (as.set i (as.get j)).size

case a
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ j ≅ ⋯ ▸ j
Theorem: Array.get_swap_fst
Proof state before:
case a
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ as.size = (as.set i (as.get j)).size

case a
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ j ≅ ⋯ ▸ j
Tactic:
rw [size_set]
Proof state after:
case a
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ j ≅ ⋯ ▸ j
Theorem: Array.get_swap_fst
Proof state before:
case a
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ j ≅ ⋯ ▸ j
Tactic:
elim_casts
Proof state after:
case a
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ j ≅ j
Theorem: Array.get_swap_fst
Proof state before:
case a
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ j ≅ j
Tactic:
reflexivity
Proof state after:
no goals
Theorem: Array.get_swap_fst
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ¬↑(⋯ ▸ j) = ↑i
⊢ (as.set i (as.get j))[↑i] = as[↑j]
Tactic:
rw [get_set_eq, get_eq_getElem]
Proof state after:
no goals
Theorem: Array.get_swap_snd
Proof state before:
α : Type ?u.4204
as : Array α
i j : Fin as.size
⊢ ↑j < (as.swap i j).size
Tactic:
simp [j.isLt]
Proof state after:
no goals
Theorem: Array.get_swap_snd
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (as.swap i j)[↑j] = as[↑i]
Tactic:
simp only [swap]
Proof state after:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ((as.set i (as.get j)).set (⋯ ▸ j) (as.get i))[↑j] = as[↑i]
Theorem: Array.get_swap_snd
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ((as.set i (as.get j)).set (⋯ ▸ j) (as.get i))[↑j] = as[↑i]
Tactic:
rw [get_set_of_eq]
Proof state after:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ as.get i = as[↑i]

case a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑(⋯ ▸ j) = ↑j
Theorem: Array.get_swap_snd
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ as.get i = as[↑i]

case a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑(⋯ ▸ j) = ↑j
Tactic:
rw [get_eq_getElem]
Proof state after:
case a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑(⋯ ▸ j) = ↑j
Theorem: Array.get_swap_snd
Proof state before:
case a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑(⋯ ▸ j) = ↑j
Tactic:
apply Fin.val_eq_val_of_heq
Proof state after:
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (as.set i (as.get j)).size = as.size

case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ⋯ ▸ j ≅ j
Theorem: Array.get_swap_snd
Proof state before:
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (as.set i (as.get j)).size = as.size

case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ⋯ ▸ j ≅ j
Tactic:
rw [size_set]
Proof state after:
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ⋯ ▸ j ≅ j
Theorem: Array.get_swap_snd
Proof state before:
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ⋯ ▸ j ≅ j
Tactic:
elim_casts
Proof state after:
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ j ≅ j
Theorem: Array.get_swap_snd
Proof state before:
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ j ≅ j
Tactic:
reflexivity
Proof state after:
no goals
Theorem: Array.get_swap_other
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
⊢ ↑i ≠ k → ↑j ≠ k → (as.swap i j)[k] = as[k]
Tactic:
intro hik hjk
Proof state after:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk : ↑j ≠ k
⊢ (as.swap i j)[k] = as[k]
Theorem: Array.get_swap_other
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk : ↑j ≠ k
⊢ (as.swap i j)[k] = as[k]
Tactic:
have hjk : ((size_set as i (get as j)).symm ▸ j).val ≠ k := by
  intro h
  cases h
  apply hjk
  apply Fin.val_eq_val_of_heq
  rw [size_set]
  elim_casts
  reflexivity
Proof state after:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ (as.swap i j)[k] = as[k]
Theorem: Array.get_swap_other
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ (as.swap i j)[k] = as[k]
Tactic:
simp only [swap]
Proof state after:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ ((as.set i (as.get j)).set (⋯ ▸ j) (as.get i))[k] = as[k]
Theorem: Array.get_swap_other
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ ((as.set i (as.get j)).set (⋯ ▸ j) (as.get i))[k] = as[k]
Tactic:
rw [get_set_of_ne]
Proof state after:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ (as.set i (as.get j))[k] = as[k]

case a
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ ↑(⋯ ▸ j) ≠ k
Theorem: Array.get_swap_other
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ (as.set i (as.get j))[k] = as[k]

case a
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ ↑(⋯ ▸ j) ≠ k
Tactic:
rw [get_set_of_ne as hik]
Proof state after:
case a
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ ↑(⋯ ▸ j) ≠ k
Theorem: Array.get_swap_other
Proof state before:
case a
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ ↑(⋯ ▸ j) ≠ k
Tactic:
exact hjk
Proof state after:
no goals
Theorem: Array.get_swap_other
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk : ↑j ≠ k
⊢ ↑(⋯ ▸ j) ≠ k
Tactic:
intro h
Proof state after:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk : ↑j ≠ k
h : ↑(⋯ ▸ j) = k
⊢ False
Theorem: Array.get_swap_other
Proof state before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk : ↑j ≠ k
h : ↑(⋯ ▸ j) = k
⊢ False
Tactic:
cases h
Proof state after:
case refl
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ False
Theorem: Array.get_swap_other
Proof state before:
case refl
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ False
Tactic:
apply hjk
Proof state after:
case refl
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ ↑j = ↑(⋯ ▸ j)
Theorem: Array.get_swap_other
Proof state before:
case refl
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ ↑j = ↑(⋯ ▸ j)
Tactic:
apply Fin.val_eq_val_of_heq
Proof state after:
case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ as.size = (as.set i (as.get j)).size

case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ j ≅ ⋯ ▸ j
Theorem: Array.get_swap_other
Proof state before:
case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ as.size = (as.set i (as.get j)).size

case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ j ≅ ⋯ ▸ j
Tactic:
rw [size_set]
Proof state after:
case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ j ≅ ⋯ ▸ j
Theorem: Array.get_swap_other
Proof state before:
case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ j ≅ ⋯ ▸ j
Tactic:
elim_casts
Proof state after:
case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ j ≅ j
Theorem: Array.get_swap_other
Proof state before:
case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ j ≅ j
Tactic:
reflexivity
Proof state after:
no goals
Theorem: Array.size_del
Proof state before:
α : Type u_1
as : Array α
k : Fin as.size
⊢ (as.del k).size = as.size - 1
Tactic:
simp [del]
Proof state after:
no goals
Theorem: Array.get_del
Proof state before:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
⊢ (as.del k)[i] = if i = ↑k then as[as.size - 1] else as[i]
Tactic:
have hi' : i ≠ as.size - 1 := Nat.ne_of_lt <| size_del as k ▸ hi
Proof state after:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.del k)[i] = if i = ↑k then as[as.size - 1] else as[i]
Theorem: Array.get_del
Proof state before:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.del k)[i] = if i = ↑k then as[as.size - 1] else as[i]
Tactic:
simp only [del]
Proof state after:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.swap k ⟨as.size - 1, ⋯⟩).pop[i] = if i = ↑k then as[as.size - 1] else as[i]
Theorem: Array.get_del
Proof state before:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.swap k ⟨as.size - 1, ⋯⟩).pop[i] = if i = ↑k then as[as.size - 1] else as[i]
Tactic:
rw [get_pop]
Proof state after:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.swap k ⟨as.size - 1, ⋯⟩)[i] = if i = ↑k then as[as.size - 1] else as[i]
Theorem: Array.get_del
Proof state before:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.swap k ⟨as.size - 1, ⋯⟩)[i] = if i = ↑k then as[as.size - 1] else as[i]
Tactic:
rw [get_swap]
Proof state after:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (if i = ↑k then as[⟨as.size - 1, ⋯⟩] else if i = ↑⟨as.size - 1, ⋯⟩ then as[k] else as[i]) =
    if i = ↑k then as[as.size - 1] else as[i]

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size
Theorem: Array.get_del
Proof state before:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (if i = ↑k then as[⟨as.size - 1, ⋯⟩] else if i = ↑⟨as.size - 1, ⋯⟩ then as[k] else as[i]) =
    if i = ↑k then as[as.size - 1] else as[i]

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size
Tactic:
rw [if_neg hi']
Proof state after:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (if i = ↑k then as[⟨as.size - 1, ⋯⟩] else as[i]) = if i = ↑k then as[as.size - 1] else as[i]

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size
Theorem: Array.get_del
Proof state before:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (if i = ↑k then as[⟨as.size - 1, ⋯⟩] else as[i]) = if i = ↑k then as[as.size - 1] else as[i]

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.foldlM_stop
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldlM f b as stop stop = pure b
Tactic:
simp only [Array.foldlM]
Proof state after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - stop) stop b
    else foldlM.loop f as as.size ⋯ (as.size - stop) stop b) =
    pure b
Theorem: Array.foldlM_stop
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - stop) stop b
    else foldlM.loop f as as.size ⋯ (as.size - stop) stop b) =
    pure b
Tactic:
rw [dif_pos hstop]
Proof state after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldlM.loop f as stop ⋯ (stop - stop) stop b = pure b
Theorem: Array.foldlM_stop
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldlM.loop f as stop ⋯ (stop - stop) stop b = pure b
Tactic:
rw [Array.foldlM.loop]
Proof state after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if hlt : stop < stop then
      match stop - stop with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b as[stop]
        foldlM.loop f as stop ⋯ i' (stop + 1) __do_lift
    else pure b) =
    pure b
Theorem: Array.foldlM_stop
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if hlt : stop < stop then
      match stop - stop with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b as[stop]
        foldlM.loop f as stop ⋯ i' (stop + 1) __do_lift
    else pure b) =
    pure b
Tactic:
rw [dif_neg (by irreflexivity)]
Proof state after:
no goals
Theorem: Array.foldlM_stop
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ ¬stop < stop
Tactic:
irreflexivity
Proof state after:
no goals
Theorem: Array.foldlM_step
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ let_fun this := ⋯;
  foldlM f b as start stop = do
    let b ← f b as[start]
    foldlM f b as (start + 1) stop
Tactic:
simp only [Array.foldlM]
Proof state after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - start) start b
    else foldlM.loop f as as.size ⋯ (as.size - start) start b) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Theorem: Array.foldlM_step
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - start) start b
    else foldlM.loop f as as.size ⋯ (as.size - start) start b) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
rw [dif_pos hstop]
Proof state after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ foldlM.loop f as stop ⋯ (stop - start) start b = do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b