α : Type u_1
β : Type ?u.387659
γ : Type ?u.387662
inst✝ : DecidableEq α
a : α
t : Multiset α
⊢ ∀ (s : Multiset α), count a (s - t) = count a s - count a t
α : Type u_1
β : Type ?u.387659
γ : Type ?u.387662
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s - t) = count a s - count a t
revert s
α : Type u_1
β : Type ?u.387659
γ : Type ?u.387662
inst✝ : DecidableEq α
a : α
t✝ : Multiset α
b : α
t : Multiset α
IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t
s : Multiset α
⊢ count a (s - b ::ₘ t) = count a s - count a (b ::ₘ t)
α : Type u_1
β : Type ?u.387659
γ : Type ?u.387662
inst✝ : DecidableEq α
a : α
t : Multiset α
⊢ ∀ (s : Multiset α), count a (s - t) = count a s - count a t
refine' Multiset.induction_on t (by simp) fun b t IH s => _
α : Type u_1
β : Type ?u.387659
γ : Type ?u.387662
inst✝ : DecidableEq α
a : α
t✝ : Multiset α
b : α
t : Multiset α
IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t
s : Multiset α
⊢ count a (erase s b) - count a t = count a s - count a (b ::ₘ t)
α : Type u_1
β : Type ?u.387659
γ : Type ?u.387662
inst✝ : DecidableEq α
a : α
t✝ : Multiset α
b : α
t : Multiset α
IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t
s : Multiset α
⊢ count a (s - b ::ₘ t) = count a s - count a (b ::ₘ t)
rw [sub_cons, IH]
case inl
α : Type u_1
β : Type ?u.387659
γ : Type ?u.387662
inst✝ : DecidableEq α
a : α
t✝ t : Multiset α
IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t
s : Multiset α
⊢ count a (erase s a) - count a t = count a s - count a (a ::ₘ t)

case inr
α : Type u_1
β : Type ?u.387659
γ : Type ?u.387662
inst✝ : DecidableEq α
a : α
t✝ : Multiset α
b : α
t : Multiset α
IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t
s : Multiset α
ab : a ≠ b
⊢ count a (erase s b) - count a t = count a s - count a (b ::ₘ t)
α : Type u_1
β : Type ?u.387659
γ : Type ?u.387662
inst✝ : DecidableEq α
a : α
t✝ : Multiset α
b : α
t : Multiset α
IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t
s : Multiset α
⊢ count a (erase s b) - count a t = count a s - count a (b ::ₘ t)
rcases Decidable.eq_or_ne a b with rfl | ab
no goals
α : Type u_1
β : Type ?u.387659
γ : Type ?u.387662
inst✝ : DecidableEq α
a : α
t : Multiset α
⊢ ∀ (s : Multiset α), count a (s - 0) = count a s - count a 0
simp
no goals
case inl
α : Type u_1
β : Type ?u.387659
γ : Type ?u.387662
inst✝ : DecidableEq α
a : α
t✝ t : Multiset α
IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t
s : Multiset α
⊢ count a (erase s a) - count a t = count a s - count a (a ::ₘ t)
rw [count_erase_self, count_cons_self, Nat.sub_sub, add_comm]
no goals
case inr
α : Type u_1
β : Type ?u.387659
γ : Type ?u.387662
inst✝ : DecidableEq α
a : α
t✝ : Multiset α
b : α
t : Multiset α
IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t
s : Multiset α
ab : a ≠ b
⊢ count a (erase s b) - count a t = count a s - count a (b ::ₘ t)
rw [count_erase_of_ne ab, count_cons_of_ne ab]