awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
funProp : ∀ x ∈ closedBall c R₁ \ {c}, (x - c) ^ (n + 1) ≠ 0
⊢ DifferentiableOn ℂ (F := ℂ) (fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹) (closedBall c R₁ \ {c})

Tactic:
fun_prop (disch := simp +contextual [sub_eq_zero])

Premises used: sub_eq_zero
-- 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)
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ g z - g c) fun (z : ℂ) ↦ (z - c)⁻¹

Tactic:
Asymptotics.isBigO_refl (fun w ↦ ((w - c) ^ (n + 1))⁻¹) _ |>.mul_isLittleO hn
        |>.mono (nhdsWithin_le_nhds (s := {c}ᶜ)) |>.congr' ?_ ?_

Premises used: HSub.hSub, Asymptotics.IsLittleO.congr', Asymptotics.IsBigO.mul_isLittleO, nhdsWithin_le_nhds, Inv.inv, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Asymptotics.IsLittleO.mono, Asymptotics.isBigO_refl
-- 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)
ho : (𝓝[≠] c).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (f x - f c)) fun (z : ℂ) ↦ g z - g c
ho₁ : (𝓝[≠] c).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) fun (z : ℂ) ↦ (z - c)⁻¹
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ g z - g c) 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' ?_ ?_

Premises used: HSub.hSub, Asymptotics.IsLittleO.congr', Asymptotics.IsBigO.mul_isLittleO, nhdsWithin_le_nhds, Inv.inv, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Asymptotics.IsLittleO.mono, Asymptotics.isBigO_refl
-- 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)
⊢ (𝓝[≠] c).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (f x - f c)) fun (z : ℂ) ↦ g z - g c

Tactic:
simp [g]
-- 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)
⊢ (𝓝[≠] c).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) fun (z : ℂ) ↦ (z - c)⁻¹

Tactic:
eventually_mem_nhdsWithin.mono fun w hw ↦ ?_

Premises used: eventually_mem_nhdsWithin, Filter.EventuallyEq, Filter.Eventually.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)
ho :
  ∀ (w : ℂ) (hw : Membership.mem (γ := Set ℂ) {c}ᶜ w),
    Eq (α := ℂ) ((fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) w) ((fun (z : ℂ) ↦ (z - c)⁻¹) w)
⊢ (𝓝[≠] c).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) fun (z : ℂ) ↦ (z - c)⁻¹

Tactic:
refine eventually_mem_nhdsWithin.mono fun w hw ↦ ?_

Premises used: eventually_mem_nhdsWithin, Filter.Eventually.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)
w : ℂ
hw : Membership.mem (γ := Set ℂ) {c}ᶜ w
⊢ w - c ≠ 0

Tactic:
rw [mem_compl_singleton_iff, ← sub_ne_zero] at hw

Premises used: sub_ne_zero, Set.mem_compl_singleton_iff
-- 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)
w : ℂ
hw : w - c ≠ 0
⊢ Eq (α := ℂ) ((fun (x : ℂ) ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) w) ((fun (z : ℂ) ↦ (z - c)⁻¹) w)

Tactic:
simp [pow_succ, field]

Premises used: pow_succ
-- 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:
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]
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
this : ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
⊢ ‖z - c‖ ≠ 0

Tactic:
simpa [sub_eq_zero] using hne

Premises used: sub_eq_zero
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
this : ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
⊢ ‖z - c‖ ≠ 0

Tactic:
have hz' : ‖z - c‖ ≠ 0 := by simpa [sub_eq_zero] using hne
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
this : ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
hz' : ‖z - c‖ ≠ 0
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
simpa [g', hne, g, div_pow, mul_comm, field] using this

Premises used: div_pow, mul_comm
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
inr : ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / 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
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)

Tactic:
norm_le_of_forall_mem_frontier_norm_le isBounded_ball (hdg'.diffContOnCl_ball subset_rfl)
    ?_ ?_

Premises used: Metric.isBounded_ball, DifferentiableOn.diffContOnCl_ball, Complex.norm_le_of_forall_mem_frontier_norm_le, subset_rfl
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
inr : ∀ z ∈ frontier (ball c R₁), ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
inr₁ : z ∈ closure (ball c R₁)
⊢ ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)

Tactic:
refine norm_le_of_forall_mem_frontier_norm_le isBounded_ball (hdg'.diffContOnCl_ball subset_rfl)
    ?_ ?_

Premises used: Metric.isBounded_ball, DifferentiableOn.diffContOnCl_ball, Complex.norm_le_of_forall_mem_frontier_norm_le, subset_rfl
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
inr : ∀ z ∈ sphere c R₁, ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
⊢ ∀ z ∈ frontier (ball c R₁), ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)

