Let X, Tx and n be given.
Assume Hdim: covering_dimension X Tx n.
We prove the intermediate claim Hcore: topology_on X Tx ∧ n ∈ ω.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ n ∈ ω) (∀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 n) Hdim).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (n ∈ ω) Hcore).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (andER (topology_on X Tx) (n ∈ ω) Hcore).
We prove the intermediate claim Hprop: ∀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 n.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ n ∈ ω) (∀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 n) Hdim).
We will prove finite_dimensional_space X Tx.
We will prove topology_on X Tx ∧ ∃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.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HnO.
An exact proof term for the current goal is Hprop.
∎