α : Type u_1
β : Type ?u.68450
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
l : List α
hl : List.length l = n + 1
⊢ Tendsto (fun x => ↑(removeNth i x)) (𝓝 { val := l, property := hl })
    (𝓝
      ↑(match { val := l, property := hl } with
        | { val := l, property := p } =>
          { val := List.removeNth l ↑i, property := (_ : List.length (List.removeNth l ↑i) = n + 1 - 1) }))
α : Type u_1
β : Type ?u.68450
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
l : List α
hl : List.length l = n + 1
⊢ ContinuousAt (removeNth i) { val := l, property := hl }
rw [ContinuousAt, removeNth, tendsto_subtype_rng]
α : Type u_1
β : Type ?u.68450
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
l : List α
hl : List.length l = n + 1
⊢ Tendsto (fun x => List.removeNth ↑x ↑i) (𝓝 { val := l, property := hl }) (𝓝 (List.removeNth l ↑i))
α : Type u_1
β : Type ?u.68450
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
l : List α
hl : List.length l = n + 1
⊢ Tendsto (fun x => ↑(removeNth i x)) (𝓝 { val := l, property := hl })
    (𝓝
      ↑(match { val := l, property := hl } with
        | { val := l, property := p } =>
          { val := List.removeNth l ↑i, property := (_ : List.length (List.removeNth l ↑i) = n + 1 - 1) }))
simp only [Vector.removeNth_val]
no goals
α : Type u_1
β : Type ?u.68450
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
l : List α
hl : List.length l = n + 1
⊢ Tendsto (fun x => List.removeNth ↑x ↑i) (𝓝 { val := l, property := hl }) (𝓝 (List.removeNth l ↑i))
exact Tendsto.comp List.tendsto_removeNth continuousAt_subtype_val