case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
v : E
c : ℕ → 𝕜
d : ℕ → E
dtop : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
clim : Tendsto (fun n => ‖c n‖) atTop atTop
cdlim : Tendsto (fun n => c n • d n) atTop (𝓝 v)
⊢ ↑f' v ∈ tangentConeAt 𝕜 (f '' s) (f x)
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
⊢ MapsTo (↑f') (tangentConeAt 𝕜 s x) (tangentConeAt 𝕜 (f '' s) (f x))
rintro v ⟨c, d, dtop, clim, cdlim⟩
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
v : E
c : ℕ → 𝕜
d : ℕ → E
dtop : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
clim : Tendsto (fun n => ‖c n‖) atTop atTop
cdlim : Tendsto (fun n => c n • d n) atTop (𝓝 v)
⊢ {x_1 | (fun n => x + d n ∈ s) x_1} ⊆ {x_1 | (fun n => f x + (fun n => f (x + d n) - f x) n ∈ f '' s) x_1}
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
v : E
c : ℕ → 𝕜
d : ℕ → E
dtop : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
clim : Tendsto (fun n => ‖c n‖) atTop atTop
cdlim : Tendsto (fun n => c n • d n) atTop (𝓝 v)
⊢ ↑f' v ∈ tangentConeAt 𝕜 (f '' s) (f x)
refine'
  ⟨c, fun n => f (x + d n) - f x, mem_of_superset dtop _, clim, h.lim atTop dtop clim cdlim⟩
no goals
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
v : E
c : ℕ → 𝕜
d : ℕ → E
dtop : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
clim : Tendsto (fun n => ‖c n‖) atTop atTop
cdlim : Tendsto (fun n => c n • d n) atTop (𝓝 v)
⊢ {x_1 | (fun n => x + d n ∈ s) x_1} ⊆ {x_1 | (fun n => f x + (fun n => f (x + d n) - f x) n ∈ f '' s) x_1}
simp (config := { contextual := true }) [-mem_image, mem_image_of_mem]