awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] x, DifferentiableAt ℂ f z

Tactic:
eventually_nhdsWithin_iff.2 ((eventually_mem_nhds_iff.2 hs).mono fun z hz hzx => ?_)

Premises used: Iff.mpr, eventually_mem_nhds_iff, Filter.Eventually.mono, eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
inl : ∀ (z : ℂ) (hz : s ∈ 𝓝 z) (hzx : Membership.mem (γ := Set ℂ) {x}ᶜ z), DifferentiableAt ℂ f z
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] x, DifferentiableAt ℂ f z

Tactic:
refine eventually_nhdsWithin_iff.2 ((eventually_mem_nhds_iff.2 hs).mono fun z hz hzx => ?_)

Premises used: Iff.mpr, eventually_mem_nhds_iff, Filter.Eventually.mono, eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
z : ℂ
hz : s ∈ 𝓝 z
hzx : Membership.mem (γ := Set ℂ) {x}ᶜ z
⊢ DifferentiableAt ℂ f z

Tactic:
hd.differentiableAt (inter_mem hz (isOpen_ne.mem_nhds hzx))

Premises used: Filter.inter_mem, DifferentiableOn.differentiableAt, isOpen_ne, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
z : ℂ
hz : s ∈ 𝓝 z
hzx : Membership.mem (γ := Set ℂ) {x}ᶜ z
⊢ DifferentiableAt ℂ f z

Tactic:
exact hd.differentiableAt (inter_mem hz (isOpen_ne.mem_nhds hzx))

Premises used: Filter.inter_mem, DifferentiableOn.differentiableAt, isOpen_ne, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
hc : ContinuousAt f c
x : ℂ
hx : x ∈ s
hne : x ≠ c
⊢ DifferentiableWithinAt ℂ f s x

Tactic:
simpa only [DifferentiableWithinAt, HasFDerivWithinAt, hne.nhdsWithin_diff_singleton] using
      hd x ⟨hx, hne⟩

Premises used: HasFDerivWithinAt, Ne.nhdsWithin_diff_singleton, And.intro, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
⊢ DifferentiableOn ℂ (dslope f c) s ↔ DifferentiableOn ℂ f s

Tactic:
⟨fun h => h.of_dslope, fun h =>
    (differentiableOn_compl_singleton_and_continuousAt_iff hc).mp <|
      ⟨Iff.mpr (differentiableOn_dslope_of_notMem fun h => h.2 rfl) (h.mono diff_subset),
        continuousAt_dslope_same.2 <| h.differentiableAt hc⟩⟩

Premises used: Iff.mpr, Set.diff_subset, differentiableOn_dslope_of_notMem, continuousAt_dslope_same, DifferentiableOn.differentiableAt, Complex.differentiableOn_compl_singleton_and_continuousAt_iff, And.right, And.intro, Iff.intro, Iff.mp, DifferentiableOn.mono, rfl, DifferentiableOn.of_dslope
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
this : DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c
⊢ DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c (deriv (fun (x : ℂ) ↦ (x - c) • f x) c)) s

Tactic:
rw [differentiableOn_compl_singleton_and_continuousAt_iff hc, ← differentiableOn_dslope hc,
      dslope_sub_smul] at this

Premises used: Complex.differentiableOn_dslope, dslope_sub_smul, Complex.differentiableOn_compl_singleton_and_continuousAt_iff
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
this : DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c (deriv (fun (x : ℂ) ↦ (x - c) • f x) c)) s
⊢ Tendsto f (𝓝[≠] c) (𝓝 (deriv F c))

Tactic:
have hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c)) :=
      continuousAt_update_same.mp (this.continuousOn.continuousAt hc)
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc_1 : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
this : DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c (deriv (fun (x : ℂ) ↦ (x - c) • f x) c)) s
hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c))
rwa rwa₁ rwa₂ rwa₃ : DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c (deriv F c)) s
⊢ DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c ((𝓝[≠] c).limUnder f)) s

Tactic:
rwa [hc.limUnder_eq]

Premises used: Filter.Tendsto.limUnder_eq
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
suffices : DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c
⊢ DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c ((𝓝[≠] c).limUnder f)) s

Tactic:
suffices DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c by
    rw [differentiableOn_compl_singleton_and_continuousAt_iff hc, ← differentiableOn_dslope hc,
      dslope_sub_smul] at this
    have hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c)) :=
      continuousAt_update_same.mp (this.continuousOn.continuousAt hc)
    rwa [hc.limUnder_eq]
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
⊢ DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c

