𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
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 uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
y : E
⊢ (∀ (m : ℕ), ↑m ≤ n → ∃ u, u ∈ 𝓝[insert x (insert y s)] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u) ↔
    ∀ (m : ℕ), ↑m ≤ n → ∃ u, u ∈ 𝓝[insert x s] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
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 uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
y : E
⊢ ContDiffWithinAt 𝕜 n f (insert y s) x ↔ ContDiffWithinAt 𝕜 n f s x
simp_rw [ContDiffWithinAt]
case inl
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
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 uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
⊢ (∀ (m : ℕ), ↑m ≤ n → ∃ u, u ∈ 𝓝[insert x (insert x s)] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u) ↔
    ∀ (m : ℕ), ↑m ≤ n → ∃ u, u ∈ 𝓝[insert x s] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u

case inr
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
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 uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
y : E
h : x ≠ y
⊢ (∀ (m : ℕ), ↑m ≤ n → ∃ u, u ∈ 𝓝[insert x (insert y s)] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u) ↔
    ∀ (m : ℕ), ↑m ≤ n → ∃ u, u ∈ 𝓝[insert x s] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
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 uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
y : E
⊢ (∀ (m : ℕ), ↑m ≤ n → ∃ u, u ∈ 𝓝[insert x (insert y s)] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u) ↔
    ∀ (m : ℕ), ↑m ≤ n → ∃ u, u ∈ 𝓝[insert x s] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
rcases eq_or_ne x y with (rfl | h)
no goals
case inr
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
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 uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
y : E
h : x ≠ y
⊢ (∀ (m : ℕ), ↑m ≤ n → ∃ u, u ∈ 𝓝[insert x (insert y s)] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u) ↔
    ∀ (m : ℕ), ↑m ≤ n → ∃ u, u ∈ 𝓝[insert x s] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
simp_rw [insert_comm x y, nhdsWithin_insert_of_ne h]
no goals
case inl
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
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 uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
⊢ (∀ (m : ℕ), ↑m ≤ n → ∃ u, u ∈ 𝓝[insert x (insert x s)] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u) ↔
    ∀ (m : ℕ), ↑m ≤ n → ∃ u, u ∈ 𝓝[insert x s] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
simp_rw [insert_eq_of_mem (mem_insert _ _)]