Theorem: SciLean.approx_consistency (SciLean/Core/Approx/ApproxSolution.lean)

State before:
α : 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
Tactic:
induction approx
State after:
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

State before:
α : 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
Tactic:
case exact impl h =>
  simp[ApproxSolution.val]
  sorry_proof
State after:
no goals

State before:
α : 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 : α),
    (a =
        limit n ∈ Filter.prod lN lM,
          ApproxSolution.val (ApproxSolution.approx specₙ lN lM consistent convergence impl) n) →
      spec✝ a
Tactic:
case approx specₙ lN lM consistent convergence impl hn =>
  simp[ApproxSolution.val]
  let aₙ := λ n => lim (lM.map λ m => (impl n).val m)
  sorry_proof
State after:
no goals

State before:
α : 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
Tactic:
simp[ApproxSolution.val]
State after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN : Filter N
inst✝ : T2Space α
spec spec✝ : α → Prop
impl : α
h : spec✝ impl
⊢ spec✝ impl

State before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN : Filter N
inst✝ : T2Space α
spec spec✝ : α → Prop
impl : α
h : spec✝ impl
⊢ spec✝ impl
Tactic:
sorry_proof
State after:
no goals

State before:
α : 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 : α),
    (a =
        limit n ∈ Filter.prod lN lM,
          ApproxSolution.val (ApproxSolution.approx specₙ lN lM consistent convergence impl) n) →
      spec✝ a
Tactic:
simp[ApproxSolution.val]
State after:
α : 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
⊢ spec✝ (limit n ∈ Filter.prod lN lM, ApproxSolution.val (impl n.1) n.2)

State before:
α : 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
⊢ spec✝ (limit n ∈ Filter.prod lN lM, ApproxSolution.val (impl n.1) n.2)
Tactic:
let aₙ := λ n => lim (lM.map λ m => (impl n).val m)
State after:
α : 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)

State before:
α : 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)
Tactic:
sorry_proof
State after:
no goals