Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace

Goal state before:
pp: case refine_1.hd₀
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := ⋯
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto (d ∘ φ) atTop (𝓝 0)

pp: case refine_1.hds
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := ⋯
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, x + (d ∘ φ) n ∈ s

pp: case refine_1.hcd
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := ⋯
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto (fun n ↦ (c ∘ φ) n • (d ∘ φ) n) atTop (𝓝 l)

Tactic:
· refine Tendsto.comp ?_ φ_strict.tendsto_atTop
    exact squeeze_zero_norm (by simpa [dist_eq_norm] using hvu) u_lim

Goal state after:
case refine_1.hds
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := ⋯
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, x + (d ∘ φ) n ∈ s

case refine_1.hcd
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := ⋯
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto (fun n ↦ (c ∘ φ) n • (d ∘ φ) n) atTop (𝓝 l)