Let X and Tx be given.
Assume Hfd: finite_dimensional_space X Tx.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (finite_dimensional_space_topology_on X Tx Hfd).
We prove the intermediate claim Hexm: ∃m : set, m ∈ ω ∧ ∀A : set, open_cover_of X Tx A → ∃B : set, open_cover_of X Tx B ∧ refines_cover B A ∧ collection_has_order_at_most_m_plus_one X B m.
An exact proof term for the current goal is (finite_dimensional_space_exists_bound X Tx Hfd).
Apply Hexm to the current goal.
Let m be given.
Assume Hmpack.
We prove the intermediate claim HmO: m ∈ ω.
An exact proof term for the current goal is (andEL (m ∈ ω) (∀A : set, open_cover_of X Tx A → ∃B : set, open_cover_of X Tx B ∧ refines_cover B A ∧ collection_has_order_at_most_m_plus_one X B m) Hmpack).
We prove the intermediate claim Hmprop: ∀A : set, open_cover_of X Tx A → ∃B : set, open_cover_of X Tx B ∧ refines_cover B A ∧ collection_has_order_at_most_m_plus_one X B m.
An exact proof term for the current goal is (andER (m ∈ ω) (∀A : set, open_cover_of X Tx A → ∃B : set, open_cover_of X Tx B ∧ refines_cover B A ∧ collection_has_order_at_most_m_plus_one X B m) Hmpack).
We use m to witness the existential quantifier.
We will prove covering_dimension X Tx m.
We will prove topology_on X Tx ∧ m ∈ ω ∧ ∀A : set, open_cover_of X Tx A → ∃B : set, open_cover_of X Tx B ∧ refines_cover B A ∧ collection_has_order_at_most_m_plus_one X B m.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HmO.
An exact proof term for the current goal is Hmprop.
∎