internlm/Lean-Github huggingface dataset:
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k n : Nat
⊢ k < log2' (succ n) + 1 ↔ 2 ^ k < succ (succ n)
Tactic:
have : ∀ (a b : Nat), (a < b+1) = (a ≤ b) :=
  λ a b => propext ⟨Nat.le_of_lt_succ, Nat.lt_succ_of_le⟩
Proof state after:
k n : Nat
this : ∀ (a b : Nat), (a < b + 1) = (a ≤ b)
⊢ k < log2' (succ n) + 1 ↔ 2 ^ k < succ (succ n)
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k n : Nat
this : ∀ (a b : Nat), (a < b + 1) = (a ≤ b)
⊢ k < log2' (succ n) + 1 ↔ 2 ^ k < succ (succ n)
Tactic:
rw [this, this]
Proof state after:
k n : Nat
this : ∀ (a b : Nat), (a < b + 1) = (a ≤ b)
⊢ k ≤ log2' (succ n) ↔ 2 ^ k ≤ n + 1
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k n : Nat
this : ∀ (a b : Nat), (a < b + 1) = (a ≤ b)
⊢ k ≤ log2' (succ n) ↔ 2 ^ k ≤ n + 1
Tactic:
exact le_log2'_iff_pow2_le n.zero_lt_succ
Proof state after:
no goals
Theorem: Nat.le_pow2_log2RU_self
Proof state before:
n : Nat
⊢ n ≤ 2 ^ log2RU n
Tactic:
cases Nat.lt_or_ge (2^log2RU n) n
Proof state after:
case inl
n : Nat
h✝ : 2 ^ log2RU n < n
⊢ n ≤ 2 ^ log2RU n

case inr
n : Nat
h✝ : 2 ^ log2RU n ≥ n
⊢ n ≤ 2 ^ log2RU n
Theorem: Nat.le_pow2_log2RU_self
Proof state before:
n : Nat
hge : 2 ^ log2RU n ≥ n
⊢ n ≤ 2 ^ log2RU n
Tactic:
case inr hge => exact hge
Proof state after:
no goals
Theorem: Nat.le_pow2_log2RU_self
Proof state before:
n : Nat
hlt : 2 ^ log2RU n < n
⊢ n ≤ 2 ^ log2RU n
Tactic:
case inl hlt =>
  have : n.log2RU < n.log2RU := Nat.lt_log2RU_iff_pow2_lt.mpr hlt
  exact absurd this (Nat.lt_irrefl _)
Proof state after:
no goals
Theorem: Nat.le_pow2_log2RU_self
Proof state before:
n : Nat
hge : 2 ^ log2RU n ≥ n
⊢ n ≤ 2 ^ log2RU n
Tactic:
exact hge
Proof state after:
no goals
Theorem: Nat.le_pow2_log2RU_self
Proof state before:
n : Nat
hlt : 2 ^ log2RU n < n
⊢ n ≤ 2 ^ log2RU n
Tactic:
have : n.log2RU < n.log2RU := Nat.lt_log2RU_iff_pow2_lt.mpr hlt
Proof state after:
n : Nat
hlt : 2 ^ log2RU n < n
this : log2RU n < log2RU n
⊢ n ≤ 2 ^ log2RU n
Theorem: Nat.le_pow2_log2RU_self
Proof state before:
n : Nat
hlt : 2 ^ log2RU n < n
this : log2RU n < log2RU n
⊢ n ≤ 2 ^ log2RU n
Tactic:
exact absurd this (Nat.lt_irrefl _)
Proof state after:
no goals
Theorem: List.id_map
Proof state before:
α β : Type u
γ : Type w
as : List α
⊢ map id as = as
Tactic:
induction as with
| nil => rfl
| cons a as hi =>
  rw [map, hi]
  rfl
