Wkp U limit of cauchy Seq

lemma WkpU.limit_of_cauchySeq [Fact (1 ≤ p)]    {fₙ : ℕ → WkpU d k p U hU}    (hcauchy : CauchySeq fₙ) :    ∃ f_lim : WkpU d k p U hU,      Tendsto (fun n => WkpU.toLp (fₙ n)) atTop (𝓝 (WkpU.toLp f_lim)) ∧      ∀ (n : ℕ+) (hn : n ≤ k) (s : Fin n → Fin d),        Tendsto (fun j => WkpU.derivtoLp (fₙ j) n hn s) atTop          (𝓝 (WkpU.derivtoLp f_lim n hn s)) := by  obtain ⟨g, hg⟩ := cauchySeq_tendsto_of_complete (WkpU.cauchySeq_toLp hcauchy)  have hg_ns : ∀ (n : ℕ+) (hn : n ≤ k) (s : Fin n → Fin d),      ∃ g_ns : Lp ℝ p (μU d U),        Tendsto (fun j => WkpU.derivtoLp (fₙ j) n hn s) atTop (𝓝 g_ns)        ∧ ∀ ψ ∈ Cc_inftyU d U,          ∫ x, (g : (Fin d → ℝ) → ℝ) x • (iteratedFDeriv ℝ n ψ x) (unitSeq s) ∂ μU d U          = (-1 : ℝ)^(n : ℕ) • ∫ x, ψ x • (g_ns : (Fin d → ℝ) → ℝ) x ∂ μU d U :=    fun n hn s => by      obtain ⟨g_ns, hg_ns_lim⟩ :=        cauchySeq_tendsto_of_complete (WkpU.cauchySeq_derivtoLp hcauchy n hn s)      exact ⟨g_ns, hg_ns_lim, WkpU.ibp_tendsto g hg n hn s g_ns hg_ns_lim⟩  let f_lim : WkpU d k p U hU := ⟨⟨g, Lp.mem_Lp_locU g⟩,    WkpU.limit_mem g      (fun n hn s => (hg_ns n hn s).choose)      (fun n hn s => (hg_ns n hn s).choose_spec.2)⟩  refine ⟨f_lim,    by simp_rw [show WkpU.toLp f_lim = g from Lp.ext (Lp.memLp g).coeFn_toLp]; exact hg,    fun n hn s => ?_⟩  have hfl_deriv : WkpU.derivtoLp f_lim n hn s = (hg_ns n hn s).choose := by    let g_ns := (hg_ns n hn s).choose    have hid := (hg_ns n hn s).choose_spec.2    have hg_ns_loc : (g_ns : (Fin d → ℝ) →ₘ[μU d U] ℝ) ∈ Lp_locU d 1 U :=      Lp.mem_Lp_locU g_ns    apply Lp.ext    filter_upwards [(WkpU.weakDeriv_memLp f_lim n hn s).coeFn_toLp,        WeakmultiderivU_unique hU s f_lim.val (WkpU.hasWeakDeriv f_lim n hn s)          ⟨(g_ns : (Fin d → ℝ) →ₘ[μU d U] ℝ), hg_ns_loc⟩ hid,        (Lp.memLp g_ns).coeFn_toLp] with x h1 h2 h3    simp only [WkpU.derivtoLp, WkpU.weakDeriv] at h1 ⊢    rw [h1]; exact h2  rw [hfl_deriv]  exact (hg_ns n hn s).choose_spec.1