Let X, Tx and m be given.

Assume Hm: m ∈ ω.

Assume Hcomp: compact_space X Tx.

Assume Hman: m_manifold X Tx m.

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

∎