Theorem: Tutorial.hasDerivAt_iff_tendsto (Solution/Advanced/Analysis/Lecture1.lean)

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝[≠] a) (𝓝 0)
Tactic:
calc HasDerivAt f f' a
  _ ↔ Tendsto (fun x ↦ (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0)      := ?iff1
  _ ↔ Tendsto (fun x ↦ (f x - f a - (x - a) * f') / (x - a)) (𝓝[≠] a) (𝓝 0)   := ?iff2
State after:
case iff1
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0)

case iff2
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝[≠] a) (𝓝 0)

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0)
Tactic:
case iff1 => rw [hasDerivAt_iff_isLittleO, Asymptotics.isLittleO_iff_tendsto (by intro _ h; simp [sub_eq_zero.1 h])]
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝[≠] a) (𝓝 0)
Tactic:
case iff2 => exact .symm <| tendsto_inf_principal_nhds_iff_of_forall_eq <| by simp
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0)
Tactic:
rw [hasDerivAt_iff_isLittleO, Asymptotics.isLittleO_iff_tendsto (by intro _ h; simp [sub_eq_zero.1 h])]
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ ∀ (x : ℝ), x - a = 0 → f x - f a - (x - a) * f' = 0
Tactic:
intro _ h
State after:
f : ℝ → ℝ
f' a x✝ : ℝ
h : x✝ - a = 0
⊢ f x✝ - f a - (x✝ - a) * f' = 0

State before:
f : ℝ → ℝ
f' a x✝ : ℝ
h : x✝ - a = 0
⊢ f x✝ - f a - (x✝ - a) * f' = 0
Tactic:
simp [sub_eq_zero.1 h]
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝[≠] a) (𝓝 0)
Tactic:
exact .symm <| tendsto_inf_principal_nhds_iff_of_forall_eq <| by simp
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ ∀ a_1 ∉ {a}ᶜ, (f a_1 - f a - (a_1 - a) * f') / (a_1 - a) = 0
Tactic:
simp
State after:
no goals