case intro.intro.intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ y ∈ tangentConeAt 𝕜 t x
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x
rintro y ⟨c, d, ds, ctop, clim⟩
case intro.intro.intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ ∀ᶠ (n : ℕ) in atTop, x + d n ∈ t
case intro.intro.intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ y ∈ tangentConeAt 𝕜 t x
refine' ⟨c, d, _, ctop, clim⟩
case intro.intro.intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
this : Tendsto (fun n => x + d n) atTop (𝓝[t] x)
⊢ ∀ᶠ (n : ℕ) in atTop, x + d n ∈ t

case this
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ Tendsto (fun n => x + d n) atTop (𝓝[t] x)
case intro.intro.intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ ∀ᶠ (n : ℕ) in atTop, x + d n ∈ t
suffices : Tendsto (fun n => x + d n) atTop (𝓝[t] x)
case this
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ Tendsto (fun n => x + d n) atTop (𝓝[t] x)
case intro.intro.intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
this : Tendsto (fun n => x + d n) atTop (𝓝[t] x)
⊢ ∀ᶠ (n : ℕ) in atTop, x + d n ∈ t

case this
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ Tendsto (fun n => x + d n) atTop (𝓝[t] x)
exact tendsto_principal.1 (tendsto_inf.1 this).2
case this
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ Tendsto (fun a => x + d a) atTop (𝓝 x)
case this
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ Tendsto (fun n => x + d n) atTop (𝓝[t] x)
refine' (tendsto_inf.2 ⟨_, tendsto_principal.2 ds⟩).mono_right h
no goals
case this
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.28939
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.29029
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ Tendsto (fun a => x + d a) atTop (𝓝 x)
simpa only [add_zero] using tendsto_const_nhds.add (tangentConeAt.lim_zero atTop ctop clim)