Theorem: Array.nodup_swap (Fifteen/Data/Array/Basic.lean)

State before:
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
⊢ Nodup (swap as i j)
Tactic:
apply nodup_of_get_inj
State after:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
⊢ ∀ (i_1 j_1 : Nat) (hi : i_1 < size (swap as i j)) (hj : j_1 < size (swap as i j)),
    (swap as i j)[i_1] = (swap as i j)[j_1] → i_1 = j_1

State before:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
⊢ ∀ (i_1 j_1 : Nat) (hi : i_1 < size (swap as i j)) (hj : j_1 < size (swap as i j)),
    (swap as i j)[i_1] = (swap as i j)[j_1] → i_1 = j_1
Tactic:
intro k l hk hl has
State after:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
has : (swap as i j)[k] = (swap as i j)[l]
⊢ k = l

State before:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
has : (swap as i j)[k] = (swap as i j)[l]
⊢ k = l
Tactic:
apply h.get_inj k l (as.size_swap i j ▸ hk) (as.size_swap i j ▸ hl)
State after:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
has : (swap as i j)[k] = (swap as i j)[l]
⊢ as[k] = as[l]

State before:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
has : (swap as i j)[k] = (swap as i j)[l]
⊢ as[k] = as[l]
Tactic:
simp only [getElem_swap] at has
State after:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
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]
⊢ as[k] = as[l]

State before:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
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]
⊢ as[k] = as[l]
Tactic:
rewrite [as.size_swap i j] at hk hl
State after:
case h
α : 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]
⊢ as[k] = as[l]

State before:
case h
α : 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]
⊢ as[k] = as[l]
Tactic:
apply dite (j.val = k) <;> apply dite (i.val = k)
  <;> apply dite (j.val = l) <;> apply dite (i.val = l)
  <;> intro hil hjl hik hjk
State after:
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]

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)
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]

State before:
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]
Tactic:
all_goals try (cases hjk.symm.trans hjl; rfl)
State after:
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.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]

State before:
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.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]
Tactic:
all_goals iterate rewrite [if_pos ‹_›] at has
State after:
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 : 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]

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

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]

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]

State before:
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 : 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]

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

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]

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]
Tactic:
all_goals iterate rewrite [if_neg ‹_›] at has
State after:
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 : as[i.val] = 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 : as[i.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]

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

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]

State before:
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 : as[i.val] = 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 : as[i.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]

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

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:
all_goals iterate rewrite [if_pos ‹_›] at has
State after:
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 : as[i.val] = 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 : as[i.val] = as[j.val]
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 : as[i.val] = 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 : as[j.val] = as[i.val]
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 : 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]

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 : as[k] = as[i.val]
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 : as[k] = as[i.val]
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 : 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]

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]

State before:
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 : as[i.val] = 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 : as[i.val] = as[j.val]
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 : as[i.val] = 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 : as[j.val] = as[i.val]
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 : 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]

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 : as[k] = as[i.val]
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 : as[k] = as[i.val]
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 : 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]

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:
all_goals iterate rewrite [if_neg ‹_›] at has
State after:
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 : as[i.val] = 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 : as[i.val] = as[j.val]
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 : as[i.val] = 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 : as[j.val] = as[i.val]
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 : 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]

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 : as[k] = as[i.val]
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 : as[k] = as[i.val]
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 : 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]

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]

State before:
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 : as[i.val] = 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 : as[i.val] = as[j.val]
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 : as[i.val] = 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 : as[j.val] = as[i.val]
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 : 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]

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 : as[k] = as[i.val]
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 : as[k] = as[i.val]
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 : 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]

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:
all_goals try cases ‹_ = k›
State after:
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]

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

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]

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

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]

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 : as[k] = as[i.val]
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 : as[k] = as[i.val]
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 : 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]

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]

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]

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

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]

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

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]

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 : as[k] = as[i.val]
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 : as[k] = as[i.val]
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 : 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]

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:
all_goals try cases ‹_ = l›
State after:
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]

case h.t.e.e.t.refl.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
has : as[i.val] = as[j.val]
hk✝ : j.val < size (swap as i j)
hk : j.val < size as
hik : ¬i.val = j.val
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[j.val] = as[i.val]

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]

case h.e.t.t.e.refl.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
has : as[j.val] = as[i.val]
hk✝ : i.val < size (swap as i j)
hk : i.val < size as
hjk : ¬j.val = i.val
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.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]

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[k] = as[j.val]

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[k] = 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[k] = as[i.val]

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]

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]

case h.t.e.e.t.refl.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
has : as[i.val] = as[j.val]
hk✝ : j.val < size (swap as i j)
hk : j.val < size as
hik : ¬i.val = j.val
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[j.val] = as[i.val]

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]

case h.e.t.t.e.refl.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
has : as[j.val] = as[i.val]
hk✝ : i.val < size (swap as i j)
hk : i.val < size as
hjk : ¬j.val = i.val
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.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]

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[k] = as[j.val]

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[k] = 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[k] = as[i.val]

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:
all_goals try simp [has]
State after:
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]

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]

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]

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]

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]

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]

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]

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]

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]

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:
. simp only [← hik, has]
State after:
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]

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]

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]

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]

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]

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]

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]

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 hil <| h.get_inj _ _ _ _ has
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]

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]

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]

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]

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]

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 hjl <| h.get_inj _ _ _ _ has
State after:
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]

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]

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]

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:
. simp only [hil]
State after:
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]

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

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
State after:
no goals

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)
State after:
no goals

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)
State after:
no goals

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

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
State after:
no goals

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)
State after:
no goals

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)
State after:
no goals

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

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
State after:
no goals

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

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
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

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

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

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

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

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

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

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›
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]

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›
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]

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›
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]

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›
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]

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]
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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]
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals