-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub
    (hf : HasFPowerSeriesWithinAt f p s x) :
    (fun y : E × E => f y.1 - f y.2 - p 1 fun _ => y.1 - y.2)
      =O[𝓝[(insert x s) ×ˢ (insert x s)] (x, x)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖

Proof state:
case intro
𝕜 : 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
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓝[insert x s ×ˢ insert x s] (x, x)] fun y =>
    ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hf.r_pos with ⟨r', r'0, h⟩

Result:
case intro.intro.intro
𝕜 : 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
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
⊢ (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓝[insert x s ×ˢ insert x s] (x, x)] fun y =>
    ‖y - (x, x)‖ * ‖y.1 - y.2‖

Proof state:
case intro.intro.intro
𝕜 : 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
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
⊢ (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓝[insert x s ×ˢ insert x s] (x, x)] fun y =>
    ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
refine (hf.isBigO_image_sub_image_sub_deriv_principal h).mono ?_

Result:
case intro.intro.intro
𝕜 : 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
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
⊢ 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (EMetric.ball (x, x) ↑r' ∩ insert x s ×ˢ insert x s)

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
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f p s x
⊢ (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓝[insert x s ×ˢ insert x s] (x, x)] fun y =>
    ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
rcases hf with ⟨r, hf⟩

Result:
case intro
𝕜 : 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
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓝[insert x s ×ˢ insert x s] (x, x)] fun y =>
    ‖y - (x, x)‖ * ‖y.1 - y.2‖

Proof state:
case intro.intro.intro
𝕜 : 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
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
⊢ 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (insert x s ×ˢ insert x s ∩ EMetric.ball (x, x) ↑r')

Tactic:
exact le_principal_iff.2 (inter_mem_nhdsWithin _ (EMetric.ball_mem_nhds _ r'0))

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : 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
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
⊢ 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (EMetric.ball (x, x) ↑r' ∩ insert x s ×ˢ insert x s)

Tactic:
rw [inter_comm]

Result:
case intro.intro.intro
𝕜 : 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
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
⊢ 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (insert x s ×ˢ insert x s ∩ EMetric.ball (x, x) ↑r')