internlm/Lean-Github huggingface dataset:
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.t.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : ¬i.val = j.val
⊢ as[i.val] = as[j.val]

case h.e.e.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[j.val] = as[i.val]
Tactic:
. exfalso; exact hik <| Eq.symm <| h.get_inj _ _ _ _ has
Proof state after:
case h.e.e.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[j.val] = as[i.val]
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[j.val] = as[i.val]
Tactic:
. exfalso; exact hjk <| Eq.symm <| h.get_inj _ _ _ _ has
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.e.t.e.t
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : i.val = l
hjl : ¬j.val = l
hik : i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
try (cases hik.symm.trans hil; rfl)
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.e.t.e.t
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : i.val = l
hjl : ¬j.val = l
hik : i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
(cases hik.symm.trans hil; rfl)
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.e.t.e.t
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : i.val = l
hjl : ¬j.val = l
hik : i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
cases hik.symm.trans hil
Proof state after:
case h.e.t.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hik : i.val = k
hjk : ¬j.val = k
hl✝ : k < size (swap as i j)
hl : k < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]
hil : i.val = k
hjl : ¬j.val = k
⊢ as[k] = as[k]
Theorem: Array.nodup_swap
Proof state before:
case h.e.t.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hik : i.val = k
hjk : ¬j.val = k
hl✝ : k < size (swap as i j)
hl : k < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]
hil : i.val = k
hjl : ¬j.val = k
⊢ as[k] = as[k]
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.t.e.t.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : ¬i.val = l
hjl : j.val = l
hik : ¬i.val = k
hjk : j.val = k
⊢ as[k] = as[l]
Tactic:
try (cases hjk.symm.trans hjl; rfl)
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.t.e.t.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : ¬i.val = l
hjl : j.val = l
hik : ¬i.val = k
hjk : j.val = k
⊢ as[k] = as[l]
Tactic:
(cases hjk.symm.trans hjl; rfl)
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.t.e.t.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : ¬i.val = l
hjl : j.val = l
hik : ¬i.val = k
hjk : j.val = k
⊢ as[k] = as[l]
Tactic:
cases hjk.symm.trans hjl
Proof state after:
case h.t.e.t.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hik : ¬i.val = k
hjk : j.val = k
hl✝ : k < size (swap as i j)
hl : k < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]
hil : ¬i.val = k
hjl : j.val = k
⊢ as[k] = as[k]
Theorem: Array.nodup_swap
Proof state before:
case h.t.e.t.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hik : ¬i.val = k
hjk : j.val = k
hl✝ : k < size (swap as i j)
hl : k < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]
hil : ¬i.val = k
hjl : j.val = k
⊢ as[k] = as[k]
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.t.e.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : j.val = k
⊢ as[k] = as[l]
Tactic:
iterate rewrite [if_pos ‹_›] at has
Proof state after:
case h.t.e.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[i.val] = if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : j.val = k
⊢ as[k] = as[l]
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
rewrite [if_pos ‹_›] at has
Proof state after:
case h.e.e.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[i.val] = if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]

