Theorem: Array.nodup_swap
Proof state before:
case h.t.t.t.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]

case h.t.t.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]

case h.t.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]

case h.t.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 :
  (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]

case h.t.e.t.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]

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]

case h.t.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 :
  (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]

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]

case h.e.t.t.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]

case h.e.t.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]

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]

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 :
  (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]

case h.e.e.t.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]

case h.e.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]

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 :
  (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]

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:
all_goals try (cases hik.symm.trans hil; rfl)
Proof state after:
case h.t.t.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]

case h.t.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 :
  (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]

case h.t.e.t.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]

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]

case h.t.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 :
  (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]

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]

case h.e.t.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]

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 :
  (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]

case h.e.e.t.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]

case h.e.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]

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 :
  (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]

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]