Let x be given.
Assume HxR: x ∈ R.
Let U be given.
Assume HU: U ∈ finite_complement_topology R.
Assume HxU: x ∈ U.
We will prove ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq_one_over_n n ∈ U.
We prove the intermediate claim HUpow: U ∈ 𝒫 R.
An exact proof term for the current goal is (SepE1 (𝒫 R) (λU0 : set ⇒ finite (R ∖ U0) ∨ U0 = Empty) U HU).
We prove the intermediate claim Hcases: finite (R ∖ U) ∨ U = Empty.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ finite (R ∖ U0) ∨ U0 = Empty) U HU).
We prove the intermediate claim HUne: U ≠ Empty.
Assume HUe: U = Empty.
We prove the intermediate claim HxEmpty: x ∈ Empty.
rewrite the current goal using HUe (from right to left).
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is (EmptyE x HxEmpty).
We prove the intermediate claim HF: finite (R ∖ U).
Apply Hcases to the current goal.
Assume Hfin.
An exact proof term for the current goal is Hfin.
Assume HUe.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HUne HUe).
Set F to be the term R ∖ U.
We prove the intermediate claim HF_def: F = R ∖ U.
Use reflexivity.
We prove the intermediate claim HF_fin: finite F.
rewrite the current goal using HF_def (from left to right).
An exact proof term for the current goal is HF.
We prove the intermediate claim Hbound: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq_one_over_n n ∉ F.
Apply (finite_ind (λA : set ⇒ ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq_one_over_n n ∉ A)) to the current goal.
We will prove ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq_one_over_n n ∉ Empty.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
Let n be given.
Assume Hn.
Assume Hsub.
An exact proof term for the current goal is (EmptyE (apply_fun seq_one_over_n n)).
Let A and y be given.
Assume HAfin: finite A.
Assume HynA: y ∉ A.
Assume HIA: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq_one_over_n n ∉ A.
We will prove ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq_one_over_n n ∉ (A ∪ {y}).
Apply HIA to the current goal.
Let N0 be given.
Assume HN0.
We prove the intermediate claim HN0o: N0 ∈ ω.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (∀n : set, n ∈ ω → N0 ⊆ n → apply_fun seq_one_over_n n ∉ A) HN0).
We prove the intermediate claim HN0prop: ∀n : set, n ∈ ω → N0 ⊆ n → apply_fun seq_one_over_n n ∉ A.
An exact proof term for the current goal is (andER (N0 ∈ ω) (∀n : set, n ∈ ω → N0 ⊆ n → apply_fun seq_one_over_n n ∉ A) HN0).
Apply (xm (∃k : set, k ∈ ω ∧ apply_fun seq_one_over_n k = y)) to the current goal.
Assume Hexk: ∃k : set, k ∈ ω ∧ apply_fun seq_one_over_n k = y.
Apply Hexk to the current goal.
Let k be given.
Assume Hkpair.
We prove the intermediate claim Hk: k ∈ ω.
An exact proof term for the current goal is (andEL (k ∈ ω) (apply_fun seq_one_over_n k = y) Hkpair).
We prove the intermediate claim Hkeq: apply_fun seq_one_over_n k = y.
An exact proof term for the current goal is (andER (k ∈ ω) (apply_fun seq_one_over_n k = y) Hkpair).
Set N to be the term ordsucc (N0 ∪ ordsucc k).
We use N to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hk1: ordsucc k ∈ ω.
An exact proof term for the current goal is (omega_ordsucc k Hk).
We prove the intermediate claim Hmax: N0 ∪ ordsucc k ∈ ω.
An exact proof term for the current goal is (omega_binunion N0 (ordsucc k) HN0o Hk1).
An exact proof term for the current goal is (omega_ordsucc (N0 ∪ ordsucc k) Hmax).
Let n be given.
Assume Hn: n ∈ ω.
Assume HNsub: N ⊆ n.
We will prove apply_fun seq_one_over_n n ∉ (A ∪ {y}).
We prove the intermediate claim HN0sub: N0 ⊆ n.
Let t be given.
Assume Ht: t ∈ N0.
We prove the intermediate claim HtN: t ∈ N.
We prove the intermediate claim Htmax: t ∈ (N0 ∪ ordsucc k).
An exact proof term for the current goal is (binunionI1 N0 (ordsucc k) t Ht).
An exact proof term for the current goal is (ordsuccI1 (N0 ∪ ordsucc k) t Htmax).
An exact proof term for the current goal is (HNsub t HtN).
We prove the intermediate claim HnotA: apply_fun seq_one_over_n n ∉ A.
An exact proof term for the current goal is (HN0prop n Hn HN0sub).
We prove the intermediate claim HkInN: k ∈ N.
We prove the intermediate claim HkInSk: k ∈ ordsucc k.
An exact proof term for the current goal is (ordsuccI2 k).
We prove the intermediate claim HkInMax: k ∈ (N0 ∪ ordsucc k).
An exact proof term for the current goal is (binunionI2 N0 (ordsucc k) k HkInSk).
An exact proof term for the current goal is (ordsuccI1 (N0 ∪ ordsucc k) k HkInMax).
We prove the intermediate claim HkInNn: k ∈ n.
An exact proof term for the current goal is (HNsub k HkInN).
We prove the intermediate claim Hneqnk: n ≠ k.
Assume Hnk: n = k.
We prove the intermediate claim Hkin: k ∈ k.
rewrite the current goal using Hnk (from right to left) at position 2.
An exact proof term for the current goal is HkInNn.
An exact proof term for the current goal is (In_irref k Hkin).
We prove the intermediate claim Hneqval: apply_fun seq_one_over_n n ≠ y.
Assume Hval: apply_fun seq_one_over_n n = y.
We prove the intermediate claim HnEqk: n = k.
We prove the intermediate claim Hkeq': y = apply_fun seq_one_over_n k.
We will prove y = apply_fun seq_one_over_n k.
Use symmetry.
An exact proof term for the current goal is Hkeq.
We prove the intermediate claim Heqnk: apply_fun seq_one_over_n n = apply_fun seq_one_over_n k.
An exact proof term for the current goal is (eq_i_tra (apply_fun seq_one_over_n n) y (apply_fun seq_one_over_n k) Hval Hkeq').
An exact proof term for the current goal is (seq_one_over_n_inj n k Hn Hk Heqnk).
An exact proof term for the current goal is (Hneqnk HnEqk).
Assume Hmem: apply_fun seq_one_over_n n ∈ (A ∪ {y}).
Apply (binunionE' A {y} (apply_fun seq_one_over_n n) False) to the current goal.
Assume HinA.
An exact proof term for the current goal is (HnotA HinA).
Assume HinSing.
We prove the intermediate claim Heqv: apply_fun seq_one_over_n n = y.
An exact proof term for the current goal is (SingE y (apply_fun seq_one_over_n n) HinSing).
An exact proof term for the current goal is (Hneqval Heqv).
An exact proof term for the current goal is Hmem.
Assume Hno: ¬ (∃k : set, k ∈ ω ∧ apply_fun seq_one_over_n k = y).
We use N0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN0o.
Let n be given.
Assume Hn: n ∈ ω.
Assume HN0sub: N0 ⊆ n.
We will prove apply_fun seq_one_over_n n ∉ (A ∪ {y}).
We prove the intermediate claim HnotA: apply_fun seq_one_over_n n ∉ A.
An exact proof term for the current goal is (HN0prop n Hn HN0sub).
We prove the intermediate claim Hnoty: apply_fun seq_one_over_n n ∉ {y}.
Assume Hin.
We prove the intermediate claim Heqv: apply_fun seq_one_over_n n = y.
An exact proof term for the current goal is (SingE y (apply_fun seq_one_over_n n) Hin).
Apply Hno to the current goal.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is Heqv.
Assume Hmem: apply_fun seq_one_over_n n ∈ (A ∪ {y}).
Apply (binunionE' A {y} (apply_fun seq_one_over_n n) False) to the current goal.
Assume HinA.
An exact proof term for the current goal is (HnotA HinA).
Assume HinS.
An exact proof term for the current goal is (Hnoty HinS).
An exact proof term for the current goal is Hmem.
An exact proof term for the current goal is HF_fin.
Apply Hbound to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HN: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → apply_fun seq_one_over_n n ∉ F) HNpair).
We prove the intermediate claim HNprop: ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq_one_over_n n ∉ F.
An exact proof term for the current goal is (andER (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → apply_fun seq_one_over_n n ∉ F) HNpair).
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN.
Let n be given.
Assume Hn: n ∈ ω.
Assume HNsub: N ⊆ n.
We prove the intermediate claim HvalR: apply_fun seq_one_over_n n ∈ R.
rewrite the current goal using (seq_one_over_n_apply n Hn) (from left to right).
An exact proof term for the current goal is (inv_nat_real (ordsucc n) (omega_ordsucc n Hn)).
We prove the intermediate claim HnotF: apply_fun seq_one_over_n n ∉ F.
An exact proof term for the current goal is (HNprop n Hn HNsub).
Apply (xm (apply_fun seq_one_over_n n ∈ U)) to the current goal.
Assume HvalU.
An exact proof term for the current goal is HvalU.
Assume HnotU: ¬ (apply_fun seq_one_over_n n ∈ U).
We prove the intermediate claim HinF: apply_fun seq_one_over_n n ∈ F.
We will prove apply_fun seq_one_over_n n ∈ F.
rewrite the current goal using HF_def (from left to right).
Apply setminusI to the current goal.
An exact proof term for the current goal is HvalR.
An exact proof term for the current goal is HnotU.
An exact proof term for the current goal is (FalseE (HnotF HinF) (apply_fun seq_one_over_n n ∈ U)).
∎