case mk.mk
α : Type u_1
β : Type ?u.52511
γ : Type ?u.52514
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk Setoid.r l)
⊢ card (permsOfFinset { val := Quot.mk Setoid.r l, nodup := hs }) = (card { val := Quot.mk Setoid.r l, nodup := hs })!
α : Type u_1
β : Type ?u.52511
γ : Type ?u.52514
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ ∀ (s : Finset α), card (permsOfFinset s) = (card s)!
rintro ⟨⟨l⟩, hs⟩
no goals
case mk.mk
α : Type u_1
β : Type ?u.52511
γ : Type ?u.52514
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk Setoid.r l)
⊢ card (permsOfFinset { val := Quot.mk Setoid.r l, nodup := hs }) = (card { val := Quot.mk Setoid.r l, nodup := hs })!
exact length_permsOfList l