-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMaxOn.hasFDerivWithinAt_nonpos (h : IsLocalMaxOn f s a)
    (hf : HasFDerivWithinAt f f' s a) (hy : y ∈ posTangentConeAt s a) : f' y ≤ 0

Proof state:
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
c : ℕ → ℝ
d : ℕ → E
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
hd : Tendsto (fun n => a + d n) atTop (𝓝[s] (a + 0))
⊢ ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0

Tactic:
rw [add_zero] at hd

Result:
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
c : ℕ → ℝ
d : ℕ → E
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
hd : Tendsto (fun n => a + d n) atTop (𝓝[s] a)
⊢ ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0

Proof state:
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
⊢ f' y ≤ 0

Tactic:
suffices ∀ᶠ n in atTop, c n • (f (a + d n) - f a) ≤ 0 from
  le_of_tendsto (hf.lim atTop hd hc' hcd) this

Result:
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
⊢ ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0

Proof state:
case h
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
c : ℕ → ℝ
d : ℕ → E
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
hd : Tendsto (fun n => a + d n) atTop (𝓝[s] a)
n : ℕ
hfn : f (a + d n) ≤ f a
hcn : 0 ≤ c n
⊢ c n • (f (a + d n) - f a) ≤ 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos hcn (sub_nonpos.2 hfn)

Result:
no goals

Proof state:
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
⊢ ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0

Tactic:
replace hd : Tendsto (fun n => a + d n) atTop (𝓝[s] (a + 0)) :=
  tendsto_nhdsWithin_iff.2 ⟨tendsto_const_nhds.add (tangentConeAt.lim_zero _ hc' hcd), hd⟩

Result:
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
c : ℕ → ℝ
d : ℕ → E
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
hd : Tendsto (fun n => a + d n) atTop (𝓝[s] (a + 0))
⊢ ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0

Proof state:
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
c : ℕ → ℝ
d : ℕ → E
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
hd : Tendsto (fun n => a + d n) atTop (𝓝[s] a)
⊢ ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0

Tactic:
filter_upwards [hd.eventually h, hc.eventually_ge_atTop 0] with n hfn hcn

Result:
case h
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
c : ℕ → ℝ
d : ℕ → E
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
hd : Tendsto (fun n => a + d n) atTop (𝓝[s] a)
n : ℕ
hfn : f (a + d n) ≤ f a
hcn : 0 ≤ c n
⊢ c n • (f (a + d n) - f a) ≤ 0

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
⊢ f' y ≤ 0

Tactic:
rcases hy with ⟨c, d, hd, hc, hcd⟩

Result:
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ f' y ≤ 0