Let X and Tx be given.
Assume Hcase: (compact_space X Tx ∧ Hausdorff_space X Tx) ∨ (∃d : set, complete_metric_space X d ∧ Tx = metric_topology X d).
We will prove Baire_space X Tx.
Apply Hcase to the current goal.
Assume Hcomp: compact_space X Tx ∧ Hausdorff_space X Tx.
An exact proof term for the current goal is (Baire_category_compact_Hausdorff X Tx (andEL (compact_space X Tx) (Hausdorff_space X Tx) Hcomp) (andER (compact_space X Tx) (Hausdorff_space X Tx) Hcomp)).
Assume Hmet: ∃d : set, complete_metric_space X d ∧ Tx = metric_topology X d.
Apply Hmet to the current goal.
Let d be given.
Assume Hd: complete_metric_space X d ∧ Tx = metric_topology X d.
We prove the intermediate claim Hcomp: complete_metric_space X d.
An exact proof term for the current goal is (andEL (complete_metric_space X d) (Tx = metric_topology X d) Hd).
We prove the intermediate claim HtopEq: Tx = metric_topology X d.
An exact proof term for the current goal is (andER (complete_metric_space X d) (Tx = metric_topology X d) Hd).
rewrite the current goal using HtopEq (from left to right).
An exact proof term for the current goal is (Baire_category_complete_metric X d Hcomp).
∎