Let X be given.
We prove the intermediate claim Htop: topology_on X (finite_complement_topology X).
An exact proof term for the current goal is (finite_complement_topology_on X).
We will prove topology_on X (finite_complement_topology X) ∧ (∀F : set, F ⊆ X → finite F → closed_in X (finite_complement_topology X) F).
Apply andI to the current goal.
An exact proof term for the current goal is Htop.
Let F be given.
Assume HFsub: F ⊆ X.
Assume HFfin: finite F.
We will prove closed_in X (finite_complement_topology X) F.
We will prove topology_on X (finite_complement_topology X) ∧ (F ⊆ X ∧ ∃U ∈ finite_complement_topology X, F = X ∖ U).
Apply andI to the current goal.
An exact proof term for the current goal is Htop.
Apply andI to the current goal.
An exact proof term for the current goal is HFsub.
We use (X ∖ F) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HUpow: (X ∖ F) ∈ 𝒫 X.
An exact proof term for the current goal is (setminus_In_Power X F).
We prove the intermediate claim Hfin: finite (X ∖ (X ∖ F)).
rewrite the current goal using (setminus_setminus_eq X F HFsub) (from left to right).
An exact proof term for the current goal is HFfin.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) (X ∖ F) HUpow (orIL (finite (X ∖ (X ∖ F))) ((X ∖ F) = Empty) Hfin)).
rewrite the current goal using (setminus_setminus_eq X F HFsub) (from left to right).
Use reflexivity.
∎