Let X, d, seq and x be given.
Assume Hconv: sequence_converges_metric X d seq x.
We prove the intermediate claim Hm: metric_on X d.
An exact proof term for the current goal is (sequence_converges_metric_metric_on X d seq x Hconv).
We prove the intermediate claim Hseq: sequence_on seq X.
An exact proof term for the current goal is (sequence_converges_metric_sequence_on X d seq x Hconv).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (sequence_converges_metric_point_in_X X d seq x Hconv).
We will prove converges_to X (metric_topology X d) seq x.
We will prove topology_on X (metric_topology X d) ∧ sequence_on seq X ∧ x ∈ X ∧ ∀U : set, U ∈ metric_topology X d → x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.
Apply and4I to the current goal.
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
An exact proof term for the current goal is Hseq.
An exact proof term for the current goal is HxX.
Let U be given.
Assume HU: U ∈ metric_topology X d.
Assume HxU: x ∈ U.
We prove the intermediate claim Hexr: ∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ U).
An exact proof term for the current goal is (metric_topology_neighborhood_contains_ball X d x U Hm HxX HU HxU).
Apply Hexr to the current goal.
Let r be given.
Assume Hrpack.
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (andEL (r ∈ R) (Rlt 0 r ∧ open_ball X d x r ⊆ U) Hrpack).
We prove the intermediate claim Hrrest: Rlt 0 r ∧ open_ball X d x r ⊆ U.
An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r ∧ open_ball X d x r ⊆ U) Hrpack).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (andEL (Rlt 0 r) (open_ball X d x r ⊆ U) Hrrest).
We prove the intermediate claim Hballsub: open_ball X d x r ⊆ U.
An exact proof term for the current goal is (andER (Rlt 0 r) (open_ball X d x r ⊆ U) Hrrest).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun d (apply_fun seq n,x)) r.
An exact proof term for the current goal is (sequence_converges_metric_eps X d seq x Hconv r (andI (r ∈ R) (Rlt 0 r) HrR Hrpos)).
Apply HexN to the current goal.
Let N be given.
Assume HNpack.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun d (apply_fun seq n,x)) r) HNpack).
Let n be given.
Assume HnO: n ∈ ω.
Assume HNn: N ⊆ n.
We will prove apply_fun seq n ∈ U.
We prove the intermediate claim HseqnX: apply_fun seq n ∈ X.
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim Hlt0: Rlt (apply_fun d (apply_fun seq n,x)) r.
An exact proof term for the current goal is (andER (N ∈ ω) (∀n0 : set, n0 ∈ ω → N ⊆ n0 → Rlt (apply_fun d (apply_fun seq n0,x)) r) HNpack n HnO HNn).
We prove the intermediate claim Hsym: apply_fun d (x,apply_fun seq n) = apply_fun d (apply_fun seq n,x).
An exact proof term for the current goal is (metric_on_symmetric X d x (apply_fun seq n) Hm HxX HseqnX).
We prove the intermediate claim Hlt: Rlt (apply_fun d (x,apply_fun seq n)) r.
rewrite the current goal using Hsym (from left to right).
An exact proof term for the current goal is Hlt0.
We prove the intermediate claim Hball: apply_fun seq n ∈ open_ball X d x r.
An exact proof term for the current goal is (open_ballI X d x r (apply_fun seq n) HseqnX Hlt).
An exact proof term for the current goal is (Hballsub (apply_fun seq n) Hball).
∎