-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem HasFiniteFPowerSeriesOnBall.cPolynomialAt_of_mem
    (hf : HasFiniteFPowerSeriesOnBall f p x n r) (h : y ∈ EMetric.ball x r) :
    CPolynomialAt 𝕜 f y

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ EMetric.ball x r
⊢ ↑‖y - x‖₊ < r

Tactic:
simpa [edist_eq_enorm_sub] using h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ EMetric.ball x r
this✝ : ↑‖y - x‖₊ < r
this : HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) y n (r - ↑‖y - x‖₊)
⊢ CPolynomialAt 𝕜 f y

Tactic:
exact this.cPolynomialAt

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ EMetric.ball x r
this : ↑‖y - x‖₊ < r
⊢ CPolynomialAt 𝕜 f y

Tactic:
have := hf.changeOrigin this

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ EMetric.ball x r
this✝ : ↑‖y - x‖₊ < r
this : HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) (x + (y - x)) n (r - ↑‖y - x‖₊)
⊢ CPolynomialAt 𝕜 f y

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ EMetric.ball x r
⊢ CPolynomialAt 𝕜 f y

Tactic:
have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using h

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ EMetric.ball x r
this : ↑‖y - x‖₊ < r
⊢ CPolynomialAt 𝕜 f y

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ EMetric.ball x r
this✝ : ↑‖y - x‖₊ < r
this : HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) (x + (y - x)) n (r - ↑‖y - x‖₊)
⊢ CPolynomialAt 𝕜 f y

Tactic:
rw [add_sub_cancel] at this

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ EMetric.ball x r
this✝ : ↑‖y - x‖₊ < r
this : HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) y n (r - ↑‖y - x‖₊)
⊢ CPolynomialAt 𝕜 f y