case intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
⊢ ↑(LinearMap.single i) w ∈ tangentConeAt 𝕜 (Set.pi univ s) x
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
⊢ MapsTo (↑(LinearMap.single i)) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.pi univ s) x)
rintro w ⟨c, d, hd, hc, hy⟩
case intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
this : ∀ (n : ℕ) (j : ι), j ≠ i → ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2) ^ n
⊢ ↑(LinearMap.single i) w ∈ tangentConeAt 𝕜 (Set.pi univ s) x
case intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
⊢ ↑(LinearMap.single i) w ∈ tangentConeAt 𝕜 (Set.pi univ s) x
have : ∀ (n) (j) (_ : j ≠ i), ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2 : ℝ) ^ n := by
  intro n j hj
  rcases mem_closure_iff_nhds.1 (hi j hj) _
      (eventually_nhds_norm_smul_sub_lt (c n) (x j) (pow_pos one_half_pos n)) with
    ⟨z, hz, hzs⟩
  exact ⟨z - x j, by simpa using hzs, by simpa using hz⟩
case intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
⊢ ↑(LinearMap.single i) w ∈ tangentConeAt 𝕜 (Set.pi univ s) x
case intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
this : ∀ (n : ℕ) (j : ι), j ≠ i → ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2) ^ n
⊢ ↑(LinearMap.single i) w ∈ tangentConeAt 𝕜 (Set.pi univ s) x
choose! d' hd's hcd' using this
case intro.intro.intro.intro.refine'_1
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝¹ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
n : ℕ
hn : x i + d n ∈ s i
j : ι
x✝ : j ∈ univ
⊢ (x + (fun n => Function.update (d' n) i (d n)) n) j ∈ s j

case intro.intro.intro.intro.refine'_2
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
⊢ Tendsto (fun i_1 => (c i_1 • (fun n => Function.update (d' n) i (d n)) i_1) j) atTop (𝓝 (↑(LinearMap.single i) w j))
case intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
⊢ ↑(LinearMap.single i) w ∈ tangentConeAt 𝕜 (Set.pi univ s) x
refine' ⟨c, fun n => Function.update (d' n) i (d n), hd.mono fun n hn j _ => _, hc,
    tendsto_pi_nhds.2 fun j => _⟩
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
n : ℕ
j : ι
hj : j ≠ i
⊢ ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2) ^ n
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
⊢ ∀ (n : ℕ) (j : ι), j ≠ i → ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2) ^ n
intro n j hj
case intro.intro
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
n : ℕ
j : ι
hj : j ≠ i
z : E j
hz : z ∈ {x_1 | (fun y => ‖c n • (y - x j)‖ < (1 / 2) ^ n) x_1}
hzs : z ∈ s j
⊢ ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2) ^ n
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
n : ℕ
j : ι
hj : j ≠ i
⊢ ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2) ^ n
rcases mem_closure_iff_nhds.1 (hi j hj) _
    (eventually_nhds_norm_smul_sub_lt (c n) (x j) (pow_pos one_half_pos n)) with
  ⟨z, hz, hzs⟩
no goals
case intro.intro
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
n : ℕ
j : ι
hj : j ≠ i
z : E j
hz : z ∈ {x_1 | (fun y => ‖c n • (y - x j)‖ < (1 / 2) ^ n) x_1}
hzs : z ∈ s j
⊢ ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2) ^ n
exact ⟨z - x j, by simpa using hzs, by simpa using hz⟩
no goals
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
n : ℕ
j : ι
hj : j ≠ i
z : E j
hz : z ∈ {x_1 | (fun y => ‖c n • (y - x j)‖ < (1 / 2) ^ n) x_1}
hzs : z ∈ s j
⊢ x j + (z - x j) ∈ s j
simpa using hzs
no goals
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
n : ℕ
j : ι
hj : j ≠ i
z : E j
hz : z ∈ {x_1 | (fun y => ‖c n • (y - x j)‖ < (1 / 2) ^ n) x_1}
hzs : z ∈ s j
⊢ ‖c n • (z - x j)‖ < (1 / 2) ^ n
simpa using hz
no goals
case intro.intro.intro.intro.refine'_1
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝¹ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
n : ℕ
hn : x i + d n ∈ s i
j : ι
x✝ : j ∈ univ
⊢ (x + (fun n => Function.update (d' n) i (d n)) n) j ∈ s j
rcases em (j = i) with (rfl | hj) <;> simp [*]
case intro.intro.intro.intro.refine'_2.inl
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
c : ℕ → 𝕜
hc : Tendsto (fun n => ‖c n‖) atTop atTop
d' : ℕ → (j : ι) → E j
j : ι
hi : ∀ (j_1 : ι), j_1 ≠ j → x j_1 ∈ closure (s j_1)
w : E j
d : ℕ → E j
hd : ∀ᶠ (n : ℕ) in atTop, x j + d n ∈ s j
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
hd's : ∀ (n : ℕ) (j_1 : ι), j_1 ≠ j → x j_1 + d' n j_1 ∈ s j_1
hcd' : ∀ (n : ℕ) (j_1 : ι), j_1 ≠ j → ‖c n • d' n j_1‖ < (1 / 2) ^ n
⊢ Tendsto (fun i => (c i • (fun n => Function.update (d' n) j (d n)) i) j) atTop (𝓝 (↑(LinearMap.single j) w j))

case intro.intro.intro.intro.refine'_2.inr
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
hj : ¬j = i
⊢ Tendsto (fun i_1 => (c i_1 • (fun n => Function.update (d' n) i (d n)) i_1) j) atTop (𝓝 (↑(LinearMap.single i) w j))
case intro.intro.intro.intro.refine'_2
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
⊢ Tendsto (fun i_1 => (c i_1 • (fun n => Function.update (d' n) i (d n)) i_1) j) atTop (𝓝 (↑(LinearMap.single i) w j))
rcases em (j = i) with (rfl | hj)
no goals
case intro.intro.intro.intro.refine'_2.inl
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
c : ℕ → 𝕜
hc : Tendsto (fun n => ‖c n‖) atTop atTop
d' : ℕ → (j : ι) → E j
j : ι
hi : ∀ (j_1 : ι), j_1 ≠ j → x j_1 ∈ closure (s j_1)
w : E j
d : ℕ → E j
hd : ∀ᶠ (n : ℕ) in atTop, x j + d n ∈ s j
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
hd's : ∀ (n : ℕ) (j_1 : ι), j_1 ≠ j → x j_1 + d' n j_1 ∈ s j_1
hcd' : ∀ (n : ℕ) (j_1 : ι), j_1 ≠ j → ‖c n • d' n j_1‖ < (1 / 2) ^ n
⊢ Tendsto (fun i => (c i • (fun n => Function.update (d' n) j (d n)) i) j) atTop (𝓝 (↑(LinearMap.single j) w j))
simp [hy]
case intro.intro.intro.intro.refine'_2.inr
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
hj : ¬j = i
⊢ Tendsto (fun n => c n • d' n j) atTop (𝓝 0)
case intro.intro.intro.intro.refine'_2.inr
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
hj : ¬j = i
⊢ Tendsto (fun i_1 => (c i_1 • (fun n => Function.update (d' n) i (d n)) i_1) j) atTop (𝓝 (↑(LinearMap.single i) w j))
suffices Tendsto (fun n => c n • d' n j) atTop (𝓝 0) by simpa [hj]
case intro.intro.intro.intro.refine'_2.inr
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
hj : ¬j = i
⊢ Tendsto (fun n => (1 / 2) ^ n) atTop (𝓝 0)
case intro.intro.intro.intro.refine'_2.inr
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
hj : ¬j = i
⊢ Tendsto (fun n => c n • d' n j) atTop (𝓝 0)
refine' squeeze_zero_norm (fun n => (hcd' n j hj).le) _
no goals
case intro.intro.intro.intro.refine'_2.inr
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
hj : ¬j = i
⊢ Tendsto (fun n => (1 / 2) ^ n) atTop (𝓝 0)
exact tendsto_pow_atTop_nhds_0_of_lt_1 one_half_pos.le one_half_lt_one
no goals
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.63756
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.63851
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.63941
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : DecidableEq ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
hj : ¬j = i
this : Tendsto (fun n => c n • d' n j) atTop (𝓝 0)
⊢ Tendsto (fun i_1 => (c i_1 • (fun n => Function.update (d' n) i (d n)) i_1) j) atTop (𝓝 (↑(LinearMap.single i) w j))
simpa [hj]