Let X, d, seq and x be given.
Assume Hm: metric_on X d.
Assume Htop: converges_to X (metric_topology X d) seq x.
We will prove sequence_converges_metric X d seq x.
We will prove metric_on X d ∧ sequence_on seq X ∧ x ∈ X ∧ ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun d (apply_fun seq n,x)) eps.
We prove the intermediate claim Hseq: sequence_on seq X.
An exact proof term for the current goal is (converges_to_sequence_on X (metric_topology X d) seq x Htop).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (converges_to_point_in_X X (metric_topology X d) seq x Htop).
We prove the intermediate claim Hevent: ∀U : set, U ∈ metric_topology X d → x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.
An exact proof term for the current goal is (andER ((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) Htop).
Apply and4I to the current goal.
An exact proof term for the current goal is Hm.
An exact proof term for the current goal is Hseq.
An exact proof term for the current goal is HxX.
Let eps be given.
Assume Heps12: eps ∈ R ∧ Rlt 0 eps.
We will prove ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun d (apply_fun seq n,x)) eps.
We prove the intermediate claim HepsR: eps ∈ R.
An exact proof term for the current goal is (andEL (eps ∈ R) (Rlt 0 eps) Heps12).
We prove the intermediate claim HepsPos: Rlt 0 eps.
An exact proof term for the current goal is (andER (eps ∈ R) (Rlt 0 eps) Heps12).
Set U to be the term open_ball X d x eps.
We prove the intermediate claim HU: U ∈ metric_topology X d.
An exact proof term for the current goal is (open_ball_in_metric_topology X d x eps Hm HxX HepsPos).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (center_in_open_ball X d x eps Hm HxX HepsPos).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.
An exact proof term for the current goal is (Hevent U HU HxU).
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 → apply_fun seq n ∈ U) HNpack).
Let n be given.
Assume HnO: n ∈ ω.
Assume HNn: N ⊆ n.
We will prove Rlt (apply_fun d (apply_fun seq n,x)) eps.
We prove the intermediate claim HseqnU: apply_fun seq n ∈ U.
An exact proof term for the current goal is (andER (N ∈ ω) (∀n0 : set, n0 ∈ ω → N ⊆ n0 → apply_fun seq n0 ∈ U) HNpack n HnO HNn).
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 (x,apply_fun seq n)) eps.
An exact proof term for the current goal is (open_ballE2 X d x eps (apply_fun seq n) HseqnU).
We prove the intermediate claim Hsym: apply_fun d (apply_fun seq n,x) = apply_fun d (x,apply_fun seq n).
An exact proof term for the current goal is (metric_on_symmetric X d (apply_fun seq n) x Hm HseqnX HxX).
rewrite the current goal using Hsym (from left to right).
An exact proof term for the current goal is Hlt0.
∎