Theorem: Sym.count_coe_fill_of_ne (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 x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
⊢ count x ↑(fill a i s) = count x ↑s
Tactic:
suffices : x ∉ Multiset.replicate i a
State after:
𝕜 : 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 x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
this : x ∉ Multiset.replicate (↑i) a
⊢ count x ↑(fill a i s) = count x ↑s

case this
𝕜 : 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 x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
⊢ x ∉ Multiset.replicate (↑i) a

State before:
case this
𝕜 : 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 x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
⊢ x ∉ Multiset.replicate (↑i) a
Tactic:
simp [Multiset.mem_replicate, hx]
State after:
no goals

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 x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
this : x ∉ Multiset.replicate (↑i) a
⊢ count x ↑(fill a i s) = count x ↑s
Tactic:
simp [coe_fill, coe_replicate, this]
State after:
no goals