α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ j.val = k
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
iterate rewrite [if_neg ‹_›] at has
Proof state after:
case h.e.e.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[k] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[k] = if i.val = l then as[j.val] else as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
rewrite [if_neg ‹_›] at has
Proof state after:
case h.e.e.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[k] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.e.t
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[k] = if i.val = l then as[j.val] else as[l]
hil : i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
iterate rewrite [if_pos ‹_›] at has
Proof state after:
case h.e.e.e.t
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[k] = as[j.val]
hil : i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.e.t
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[k] = if i.val = l then as[j.val] else as[l]
hil : i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
rewrite [if_pos ‹_›] at has
Proof state after:
case h.e.e.e.t
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[k] = as[j.val]
hil : i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Theorem: Array.nodup_swap
Proof state before:
case h.e.t.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
iterate rewrite [if_neg ‹_›] at has
Proof state after:
case h.e.t.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Theorem: Array.nodup_swap
Proof state before:
case h.e.t.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = if i.val = l then as[j.val] else as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
rewrite [if_neg ‹_›] at has
Proof state after:
case h.e.t.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Theorem: Array.nodup_swap
Proof state before:
case h.e.t.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
try cases ‹_ = k›
Proof state after:
case h.e.t.e.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : i.val < size (swap as i j)
hk : i.val < size as
hjk : ¬j.val = i.val
⊢ as[i.val] = as[l]
Theorem: Array.nodup_swap
Proof state before:
case h.e.t.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
cases ‹_ = k›
Proof state after:
case h.e.t.e.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : i.val < size (swap as i j)
hk : i.val < size as
hjk : ¬j.val = i.val
⊢ as[i.val] = as[l]
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.e.t
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[k] = as[j.val]
hil : i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
try cases ‹_ = l›
Proof state after:
case h.e.e.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[k] = as[i.val]
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.e.t
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[k] = as[j.val]
hil : i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
cases ‹_ = l›
Proof state after:
case h.e.e.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[k] = as[i.val]
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[k] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
try simp [has]
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.e.e
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[k] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hik : ¬i.val = k
hjk : ¬j.val = k
⊢ as[k] = as[l]
Tactic:
simp [has]
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.t.t.e.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[i.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : j.val < size (swap as i j)
hk : j.val < size as
hik : i.val = j.val
⊢ as[j.val] = as[l]
Tactic:
simp only [← hik, has]
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.t.e.e.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[i.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : j.val < size (swap as i j)
hk : j.val < size as
hik : ¬i.val = j.val
⊢ as[j.val] = as[l]
Tactic:
exfalso
Proof state after:
case h.t.e.e.e.refl.h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[i.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : j.val < size (swap as i j)
hk : j.val < size as
hik : ¬i.val = j.val
⊢ False
Theorem: Array.nodup_swap
Proof state before:
case h.t.e.e.e.refl.h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[i.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : j.val < size (swap as i j)
hk : j.val < size as
hik : ¬i.val = j.val
⊢ False
Tactic:
exact hil <| h.get_inj _ _ _ _ has
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.e.t.e.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : i.val < size (swap as i j)
hk : i.val < size as
hjk : ¬j.val = i.val
⊢ as[i.val] = as[l]
Tactic:
exfalso
Proof state after:
case h.e.t.e.e.refl.h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : i.val < size (swap as i j)
hk : i.val < size as
hjk : ¬j.val = i.val
⊢ False
Theorem: Array.nodup_swap
Proof state before:
case h.e.t.e.e.refl.h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : i.val < size (swap as i j)
hk : i.val < size as
hjk : ¬j.val = i.val
⊢ False
Tactic:
exact hjl <| h.get_inj _ _ _ _ has
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.t.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : i.val = j.val
⊢ as[i.val] = as[j.val]
Tactic:
simp only [hil]
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.t.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : ¬i.val = j.val
⊢ as[i.val] = as[j.val]
Tactic:
exfalso
Proof state after:
case h.e.e.t.e.refl.h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : ¬i.val = j.val
⊢ False
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.t.e.refl.h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : ¬i.val = j.val
⊢ False
Tactic:
exact hik <| Eq.symm <| h.get_inj _ _ _ _ has
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[j.val] = as[i.val]
Tactic:
exfalso
Proof state after:
case h.e.e.e.t.refl.h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ False
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.e.t.refl.h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ False
Tactic:
exact hjk <| Eq.symm <| h.get_inj _ _ _ _ has
Proof state after:
no goals
Theorem: Fin.restrict_inj
Proof state before:
m n : Nat
i j : Fin m
hi : ↑i < n
hj : ↑j < n
h : restrict i hi = restrict j hj
⊢ i = j
Tactic:
rcases i with ⟨i,hi'⟩
Proof state after:
case mk
m n : Nat
j : Fin m
hj : ↑j < n
i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
h : restrict { val := i, isLt := hi' } hi = restrict j hj
⊢ { val := i, isLt := hi' } = j
Theorem: Fin.restrict_inj
Proof state before:
case mk
m n : Nat
j : Fin m
hj : ↑j < n
i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
h : restrict { val := i, isLt := hi' } hi = restrict j hj
⊢ { val := i, isLt := hi' } = j
Tactic:
rcases j with ⟨j,hj'⟩
Proof state after:
case mk.mk
m n i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
j : Nat
hj' : j < m
hj : ↑{ val := j, isLt := hj' } < n
h : restrict { val := i, isLt := hi' } hi = restrict { val := j, isLt := hj' } hj
⊢ { val := i, isLt := hi' } = { val := j, isLt := hj' }
Theorem: Fin.restrict_inj
Proof state before:
case mk.mk
m n i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
j : Nat
hj' : j < m
hj : ↑{ val := j, isLt := hj' } < n
h : restrict { val := i, isLt := hi' } hi = restrict { val := j, isLt := hj' } hj
⊢ { val := i, isLt := hi' } = { val := j, isLt := hj' }
Tactic:
cases h
Proof state after:
case mk.mk.refl
m n i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
hj' : i < m
hj : ↑{ val := i, isLt := hj' } < n
⊢ { val := i, isLt := hi' } = { val := i, isLt := hj' }
Theorem: Fin.restrict_inj
Proof state before:
case mk.mk.refl
m n i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
hj' : i < m
hj : ↑{ val := i, isLt := hj' } < n
⊢ { val := i, isLt := hi' } = { val := i, isLt := hj' }
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∃ l', l = List.map castSucc l'
Tactic:
refine .intro (l.pmap (fun i (hi : i.1 < n) => ⟨i.1,hi⟩) ?_) ?_
Proof state after:
case refine_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (a : Fin (n + 1)), a ∈ l → ↑a < n

case refine_2
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ l = List.map castSucc (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l ?refine_1)
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (a : Fin (n + 1)), a ∈ l → ↑a < n

case refine_2
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ l = List.map castSucc (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l ?refine_1)
Tactic:
. intro i hi
  cases Nat.eq_or_lt_of_le i.2 with
  | inl heq => cases i; cases heq; exact absurd hi h
  | inr hlt => exact Nat.lt_of_succ_lt_succ hlt
Proof state after:
case refine_2
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ l = List.map castSucc (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_2
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ l = List.map castSucc (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))
Tactic:
. apply List.ext_get
  . rw [List.length_map, List.length_pmap]
  . intro i hi _
    rewrite [List.get_map, List.get_pmap]
    rfl
Proof state after:
no goals