Let X and Tx be given.
Let m be given.
Assume Hman: m_manifold X Tx m.
Assume Hcomp: compact_space X Tx.
We will prove ∃N : set, ∃e : set, N ∈ ω ∧ N ≠ Empty ∧ embedding_of X Tx (euclidean_space N) (euclidean_topology N) e.
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 HmO: m ∈ ω.
An exact proof term for the current goal is (andER (Hausdorff_space X Tx ∧ second_countable_space X Tx) (m ∈ ω) Hman12).
We prove the intermediate claim HexEmb: ∃N : set, ∃e : set, N = add_nat (mul_nat two m) (Sing Empty) ∧ embedding_of X Tx (euclidean_space N) (euclidean_topology N) e.
An exact proof term for the current goal is (compact_m_manifold_embeds_R2mp1 X Tx m HmO Hcomp Hman).
Apply HexEmb to the current goal.
Let N be given.
Assume Hexe: ∃e : set, N = add_nat (mul_nat two m) (Sing Empty) ∧ embedding_of X Tx (euclidean_space N) (euclidean_topology N) e.
Apply Hexe to the current goal.
Let e be given.
Assume HNe: N = add_nat (mul_nat two m) (Sing Empty) ∧ embedding_of X Tx (euclidean_space N) (euclidean_topology N) e.
We use N to witness the existential quantifier.
We use e to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HNeq: N = add_nat (mul_nat two m) (Sing Empty).
An exact proof term for the current goal is (andEL (N = add_nat (mul_nat two m) (Sing Empty)) (embedding_of X Tx (euclidean_space N) (euclidean_topology N) e) HNe).
We prove the intermediate claim HmNat: nat_p m.
An exact proof term for the current goal is (omega_nat_p m HmO).
We prove the intermediate claim HtwoEq: two = 2.
Use reflexivity.
We prove the intermediate claim HtwoNat: nat_p two.
rewrite the current goal using HtwoEq (from left to right).
An exact proof term for the current goal is nat_2.
We prove the intermediate claim HoneEq: (Sing Empty) = 1.
We prove the intermediate claim Hsucc0eq1: ordsucc 0 = 1.
Use reflexivity.
rewrite the current goal using Hsucc0eq1 (from right to left).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (Sing Empty).
We prove the intermediate claim HxeqE: x = Empty.
An exact proof term for the current goal is (SingE Empty x Hx).
We prove the intermediate claim H0EqE: 0 = Empty.
Use reflexivity.
We prove the intermediate claim Hxeq0: x = 0.
rewrite the current goal using H0EqE (from right to left).
An exact proof term for the current goal is HxeqE.
rewrite the current goal using Hxeq0 (from left to right).
An exact proof term for the current goal is (ordsuccI2 0).
Let x be given.
Assume Hx: x ∈ ordsucc 0.
Apply (ordsuccE 0 x Hx (x ∈ Sing Empty)) to the current goal.
Assume Hx0: x ∈ 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE x) Hx0).
Assume Hxeq0: x = 0.
We prove the intermediate claim H0EqE: 0 = Empty.
Use reflexivity.
We prove the intermediate claim HxeqE: x = Empty.
rewrite the current goal using H0EqE (from left to right).
An exact proof term for the current goal is Hxeq0.
rewrite the current goal using HxeqE (from left to right).
An exact proof term for the current goal is (SingI Empty).
We prove the intermediate claim HoneNat: nat_p (Sing Empty).
rewrite the current goal using HoneEq (from left to right).
An exact proof term for the current goal is nat_1.
We prove the intermediate claim HmulNat: nat_p (mul_nat two m).
An exact proof term for the current goal is (mul_nat_p two HtwoNat m HmNat).
We prove the intermediate claim HaddNat: nat_p (add_nat (mul_nat two m) (Sing Empty)).
An exact proof term for the current goal is (add_nat_p (mul_nat two m) HmulNat (Sing Empty) HoneNat).
We prove the intermediate claim HNatN: nat_p N.
rewrite the current goal using HNeq (from left to right).
An exact proof term for the current goal is HaddNat.
An exact proof term for the current goal is (nat_p_omega N HNatN).
We prove the intermediate claim HNeq: N = add_nat (mul_nat two m) (Sing Empty).
An exact proof term for the current goal is (andEL (N = add_nat (mul_nat two m) (Sing Empty)) (embedding_of X Tx (euclidean_space N) (euclidean_topology N) e) HNe).
We prove the intermediate claim Hsucc0eq1: ordsucc 0 = 1.
Use reflexivity.
We prove the intermediate claim HoneEq: (Sing Empty) = 1.
We prove the intermediate claim Hsucc0eq1': ordsucc 0 = 1.
Use reflexivity.
rewrite the current goal using Hsucc0eq1' (from right to left).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (Sing Empty).
We prove the intermediate claim HxeqE: x = Empty.
An exact proof term for the current goal is (SingE Empty x Hx).
We prove the intermediate claim H0EqE: 0 = Empty.
Use reflexivity.
We prove the intermediate claim Hxeq0: x = 0.
rewrite the current goal using H0EqE (from right to left).
An exact proof term for the current goal is HxeqE.
rewrite the current goal using Hxeq0 (from left to right).
An exact proof term for the current goal is (ordsuccI2 0).
Let x be given.
Assume Hx: x ∈ ordsucc 0.
Apply (ordsuccE 0 x Hx (x ∈ Sing Empty)) to the current goal.
Assume Hx0: x ∈ 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE x) Hx0).
Assume Hxeq0: x = 0.
We prove the intermediate claim H0EqE: 0 = Empty.
Use reflexivity.
We prove the intermediate claim HxeqE: x = Empty.
rewrite the current goal using H0EqE (from left to right).
An exact proof term for the current goal is Hxeq0.
rewrite the current goal using HxeqE (from left to right).
An exact proof term for the current goal is (SingI Empty).
Set base to be the term mul_nat two m.
We prove the intermediate claim HbaseSucc: add_nat base (Sing Empty) = ordsucc (add_nat base 0).
rewrite the current goal using HoneEq (from left to right).
rewrite the current goal using Hsucc0eq1 (from right to left) at position 1.
An exact proof term for the current goal is (add_nat_SR base 0 nat_0).
We prove the intermediate claim HNsucc: N = ordsucc (add_nat base 0).
rewrite the current goal using HNeq (from left to right).
rewrite the current goal using HbaseSucc (from left to right).
Use reflexivity.
Assume HN0: N = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HtIn: (add_nat base 0) ∈ ordsucc (add_nat base 0).
An exact proof term for the current goal is (ordsuccI2 (add_nat base 0)).
We prove the intermediate claim HtN: (add_nat base 0) ∈ N.
rewrite the current goal using HNsucc (from left to right).
An exact proof term for the current goal is HtIn.
We prove the intermediate claim HtEmpty: (add_nat base 0) ∈ Empty.
rewrite the current goal using HN0 (from right to left) at position 2.
An exact proof term for the current goal is HtN.
An exact proof term for the current goal is ((EmptyE (add_nat base 0)) HtEmpty).
An exact proof term for the current goal is (andER (N = add_nat (mul_nat two m) (Sing Empty)) (embedding_of X Tx (euclidean_space N) (euclidean_topology N) e) HNe).
∎