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

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