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

State before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto f (𝓝 a) (𝓝 (f a))
Tactic:
have : Tendsto (fun x ↦ f x - f a + f a) (𝓝 a) (𝓝 (0 + f a)) := by
  apply Tendsto.add _ tendsto_const_nhds
  apply h.isBigO_sub.trans_tendsto
  rw [← sub_self a]
  apply tendsto_id.sub tendsto_const_nhds
State after:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
this : Tendsto (fun x => f x - f a + f a) (𝓝 a) (𝓝 (0 + f a))
⊢ Tendsto f (𝓝 a) (𝓝 (f a))

State before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
this : Tendsto (fun x => f x - f a + f a) (𝓝 a) (𝓝 (0 + f a))
⊢ Tendsto f (𝓝 a) (𝓝 (f a))
Tactic:
rw [zero_add] at this
State after:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
this : Tendsto (fun x => f x - f a + f a) (𝓝 a) (𝓝 (f a))
⊢ Tendsto f (𝓝 a) (𝓝 (f a))

State before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
this : Tendsto (fun x => f x - f a + f a) (𝓝 a) (𝓝 (f a))
⊢ Tendsto f (𝓝 a) (𝓝 (f a))
Tactic:
exact this.congr (by simp)
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => f x - f a + f a) (𝓝 a) (𝓝 (0 + f a))
Tactic:
apply Tendsto.add _ tendsto_const_nhds
State after:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => f x - f a) (𝓝 a) (𝓝 0)

State before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => f x - f a) (𝓝 a) (𝓝 0)
Tactic:
apply h.isBigO_sub.trans_tendsto
State after:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => x - a) (𝓝 a) (𝓝 0)

State before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => x - a) (𝓝 a) (𝓝 0)
Tactic:
rw [← sub_self a]
State after:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => x - a) (𝓝 a) (𝓝 (a - a))

State before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => x - a) (𝓝 a) (𝓝 (a - a))
Tactic:
apply tendsto_id.sub tendsto_const_nhds
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
this : Tendsto (fun x => f x - f a + f a) (𝓝 a) (𝓝 (f a))
⊢ ∀ (x : ℝ), f x - f a + f a = f x
Tactic:
simp
State after:
no goals