Let X, Tx and m be given.
Assume HmO: m ∈ ω.
Assume Hcomp: compact_space X Tx.
Assume Hman: m_manifold X Tx m.
We prove the intermediate claim Hman12: (Hausdorff_space X Tx ∧ second_countable_space X Tx) ∧ m ∈ ω.
An exact proof term for the current goal is (andEL ((Hausdorff_space X Tx ∧ second_countable_space X Tx) ∧ m ∈ ω) (∀x : set, x ∈ X → ∃U : set, U ∈ Tx ∧ x ∈ U ∧ ∃V : set, V ∈ (euclidean_topology m) ∧ ∃f : set, homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f) Hman).
We prove the intermediate claim Hman1: (Hausdorff_space X Tx ∧ second_countable_space X Tx).
An exact proof term for the current goal is (andEL (Hausdorff_space X Tx ∧ second_countable_space X Tx) (m ∈ ω) Hman12).
We prove the intermediate claim HH: Hausdorff_space X Tx.
An exact proof term for the current goal is (andEL (Hausdorff_space X Tx) (second_countable_space X Tx) Hman1).
We prove the intermediate claim Hscc: second_countable_space X Tx.
An exact proof term for the current goal is (andER (Hausdorff_space X Tx) (second_countable_space X Tx) Hman1).
We prove the intermediate claim Hnorm: normal_space X Tx.
An exact proof term for the current goal is (compact_Hausdorff_normal X Tx Hcomp HH).
We prove the intermediate claim Hreg: regular_space X Tx.
An exact proof term for the current goal is (normal_space_implies_regular X Tx Hnorm).
We prove the intermediate claim Hmet: metrizable X Tx.
An exact proof term for the current goal is (Urysohn_metrization_theorem X Tx Hreg Hscc).
We prove the intermediate claim Hdim: covering_dimension X Tx m.
An exact proof term for the current goal is (compact_m_manifold_dimension_le_m X Tx m HmO Hcomp Hman).
An exact proof term for the current goal is (Menger_Nobeling_embedding_full X Tx m Hcomp Hmet Hdim HmO).
∎