-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem HasFDerivWithinAt.eventually_ne (h : HasFDerivWithinAt f f' s x)
    (hf' : ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖) : ∀ᶠ z in 𝓝[s \ {x}] x, f z ≠ f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
⊢ ∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ≠ f x

Tactic:
rw [nhdsWithin, diff_eq, ← inf_principal, ← inf_assoc, eventually_inf_principal]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
⊢ ∀ᶠ (x_1 : E) in 𝓝 x ⊓ 𝓟 s, x_1 ∈ {x}ᶜ → f x_1 ≠ f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
A : (fun z => z - x) =O[𝓝[s] x] fun z => f' (z - x)
⊢ ∀ᶠ (x_1 : E) in 𝓝 x ⊓ 𝓟 s, x_1 ∈ {x}ᶜ → f x_1 ≠ f x

Tactic:
have : (fun z => f z - f x) ~[𝓝[s] x] fun z => f' (z - x) := h.isLittleO.trans_isBigO A

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
A : (fun z => z - x) =O[𝓝[s] x] fun z => f' (z - x)
this : (fun z => f z - f x) ~[𝓝[s] x] fun z => f' (z - x)
⊢ ∀ᶠ (x_1 : E) in 𝓝 x ⊓ 𝓟 s, x_1 ∈ {x}ᶜ → f x_1 ≠ f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
⊢ ∀ᶠ (x_1 : E) in 𝓝 x ⊓ 𝓟 s, x_1 ∈ {x}ᶜ → f x_1 ≠ f x

Tactic:
have A : (fun z => z - x) =O[𝓝[s] x] fun z => f' (z - x) :=
  isBigO_iff.2 <| hf'.imp fun C hC => Eventually.of_forall fun z => hC _

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
A : (fun z => z - x) =O[𝓝[s] x] fun z => f' (z - x)
⊢ ∀ᶠ (x_1 : E) in 𝓝 x ⊓ 𝓟 s, x_1 ∈ {x}ᶜ → f x_1 ≠ f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
A : (fun z => z - x) =O[𝓝[s] x] fun z => f' (z - x)
this : (fun z => f z - f x) ~[𝓝[s] x] fun z => f' (z - x)
⊢ ∀ᶠ (x_1 : E) in 𝓝 x ⊓ 𝓟 s, x_1 ∈ {x}ᶜ → f x_1 ≠ f x

Tactic:
simpa [not_imp_not, sub_eq_zero] using (A.trans this.isBigO_symm).eq_zero_imp

Result:
no goals