case zero
α : Type u_1
β : Type ?u.46161
γ : Type ?u.46164
a : α
s : Multiset α
n : ℕ
h✝ : a ∈ n • s
h : a ∈ zero • s
⊢ a ∈ s

case succ
α : Type u_1
β : Type ?u.46161
γ : Type ?u.46164
a : α
s : Multiset α
n✝ : ℕ
h✝ : a ∈ n✝ • s
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ succ n • s
⊢ a ∈ s
α : Type u_1
β : Type ?u.46161
γ : Type ?u.46164
a : α
s : Multiset α
n : ℕ
h : a ∈ n • s
⊢ a ∈ s
induction' n with n ih
case zero
α : Type u_1
β : Type ?u.46161
γ : Type ?u.46164
a : α
s : Multiset α
n : ℕ
h✝ : a ∈ n • s
h : a ∈ 0
⊢ a ∈ s
case zero
α : Type u_1
β : Type ?u.46161
γ : Type ?u.46164
a : α
s : Multiset α
n : ℕ
h✝ : a ∈ n • s
h : a ∈ zero • s
⊢ a ∈ s
rw [zero_nsmul] at h
no goals
case zero
α : Type u_1
β : Type ?u.46161
γ : Type ?u.46164
a : α
s : Multiset α
n : ℕ
h✝ : a ∈ n • s
h : a ∈ 0
⊢ a ∈ s
exact absurd h (not_mem_zero _)
case succ
α : Type u_1
β : Type ?u.46161
γ : Type ?u.46164
a : α
s : Multiset α
n✝ : ℕ
h✝ : a ∈ n✝ • s
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ s ∨ a ∈ n • s
⊢ a ∈ s
case succ
α : Type u_1
β : Type ?u.46161
γ : Type ?u.46164
a : α
s : Multiset α
n✝ : ℕ
h✝ : a ∈ n✝ • s
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ succ n • s
⊢ a ∈ s
rw [succ_nsmul, mem_add] at h
no goals
case succ
α : Type u_1
β : Type ?u.46161
γ : Type ?u.46164
a : α
s : Multiset α
n✝ : ℕ
h✝ : a ∈ n✝ • s
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ s ∨ a ∈ n • s
⊢ a ∈ s
exact h.elim id ih