Tactic:
⟨(differentiableOn_id.sub_const _).smul hd, ?_⟩

Premises used: DifferentiableOn.smul, And.intro
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
refine : ContinuousAt F c
⊢ DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c

Tactic:
refine ⟨(differentiableOn_id.sub_const _).smul hd, ?_⟩
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
rw : ContinuousWithinAt F {c}ᶜ c
⊢ ContinuousAt F c

Tactic:
rw [← continuousWithinAt_compl_self]

Premises used: continuousWithinAt_compl_self
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
⊢ Tendsto.{0, u} (β := E) (fun (x : ℂ) ↦ (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[≠] c) (𝓝 0)

Tactic:
have H := ho.tendsto_inv_smul_nhds_zero
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
H : Tendsto.{0, u} (β := E) (fun (x : ℂ) ↦ (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[≠] c) (𝓝 0)
⊢ Tendsto (fun (z : ℂ) ↦ (z - c) • f c) (𝓝[≠] c) (𝓝 (F c))

Tactic:
have H' : Tendsto (fun z => (z - c) • f c) (𝓝[≠] c) (𝓝 (F c)) :=
    (continuousWithinAt_id.tendsto.sub tendsto_const_nhds).smul tendsto_const_nhds
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
H : Tendsto.{0, u} (β := E) (fun (x : ℂ) ↦ (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[≠] c) (𝓝 0)
H' : Tendsto (fun (z : ℂ) ↦ (z - c) • f c) (𝓝[≠] c) (𝓝 (F c))
⊢ ContinuousWithinAt F {c}ᶜ c

Tactic:
simpa [← smul_add, ContinuousWithinAt] using H.add H'

Premises used: ContinuousWithinAt, Filter.Tendsto.add, smul_add
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝[≠] c
hd : DifferentiableOn ℂ f s
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
⊢ DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c ((𝓝[≠] c).limUnder f)) (insert c s)

Tactic:
differentiableOn_update_limUnder_of_isLittleO (insert_mem_nhds_iff.2 hc)
    (hd.mono fun _ hz => hz.1.resolve_left hz.2) ho

Premises used: Iff.mpr, Complex.differentiableOn_update_limUnder_of_isLittleO, Or.resolve_left, And.right, And.left, DifferentiableOn.mono, insert_mem_nhds_iff
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
hb : BddAbove (norm ∘ f '' (s \ {c}))
⊢ DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c ((𝓝[≠] c).limUnder f)) s

Tactic:
differentiableOn_update_limUnder_of_isLittleO hc hd <| IsBoundedUnder.isLittleO_sub_self_inv <|
    let ⟨C, hC⟩ := hb
    ⟨C + ‖f c‖, eventually_map.2 <| mem_nhdsWithin_iff_exists_mem_nhds_inter.2
      ⟨s, hc, fun _ hz => norm_sub_le_of_le (hC <| mem_image_of_mem _ hz) le_rfl⟩⟩

Premises used: Iff.mpr, Norm.norm, le_rfl, Compl.compl, nhdsWithin, Complex.differentiableOn_update_limUnder_of_isLittleO, HSub.hSub, Function.comp, LE.le, Filter.eventually_map, norm_sub_le_of_le, HAdd.hAdd, Set.mem_image_of_mem, And.intro, Exists.intro, _private.0.Complex.differentiableOn_update_limUnder_of_bddAbove.match_1, Singleton.singleton, Filter.IsBoundedUnder, mem_nhdsWithin_iff_exists_mem_nhds_inter, Filter.IsBoundedUnder.isLittleO_sub_self_inv
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x

Tactic:
rw [eventually_nhdsWithin_iff] at hd

Premises used: eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
hd₁ : ∀ᶠ (x : ℂ) in 𝓝 c, Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x
⊢ IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹

Tactic:
rw [eventually_nhdsWithin_iff] at hd

Premises used: eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
⊢ DifferentiableOn ℂ f ({z : ℂ | z ≠ c → DifferentiableAt ℂ f z} \ {c})

Tactic:
have : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c}) := fun z hz =>
    (hz.1 hz.2).differentiableWithinAt
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
this : DifferentiableOn ℂ f ({z : ℂ | z ≠ c → DifferentiableAt ℂ f z} \ {c})
⊢ DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c ((𝓝[≠] c).limUnder f))
    {x : ℂ | (fun (x : ℂ) ↦ Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x) x}

