𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
⊢ y ∈ tangentConeAt 𝕜 univ x
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
⊢ tangentConeAt 𝕜 univ x = univ
refine' univ_subset_iff.1 fun y _ => _
case intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
⊢ y ∈ tangentConeAt 𝕜 univ x
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
⊢ y ∈ tangentConeAt 𝕜 univ x
rcases exists_one_lt_norm 𝕜 with ⟨w, hw⟩
case intro.refine'_1
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
⊢ Tendsto (fun n => ‖(fun n => w ^ n) n‖) atTop atTop

case intro.refine'_2
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
⊢ Tendsto (fun n => (fun n => w ^ n) n • (fun n => (w ^ n)⁻¹ • y) n) atTop (𝓝 y)
case intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
⊢ y ∈ tangentConeAt 𝕜 univ x
refine' ⟨fun n => w ^ n, fun n => (w ^ n)⁻¹ • y, univ_mem' fun n => mem_univ _, _, _⟩
case intro.refine'_1
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
⊢ Tendsto (fun n => ‖w‖ ^ n) atTop atTop
case intro.refine'_1
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
⊢ Tendsto (fun n => ‖(fun n => w ^ n) n‖) atTop atTop
simp only [norm_pow]
no goals
case intro.refine'_1
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
⊢ Tendsto (fun n => ‖w‖ ^ n) atTop atTop
exact tendsto_pow_atTop_atTop_of_one_lt hw
case h.e'_3.h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
n : ℕ
⊢ (fun n => w ^ n) n • (fun n => (w ^ n)⁻¹ • y) n = y
case intro.refine'_2
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
⊢ Tendsto (fun n => (fun n => w ^ n) n • (fun n => (w ^ n)⁻¹ • y) n) atTop (𝓝 y)
convert @tendsto_const_nhds E ℕ _ _ atTop with n
case h.e'_3.h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
n : ℕ
this : w ^ n * (w ^ n)⁻¹ = 1
⊢ (fun n => w ^ n) n • (fun n => (w ^ n)⁻¹ • y) n = y
case h.e'_3.h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
n : ℕ
⊢ (fun n => w ^ n) n • (fun n => (w ^ n)⁻¹ • y) n = y
have : w ^ n * (w ^ n)⁻¹ = 1 := by
  apply mul_inv_cancel
  apply pow_ne_zero
  simpa [norm_eq_zero] using (ne_of_lt (lt_trans zero_lt_one hw)).symm
no goals
case h.e'_3.h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
n : ℕ
this : w ^ n * (w ^ n)⁻¹ = 1
⊢ (fun n => w ^ n) n • (fun n => (w ^ n)⁻¹ • y) n = y
rw [smul_smul, this, one_smul]
case h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
n : ℕ
⊢ w ^ n ≠ 0
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
n : ℕ
⊢ w ^ n * (w ^ n)⁻¹ = 1
apply mul_inv_cancel
case h.h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
n : ℕ
⊢ w ≠ 0
case h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
n : ℕ
⊢ w ^ n ≠ 0
apply pow_ne_zero
no goals
case h.h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.5583
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.5673
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t : Set E
y : E
x✝ : y ∈ univ
w : 𝕜
hw : 1 < ‖w‖
n : ℕ
⊢ w ≠ 0
simpa [norm_eq_zero] using (ne_of_lt (lt_trans zero_lt_one hw)).symm