-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesWithinOnBall.image_sub_sub_deriv_le
    (hf : HasFPowerSeriesWithinOnBall f p s x r) (hr : r' < r) :
    ∃ C, ∀ᵉ (y ∈ insert x s ∩ EMetric.ball x r') (z ∈ insert x s ∩ EMetric.ball x r'),
      ‖f y - f z - p 1 fun _ => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖

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
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
⊢ ∃ C,
    ∀ y ∈ insert x s ∩ EMetric.ball x r',
      ∀ z ∈ insert x s ∩ EMetric.ball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * (‖y - x‖ ⊔ ‖z - x‖) * ‖y - z‖

Tactic:
have := hf.isBigO_image_sub_image_sub_deriv_principal hr

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
s : Set E
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
this :
  (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) r' ∩ insert x s ×ˢ insert x s)] fun y =>
    ‖y - (x, x)‖ * ‖y.1 - y.2‖
⊢ ∃ C,
    ∀ y ∈ insert x s ∩ EMetric.ball x r',
      ∀ z ∈ insert x s ∩ EMetric.ball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * (‖y - x‖ ⊔ ‖z - x‖) * ‖y - z‖

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
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
this :
  (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) r' ∩ insert x s ×ˢ insert x s)] fun y =>
    ‖y - (x, x)‖ * ‖y.1 - y.2‖
⊢ ∃ C,
    ∀ y ∈ insert x s ∩ EMetric.ball x r',
      ∀ z ∈ insert x s ∩ EMetric.ball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * (‖y - x‖ ⊔ ‖z - x‖) * ‖y - z‖

Tactic:
simp only [isBigO_principal, mem_inter_iff, EMetric.mem_ball, Prod.edist_eq, max_lt_iff, mem_prod,
  norm_mul, Real.norm_eq_abs, abs_norm, and_imp, Prod.forall, mul_assoc] 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
s : Set E
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
this :
  ∃ c,
    ∀ (a b : E),
      edist a x < r' →
        edist b x < r' →
          a ∈ insert x s → b ∈ insert x s → ‖f a - f b - (p 1) fun x => a - b‖ ≤ c * (‖(a, b) - (x, x)‖ * ‖a - b‖)
⊢ ∃ C,
    ∀ y ∈ insert x s,
      edist y x < r' →
        ∀ z ∈ insert x s, edist z x < r' → ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * ((‖y - x‖ ⊔ ‖z - x‖) * ‖y - z‖)

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
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
this :
  ∃ c,
    ∀ (a b : E),
      edist a x < r' →
        edist b x < r' →
          a ∈ insert x s → b ∈ insert x s → ‖f a - f b - (p 1) fun x => a - b‖ ≤ c * (‖(a, b) - (x, x)‖ * ‖a - b‖)
⊢ ∃ C,
    ∀ y ∈ insert x s,
      edist y x < r' →
        ∀ z ∈ insert x s, edist z x < r' → ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * ((‖y - x‖ ⊔ ‖z - x‖) * ‖y - z‖)

Tactic:
rcases this with ⟨C, hC⟩

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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
C : ℝ
hC :
  ∀ (a b : E),
    edist a x < r' →
      edist b x < r' →
        a ∈ insert x s → b ∈ insert x s → ‖f a - f b - (p 1) fun x => a - b‖ ≤ C * (‖(a, b) - (x, x)‖ * ‖a - b‖)
⊢ ∃ C,
    ∀ y ∈ insert x s,
      edist y x < r' →
        ∀ z ∈ insert x s, edist z x < r' → ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * ((‖y - x‖ ⊔ ‖z - x‖) * ‖y - z‖)

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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
C : ℝ
hC :
  ∀ (a b : E),
    edist a x < r' →
      edist b x < r' →
        a ∈ insert x s → b ∈ insert x s → ‖f a - f b - (p 1) fun x => a - b‖ ≤ C * (‖(a, b) - (x, x)‖ * ‖a - b‖)
⊢ ∃ C,
    ∀ y ∈ insert x s,
      edist y x < r' →
        ∀ z ∈ insert x s, edist z x < r' → ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * ((‖y - x‖ ⊔ ‖z - x‖) * ‖y - z‖)

Tactic:
exact ⟨C, fun y ys hy z zs hz ↦ hC y z hy hz ys zs⟩

Result:
no goals