α : Type u_1
β : Type ?u.30399
n n' m : ℕ
s : Sym α n
a b : α
⊢ (↑Multiset.card ↑s = n ∧ ∀ (b : α), b ∈ ↑s → b = a) ↔ ∀ (b : α), b ∈ s → b = a
α : Type u_1
β : Type ?u.30399
n n' m : ℕ
s : Sym α n
a b : α
⊢ s = replicate n a ↔ ∀ (b : α), b ∈ s → b = a
erw [Subtype.ext_iff, Multiset.eq_replicate]
no goals
α : Type u_1
β : Type ?u.30399
n n' m : ℕ
s : Sym α n
a b : α
⊢ (↑Multiset.card ↑s = n ∧ ∀ (b : α), b ∈ ↑s → b = a) ↔ ∀ (b : α), b ∈ s → b = a
exact and_iff_right s.2