Tactic:
grw [frontier_ball_subset_sphere]

Premises used: Metric.frontier_ball_subset_sphere
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
w : ℂ
hw : w ∈ sphere c R₁
⊢ w ≠ c

Tactic:
have hwc := ne_of_mem_sphere hw hR₁.ne'
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
w : ℂ
hw : w ∈ sphere c R₁
hwc : w ≠ c
⊢ ‖f w - f c‖ ≤ R₂

Tactic:
simpa [dist_eq_norm] using h_maps (sphere_subset_closedBall hw)

Premises used: dist_eq_norm, Metric.sphere_subset_closedBall
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
w : ℂ
hw : w ∈ sphere c R₁
hwc : w ≠ c
⊢ ‖f w - f c‖ ≤ R₂

Tactic:
have hfw : ‖f w - f c‖ ≤ R₂ := by
      simpa [dist_eq_norm] using h_maps (sphere_subset_closedBall hw)
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
w : ℂ
hw : w ∈ sphere c R₁
hwc : w ≠ c
hfw : ‖f w - f c‖ ≤ R₂
⊢ ‖w - c‖ = R₁

Tactic:
rw [mem_sphere_iff_norm] at hw

Premises used: mem_sphere_iff_norm
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
w : ℂ
hw : w ∈ sphere c R₁
hwc : w ≠ c
hfw : ‖f w - f c‖ ≤ R₂
hw₁ : ‖w - c‖ = R₁
⊢ w ≠ c

Tactic:
rw [mem_sphere_iff_norm] at hw

Premises used: mem_sphere_iff_norm
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
w : ℂ
hw : w ∈ sphere c R₁
hwc : w ≠ c
hfw : ‖f w - f c‖ ≤ R₂
hw₁ : ‖w - c‖ = R₁
hwc₁ : w ≠ c
⊢ ‖f w - f c‖ ≤ R₂

Tactic:
rw [mem_sphere_iff_norm] at hw

Premises used: mem_sphere_iff_norm
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
w : ℂ
hw : ‖w - c‖ = R₁
hwc : w ≠ c
hfw : ‖f w - f c‖ ≤ R₂
⊢ ‖g' w‖ ≤ R₂ / R₁ ^ (n + 1)

Tactic:
simpa [g', hwc, g, hw, field]
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ z ∈ closure (ball c R₁)

Tactic:
subset_closure hz

Premises used: subset_closure
-- 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)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ z ∈ closure (ball c R₁)

Tactic:
exact subset_closure hz

Premises used: subset_closure
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
⊢ 0 < R₁

Tactic:
have hR₁ : 0 < R₁ := nonempty_ball.mp ⟨_, hz⟩
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ 0 ≤ R₂

Tactic:
have hR₂ : 0 ≤ R₂ := nonempty_closedBall.mp ⟨_, h_maps hz⟩
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
inl : ∀ (heq : f z = f c), dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
inr : ∀ (hfne : f z ≠ f c), dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
rcases eq_or_ne (f z) (f c) with heq | hfne

Premises used: eq_or_ne
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
heq : f z = f c
trans : dist (f z) (f c) ≤ 0
trans₁ : 0 ≤ R₂ * (dist z c / R₁) ^ (n + 1)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
trans 0
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
heq : f z = f c
⊢ dist (f z) (f c) ≤ 0

Tactic:
simp [heq]
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
heq : f z = f c
⊢ 0 ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
heq : f z = f c
trans : dist (f z) (f c) ≤ 0
trans₁ : 0 ≤ R₂ * (dist z c / R₁) ^ (n + 1)
trans₂ : dist (f z) (f c) ≤ 0
trans₃ : 0 ≤ R₂ * (dist z c / R₁) ^ (n + 1)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
trans 0 <;> [simp [heq]; positivity]
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
⊢ z ≠ c

Tactic:
have hne : z ≠ c := ne_of_apply_ne _ hfne
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
inr :
  ∀ (g : StrongDual ℂ F) (hg : ‖g‖ = 1)
    (hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)),
    dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
rcases exists_dual_vector ℂ _ (norm_sub_eq_zero_iff.not.mpr hfne) with ⟨g, hg, hgf⟩

Premises used: Iff.mpr, norm_sub_eq_zero_iff, Iff.not, exists_dual_vector, Complex