induction approx
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN : Filter N
inst✝ : T2Space α
spec : α → Prop
approx : ApproxSolution lN spec
⊢ ∀ (a : α), (a = limit n ∈ lN, ApproxSolution.val approx n) → spec a
case exact
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN : Filter N
inst✝ : T2Space α
spec spec✝ : α → Prop
impl✝ : α
h✝ : spec✝ impl✝
⊢ ∀ (a : α), (a = limit n ∈ ⊤, ApproxSolution.val (ApproxSolution.exact impl✝ h✝) n) → spec✝ a

case approx
α : 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)
impl_ih✝ : ∀ (n : N✝) (a : α), (a = limit n_1 ∈ lM✝, ApproxSolution.val (impl✝ n) n_1) → specₙ✝ n a
⊢ ∀ (a : α),
    (a =
        limit n ∈ Filter.prod lN✝ lM✝,
          ApproxSolution.val (ApproxSolution.approx specₙ✝ lN✝ lM✝ consistent✝ convergence✝ impl✝) n) →
      spec✝ a