no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hxy : x ≠ y
⊢ Multiset.Nodup (x ::ₘ y ::ₘ 0)
simp [hxy]
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hxy : x ≠ y
⊢ support (swap x y) = { val := x ::ₘ y ::ₘ 0, nodup := (_ : Multiset.Nodup (x ::ₘ {y})) }
simp [support_swap hxy, *, Finset.ext_iff]