-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivAtFilter_iff_tendsto :
    HasFDerivAtFilter f f' x L ↔
      Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)

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
L : Filter E
x' : E
hx' : ‖x' - x‖ = 0
⊢ ‖f x' - f x - f' (x' - x)‖ = 0

Tactic:
rw [sub_eq_zero.1 (norm_eq_zero.1 hx')]

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
L : Filter E
x' : E
hx' : ‖x' - x‖ = 0
⊢ ‖f x - f x - f' (x - x)‖ = 0

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
L : Filter E
h : ∀ (x' : E), ‖x' - x‖ = 0 → ‖f x' - f x - f' (x' - x)‖ = 0
⊢ HasFDerivAtFilter f f' x L ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)

Tactic:
rw [hasFDerivAtFilter_iff_isLittleO, ← isLittleO_norm_left, ← isLittleO_norm_right,
  isLittleO_iff_tendsto h]

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
L : Filter E
h : ∀ (x' : E), ‖x' - x‖ = 0 → ‖f x' - f x - f' (x' - x)‖ = 0
⊢ Tendsto (fun x_1 => ‖f x_1 - f x - f' (x_1 - x)‖ / ‖x_1 - x‖) L (𝓝 0) ↔
    Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)

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
L : Filter E
h : ∀ (x' : E), ‖x' - x‖ = 0 → ‖f x' - f x - f' (x' - x)‖ = 0
⊢ Tendsto (fun x_1 => ‖f x_1 - f x - f' (x_1 - x)‖ / ‖x_1 - x‖) L (𝓝 0) ↔
    Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)

Tactic:
exact tendsto_congr fun _ => div_eq_inv_mul _ _

Result:
no goals

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
L : Filter E
⊢ HasFDerivAtFilter f f' x L ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)

Tactic:
have h : ∀ x', ‖x' - x‖ = 0 → ‖f x' - f x - f' (x' - x)‖ = 0 := fun x' hx' => by
  rw [sub_eq_zero.1 (norm_eq_zero.1 hx')]
  simp

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
L : Filter E
h : ∀ (x' : E), ‖x' - x‖ = 0 → ‖f x' - f x - f' (x' - x)‖ = 0
⊢ HasFDerivAtFilter f f' x L ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)

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
L : Filter E
x' : E
hx' : ‖x' - x‖ = 0
⊢ ‖f x - f x - f' (x - x)‖ = 0

Tactic:
simp

Result:
no goals