Proof state after:
no goals
Theorem: List.id_map
Proof state before:
case nil
α β : Type u
γ : Type w
⊢ map id [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: List.id_map
Proof state before:
case cons
α β : Type u
γ : Type w
a : α
as : List α
hi : map id as = as
⊢ map id (a :: as) = a :: as
Tactic:
rw [map, hi]
Proof state after:
case cons
α β : Type u
γ : Type w
a : α
as : List α
hi : map id as = as
⊢ id a :: as = a :: as
Theorem: List.id_map
Proof state before:
case cons
α β : Type u
γ : Type w
a : α
as : List α
hi : map id as = as
⊢ id a :: as = a :: as
Tactic:
rfl
Proof state after:
no goals
Theorem: List.bind_singleton_comp
Proof state before:
α β : Type u
γ : Type w
f : α → β
a : α
as : List α
⊢ (List.bind (a :: as) fun a => [f a]) = map f (a :: as)
Tactic:
rw [cons_bind, map]
Proof state after:
α β : Type u
γ : Type w
f : α → β
a : α
as : List α
⊢ ([f a] ++ List.bind as fun a => [f a]) = f a :: map f as
Theorem: List.bind_singleton_comp
Proof state before:
α β : Type u
γ : Type w
f : α → β
a : α
as : List α
⊢ ([f a] ++ List.bind as fun a => [f a]) = f a :: map f as
Tactic:
rw [cons_append, nil_append]
Proof state after:
α β : Type u
γ : Type w
f : α → β
a : α
as : List α
⊢ (f a :: List.bind as fun a => [f a]) = f a :: map f as
Theorem: List.bind_singleton_comp
Proof state before:
α β : Type u
γ : Type w
f : α → β
a : α
as : List α
⊢ (f a :: List.bind as fun a => [f a]) = f a :: map f as
Tactic:
rw [bind_singleton_comp f as]
Proof state after:
no goals
Theorem: List.singleton_bind
Proof state before:
α β : Type u
γ : Type w
a : α
f : α → List β
⊢ List.bind [a] f = f a
Tactic:
rw [List.bind, map, map, join, join]
Proof state after:
α β : Type u
γ : Type w
a : α
f : α → List β
⊢ f a ++ [] = f a
Theorem: List.singleton_bind
Proof state before:
α β : Type u
γ : Type w
a : α
f : α → List β
⊢ f a ++ [] = f a
Tactic:
simp
Proof state after:
no goals
Theorem: List.bind_assoc
Proof state before:
α β : Type u
γ : Type w
as : List α
f : α → List β
g : β → List γ
⊢ List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
Tactic:
induction as with
| nil => rfl
| cons a as hi =>
  rw [cons_bind, cons_bind]
  rw [append_bind]
  rw [hi]
Proof state after:
no goals
Theorem: List.bind_assoc
Proof state before:
case nil
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
⊢ List.bind (List.bind [] f) g = List.bind [] fun x => List.bind (f x) g
Tactic:
rfl
Proof state after:
no goals
Theorem: List.bind_assoc
Proof state before:
case cons
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
a : α
as : List α
hi : List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
⊢ List.bind (List.bind (a :: as) f) g = List.bind (a :: as) fun x => List.bind (f x) g
Tactic:
rw [cons_bind, cons_bind]
Proof state after:
case cons
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
a : α
as : List α
hi : List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
⊢ List.bind (f a ++ List.bind as f) g = List.bind (f a) g ++ List.bind as fun x => List.bind (f x) g
Theorem: List.bind_assoc
Proof state before:
case cons
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
a : α
as : List α
hi : List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
⊢ List.bind (f a ++ List.bind as f) g = List.bind (f a) g ++ List.bind as fun x => List.bind (f x) g
Tactic:
rw [append_bind]
Proof state after:
case cons
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
a : α
as : List α
hi : List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
⊢ List.bind (f a) g ++ List.bind (List.bind as f) g = List.bind (f a) g ++ List.bind as fun x => List.bind (f x) g
Theorem: List.bind_assoc
Proof state before:
case cons
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
a : α
as : List α
hi : List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
⊢ List.bind (f a) g ++ List.bind (List.bind as f) g = List.bind (f a) g ++ List.bind as fun x => List.bind (f x) g
Tactic:
rw [hi]
Proof state after:
no goals
Theorem: Array.get_push'
Proof state before:
α : Type u
a : α
as : Array α
i : Nat
h : i < size (push as a)
⊢ (push as a)[i] = if h : i < size as then as[i] else a
Tactic:
cases as with | mk l =>
simp only [getElem_eq_data_get]
dsimp [push, size] at h ⊢
rw [List.get_of_eq (l.concat_eq_append a)]
if hil : i < l.length
then rw [dif_pos hil]; apply List.get_append_left
else
  rw [dif_neg hil]
  have : i = l.length := by
    refine Nat.le_antisymm ?_ (Nat.ge_of_not_lt hil)
    rw [l.length_concat a] at h
    exact Nat.le_of_succ_le_succ h
  simp only [this]
  exact l.get_concat_length a _
Proof state after:
no goals
Theorem: Array.get_push'
Proof state before:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < size (push { data := l } a)
⊢ (push { data := l } a)[i] = if h : i < size { data := l } then { data := l }[i] else a
Tactic:
simp only [getElem_eq_data_get]
Proof state after:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < size (push { data := l } a)
⊢ List.get (push { data := l } a).data { val := i, isLt := h } =
    if h : i < size { data := l } then List.get l { val := i, isLt := (_ : i < size { data := l }) } else a
Theorem: Array.get_push'
Proof state before:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < size (push { data := l } a)
⊢ List.get (push { data := l } a).data { val := i, isLt := h } =
    if h : i < size { data := l } then List.get l { val := i, isLt := (_ : i < size { data := l }) } else a
Tactic:
dsimp [push, size] at h ⊢
Proof state after:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
⊢ List.get (List.concat l a) { val := i, isLt := h } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a
Theorem: Array.get_push'
Proof state before:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
⊢ List.get (List.concat l a) { val := i, isLt := h } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a
Tactic:
rw [List.get_of_eq (l.concat_eq_append a)]
Proof state after:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a
Theorem: Array.get_push'
Proof state before:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a
Tactic:
if hil : i < l.length
then rw [dif_pos hil]; apply List.get_append_left
else
  rw [dif_neg hil]
  have : i = l.length := by
    refine Nat.le_antisymm ?_ (Nat.ge_of_not_lt hil)
    rw [l.length_concat a] at h
    exact Nat.le_of_succ_le_succ h
  simp only [this]
  exact l.get_concat_length a _
Proof state after:
no goals
Theorem: Array.get_push'
Proof state before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : i < List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a
Tactic:
rw [dif_pos hil]
Proof state after:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : i < List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    List.get l { val := i, isLt := (_ : i < List.length l) }
Theorem: Array.get_push'
Proof state before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : i < List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    List.get l { val := i, isLt := (_ : i < List.length l) }
Tactic:
apply List.get_append_left
Proof state after:
no goals
Theorem: Array.get_push'
Proof state before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a
Tactic:
rw [dif_neg hil]
Proof state after:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    a
Theorem: Array.get_push'
Proof state before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    a
Tactic:
have : i = l.length := by
  refine Nat.le_antisymm ?_ (Nat.ge_of_not_lt hil)
  rw [l.length_concat a] at h
  exact Nat.le_of_succ_le_succ h
Proof state after:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
this : i = List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    a
Theorem: Array.get_push'
Proof state before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
this : i = List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    a
Tactic:
simp only [this]
Proof state after:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
this : i = List.length l
⊢ List.get (l ++ [a]) { val := List.length l, isLt := (_ : List.length l < List.length (l ++ [a])) } = a
Theorem: Array.get_push'
Proof state before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
this : i = List.length l
⊢ List.get (l ++ [a]) { val := List.length l, isLt := (_ : List.length l < List.length (l ++ [a])) } = a
Tactic:
exact l.get_concat_length a _
Proof state after:
no goals
Theorem: Array.get_push'
Proof state before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ i = List.length l
Tactic:
refine Nat.le_antisymm ?_ (Nat.ge_of_not_lt hil)
Proof state after:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ i ≤ List.length l
Theorem: Array.get_push'
Proof state before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ i ≤ List.length l
Tactic:
rw [l.length_concat a] at h
Proof state after:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length l + 1
hil : ¬i < List.length l
⊢ i ≤ List.length l
Theorem: Array.get_push'
Proof state before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length l + 1
hil : ¬i < List.length l
⊢ i ≤ List.length l
Tactic:
exact Nat.le_of_succ_le_succ h
Proof state after:
no goals
Theorem: Array.get_push_eq_safe
Proof state before:
α : Type u
as : Array α
a : α
⊢ (push as a)[size as] = a
Tactic:
simp only [get_push', size_push, dif_neg (Nat.lt_irrefl as.size)]
Proof state after:
no goals
Theorem: Array.get_pop
Proof state before:
α : Type u
as : Array α
i : Nat
hi₁ : i < size (pop as)
hi₂ : i < size as
⊢ (pop as)[i] = as[i]
Tactic:
simp only [pop, getElem_eq_data_get, List.dropLast_eq_take]
Proof state after:
α : Type u
as : Array α
i : Nat
hi₁ : i < size (pop as)
hi₂ : i < size as
⊢ List.get (List.take (List.length as.data - 1) as.data)
      { val := i, isLt := (_ : (fun xs i => i < size xs) { data := List.take (List.length as.data - 1) as.data } i) } =
    List.get as.data { val := i, isLt := hi₂ }
Theorem: Array.get_pop
Proof state before:
α : Type u
as : Array α
i : Nat
hi₁ : i < size (pop as)
hi₂ : i < size as
⊢ List.get (List.take (List.length as.data - 1) as.data)
      { val := i, isLt := (_ : (fun xs i => i < size xs) { data := List.take (List.length as.data - 1) as.data } i) } =
    List.get as.data { val := i, isLt := hi₂ }
Tactic:
exact as.data.get_take _ i
Proof state after:
no goals
Theorem: Array.push_pop_back'
Proof state before:
α : Type u
as : Array α
h✝ : size as > 0
l : List α
h : size { data := l } > 0
⊢ push (pop { data := l }) (back' { data := l } h) = { data := l }
Tactic:
simp only [back'_eq_data_getLast, pop, push, size, getElem_eq_data_get, List.concat_eq_append]
Proof state after:
α : Type u
as : Array α
h✝ : size as > 0
l : List α
h : size { data := l } > 0
⊢ { data := List.dropLast l ++ [List.getLast l (_ : { data := l }.data ≠ [])] } = { data := l }
Theorem: Array.push_pop_back'
Proof state before:
α : Type u
as : Array α
h✝ : size as > 0
l : List α
h : size { data := l } > 0
⊢ { data := List.dropLast l ++ [List.getLast l (_ : { data := l }.data ≠ [])] } = { data := l }
Tactic:
apply congrArg Array.mk
Proof state after:
α : Type u
as : Array α
h✝ : size as > 0
l : List α
h : size { data := l } > 0
⊢ List.dropLast l ++ [List.getLast l (_ : { data := l }.data ≠ [])] = l
Theorem: Array.push_pop_back'
Proof state before:
α : Type u
as : Array α
h✝ : size as > 0
l : List α
h : size { data := l } > 0
⊢ List.dropLast l ++ [List.getLast l (_ : { data := l }.data ≠ [])] = l
Tactic:
apply l.dropLast_concat_getLast
Proof state after:
no goals
Theorem: Array.push_induction
Proof state before:
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ motive as
Tactic:
rw [← as.push_pop_back' (hn ▸ n.zero_lt_succ)]
Proof state after:
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ motive (Array.push (pop as) (back' as (_ : size as > 0)))
Theorem: Array.push_induction
Proof state before:
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ motive (Array.push (pop as) (back' as (_ : size as > 0)))
Tactic:
apply push
Proof state after:
case a
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ motive (pop as)
Theorem: Array.push_induction
Proof state before:
case a
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ motive (pop as)
Tactic:
apply IH
Proof state after:
case a.a
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ size (pop as) = n
Theorem: Array.getElem_swap
Proof state before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
⊢ (swap x i j)[k] = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
dsimp [swap] at hk ⊢
Proof state after:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
⊢ (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])[k] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Theorem: Array.getElem_swap
Proof state before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
⊢ (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])[k] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
conv at hk => rewrite [Array.size_set]
Proof state after:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])[k] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Theorem: Array.getElem_swap
Proof state before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])[k] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
rewrite [(x.set i x[j.1]).get_set _ k hk]
Proof state after:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (if ↑((_ : size x = size (set x i (get x j))) ▸ j) = k then x[↑i] else (set x i x[↑j])[k]) =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Theorem: Array.getElem_swap
Proof state before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (if ↑((_ : size x = size (set x i (get x j))) ▸ j) = k then x[↑i] else (set x i x[↑j])[k]) =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
simp only [← Fin.cast_eq_subst _ j, Fin.coe_cast]
Proof state after:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (if ↑j = k then x[↑i] else (set x i x[↑j])[k]) = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Theorem: Array.getElem_swap
Proof state before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (if ↑j = k then x[↑i] else (set x i x[↑j])[k]) = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
conv at hk => rewrite [Array.size_set]
Proof state after:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝¹ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk✝ : k < size (set x i x[↑j])
hk : k < size x
⊢ (if ↑j = k then x[↑i] else (set x i x[↑j])[k]) = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Theorem: Array.getElem_swap
Proof state before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝¹ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk✝ : k < size (set x i x[↑j])
hk : k < size x
⊢ (if ↑j = k then x[↑i] else (set x i x[↑j])[k]) = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
rw [x.get_set i k hk]
Proof state after:
no goals
Theorem: Array.getElem_swap_ne
Proof state before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hik : ↑i ≠ k
hjk : ↑j ≠ k
⊢ (swap x i j)[k] = x[k]
Tactic:
rw [getElem_swap, if_neg hjk, if_neg hik]
Proof state after:
no goals
Theorem: Array.swap_comm
Proof state before:
α : Type u
x : Array α
i j : Fin (size x)
⊢ swap x i j = swap x j i
Tactic:
refine Array.ext _ _ (by simp only [size_swap]) ?_
Proof state after:
α : Type u
x : Array α
i j : Fin (size x)
⊢ ∀ (i_1 : Nat) (hi₁ : i_1 < size (swap x i j)) (hi₂ : i_1 < size (swap x j i)), (swap x i j)[i_1] = (swap x j i)[i_1]
Theorem: Array.swap_comm
Proof state before:
α : Type u
x : Array α
i j : Fin (size x)
⊢ ∀ (i_1 : Nat) (hi₁ : i_1 < size (swap x i j)) (hi₂ : i_1 < size (swap x j i)), (swap x i j)[i_1] = (swap x j i)[i_1]
Tactic:
intro k hk hk'
Proof state after:
α : 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)
⊢ (swap x i j)[k] = (swap x j i)[k]
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)
⊢ (swap x i j)[k] = (swap x j i)[k]
Tactic:
simp only [getElem_swap]
Proof state after:
α : 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]