Let X, Tx and m be given.
Assume Hman: m_manifold X Tx m.
We will prove locally_m_euclidean X Tx m.
We prove the intermediate claim Hparts: ((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).
An exact proof term for the current goal is Hman.
We prove the intermediate claim H123: (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) Hparts).
We prove the intermediate claim Hlocal: ∀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.
An exact proof term for the current goal is (andER ((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) Hparts).
We prove the intermediate claim H12: 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 ∈ ω) H123).
We prove the intermediate claim HHaus: Hausdorff_space X Tx.
An exact proof term for the current goal is (andEL (Hausdorff_space X Tx) (second_countable_space X Tx) H12).
We prove the intermediate claim Hmomega: m ∈ ω.
An exact proof term for the current goal is (andER (Hausdorff_space X Tx ∧ second_countable_space X Tx) (m ∈ ω) H123).
We prove the intermediate claim Htop: topology_on X Tx.
An exact proof term for the current goal is (Hausdorff_space_topology X Tx HHaus).
We prove the intermediate claim HeuTop: topology_on (euclidean_space m) (euclidean_topology m).
An exact proof term for the current goal is (Hausdorff_space_topology (euclidean_space m) (euclidean_topology m) (euclidean_space_Hausdorff m)).
We will prove (m ∈ ω ∧ topology_on X Tx) ∧ (∀x0 : set, x0 ∈ X → ∃U0 : set, ∃V0 : set, ∃f0 : set, open_in X Tx U0 ∧ x0 ∈ U0 ∧ V0 ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V0 ∧ homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0).
Apply andI to the current goal.
An exact proof term for the current goal is (andI (m ∈ ω) (topology_on X Tx) Hmomega Htop).
Let x0 be given.
Assume Hx0X: x0 ∈ X.
We will prove ∃U0 : set, ∃V0 : set, ∃f0 : set, open_in X Tx U0 ∧ x0 ∈ U0 ∧ V0 ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V0 ∧ homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0.
We prove the intermediate claim Hex: ∃U0 : set, U0 ∈ Tx ∧ x0 ∈ U0 ∧ ∃V0 : set, V0 ∈ (euclidean_topology m) ∧ ∃f0 : set, homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0.
An exact proof term for the current goal is (Hlocal x0 Hx0X).
Apply Hex to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Tx ∧ x0 ∈ U0 ∧ ∃V0 : set, V0 ∈ (euclidean_topology m) ∧ ∃f0 : set, homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0.
We prove the intermediate claim HU0pair: U0 ∈ Tx ∧ x0 ∈ U0.
An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ x0 ∈ U0) (∃V0 : set, V0 ∈ (euclidean_topology m) ∧ ∃f0 : set, homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0) HU0).
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (x0 ∈ U0) HU0pair).
We prove the intermediate claim Hx0U0: x0 ∈ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (x0 ∈ U0) HU0pair).
We prove the intermediate claim HexV: ∃V0 : set, V0 ∈ (euclidean_topology m) ∧ ∃f0 : set, homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0.
An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ x0 ∈ U0) (∃V0 : set, V0 ∈ (euclidean_topology m) ∧ ∃f0 : set, homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0) HU0).
Apply HexV to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ (euclidean_topology m) ∧ ∃f0 : set, homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0.
We prove the intermediate claim HV0open: V0 ∈ (euclidean_topology m).
An exact proof term for the current goal is (andEL (V0 ∈ (euclidean_topology m)) (∃f0 : set, homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0) HV0).
We prove the intermediate claim Hexf: ∃f0 : set, homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0.
An exact proof term for the current goal is (andER (V0 ∈ (euclidean_topology m)) (∃f0 : set, homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0) HV0).
Apply Hexf to the current goal.
Let f0 be given.
Assume Hhomeo: homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0.
We use U0 to witness the existential quantifier.
We use V0 to witness the existential quantifier.
We use f0 to witness the existential quantifier.
We prove the intermediate claim HU0open: open_in X Tx U0.
An exact proof term for the current goal is (open_inI X Tx U0 Htop HU0Tx).
We prove the intermediate claim HV0open_in: open_in (euclidean_space m) (euclidean_topology m) V0.
An exact proof term for the current goal is (open_inI (euclidean_space m) (euclidean_topology m) V0 HeuTop HV0open).
We prove the intermediate claim HV0sub: V0 ⊆ (euclidean_space m).
An exact proof term for the current goal is (open_in_subset (euclidean_space m) (euclidean_topology m) V0 HV0open_in).
We will prove open_in X Tx U0 ∧ x0 ∈ U0 ∧ V0 ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V0 ∧ homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU0open.
An exact proof term for the current goal is Hx0U0.
An exact proof term for the current goal is HV0sub.
An exact proof term for the current goal is HV0open_in.
An exact proof term for the current goal is Hhomeo.
∎