sorry_proof
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN✝ : Filter N
inst✝ : T2Space α
spec : α → Prop
N✝ M✝ : Type
spec✝ : α → Prop
specₙ : N✝ → α → Prop
lN : Filter N✝
lM : Filter M✝
consistent : ∀ (aₙ : N✝ → α), (∀ (n : N✝), specₙ n (aₙ n)) → ∀ (a : α), (a = limit n ∈ lN, aₙ n) → spec✝ a
convergence :
  ∀ (a' : N✝ → M✝ → α),
    (∀ (n : N✝), specₙ n (limit m ∈ lM, a' n m)) →
      ∃ a,
        a =
          limit x ∈ Filter.prod lN lM,
            match x with
            | (n, m) => a' n m
impl : (n : N✝) → ApproxSolution lM (specₙ n)
hn : ∀ (n : N✝) (a : α), (a = limit n_1 ∈ lM, ApproxSolution.val (impl n) n_1) → specₙ n a
aₙ : N✝ → α := fun n => lim (Filter.map (fun m => ApproxSolution.val (impl n) m) lM)
⊢ spec✝ (limit n ∈ Filter.prod lN lM, ApproxSolution.val (impl n.1) n.2)
no goals