case refine'_1
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • 0) = n • filter p 0

case refine'_2
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ ∀ ⦃a : α⦄ {s : Multiset α}, filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • s) = n • filter p s
refine' s.induction_on _ _
no goals
case refine'_1
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • 0) = n • filter p 0
simp only [filter_zero, nsmul_zero]
case refine'_2
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • (a ::ₘ ha)) = n • filter p (a ::ₘ ha)
case refine'_2
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ ∀ ⦃a : α⦄ {s : Multiset α}, filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)
intro a ha ih
case refine'_2
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • {a}) + n • filter p ha = (n • if p a then {a} else 0) + n • filter p ha
case refine'_2
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • (a ::ₘ ha)) = n • filter p (a ::ₘ ha)
rw [nsmul_cons, filter_add, ih, filter_cons, nsmul_add]
case refine'_2.e_a
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • {a}) = n • if p a then {a} else 0
case refine'_2
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • {a}) + n • filter p ha = (n • if p a then {a} else 0) + n • filter p ha
congr
case refine'_2.e_a.inr
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ ∀ (a_1 : α), a_1 ∈ n • {a} → ¬p a_1
case refine'_2.e_a.inr
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ filter p (n • {a}) = n • 0
simp only [filter_eq_self, nsmul_zero, filter_eq_nil]
case refine'_2.e_a.inr
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
b : α
hb : b ∈ n • {a}
⊢ ¬p b
case refine'_2.e_a.inr
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ ∀ (a_1 : α), a_1 ∈ n • {a} → ¬p a_1
intro b hb
no goals
case refine'_2.e_a.inr
α : Type u_1
β : Type ?u.233049
γ : Type ?u.233052
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
b : α
hb : b ∈ n • {a}
⊢ ¬p b
rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]