awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this_1 :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
⊢ R₁ ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this_1 :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
funProp : R₁ ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (c_1 : ℝ) ↦ R₂ * (‖z - c‖ / c_1) ^ (n + 1)) R₁

Tactic:
fun_prop (disch := positivity)
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
inr : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
suffices ∀ᶠ r in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1) by
      refine ge_of_tendsto ?_ this
      refine ContinuousAt.continuousWithinAt ?_
      fun_prop (disch := positivity)
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
⊢ ‖z - c‖ < R₁

Tactic:
rw [mem_ball_iff_norm] at hz

Premises used: mem_ball_iff_norm
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
hz₁ : ‖z - c‖ < R₁
⊢ 0 < R₁

Tactic:
rw [mem_ball_iff_norm] at hz

Premises used: mem_ball_iff_norm
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
hz₁ : ‖z - c‖ < R₁
hR₂ : 0 < R₁
⊢ ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
rw [mem_ball_iff_norm] at hz

Premises used: mem_ball_iff_norm
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
hz₁ : ‖z - c‖ < R₁
hR₂ : 0 < R₁
this₁ :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
⊢ ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))

Tactic:
rw [mem_ball_iff_norm] at hz

Premises used: mem_ball_iff_norm
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
r : ℝ
h : ∀ (hzr : ‖z - c‖ < r) (hrR₁ : r < R₁), ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
⊢ r ∈ Ioo ‖z - c‖ R₁ → ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)

Tactic:
⟨hzr, hrR₁⟩
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
h : ∀ (r : ℝ) (hzr : ‖z - c‖ < r) (hrR₁ : r < R₁), ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)

Tactic:
filter_upwards [Ioo_mem_nhdsLT hz] with r ⟨hzr, hrR₁⟩

Premises used: Ioo_mem_nhdsLT
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
r : ℝ
hzr : ‖z - c‖ < r
hrR₁ : r < R₁
h : DifferentiableOn ℂ f (ball c r)
h₁ : MapsTo f (ball c r) (closedBall (f c) R₂)
h₂ : z ∈ ball c r
h₃ : 0 < r
h₄ : DifferentiableOn ℂ f (closedBall c r) ∧ MapsTo f (closedBall c r) (closedBall (f c) R₂)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)

Tactic:
apply this
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
r : ℝ
hzr : ‖z - c‖ < r
hrR₁ : r < R₁
⊢ ball c r ⊆ ball c R₁

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
r : ℝ
hzr : ‖z - c‖ < r
hrR₁ : r < R₁
⊢ DifferentiableOn ℂ f (ball c r)

Tactic:
exact hd.mono <| by gcongr

Premises used: DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
r : ℝ
hzr : ‖z - c‖ < r
hrR₁ : r < R₁
⊢ MapsTo f (ball c r) (closedBall (f c) R₂)

Tactic:
exact h_maps.mono_left <| by gcongr

Premises used: Set.MapsTo.mono_left
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
r : ℝ
hzr : ‖z - c‖ < r
hrR₁ : r < R₁
h h₁ h₂ h₃ : ‖z - c‖ < r
⊢ z ∈ ball c r

Tactic:
rwa [mem_ball_iff_norm]

Premises used: mem_ball_iff_norm
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
r : ℝ
hzr : ‖z - c‖ < r
hrR₁ : r < R₁
⊢ 0 < r

Tactic:
(norm_nonneg _).trans_lt hzr

Premises used: LE.le.trans_lt, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
r : ℝ
hzr : ‖z - c‖ < r
hrR₁ : r < R₁
⊢ 0 < r

Tactic:
exact (norm_nonneg _).trans_lt hzr

Premises used: LE.le.trans_lt, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
r : ℝ
hzr : ‖z - c‖ < r
hrR₁ : r < R₁
⊢ DifferentiableOn ℂ f (closedBall c r) ∧ MapsTo f (closedBall c r) (closedBall (f c) R₂)

Tactic:
⟨hd.mono <| closedBall_subset_ball hrR₁, h_maps.mono_left <|
        closedBall_subset_ball hrR₁⟩

