α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ filter ((fun x x_1 => x ≠ x_1) a) ↑m + ↑(replicate (count a ↑m) a) = ↑m
α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑(fill a (filterNe a m).fst (filterNe a m).snd) = ↑m
rw [coe_fill, filterNe, ← val_eq_coe, Subtype.coe_mk, Fin.val_mk]
case a
α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter ((fun x x_1 => x ≠ x_1) a) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m
α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ filter ((fun x x_1 => x ≠ x_1) a) ↑m + ↑(replicate (count a ↑m) a) = ↑m
ext b
case a
α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x => ¬a = x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m
case a
α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter ((fun x x_1 => x ≠ x_1) a) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m
dsimp
case a
α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ ((if ¬a = b then count b ↑m else 0) + if b = a then count a ↑m else 0) = count b ↑m
case a
α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x => ¬a = x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m
rw [count_add, count_filter, Sym.coe_replicate, count_replicate]
case a.inl
α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ((if ¬a = a then count a ↑m else 0) + if a = a then count a ↑m else 0) = count a ↑m

case a.inr
α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if b = a then count a ↑m else 0) = count b ↑m
case a
α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ ((if ¬a = b then count b ↑m else 0) + if b = a then count a ↑m else 0) = count b ↑m
obtain rfl | h := eq_or_ne a b
no goals
case a.inl
α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ((if ¬a = a then count a ↑m else 0) + if a = a then count a ↑m else 0) = count a ↑m
rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]
no goals
case a.inr
α : Type u_1
β : Type ?u.54293
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if b = a then count a ↑m else 0) = count b ↑m
rw [if_pos h, if_neg h.symm, add_zero]