Let seq be given.

Assume Hseq: sequence_on seq X.

Assume Hcauchy: cauchy_sequence X (discrete_metric X) seq.

We prove the intermediate claim Htail: ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun (discrete_metric X) (apply_fun seq m,apply_fun seq n)) eps.

An exact proof term for the current goal is (andER (metric_on X (discrete_metric X) ∧ sequence_on seq X) (∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun (discrete_metric X) (apply_fun seq m,apply_fun seq n)) eps) Hcauchy).

We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun (discrete_metric X) (apply_fun seq m,apply_fun seq n)) 1.

An exact proof term for the current goal is (Htail 1 (andI (1 ∈ R) (Rlt 0 1) real_1 Rlt_0_1)).

Set N to be the term Eps_i (λN0 : set ⇒ N0 ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → Rlt (apply_fun (discrete_metric X) (apply_fun seq m,apply_fun seq n)) 1).

We prove the intermediate claim HNprop: N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun (discrete_metric X) (apply_fun seq m,apply_fun seq n)) 1.

An exact proof term for the current goal is (Eps_i_ex (λN0 : set ⇒ N0 ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → Rlt (apply_fun (discrete_metric X) (apply_fun seq m,apply_fun seq n)) 1) HexN).

We prove the intermediate claim HNomega: N ∈ ω.

An exact proof term for the current goal is (andEL (N ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun (discrete_metric X) (apply_fun seq m,apply_fun seq n)) 1) HNprop).

We prove the intermediate claim HNtail: ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun (discrete_metric X) (apply_fun seq m,apply_fun seq n)) 1.

An exact proof term for the current goal is (andER (N ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun (discrete_metric X) (apply_fun seq m,apply_fun seq n)) 1) HNprop).

Set x0 to be the term apply_fun seq N.

We prove the intermediate claim Hx0X: x0 ∈ X.

An exact proof term for the current goal is (Hseq N HNomega).

We prove the intermediate claim Heventually_const: ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n = x0.

Let n be given.

Assume HnO: n ∈ ω.

Assume HNn: N ⊆ n.

We prove the intermediate claim HNN: N ⊆ N.

An exact proof term for the current goal is (Subq_ref N).

We prove the intermediate claim Hlt: Rlt (apply_fun (discrete_metric X) (apply_fun seq N,apply_fun seq n)) 1.

An exact proof term for the current goal is (HNtail N n HNomega HnO HNN HNn).

Set a to be the term apply_fun seq N.

Set b to be the term apply_fun seq n.

We prove the intermediate claim HaX: a ∈ X.

An exact proof term for the current goal is (Hseq N HNomega).

We prove the intermediate claim HbX: b ∈ X.

An exact proof term for the current goal is (Hseq n HnO).

We prove the intermediate claim Hlt': Rlt (If_i (a = b) 0 1) 1.

We will prove Rlt (If_i (a = b) 0 1) 1.

rewrite the current goal using (discrete_metric_apply X a b HaX HbX) (from right to left) at position 1.

An exact proof term for the current goal is Hlt.

Apply xm (a = b) to the current goal.

Assume Heq: a = b.

rewrite the current goal using Heq (from left to right).

Use reflexivity.

Assume Hneq: ¬ (a = b).

We prove the intermediate claim Hval: If_i (a = b) 0 1 = 1.

An exact proof term for the current goal is (If_i_0 (a = b) 0 1 Hneq).

Apply FalseE to the current goal.

We prove the intermediate claim Hbad: Rlt 1 1.

We will prove Rlt 1 1.

rewrite the current goal using Hval (from right to left) at position 1.

An exact proof term for the current goal is Hlt'.

An exact proof term for the current goal is ((not_Rlt_refl 1 real_1) Hbad).

We use x0 to witness the existential quantifier.

We will prove converges_to X (metric_topology X (discrete_metric X)) seq x0.

We will prove topology_on X (metric_topology X (discrete_metric X)) ∧ sequence_on seq X ∧ x0 ∈ X ∧ ∀U : set, U ∈ (metric_topology X (discrete_metric X)) → x0 ∈ U → ∃N0 : set, N0 ∈ ω ∧ ∀n : set, n ∈ ω → N0 ⊆ 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 (discrete_metric X) (discrete_metric_is_metric_on X)).

An exact proof term for the current goal is Hseq.

An exact proof term for the current goal is Hx0X.

Let U be given.

Assume HU: U ∈ metric_topology X (discrete_metric X).

Assume Hx0U: x0 ∈ U.

Set B to be the term famunion X (λx : set ⇒ {open_ball X (discrete_metric X) x r|r ∈ R, Rlt 0 r}).

We prove the intermediate claim HUsubX: U ⊆ X.

An exact proof term for the current goal is (PowerE X U (SepE1 (𝒫 X) (λU0 : set ⇒ ∀y0 ∈ U0, ∃b0 ∈ B, y0 ∈ b0 ∧ b0 ⊆ U0) U HU)).

We prove the intermediate claim HUref: ∀y0 ∈ U, ∃b0 ∈ B, y0 ∈ b0 ∧ b0 ⊆ U.

An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀y0 ∈ U0, ∃b0 ∈ B, y0 ∈ b0 ∧ b0 ⊆ U0) U HU).

We prove the intermediate claim Hexb: ∃b0 ∈ B, x0 ∈ b0 ∧ b0 ⊆ U.

An exact proof term for the current goal is (HUref x0 Hx0U).

Apply Hexb to the current goal.

Let b0 be given.

Assume Hb0.

We prove the intermediate claim Hb0B: b0 ∈ B.

An exact proof term for the current goal is (andEL (b0 ∈ B) (x0 ∈ b0 ∧ b0 ⊆ U) Hb0).

We prove the intermediate claim Hb0pack: x0 ∈ b0 ∧ b0 ⊆ U.

An exact proof term for the current goal is (andER (b0 ∈ B) (x0 ∈ b0 ∧ b0 ⊆ U) Hb0).

We prove the intermediate claim Hb0subU: b0 ⊆ U.

An exact proof term for the current goal is (andER (x0 ∈ b0) (b0 ⊆ U) Hb0pack).

We use N to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HNomega.

Let n be given.

Assume HnO: n ∈ ω.

Assume HNn: N ⊆ n.

We will prove apply_fun seq n ∈ U.

We prove the intermediate claim Heqnx0: apply_fun seq n = x0.

An exact proof term for the current goal is (Heventually_const n HnO HNn).

rewrite the current goal using Heqnx0 (from left to right).

An exact proof term for the current goal is (Hb0subU x0 (andEL (x0 ∈ b0) (b0 ⊆ U) Hb0pack)).