α : Type u_1
β : Type ?u.47121
γ : Type ?u.47124
a : α
s : Multiset α
n : ℕ
h0 : n ≠ 0
h : a ∈ s
⊢ a ∈ n • s
α : Type u_1
β : Type ?u.47121
γ : Type ?u.47124
a : α
s : Multiset α
n : ℕ
h0 : n ≠ 0
⊢ a ∈ n • s ↔ a ∈ s
refine' ⟨mem_of_mem_nsmul, fun h => _⟩
case intro
α : Type u_1
β : Type ?u.47121
γ : Type ?u.47124
a : α
s : Multiset α
h : a ∈ s
n : ℕ
h0 : succ n ≠ 0
⊢ a ∈ succ n • s
α : Type u_1
β : Type ?u.47121
γ : Type ?u.47124
a : α
s : Multiset α
n : ℕ
h0 : n ≠ 0
h : a ∈ s
⊢ a ∈ n • s
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero h0
case intro
α : Type u_1
β : Type ?u.47121
γ : Type ?u.47124
a : α
s : Multiset α
h : a ∈ s
n : ℕ
h0 : succ n ≠ 0
⊢ a ∈ s ∨ a ∈ n • s
case intro
α : Type u_1
β : Type ?u.47121
γ : Type ?u.47124
a : α
s : Multiset α
h : a ∈ s
n : ℕ
h0 : succ n ≠ 0
⊢ a ∈ succ n • s
rw [succ_nsmul, mem_add]
no goals
case intro
α : Type u_1
β : Type ?u.47121
γ : Type ?u.47124
a : α
s : Multiset α
h : a ∈ s
n : ℕ
h0 : succ n ≠ 0
⊢ a ∈ s ∨ a ∈ n • s
exact Or.inl h