case a
α : Type u_1
β : Type ?u.473165
γ : Type ?u.473168
inst✝ : DecidableEq α
l l' : List α
a : α
n : ℕ
hn : n ≠ 0
x : α
⊢ x ∈ toFinset (replicate n a) ↔ x ∈ {a}
α : Type u_1
β : Type ?u.473165
γ : Type ?u.473168
inst✝ : DecidableEq α
l l' : List α
a : α
n : ℕ
hn : n ≠ 0
⊢ toFinset (replicate n a) = {a}
ext x
no goals
case a
α : Type u_1
β : Type ?u.473165
γ : Type ?u.473168
inst✝ : DecidableEq α
l l' : List α
a : α
n : ℕ
hn : n ≠ 0
x : α
⊢ x ∈ toFinset (replicate n a) ↔ x ∈ {a}
simp [hn, List.mem_replicate]