-- Mathlib/Algebra/Order/Group/Finset.lean
lemma toFinset_eq_singleton_iff (s : Multiset α) (a : α) :
    s.toFinset = {a} ↔ card s ≠ 0 ∧ s = card s • {a}

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ count x s = s.card * if x = a then 1 else 0

Tactic:
simp_rw [hx, ite_true, mul_one, count_eq_card]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ ∀ x ∈ s, a = x

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
hy : y = a
⊢ a = y

Tactic:
exact hy.symm

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = count x (s.card • {a})

Tactic:
rw [count_nsmul, count_singleton]

Result:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = s.card * if x = a then 1 else 0

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ ∀ x ∈ s, a = x

Tactic:
intro y hy

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
hy : y ∈ s
⊢ a = y

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
hy : y ∈ s
⊢ a = y

Tactic:
rw [← mem_toFinset, H, Finset.mem_singleton] at hy

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
hy : y = a
⊢ a = y

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
h : s.card = 0
⊢ False

Tactic:
rw [card_eq_zero.1 h, toFinset_zero] at H

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : ∅ = {a}
h : s.card = 0
⊢ False

Proof state:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.card ≠ 0 ∧ s = s.card • {a}
⊢ s.toFinset = {a}

Tactic:
simpa only [toFinset_nsmul _ _ H.1, toFinset_singleton] using congr($(H.2).toFinset)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
h' : x ∈ s
⊢ x = a

Tactic:
rwa [← mem_toFinset, H, Finset.mem_singleton] at h'

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = s.card * if x = a then 1 else 0

Tactic:
by_cases hx : x = a

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ count x s = s.card * if x = a then 1 else 0

case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
⊢ count x s = s.card * if x = a then 1 else 0

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : ∅ = {a}
h : s.card = 0
⊢ False

Tactic:
exact Finset.singleton_ne_empty _ H.symm

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
⊢ count x s = s.card * if x = a then 1 else 0

Tactic:
have hx' : x ∉ s := fun h' ↦ hx <| by rwa [← mem_toFinset, H, Finset.mem_singleton] at h'

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
hx' : x ∉ s
⊢ count x s = s.card * if x = a then 1 else 0

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
hx' : x ∉ s
⊢ count x s = s.card * if x = a then 1 else 0

Tactic:
simp_rw [count_eq_zero_of_not_mem hx', hx, ite_false, Nat.mul_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ s.toFinset = {a} ↔ s.card ≠ 0 ∧ s = s.card • {a}

Tactic:
refine ⟨fun H ↦ ⟨fun h ↦ ?_, ext' fun x ↦ ?_⟩, fun H ↦ ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
h : s.card = 0
⊢ False

case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = count x (s.card • {a})

case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.card ≠ 0 ∧ s = s.card • {a}
⊢ s.toFinset = {a}