-- Mathlib/Analysis/Complex/RemovableSingularity.lean
theorem differentiableOn_update_limUnder_of_isLittleO {f : ℂ → E} {s : Set ℂ} {c : ℂ} (hc : s ∈ 𝓝 c)
    (hd : DifferentiableOn ℂ f (s \ {c}))
    (ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹) :
    DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) s

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc✝ : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this : DifferentiableOn ℂ (update f c (deriv (fun x => (x - c) • f x) c)) s
hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c))
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) s

Tactic:
rwa [hc.limUnder_eq]

Result:
no goals

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this : DifferentiableOn ℂ (update f c (deriv (fun x => (x - c) • f x) c)) s
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) s

Tactic:
have hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c)) :=
  continuousAt_update_same.mp (this.continuousOn.continuousAt hc)

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc✝ : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this : DifferentiableOn ℂ (update f c (deriv (fun x => (x - c) • f x) c)) s
hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c))
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) s

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ ContinuousWithinAt F {c}ᶜ c

Tactic:
have H := ho.tendsto_inv_smul_nhds_zero

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
H : Tendsto (fun x => (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[≠] c) (𝓝 0)
⊢ ContinuousWithinAt F {c}ᶜ c

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
H : Tendsto (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'

Result:
no goals

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) 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]

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) s

Tactic:
set F : ℂ → E := fun z => (z - c) • f z

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) s

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
H : Tendsto (fun x => (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[≠] c) (𝓝 0)
⊢ ContinuousWithinAt F {c}ᶜ 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

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
H : Tendsto (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

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c

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

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ ContinuousAt F c

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ ContinuousAt F c

Tactic:
rw [← continuousWithinAt_compl_self]

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ ContinuousWithinAt F {c}ᶜ c

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this : DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) s

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

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this : DifferentiableOn ℂ (update f c (deriv (fun x => (x - c) • f x) c)) s
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) s