awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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)
⊢ Tendsto (fun (c_1 : ℝ) ↦ R₂ * (‖z - c‖ / c_1) ^ (n + 1)) (𝓝[<] R₁) (𝓝 (R₂ * (‖z - c‖ / R₁) ^ (n + 1)))
have refine : ContinuousAt (Y := ℝ) (fun (c_1 : ℝ) ↦ R₂ * (‖z - c‖ / c_1) ^ (n + 1)) R₁
Tactic: refine ContinuousAt.continuousWithinAt ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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)
⊢ ContinuousAt (Y := ℝ) (fun (c_1 : ℝ) ↦ R₂ * (‖z - c‖ / c_1) ^ (n + 1)) R₁
have funProp : R₁ ≠ 0
Tactic: fun_prop (disch := positivity)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₂))
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
have inr : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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₂))
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
have hz₁ : ‖z - c‖ < R₁
Tactic: rw [mem_ball_iff_norm] at hz
Cleared hypotheses: hz, hR₁, this, hd'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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 : ℝ
⊢ r ∈ Ioo ‖z - c‖ R₁ → ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
have h : ∀ (hzr : ‖z - c‖ < r) (hrR₁ : r < R₁), ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
Tactic: ⟨hzr, hrR₁⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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 : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
have h : ∀ (r : ℝ) (hzr : ‖z - c‖ < r) (hrR₁ : r < R₁), ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
Tactic: filter_upwards [Ioo_mem_nhdsLT hz] with r ⟨hzr, hrR₁⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₁
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
have h : DifferentiableOn ℂ f (ball c r)
Tactic: apply this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
have h₁ : MapsTo f (ball c r) (closedBall (f c) R₂)
Tactic: apply this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₂)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
have h₂ : z ∈ ball c r
Tactic: apply this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
have h₃ : 0 < r
Tactic: apply this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
have h₄ : DifferentiableOn ℂ f (closedBall c r) ∧ MapsTo f (closedBall c r) (closedBall (f c) R₂)
Tactic: apply this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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₂)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
have hd : DifferentiableOn ℂ f (closedBall c R₁)
Tactic: rcases hd' with ⟨hd, h_maps⟩
Cleared hypotheses: hd'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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₁)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
have h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
Tactic: rcases hd' with ⟨hd, h_maps⟩
Cleared hypotheses: hd'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₂)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
have 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)
Tactic: rcases eq_or_ne z c with rfl | hne
Cleared hypotheses: c, hn, hz, hd, h_maps
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
have inr : ∀ (hne : z ≠ c), ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
Tactic: rcases eq_or_ne z c with rfl | hne
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₁)
have refine : DifferentiableOn ℂ g' (insert c (closedBall c R₁ \ {c}))
Tactic: refine .mono ?_ (subset_insert_diff_singleton c _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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' (insert c (closedBall c R₁ \ {c}))
have hc : closedBall c R₁ \ {c} ∈ 𝓝[≠] c
Tactic: apply differentiableOn_update_limUnder_insert_of_isLittleO
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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
⊢ DifferentiableOn ℂ g' (insert c (closedBall c R₁ \ {c}))
have hd₁ : DifferentiableOn ℂ g (closedBall c R₁ \ {c})
Tactic: apply differentiableOn_update_limUnder_insert_of_isLittleO
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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})
⊢ DifferentiableOn ℂ g' (insert c (closedBall c R₁ \ {c}))
have ho : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ g z - g c) fun (z : ℂ) ↦ (z - c)⁻¹
Tactic: apply differentiableOn_update_limUnder_insert_of_isLittleO
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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})
have hd₁ : DifferentiableOn ℂ (F := ℂ) (fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹) (closedBall c R₁ \ {c})
Tactic: refine .mul ?_ (hd.mono diff_subset |>.sub_const _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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 ℂ (F := ℂ) (fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹) (closedBall c R₁ \ {c})
have funProp : ∀ x ∈ closedBall c R₁ \ {c}, (x - c) ^ (n + 1) ≠ 0
Tactic: fun_prop (disch := simp +contextual [sub_eq_zero])
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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)
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ g z - g c) fun (z : ℂ) ↦ (z - c)⁻¹
have ho : (𝓝[≠] c).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (f x - f c)) fun (z : ℂ) ↦ g z - g c
Tactic: refine Asymptotics.isBigO_refl (fun w ↦ ((w - c) ^ (n + 1))⁻¹) _ |>.mul_isLittleO hn
        |>.mono (nhdsWithin_le_nhds (s := {c}ᶜ)) |>.congr' ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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)
ho : (𝓝[≠] c).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (f x - f c)) fun (z : ℂ) ↦ g z - g c
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ g z - g c) fun (z : ℂ) ↦ (z - c)⁻¹
have ho₁ : (𝓝[≠] c).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) fun (z : ℂ) ↦ (z - c)⁻¹
Tactic: refine Asymptotics.isBigO_refl (fun w ↦ ((w - c) ^ (n + 1))⁻¹) _ |>.mul_isLittleO hn
        |>.mono (nhdsWithin_le_nhds (s := {c}ᶜ)) |>.congr' ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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)
⊢ (𝓝[≠] c).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) fun (z : ℂ) ↦ (z - c)⁻¹
have ho : ∀ (w : ℂ) (hw : Membership.mem (γ := Set ℂ) {c}ᶜ w),
  Eq (α := ℂ) ((fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) w) ((fun (z : ℂ) ↦ (z - c)⁻¹) w)
Tactic: refine eventually_mem_nhdsWithin.mono fun w hw ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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)
w : ℂ
hw : Membership.mem (γ := Set ℂ) {c}ᶜ w
⊢ Eq (α := ℂ) ((fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) w) ((fun (z : ℂ) ↦ (z - c)⁻¹) w)
have hw₁ : w - c ≠ 0
Tactic: rw [mem_compl_singleton_iff, ← sub_ne_zero] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
have hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
Tactic: have hdg' : DifferentiableOn ℂ g' (closedBall c R₁) := by
    refine .mono ?_ (subset_insert_diff_singleton c _)
    apply differentiableOn_update_limUnder_insert_of_isLittleO
    · exact diff_mem_nhdsWithin_compl (closedBall_mem_nhds _ hR₁) _
    · refine .mul ?_ (hd.mono diff_subset |>.sub_const _)
      fun_prop (disch := simp +contextual [sub_eq_zero])
    · refine Asymptotics.isBigO_refl (fun w ↦ ((w - c) ^ (n + 1))⁻¹) _ |>.mul_isLittleO hn
        |>.mono (nhdsWithin_le_nhds (s := {c}ᶜ)) |>.congr' ?_ ?_
      · simp [g]
      · refine eventually_mem_nhdsWithin.mono fun w hw ↦ ?_
        rw [mem_compl_singleton_iff, ← sub_ne_zero] at hw
        simp [pow_succ, field]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
this : ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
have hz' : ‖z - c‖ ≠ 0
Tactic: have hz' : ‖z - c‖ ≠ 0 := by simpa [sub_eq_zero] using hne
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
have inr : ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
Tactic: suffices ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1) by
    have hz' : ‖z - c‖ ≠ 0 := by simpa [sub_eq_zero] using hne
    simpa [g', hne, g, div_pow, mul_comm, field] using this