Let X and Tx be given.
Assume Hlc: locally_compact X Tx.
Assume HH: Hausdorff_space X Tx.
We will prove Baire_space X Tx.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (locally_compact_topology X Tx Hlc).
We prove the intermediate claim HlocB: ∀x : set, x ∈ X → ∃U : set, U ∈ Tx ∧ x ∈ U ∧ Baire_space U (subspace_topology X Tx U).
Let x be given.
Assume HxX: x ∈ X.
Apply (locally_compact_local X Tx x Hlc HxX) to the current goal.
Let U be given.
Assume HU: (U ∈ Tx ∧ x ∈ U) ∧ compact_space (closure_of X Tx U) (subspace_topology X Tx (closure_of X Tx U)).
We prove the intermediate claim HUx: U ∈ Tx ∧ x ∈ U.
An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x ∈ U) (compact_space (closure_of X Tx U) (subspace_topology X Tx (closure_of X Tx U))) HU).
We prove the intermediate claim HcompK: compact_space (closure_of X Tx U) (subspace_topology X Tx (closure_of X Tx U)).
An exact proof term for the current goal is (andER (U ∈ Tx ∧ x ∈ U) (compact_space (closure_of X Tx U) (subspace_topology X Tx (closure_of X Tx U))) HU).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (x ∈ U) HUx).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (x ∈ U) HUx).
Set K to be the term closure_of X Tx U.
Set Tk to be the term subspace_topology X Tx K.
We prove the intermediate claim HKsubX: K ⊆ X.
An exact proof term for the current goal is (closure_in_space X Tx U HTx).
We prove the intermediate claim HHK: Hausdorff_space K Tk.
An exact proof term for the current goal is (ex17_12_subspace_Hausdorff X Tx K HH HKsubX).
We prove the intermediate claim HBK: Baire_space K Tk.
An exact proof term for the current goal is (Baire_category_compact_Hausdorff K Tk HcompK HHK).
We prove the intermediate claim HTk: topology_on K Tk.
An exact proof term for the current goal is (compact_space_topology K Tk HcompK).
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 HUsubK: U ⊆ K.
An exact proof term for the current goal is (closure_contains_set X Tx U HTx HUsubX).
We prove the intermediate claim HUcapK: U ∩ K ∈ Tk.
An exact proof term for the current goal is (subspace_topologyI X Tx K U HUinTx).
We prove the intermediate claim HcapEq: U ∩ K = U.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ K.
An exact proof term for the current goal is (binintersectE1 U K y Hy).
Let y be given.
Assume Hy: y ∈ U.
An exact proof term for the current goal is (binintersectI U K y Hy (HUsubK y Hy)).
We prove the intermediate claim HUopenK: open_in K Tk U.
We will prove topology_on K Tk ∧ U ∈ Tk.
Apply andI to the current goal.
An exact proof term for the current goal is HTk.
rewrite the current goal using HcapEq (from right to left) at position 1.
An exact proof term for the current goal is HUcapK.
We prove the intermediate claim HBU: Baire_space U (subspace_topology K Tk U).
An exact proof term for the current goal is (Baire_open_subspace K Tk U HBK HUopenK).
We prove the intermediate claim HeqTop: subspace_topology K Tk U = subspace_topology X Tx U.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx K U HTx HKsubX HUsubK).
We prove the intermediate claim HBUx: Baire_space U (subspace_topology X Tx U).
rewrite the current goal using HeqTop (from right to left).
An exact proof term for the current goal is HBU.
We use U to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUinTx.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HBUx.
An exact proof term for the current goal is (ex48_4_locally_Baire_implies_Baire X Tx HTx HlocB).
∎