Premises used: Metric.closedBall_subset_ball, Set.MapsTo.mono_left, And.intro, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
r : ℝ
hzr : ‖z - c‖ < r
hrR₁ : r < R₁
⊢ DifferentiableOn ℂ f (closedBall c r) ∧ MapsTo f (closedBall c r) (closedBall (f c) R₂)

Tactic:
exact ⟨hd.mono <| closedBall_subset_ball hrR₁, h_maps.mono_left <|
        closedBall_subset_ball hrR₁⟩
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
⊢ DifferentiableOn ℂ f (closedBall c R₁)

Tactic:
rcases hd' with ⟨hd, h_maps⟩
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hd : DifferentiableOn ℂ f (closedBall c R₁)
⊢ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)

Tactic:
rcases hd' with ⟨hd, h_maps⟩
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
inl :
  ∀ (hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 z) (fun (x : ℂ) ↦ f x - f z) fun (w : ℂ) ↦ (w - z) ^ n)
    (hz : z ∈ ball z R₁) (hd : DifferentiableOn ℂ f (closedBall z R₁))
    (h_maps : MapsTo f (closedBall z R₁) (closedBall (f z) R₂)), ‖f z - f z‖ ≤ R₂ * (‖z - z‖ / R₁) ^ (n + 1)
inr : ∀ (hne : z ≠ c), ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
rcases eq_or_ne z c with rfl | hne

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
z : ℂ
R₂ : ℝ
n : ℕ
R₁ : ℝ
hR₁ : 0 < R₁
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 z) (fun (x : ℂ) ↦ f x - f z) fun (w : ℂ) ↦ (w - z) ^ n
hz : z ∈ ball z R₁
hd : DifferentiableOn ℂ f (closedBall z R₁)
h_maps : MapsTo f (closedBall z R₁) (closedBall (f z) R₂)
⊢ ‖f z - f z‖ ≤ R₂ * (‖z - z‖ / R₁) ^ (n + 1)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
⊢ DifferentiableOn ℂ g' (closedBall c R₁)

Tactic:
.mono ?_ (subset_insert_diff_singleton c _)

Premises used: Set.subset_insert_diff_singleton, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
refine : DifferentiableOn ℂ g' (insert c (closedBall c R₁ \ {c}))
⊢ DifferentiableOn ℂ g' (closedBall c R₁)

Tactic:
refine .mono ?_ (subset_insert_diff_singleton c _)
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
hc : closedBall c R₁ \ {c} ∈ 𝓝[≠] c
hd₁ : DifferentiableOn ℂ g (closedBall c R₁ \ {c})
ho : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ g z - g c) fun (z : ℂ) ↦ (z - c)⁻¹
⊢ DifferentiableOn ℂ g' (insert c (closedBall c R₁ \ {c}))

Tactic:
apply differentiableOn_update_limUnder_insert_of_isLittleO

Premises used: Complex.differentiableOn_update_limUnder_insert_of_isLittleO
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
⊢ closedBall c R₁ \ {c} ∈ 𝓝[≠] c

Tactic:
diff_mem_nhdsWithin_compl (closedBall_mem_nhds _ hR₁) _

Premises used: Metric.closedBall_mem_nhds, diff_mem_nhdsWithin_compl
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
⊢ closedBall c R₁ \ {c} ∈ 𝓝[≠] c

Tactic:
exact diff_mem_nhdsWithin_compl (closedBall_mem_nhds _ hR₁) _

Premises used: Metric.closedBall_mem_nhds, diff_mem_nhdsWithin_compl
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
⊢ DifferentiableOn ℂ g (closedBall c R₁ \ {c})

Tactic:
.mul ?_ (hd.mono diff_subset |>.sub_const _)

Premises used: Set.diff_subset, DifferentiableOn.sub_const, DifferentiableOn.mul, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
hd₁ : DifferentiableOn ℂ (F := ℂ) (fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹) (closedBall c R₁ \ {c})
⊢ DifferentiableOn ℂ g (closedBall c R₁ \ {c})

Tactic:
refine .mul ?_ (hd.mono diff_subset |>.sub_const _)
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
⊢ ∀ x ∈ closedBall c R₁ \ {c}, (x - c) ^ (n + 1) ≠ 0

Tactic:
simp +contextual [sub_eq_zero]

Premises used: sub_eq_zero