Assume HH: Hausdorff_space R R_finite_complement_topology.
We will prove False.
We prove the intermediate claim Hsep: ∀x1 x2 : set, x1 ∈ R → x2 ∈ R → x1 ≠ x2 → ∃U V : set, U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (topology_on R R_finite_complement_topology) (∀x1 x2 : set, x1 ∈ R → x2 ∈ R → x1 ≠ x2 → ∃U V : set, U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty) HH).
We prove the intermediate claim H01ne: 0 ≠ 1.
Assume H01eq: 0 = 1.
We prove the intermediate claim H00lt: 0 < 0.
rewrite the current goal using H01eq (from left to right) at position 2.
An exact proof term for the current goal is SNoLt_0_1.
An exact proof term for the current goal is ((SNoLt_irref 0) H00lt).
We prove the intermediate claim HUVex: ∃U V : set, U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology ∧ 0 ∈ U ∧ 1 ∈ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (Hsep 0 1 real_0 real_1 H01ne).
Apply HUVex to the current goal.
Let U be given.
Assume HVex: ∃V : set, U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology ∧ 0 ∈ U ∧ 1 ∈ V ∧ U ∩ V = Empty.
Apply HVex to the current goal.
Let V be given.
Assume HUV: U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology ∧ 0 ∈ U ∧ 1 ∈ V ∧ U ∩ V = Empty.
We prove the intermediate claim Hleft: (((U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology) ∧ 0 ∈ U) ∧ 1 ∈ V).
An exact proof term for the current goal is (andEL (((U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology) ∧ 0 ∈ U) ∧ 1 ∈ V) (U ∩ V = Empty) HUV).
We prove the intermediate claim HUVempty: U ∩ V = Empty.
An exact proof term for the current goal is (andER (((U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology) ∧ 0 ∈ U) ∧ 1 ∈ V) (U ∩ V = Empty) HUV).
We prove the intermediate claim Hleft2: ((U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology) ∧ 0 ∈ U).
An exact proof term for the current goal is (andEL ((U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology) ∧ 0 ∈ U) (1 ∈ V) Hleft).
We prove the intermediate claim H1V: 1 ∈ V.
An exact proof term for the current goal is (andER ((U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology) ∧ 0 ∈ U) (1 ∈ V) Hleft).
We prove the intermediate claim Hpair: (U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology).
An exact proof term for the current goal is (andEL (U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology) (0 ∈ U) Hleft2).
We prove the intermediate claim H0U: 0 ∈ U.
An exact proof term for the current goal is (andER (U ∈ R_finite_complement_topology ∧ V ∈ R_finite_complement_topology) (0 ∈ U) Hleft2).
We prove the intermediate claim HU: U ∈ R_finite_complement_topology.
An exact proof term for the current goal is (andEL (U ∈ R_finite_complement_topology) (V ∈ R_finite_complement_topology) Hpair).
We prove the intermediate claim HV: V ∈ R_finite_complement_topology.
An exact proof term for the current goal is (andER (U ∈ R_finite_complement_topology) (V ∈ R_finite_complement_topology) Hpair).
We prove the intermediate claim HUcases: 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 HUfin: finite (R ∖ U).
Apply (HUcases (finite (R ∖ U))) to the current goal.
Assume Hfin.
An exact proof term for the current goal is Hfin.
Assume HUe: U = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim H0Empty: 0 ∈ Empty.
rewrite the current goal using HUe (from right to left) at position 2.
An exact proof term for the current goal is H0U.
An exact proof term for the current goal is (EmptyE 0 H0Empty).
We prove the intermediate claim HVcases: finite (R ∖ V) ∨ V = Empty.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ finite (R ∖ U0) ∨ U0 = Empty) V HV).
We prove the intermediate claim HVfin: finite (R ∖ V).
Apply (HVcases (finite (R ∖ V))) to the current goal.
Assume Hfin.
An exact proof term for the current goal is Hfin.
Assume HVe: V = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim H1Empty: 1 ∈ Empty.
rewrite the current goal using HVe (from right to left) at position 2.
An exact proof term for the current goal is H1V.
An exact proof term for the current goal is (EmptyE 1 H1Empty).
We prove the intermediate claim HfinUnion: finite ((R ∖ U) ∪ (R ∖ V)).
An exact proof term for the current goal is (binunion_finite (R ∖ U) HUfin (R ∖ V) HVfin).
We prove the intermediate claim Hsub: R ∖ (U ∩ V) ⊆ (R ∖ U) ∪ (R ∖ V).
Let x be given.
Assume Hx: x ∈ R ∖ (U ∩ V).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (setminusE1 R (U ∩ V) x Hx).
We prove the intermediate claim HxNotUV: x ∉ (U ∩ V).
An exact proof term for the current goal is (setminusE2 R (U ∩ V) x Hx).
Apply (xm (x ∈ U)) to the current goal.
Assume HxU: x ∈ U.
We prove the intermediate claim HxNotV: x ∉ V.
Assume HxV: x ∈ V.
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
An exact proof term for the current goal is (HxNotUV HxUV).
We prove the intermediate claim HxRV: x ∈ R ∖ V.
An exact proof term for the current goal is (setminusI R V x HxR HxNotV).
An exact proof term for the current goal is (binunionI2 (R ∖ U) (R ∖ V) x HxRV).
Assume HxNotU: ¬ (x ∈ U).
We prove the intermediate claim HxRU: x ∈ R ∖ U.
An exact proof term for the current goal is (setminusI R U x HxR HxNotU).
An exact proof term for the current goal is (binunionI1 (R ∖ U) (R ∖ V) x HxRU).
We prove the intermediate claim HfinDiff: finite (R ∖ (U ∩ V)).
An exact proof term for the current goal is (Subq_finite ((R ∖ U) ∪ (R ∖ V)) HfinUnion (R ∖ (U ∩ V)) Hsub).
We prove the intermediate claim HfinR: finite R.
We prove the intermediate claim HeqR: R ∖ (U ∩ V) = R.
rewrite the current goal using HUVempty (from left to right).
rewrite the current goal using (setminus_Empty_eq R) (from left to right).
Use reflexivity.
rewrite the current goal using HeqR (from right to left).
An exact proof term for the current goal is HfinDiff.
An exact proof term for the current goal is (infinite_R HfinR).
∎