α : Type u_1
β : Type ?u.65317
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : List.length l = n
⊢ Tendsto (fun x => ↑(insertNth x.fst i x.snd)) (𝓝 a ×ˢ 𝓝 { val := l, property := hl })
    (𝓝
      ↑{ val := List.insertNth (↑i) a ↑{ val := l, property := hl },
          property := (_ : List.length (List.insertNth (↑i) a ↑{ val := l, property := hl }) = n + 1) })
α : Type u_1
β : Type ?u.65317
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : List.length l = n
⊢ Tendsto (fun p => insertNth p.fst i p.snd) (𝓝 a ×ˢ 𝓝 { val := l, property := hl })
    (𝓝 (insertNth a i { val := l, property := hl }))
rw [insertNth, tendsto_subtype_rng]
α : Type u_1
β : Type ?u.65317
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : List.length l = n
⊢ Tendsto (fun x => List.insertNth (↑i) x.fst ↑x.snd) (𝓝 a ×ˢ 𝓝 { val := l, property := hl })
    (𝓝 (List.insertNth (↑i) a l))
α : Type u_1
β : Type ?u.65317
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : List.length l = n
⊢ Tendsto (fun x => ↑(insertNth x.fst i x.snd)) (𝓝 a ×ˢ 𝓝 { val := l, property := hl })
    (𝓝
      ↑{ val := List.insertNth (↑i) a ↑{ val := l, property := hl },
          property := (_ : List.length (List.insertNth (↑i) a ↑{ val := l, property := hl }) = n + 1) })
simp [insertNth_val]
no goals
α : Type u_1
β : Type ?u.65317
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : List.length l = n
⊢ Tendsto (fun x => List.insertNth (↑i) x.fst ↑x.snd) (𝓝 a ×ˢ 𝓝 { val := l, property := hl })
    (𝓝 (List.insertNth (↑i) a l))
exact List.tendsto_insertNth tendsto_fst (Tendsto.comp continuousAt_subtype_val tendsto_snd : _)