no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.932002
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hr : r' < r
⊢ ∃ C,
    ∀ (y : E),
      y ∈ EMetric.ball x r' →
        ∀ (z : E), z ∈ EMetric.ball x r' → ‖f y - f z - ↑(p 1) fun x => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
simpa only [isBigO_principal, mul_assoc, norm_mul, norm_norm, Prod.forall, EMetric.mem_ball,
  Prod.edist_eq, max_lt_iff, and_imp, @forall_swap (_ < _) E] using
  hf.isBigO_image_sub_image_sub_deriv_principal hr