Theorem: Sym.multinomial_coe_fill_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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ s
⊢ Multiset.multinomial ↑(fill x m s) = Nat.choose n ↑m * Multiset.multinomial ↑s
Tactic:
rw [Multiset.multinomial_filter_ne x]
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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ s
⊢ Nat.choose (Multiset.card ↑(fill x m s)) (Multiset.count x ↑(fill x m s)) *
      Multiset.multinomial (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)) =
    Nat.choose n ↑m * Multiset.multinomial ↑s

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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ s
⊢ Nat.choose (Multiset.card ↑(fill x m s)) (Multiset.count x ↑(fill x m s)) *
      Multiset.multinomial (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)) =
    Nat.choose n ↑m * Multiset.multinomial ↑s
Tactic:
rw [← mem_coe] at hx
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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Nat.choose (Multiset.card ↑(fill x m s)) (Multiset.count x ↑(fill x m s)) *
      Multiset.multinomial (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)) =
    Nat.choose n ↑m * Multiset.multinomial ↑s

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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Nat.choose (Multiset.card ↑(fill x m s)) (Multiset.count x ↑(fill x m s)) *
      Multiset.multinomial (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)) =
    Nat.choose n ↑m * Multiset.multinomial ↑s
Tactic:
refine congrArg₂ _ ?_ ?_
State after:
case refine_1
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Nat.choose (Multiset.card ↑(fill x m s)) (Multiset.count x ↑(fill x m s)) = Nat.choose n ↑m

case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.multinomial (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)) = Multiset.multinomial ↑s

State before:
case refine_1
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Nat.choose (Multiset.card ↑(fill x m s)) (Multiset.count x ↑(fill x m s)) = Nat.choose n ↑m
Tactic:
rw [card_coe, count_coe_fill_self_of_not_mem hx]
State after:
no goals

State before:
case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.multinomial (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)) = Multiset.multinomial ↑s
Tactic:
refine congrArg _ ?_
State after:
case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s) = ↑s

State before:
case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s) = ↑s
Tactic:
rw [coe_fill, coe_replicate, Multiset.filter_add]
State after:
case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 => x ≠ x_1) ↑s + Multiset.filter (fun x_1 => x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s

State before:
case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 => x ≠ x_1) ↑s + Multiset.filter (fun x_1 => x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s
Tactic:
rw [Multiset.filter_eq_self.mpr]
State after:
case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ↑s + Multiset.filter (fun x_1 => x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s

case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ ↑s, x ≠ a

State before:
case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ↑s + Multiset.filter (fun x_1 => x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s
Tactic:
rw [add_right_eq_self]
State after:
case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 => x ≠ x_1) (Multiset.replicate (↑m) x) = 0

State before:
case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 => x ≠ x_1) (Multiset.replicate (↑m) x) = 0
Tactic:
rw [Multiset.filter_eq_nil]
State after:
case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ Multiset.replicate (↑m) x, ¬x ≠ a

State before:
case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ Multiset.replicate (↑m) x, ¬x ≠ a
Tactic:
exact fun j hj ↦ by simp [Multiset.mem_replicate.mp hj]
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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
j : α
hj : j ∈ Multiset.replicate (↑m) x
⊢ ¬x ≠ j
Tactic:
simp [Multiset.mem_replicate.mp hj]
State after:
no goals

State before:
case refine_2
𝕜 : 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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ ↑s, x ≠ a
Tactic:
exact fun j hj h ↦ hx <| by simpa [h] using hj
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
n : ℕ
α : Type u_3
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
j : α
hj : j ∈ ↑s
h : x = j
⊢ x ∈ ↑s
Tactic:
simpa [h] using hj
State after:
no goals