Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero (Solution/Advanced/Analysis/Lecture2.lean)

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ f' = 0
Tactic:
apply le_antisymm ?right ?left
State after:
case right
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ f' ≤ 0

case left
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ 0 ≤ f'

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ f' ≤ 0
Tactic:
have hf : Tendsto (fun x ↦ (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f') := by
  rw [hasDerivAt_iff_tendsto_slope] at hf
  apply hf.mono_left (nhds_right'_le_nhds_ne a)
State after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
⊢ f' ≤ 0

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
⊢ f' ≤ 0
Tactic:
suffices ∀ᶠ x in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0 from le_of_tendsto hf this
State after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0
Tactic:
have ha : ∀ᶠ x in 𝓝[>] a, a < x := eventually_nhdsWithin_of_forall fun x hx ↦ hx
State after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0
Tactic:
have h : ∀ᶠ x in 𝓝[>] a, f x ≤ f a := h.filter_mono nhdsWithin_le_nhds
State after:
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0

State before:
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0
Tactic:
filter_upwards [ha, h]
State after:
case h
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
⊢ ∀ (a_1 : ℝ), a < a_1 → f a_1 ≤ f a → (f a_1 - f a) / (a_1 - a) ≤ 0

State before:
case h
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
⊢ ∀ (a_1 : ℝ), a < a_1 → f a_1 ≤ f a → (f a_1 - f a) / (a_1 - a) ≤ 0
Tactic:
intro x ha h
State after:
case h
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
x : ℝ
ha : a < x
h : f x ≤ f a
⊢ (f x - f a) / (x - a) ≤ 0

State before:
case h
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
x : ℝ
ha : a < x
h : f x ≤ f a
⊢ (f x - f a) / (x - a) ≤ 0
Tactic:
apply div_nonpos_of_nonpos_of_nonneg
State after:
case h.ha
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
x : ℝ
ha : a < x
h : f x ≤ f a
⊢ f x - f a ≤ 0

case h.hb
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
x : ℝ
ha : a < x
h : f x ≤ f a
⊢ 0 ≤ x - a

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
Tactic:
rw [hasDerivAt_iff_tendsto_slope] at hf
State after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
⊢ Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
⊢ Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
Tactic:
apply hf.mono_left (nhds_right'_le_nhds_ne a)
State after:
no goals

State before:
case h.ha
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
x : ℝ
ha : a < x
h : f x ≤ f a
⊢ f x - f a ≤ 0
Tactic:
linarith only [h]
State after:
no goals

State before:
case h.hb
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
x : ℝ
ha : a < x
h : f x ≤ f a
⊢ 0 ≤ x - a
Tactic:
linarith only [ha]
State after:
no goals

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ 0 ≤ f'
Tactic:
have hf : Tendsto (fun x ↦ (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f') := by
  rw [hasDerivAt_iff_tendsto_slope] at hf
  apply hf.mono_left (nhds_left'_le_nhds_ne a)
State after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
⊢ 0 ≤ f'

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
⊢ 0 ≤ f'
Tactic:
suffices ∀ᶠ x in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0 from ge_of_tendsto hf this
State after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0
Tactic:
have ha : ∀ᶠ x in 𝓝[<] a, x < a := eventually_nhdsWithin_of_forall fun x hx ↦ hx
State after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0
Tactic:
have h : ∀ᶠ x in 𝓝[<] a, f x ≤ f a := h.filter_mono nhdsWithin_le_nhds
State after:
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0

State before:
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0
Tactic:
filter_upwards [ha, h]
State after:
case h
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
⊢ ∀ a_1 < a, f a_1 ≤ f a → (f a_1 - f a) / (a_1 - a) ≥ 0

State before:
case h
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
⊢ ∀ a_1 < a, f a_1 ≤ f a → (f a_1 - f a) / (a_1 - a) ≥ 0
Tactic:
intro x ha h
State after:
case h
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
x : ℝ
ha : x < a
h : f x ≤ f a
⊢ (f x - f a) / (x - a) ≥ 0

State before:
case h
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
x : ℝ
ha : x < a
h : f x ≤ f a
⊢ (f x - f a) / (x - a) ≥ 0
Tactic:
apply div_nonneg_of_nonpos
State after:
case h.ha
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
x : ℝ
ha : x < a
h : f x ≤ f a
⊢ f x - f a ≤ 0

case h.hb
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
x : ℝ
ha : x < a
h : f x ≤ f a
⊢ x - a ≤ 0

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
Tactic:
rw [hasDerivAt_iff_tendsto_slope] at hf
State after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
⊢ Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
⊢ Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
Tactic:
apply hf.mono_left (nhds_left'_le_nhds_ne a)
State after:
no goals

State before:
case h.ha
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
x : ℝ
ha : x < a
h : f x ≤ f a
⊢ f x - f a ≤ 0
Tactic:
linarith
State after:
no goals

State before:
case h.hb
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
x : ℝ
ha : x < a
h : f x ≤ f a
⊢ x - a ≤ 0
Tactic:
linarith
State after:
no goals