Let X and Tx be given.

Assume Hcomp: compact_space X Tx.

Assume Hman: m_manifold X Tx (Sing Empty).

An exact proof term for the current goal is (compact_manifold_dimension_le X Tx (Sing Empty) Hman Hcomp).

∎