Theorem: Tutorial.hasDerivAt_iff_tendsto_slope (Tutorial/Advanced/Analysis/Lecture1.lean)

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

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

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

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a) / (x - a) - (x - a) / (x - a) * f') (𝓝[≠] a) (𝓝 0)
Tactic:
case iff1 => simp only [hasDerivAt_iff_tendsto, sub_div, mul_div_right_comm]
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - (x - a) / (x - a) * f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0)
Tactic:
case iff2 => exact tendsto_congr' <| (Set.EqOn.eventuallyEq fun _ h ↦ (by field_simp [sub_ne_zero.2 h])).filter_mono inf_le_right
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
Tactic:
case iff3 => rw [← nhds_translation_sub f', tendsto_comap_iff]; rfl
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a) / (x - a) - (x - a) / (x - a) * f') (𝓝[≠] a) (𝓝 0)
Tactic:
simp only [hasDerivAt_iff_tendsto, sub_div, mul_div_right_comm]
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - (x - a) / (x - a) * f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0)
Tactic:
exact tendsto_congr' <| (Set.EqOn.eventuallyEq fun _ h ↦ (by field_simp [sub_ne_zero.2 h])).filter_mono inf_le_right
State after:
no goals

State before:
f : ℝ → ℝ
f' a x✝ : ℝ
h : x✝ ∈ {a}ᶜ
⊢ (f x✝ - f a) / (x✝ - a) - (x✝ - a) / (x✝ - a) * f' = (f x✝ - f a) / (x✝ - a) - f'
Tactic:
field_simp [sub_ne_zero.2 h]
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
Tactic:
rw [← nhds_translation_sub f', tendsto_comap_iff]
State after:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto ((fun x => x - f') ∘ fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 0)

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto ((fun x => x - f') ∘ fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 0)
Tactic:
rfl
State after:
no goals