Exists seq gt tendsto of not countable

lemma exists_seq_gt_tendsto_of_not_countable [TopologicalSpace.SeparableSpace ι]    {A : Set ι} (hA : ¬ A.Countable) :    ∃ (p : ι) (u : ℕ → ι), (∀ k, u k ∈ A) ∧ (∀ k, p < u k) ∧      Tendsto u atTop (𝓝 p) := by  have : SecondCountableTopology ι := .of_separableSpace_orderTopology _  have h := countable_setOfPred_isolated_right_within (s := A)  have hsub : ¬ A ⊆ {x | x ∈ A ∧ 𝓝[A ∩ Set.Ioi x] x = ⊥} := by    intro hcon    exact hA (h.mono hcon)  rw [Set.not_subset] at hsub  obtain ⟨p, hpA, hpiso⟩ := hsub  simp only [Set.mem_ofPred_eq, not_and] at hpiso  have : (𝓝[A ∩ Set.Ioi p] p).NeBot := ⟨hpiso hpA⟩  obtain ⟨u, hu⟩ := exists_seq_tendsto (𝓝[A ∩ Set.Ioi p] p)  simp only [tendsto_nhdsWithin_iff, Set.mem_inter_iff, Set.mem_Ioi, eventually_atTop] at hu  obtain ⟨hu_tendsto, a, hu⟩ := hu  refine ⟨p, fun k ↦ u (a + k), fun k ↦ (hu (a + k) (by grind)).1,    fun k ↦ (hu (a + k) (by grind)).2, ?_⟩  simp_rw [add_comm a]  exact (tendsto_add_atTop_iff_nat a).mpr hu_tendsto