Theorem: Sym.count_coe_fill_self_of_not_mem (ForML/FDerivProd.lean)

State before:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s✝¹ s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
b✝ : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
α : Type u_3
β : Type u_4
n n' m : ℕ
s✝ : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : a ∉ s
⊢ count a ↑(fill a i s) = ↑i
Tactic:
simp [coe_fill, coe_replicate, hx]
State after:
no goals