-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
lemma one_mem_posTangentConeAt_iff_mem_closure :
    1 ∈ posTangentConeAt s a ↔ a ∈ closure (Ioi a ∩ s)

Proof state:
case h
s : Set ℝ
a : ℝ
c d : ℕ → ℝ
hs : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 1)
this : Tendsto (fun x => a + d x) atTop (𝓝 a)
n : ℕ
hcn : 0 < c n
hcdn : 0 < c n • d n
hdn : a + d n ∈ s
⊢ a + d n ∈ Ioi a ∩ s

Tactic:
simp_all

Result:
no goals

Proof state:
case mpr
s : Set ℝ
a : ℝ
⊢ a ∈ closure (Ioi a ∩ s) → 1 ∈ posTangentConeAt s a

Tactic:
intro h

Result:
case mpr
s : Set ℝ
a : ℝ
h : a ∈ closure (Ioi a ∩ s)
⊢ 1 ∈ posTangentConeAt s a

Proof state:
case mp
s : Set ℝ
a : ℝ
⊢ 1 ∈ posTangentConeAt s a → a ∈ closure (Ioi a ∩ s)

Tactic:
rintro ⟨c, d, hs, hc, hcd⟩

Result:
case mp.intro.intro.intro.intro
s : Set ℝ
a : ℝ
c d : ℕ → ℝ
hs : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 1)
⊢ a ∈ closure (Ioi a ∩ s)

Proof state:
s : Set ℝ
a : ℝ
c d : ℕ → ℝ
hs : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 1)
⊢ Tendsto (fun x => a + d x) atTop (𝓝 a)

Tactic:
simpa only [add_zero] using tendsto_const_nhds.add
  (tangentConeAt.lim_zero _ (tendsto_abs_atTop_atTop.comp hc) hcd)

Result:
no goals

Proof state:
case mpr.h
s : Set ℝ
a : ℝ
h : ∃ᶠ (a_1 : ℝ) in 𝓝 0, a + a_1 ∈ Ioi a ∩ s
⊢ ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + t • 1 ∈ s

Tactic:
simpa [nhdsWithin, frequently_inf_principal] using h

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
s : Set ℝ
a : ℝ
c d : ℕ → ℝ
hs : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 1)
this : Tendsto (fun x => a + d x) atTop (𝓝 a)
⊢ a ∈ closure (Ioi a ∩ s)

Tactic:
apply mem_closure_of_tendsto this

Result:
case mp.intro.intro.intro.intro
s : Set ℝ
a : ℝ
c d : ℕ → ℝ
hs : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 1)
this : Tendsto (fun x => a + d x) atTop (𝓝 a)
⊢ ∀ᶠ (x : ℕ) in atTop, a + d x ∈ Ioi a ∩ s

Proof state:
case mp.intro.intro.intro.intro
s : Set ℝ
a : ℝ
c d : ℕ → ℝ
hs : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 1)
this : Tendsto (fun x => a + d x) atTop (𝓝 a)
⊢ ∀ᶠ (x : ℕ) in atTop, a + d x ∈ Ioi a ∩ s

Tactic:
filter_upwards [hc.eventually_gt_atTop 0, hcd.eventually (lt_mem_nhds one_pos), hs]
  with n hcn hcdn hdn

Result:
case h
s : Set ℝ
a : ℝ
c d : ℕ → ℝ
hs : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 1)
this : Tendsto (fun x => a + d x) atTop (𝓝 a)
n : ℕ
hcn : 0 < c n
hcdn : 0 < c n • d n
hdn : a + d n ∈ s
⊢ a + d n ∈ Ioi a ∩ s

Proof state:
case mpr
s : Set ℝ
a : ℝ
h : a ∈ closure (Ioi a ∩ s)
⊢ 1 ∈ posTangentConeAt s a

Tactic:
apply mem_posTangentConeAt_of_frequently_mem

Result:
case mpr.h
s : Set ℝ
a : ℝ
h : a ∈ closure (Ioi a ∩ s)
⊢ ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + t • 1 ∈ s

Proof state:
s : Set ℝ
a : ℝ
⊢ 1 ∈ posTangentConeAt s a ↔ a ∈ closure (Ioi a ∩ s)

Tactic:
constructor

Result:
case mp
s : Set ℝ
a : ℝ
⊢ 1 ∈ posTangentConeAt s a → a ∈ closure (Ioi a ∩ s)

case mpr
s : Set ℝ
a : ℝ
⊢ a ∈ closure (Ioi a ∩ s) → 1 ∈ posTangentConeAt s a

Proof state:
case mpr.h
s : Set ℝ
a : ℝ
h : a ∈ closure (Ioi a ∩ s)
⊢ ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + t • 1 ∈ s

Tactic:
rw [mem_closure_iff_frequently, ← map_add_left_nhds_zero, frequently_map] at h

Result:
case mpr.h
s : Set ℝ
a : ℝ
h : ∃ᶠ (a_1 : ℝ) in 𝓝 0, a + a_1 ∈ Ioi a ∩ s
⊢ ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + t • 1 ∈ s