Tactic:
have H := differentiableOn_update_limUnder_of_isLittleO hd this ho
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
this : DifferentiableOn ℂ f ({z : ℂ | z ≠ c → DifferentiableAt ℂ f z} \ {c})
H :
  DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c ((𝓝[≠] c).limUnder f))
    {x : ℂ | (fun (x : ℂ) ↦ Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x) x}
⊢ Tendsto f (𝓝[≠] c) (𝓝 ((𝓝[≠] c).limUnder f))

Tactic:
continuousAt_update_same.1 (H.differentiableAt hd).continuousAt

Premises used: DifferentiableAt.continuousAt, DifferentiableOn.differentiableAt, Iff.mp, continuousAt_update_same
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
this : DifferentiableOn ℂ f ({z : ℂ | z ≠ c → DifferentiableAt ℂ f z} \ {c})
H :
  DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c ((𝓝[≠] c).limUnder f))
    {x : ℂ | (fun (x : ℂ) ↦ Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x) x}
⊢ Tendsto f (𝓝[≠] c) (𝓝 ((𝓝[≠] c).limUnder f))

Tactic:
exact continuousAt_update_same.1 (H.differentiableAt hd).continuousAt

Premises used: DifferentiableAt.continuousAt, DifferentiableOn.differentiableAt, Iff.mp, continuousAt_update_same
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hb : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[≠] c) fun (z : ℂ) ↦ ‖f z - f c‖
⊢ Tendsto f (𝓝[≠] c) (𝓝 ((𝓝[≠] c).limUnder f))

Tactic:
tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO hd hb.isLittleO_sub_self_inv

Premises used: Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO, Filter.IsBoundedUnder.isLittleO_sub_self_inv
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
⊢ DifferentiableOn ℂ (dslope f w₀) U

Tactic:
have hf' : DifferentiableOn ℂ (dslope f w₀) U :=
    (differentiableOn_dslope (hU.mem_nhds ((ball_subset_closedBall.trans hc) hw₀))).mpr hf
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀

Tactic:
have h0 := (hf'.diffContOnCl_ball hc).two_pi_i_inv_smul_circleIntegral_sub_inv_smul hw₀
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
rw :
  HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) =
    HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z)
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) = deriv f w₀

Tactic:
rw [← dslope_same, ← h0]

Premises used: dslope_same
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
e_a :
  Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z)
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) =
    HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
trans :
  Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀))
trans₁ :
  Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀))
    (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z)
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z)

Tactic:
trans ∮ z in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) (sphere c R)

Tactic:
((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => ?_

Premises used: Continuous.continuousOn, continuous_const, continuous_id', Continuous.pow, ContinuousOn.inv₀, OfNat.ofNat, Continuous.sub
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
refine : ∀ (w : ℂ) (hw : w ∈ sphere c R) (h : HPow.hPow (β := ℕ) (w - w₀) 2 = 0), False
⊢ ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) (sphere c R)

Tactic:
refine ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => ?_

Premises used: Continuous.continuousOn, continuous_const, continuous_id', Continuous.pow, ContinuousOn.inv₀, OfNat.ofNat, Continuous.sub
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
w : ℂ
hw : w ∈ sphere c R
h : HPow.hPow (β := ℕ) (w - w₀) 2 = 0
⊢ False

Tactic:
sphere_disjoint_ball.ne_of_mem hw hw₀ (sub_eq_zero.mp (sq_eq_zero_iff.mp h))

Premises used: sub_eq_zero, Iff.mp, Metric.sphere_disjoint_ball, Disjoint.ne_of_mem, sq_eq_zero_iff
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
w : ℂ
hw : w ∈ sphere c R
h : HPow.hPow (β := ℕ) (w - w₀) 2 = 0
⊢ False

Tactic:
exact sphere_disjoint_ball.ne_of_mem hw hw₀ (sub_eq_zero.mp (sq_eq_zero_iff.mp h))

Premises used: sub_eq_zero, Iff.mp, Metric.sphere_disjoint_ball, Disjoint.ne_of_mem, sq_eq_zero_iff
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) (sphere c R)

Tactic:
have h1 : ContinuousOn (fun z : ℂ => ((z - w₀) ^ 2)⁻¹) (sphere c R) := by
      refine ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => ?_
      exact sphere_disjoint_ball.ne_of_mem hw hw₀ (sub_eq_zero.mp (sq_eq_zero_iff.mp h))
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) (sphere c R)
⊢ CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) c R

Tactic:
ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le ?_

Premises used: ContinuousOn.circleIntegrable, LT.lt.le, Metric.pos_of_mem_ball