no goals
α : Type u_1
β : Type ?u.448176
γ : Type ?u.448179
inst✝ : DecidableEq α
s✝ t s : Multiset α
h : 0 ≠ 0
⊢ toFinset (0 • s) = toFinset s
contradiction
case pos
α : Type u_1
β : Type ?u.448176
γ : Type ?u.448179
inst✝ : DecidableEq α
s✝ t s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : n = 0
⊢ toFinset ((n + 1) • s) = toFinset s

case neg
α : Type u_1
β : Type ?u.448176
γ : Type ?u.448179
inst✝ : DecidableEq α
s✝ t s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ toFinset ((n + 1) • s) = toFinset s
α : Type u_1
β : Type ?u.448176
γ : Type ?u.448179
inst✝ : DecidableEq α
s✝ t s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
⊢ toFinset ((n + 1) • s) = toFinset s
by_cases h : n = 0
no goals
case pos
α : Type u_1
β : Type ?u.448176
γ : Type ?u.448179
inst✝ : DecidableEq α
s✝ t s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : n = 0
⊢ toFinset ((n + 1) • s) = toFinset s
rw [h, zero_add, one_nsmul]
no goals
case neg
α : Type u_1
β : Type ?u.448176
γ : Type ?u.448179
inst✝ : DecidableEq α
s✝ t s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ toFinset ((n + 1) • s) = toFinset s
rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]