Let Xi, Ti, A and i be given.
Assume Htops: ∀j : set, j ∈ ω → topology_on (apply_fun Xi j) (apply_fun Ti j).
Assume HAcl: closed_in (coherent_union Xi) (coherent_topology Xi Ti) A.
Assume HiO: i ∈ ω.
Set X to be the term coherent_union Xi.
Set Tx to be the term coherent_topology Xi Ti.
Set Xi_i to be the term apply_fun Xi i.
Set Ti_i to be the term apply_fun Ti i.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (closed_in_topology X Tx A HAcl).
We prove the intermediate claim HTi: topology_on Xi_i Ti_i.
An exact proof term for the current goal is (Htops i HiO).
We prove the intermediate claim HexU: ∃U ∈ Tx, A = X ∖ U.
An exact proof term for the current goal is (closed_in_exists_open_complement X Tx A HAcl).
Apply HexU to the current goal.
Let U be given.
Assume HU: U ∈ Tx ∧ A = X ∖ U.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (A = X ∖ U) HU).
We prove the intermediate claim HAeq: A = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (A = X ∖ U) HU).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUinTx).
We prove the intermediate claim HXminusA: X ∖ A = U.
rewrite the current goal using HAeq (from left to right).
An exact proof term for the current goal is (setminus_setminus_eq X U HUsubX).
Set Ui to be the term Xi_i ∖ (A ∩ Xi_i).
We prove the intermediate claim HUiEq: Ui = U ∩ Xi_i.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ Ui.
We prove the intermediate claim HyXi: y ∈ Xi_i.
An exact proof term for the current goal is (setminusE1 Xi_i (A ∩ Xi_i) y Hy).
We prove the intermediate claim HyNot: y ∉ A ∩ Xi_i.
An exact proof term for the current goal is (setminusE2 Xi_i (A ∩ Xi_i) y Hy).
We prove the intermediate claim HyNotA: y ∉ A.
Assume HyA: y ∈ A.
Apply HyNot to the current goal.
An exact proof term for the current goal is (binintersectI A Xi_i y HyA HyXi).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (coherent_union_component_subset Xi i HiO y HyXi).
We prove the intermediate claim HyU: y ∈ U.
rewrite the current goal using HXminusA (from right to left).
An exact proof term for the current goal is (setminusI X A y HyX HyNotA).
An exact proof term for the current goal is (binintersectI U Xi_i y HyU HyXi).
Let y be given.
Assume Hy: y ∈ U ∩ Xi_i.
Apply binintersectE U Xi_i y Hy to the current goal.
Assume HyU HyXi.
We will prove y ∈ Ui.
Apply setminusI to the current goal.
An exact proof term for the current goal is HyXi.
Assume HyAx: y ∈ A ∩ Xi_i.
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE1 A Xi_i y HyAx).
We prove the intermediate claim HyNotU: y ∉ U.
We prove the intermediate claim HyXminusU: y ∈ X ∖ U.
rewrite the current goal using HAeq (from right to left).
An exact proof term for the current goal is HyA.
An exact proof term for the current goal is (setminusE2 X U y HyXminusU).
An exact proof term for the current goal is (HyNotU HyU).
We prove the intermediate claim HUiOpen: Ui ∈ Ti_i.
rewrite the current goal using HUiEq (from left to right).
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀j ∈ ω, (U0 ∩ apply_fun Xi j) ∈ apply_fun Ti j) U HUinTx i HiO).
We prove the intermediate claim Hclosed: closed_in Xi_i Ti_i (Xi_i ∖ Ui).
An exact proof term for the current goal is (closed_of_open_complement Xi_i Ti_i Ui HTi HUiOpen).
We prove the intermediate claim HcapSub: (A ∩ Xi_i) ⊆ Xi_i.
Let y be given.
Assume Hy: y ∈ A ∩ Xi_i.
An exact proof term for the current goal is (binintersectE2 A Xi_i y Hy).
We prove the intermediate claim Heq: Xi_i ∖ Ui = A ∩ Xi_i.
We prove the intermediate claim HUiDef: Ui = Xi_i ∖ (A ∩ Xi_i).
Use reflexivity.
rewrite the current goal using HUiDef (from left to right).
An exact proof term for the current goal is (setminus_setminus_eq Xi_i (A ∩ Xi_i) HcapSub).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hclosed.
∎