Let X, Tx, A and f be given.
Assume Hnorm: normal_space X Tx.
Assume HA: closed_in X Tx A.
Assume Hf: continuous_map A (subspace_topology X Tx A) (open_interval (minus_SNo 1) 1) (subspace_topology R R_standard_topology (open_interval (minus_SNo 1) 1)) f.
We will prove ∃g : set, continuous_map X Tx (open_interval (minus_SNo 1) 1) (subspace_topology R R_standard_topology (open_interval (minus_SNo 1) 1)) g ∧ (∀x : set, x ∈ A → apply_fun g x = apply_fun f x).
Set U to be the term open_interval (minus_SNo 1) 1.
Set Tu to be the term subspace_topology R R_standard_topology U.
Set I to be the term closed_interval (minus_SNo 1) 1.
Set Ti to be the term closed_interval_topology (minus_SNo 1) 1.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
We prove the intermediate claim HIsubR: I ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo 1) 1).
We prove the intermediate claim HUsubR: U ⊆ R.
Let y be given.
Assume Hy: y ∈ U.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) y Hy).
We prove the intermediate claim HUsubI: U ⊆ I.
Let y be given.
Assume Hy: y ∈ U.
We will prove y ∈ I.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) y Hy).
We prove the intermediate claim Hyconj: Rlt (minus_SNo 1) y ∧ Rlt y 1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) y Hy).
We prove the intermediate claim Hm1y: Rlt (minus_SNo 1) y.
An exact proof term for the current goal is (andEL (Rlt (minus_SNo 1) y) (Rlt y 1) Hyconj).
We prove the intermediate claim Hy1: Rlt y 1.
An exact proof term for the current goal is (andER (Rlt (minus_SNo 1) y) (Rlt y 1) Hyconj).
We prove the intermediate claim HIdef: I = {x0 ∈ R|¬ (Rlt x0 (minus_SNo 1)) ∧ ¬ (Rlt 1 x0)}.
Use reflexivity.
rewrite the current goal using HIdef (from left to right).
Apply (SepI R (λx0 : set ⇒ ¬ (Rlt x0 (minus_SNo 1)) ∧ ¬ (Rlt 1 x0)) y HyR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (not_Rlt_sym (minus_SNo 1) y Hm1y).
An exact proof term for the current goal is (not_Rlt_sym y 1 Hy1).
Set j to be the term {(y,y)|y ∈ U}.
We prove the intermediate claim HjR: continuous_map U Tu R R_standard_topology j.
An exact proof term for the current goal is (subspace_inclusion_continuous R R_standard_topology U R_standard_topology_is_topology_local HUsubR).
We prove the intermediate claim HjI: continuous_map U Tu I Ti j.
We prove the intermediate claim Hrng: ∀y : set, y ∈ U → apply_fun j y ∈ I.
Let y be given.
Assume HyU: y ∈ U.
rewrite the current goal using (identity_function_apply U y HyU) (from left to right).
An exact proof term for the current goal is (HUsubI y HyU).
An exact proof term for the current goal is (continuous_map_range_restrict U Tu R R_standard_topology j I HjR HIsubR Hrng).
Set fI to be the term compose_fun A f j.
We prove the intermediate claim HfI: continuous_map A (subspace_topology X Tx A) I Ti fI.
An exact proof term for the current goal is (composition_continuous A (subspace_topology X Tx A) U Tu I Ti f j Hf HjI).
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim Hm10: Rlt (minus_SNo 1) 0.
An exact proof term for the current goal is (RltI (minus_SNo 1) 0 Hm1R real_0 minus_1_lt_0).
We prove the intermediate claim Hm11: Rlt (minus_SNo 1) 1.
An exact proof term for the current goal is (Rlt_tra (minus_SNo 1) 0 1 Hm10 Rlt_0_1).
We prove the intermediate claim Hab: Rle (minus_SNo 1) 1.
An exact proof term for the current goal is (Rlt_implies_Rle (minus_SNo 1) 1 Hm11).
We prove the intermediate claim HexgI: ∃gI : set, continuous_map X Tx I Ti gI ∧ (∀x : set, x ∈ A → apply_fun gI x = apply_fun fI x).
An exact proof term for the current goal is (Tietze_extension_interval X Tx A (minus_SNo 1) 1 fI Hab Hnorm HA HfI).
Apply HexgI to the current goal.
Let gI be given.
Assume HgI.
We prove the intermediate claim HgIcont: continuous_map X Tx I Ti gI.
An exact proof term for the current goal is (andEL (continuous_map X Tx I Ti gI) (∀x : set, x ∈ A → apply_fun gI x = apply_fun fI x) HgI).
We prove the intermediate claim HgIeq: ∀x : set, x ∈ A → apply_fun gI x = apply_fun fI x.
An exact proof term for the current goal is (andER (continuous_map X Tx I Ti gI) (∀x : set, x ∈ A → apply_fun gI x = apply_fun fI x) HgI).
Set incI to be the term {(y,y)|y ∈ I}.
We prove the intermediate claim HincI: continuous_map I Ti R R_standard_topology incI.
An exact proof term for the current goal is (subspace_inclusion_continuous R R_standard_topology I R_standard_topology_is_topology_local HIsubR).
Set gR to be the term compose_fun X gI incI.
We prove the intermediate claim HgRcont: continuous_map X Tx R R_standard_topology gR.
An exact proof term for the current goal is (composition_continuous X Tx I Ti R R_standard_topology gI incI HgIcont HincI).
We prove the intermediate claim HgR_eq_on_A: ∀x : set, x ∈ A → apply_fun gR x = apply_fun f x.
Let x be given.
Assume HxA: x ∈ A.
We will prove apply_fun gR x = apply_fun f x.
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HA).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate claim Hcomp: apply_fun gR x = apply_fun incI (apply_fun gI x).
rewrite the current goal using (compose_fun_apply X gI incI x HxX) (from left to right).
Use reflexivity.
rewrite the current goal using Hcomp (from left to right).
rewrite the current goal using (HgIeq x HxA) (from left to right).
We prove the intermediate claim HfunfI: function_on fI A I.
An exact proof term for the current goal is (continuous_map_function_on A (subspace_topology X Tx A) I Ti fI HfI).
We prove the intermediate claim HfIxI: apply_fun fI x ∈ I.
An exact proof term for the current goal is (HfunfI x HxA).
rewrite the current goal using (identity_function_apply I (apply_fun fI x) HfIxI) (from left to right).
We prove the intermediate claim HcompfI: apply_fun fI x = apply_fun j (apply_fun f x).
rewrite the current goal using (compose_fun_apply A f j x HxA) (from left to right).
Use reflexivity.
rewrite the current goal using HcompfI (from left to right).
We prove the intermediate claim Hfunf: function_on f A U.
An exact proof term for the current goal is (continuous_map_function_on A (subspace_topology X Tx A) U Tu f Hf).
We prove the intermediate claim HfxU: apply_fun f x ∈ U.
An exact proof term for the current goal is (Hfunf x HxA).
rewrite the current goal using (identity_function_apply U (apply_fun f x) HfxU) (from left to right).
Use reflexivity.
Set Dm1 to be the term preimage_of X gR {minus_SNo 1}.
Set D1 to be the term preimage_of X gR {1}.
Set D to be the term Dm1 ∪ D1.
We prove the intermediate claim Hm1closed: closed_in R R_standard_topology {minus_SNo 1}.
An exact proof term for the current goal is (Hausdorff_singletons_closed R R_standard_topology (minus_SNo 1) R_standard_topology_Hausdorff Hm1R).
We prove the intermediate claim H1closed: closed_in R R_standard_topology {1}.
An exact proof term for the current goal is (Hausdorff_singletons_closed R R_standard_topology 1 R_standard_topology_Hausdorff real_1).
We prove the intermediate claim HDm1cl: closed_in X Tx Dm1.
An exact proof term for the current goal is (continuous_map_preimage_closed X Tx R R_standard_topology gR {minus_SNo 1} HgRcont Hm1closed).
We prove the intermediate claim HD1cl: closed_in X Tx D1.
An exact proof term for the current goal is (continuous_map_preimage_closed X Tx R R_standard_topology gR {1} HgRcont H1closed).
We prove the intermediate claim HDcl: closed_in X Tx D.
An exact proof term for the current goal is (union_of_closed_is_closed X Tx Dm1 D1 HTx HDm1cl HD1cl).
We prove the intermediate claim Hdisj: D ∩ A = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ D ∩ A.
We will prove x ∈ Empty.
We prove the intermediate claim HxD: x ∈ D.
An exact proof term for the current goal is (binintersectE1 D A x Hx).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE2 D A x Hx).
Apply (binunionE' Dm1 D1 x (x ∈ Empty)) to the current goal.
Assume HxDm1: x ∈ Dm1.
We prove the intermediate claim HgRx: apply_fun gR x ∈ {minus_SNo 1}.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun gR u ∈ {minus_SNo 1}) x HxDm1).
We prove the intermediate claim HgReq: apply_fun gR x = minus_SNo 1.
An exact proof term for the current goal is (SingE (minus_SNo 1) (apply_fun gR x) HgRx).
We prove the intermediate claim Hgxfx: apply_fun gR x = apply_fun f x.
An exact proof term for the current goal is (HgR_eq_on_A x HxA).
We prove the intermediate claim HfxU: apply_fun f x ∈ U.
We prove the intermediate claim Hfunf: function_on f A U.
An exact proof term for the current goal is (continuous_map_function_on A (subspace_topology X Tx A) U Tu f Hf).
An exact proof term for the current goal is (Hfunf x HxA).
We prove the intermediate claim Hfxconj: Rlt (minus_SNo 1) (apply_fun f x) ∧ Rlt (apply_fun f x) 1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) (apply_fun f x) HfxU).
We prove the intermediate claim Hlt: Rlt (minus_SNo 1) (apply_fun f x).
An exact proof term for the current goal is (andEL (Rlt (minus_SNo 1) (apply_fun f x)) (Rlt (apply_fun f x) 1) Hfxconj).
We prove the intermediate claim HfxEq: apply_fun f x = minus_SNo 1.
rewrite the current goal using Hgxfx (from right to left) at position 1.
An exact proof term for the current goal is HgReq.
We prove the intermediate claim Hltself: Rlt (minus_SNo 1) (minus_SNo 1).
rewrite the current goal using HfxEq (from right to left) at position 2.
An exact proof term for the current goal is Hlt.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((not_Rlt_refl (minus_SNo 1) Hm1R) Hltself).
Assume HxD1: x ∈ D1.
We prove the intermediate claim HgRx: apply_fun gR x ∈ {1}.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun gR u ∈ {1}) x HxD1).
We prove the intermediate claim HgReq: apply_fun gR x = 1.
An exact proof term for the current goal is (SingE 1 (apply_fun gR x) HgRx).
We prove the intermediate claim Hgxfx: apply_fun gR x = apply_fun f x.
An exact proof term for the current goal is (HgR_eq_on_A x HxA).
We prove the intermediate claim HfxU: apply_fun f x ∈ U.
We prove the intermediate claim Hfunf: function_on f A U.
An exact proof term for the current goal is (continuous_map_function_on A (subspace_topology X Tx A) U Tu f Hf).
An exact proof term for the current goal is (Hfunf x HxA).
We prove the intermediate claim Hfxconj: Rlt (minus_SNo 1) (apply_fun f x) ∧ Rlt (apply_fun f x) 1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) (apply_fun f x) HfxU).
We prove the intermediate claim Hlt: Rlt (apply_fun f x) 1.
An exact proof term for the current goal is (andER (Rlt (minus_SNo 1) (apply_fun f x)) (Rlt (apply_fun f x) 1) Hfxconj).
We prove the intermediate claim HfxEq: apply_fun f x = 1.
rewrite the current goal using Hgxfx (from right to left) at position 1.
An exact proof term for the current goal is HgReq.
We prove the intermediate claim Hltself: Rlt 1 1.
rewrite the current goal using HfxEq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((not_Rlt_refl 1 real_1) Hltself).
An exact proof term for the current goal is HxD.
Let x be given.
Assume Hx: x ∈ Empty.
We will prove x ∈ D ∩ A.
An exact proof term for the current goal is (EmptyE x Hx (x ∈ D ∩ A)).
We prove the intermediate claim Hab01: Rle 0 1.
An exact proof term for the current goal is (Rlt_implies_Rle 0 1 Rlt_0_1).
We prove the intermediate claim Hexphi: ∃phiI : set, continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) phiI ∧ (∀x : set, x ∈ D → apply_fun phiI x = 0) ∧ (∀x : set, x ∈ A → apply_fun phiI x = 1).
An exact proof term for the current goal is (Urysohn_lemma X Tx D A 0 1 Hab01 Hnorm HDcl HA Hdisj).
Apply Hexphi to the current goal.
Let phiI be given.
Assume Hphi.
We prove the intermediate claim Hphi12: continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) phiI ∧ (∀x : set, x ∈ D → apply_fun phiI x = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) phiI ∧ (∀x : set, x ∈ D → apply_fun phiI x = 0)) (∀x : set, x ∈ A → apply_fun phiI x = 1) Hphi).
We prove the intermediate claim HphiContI: continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) phiI.
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) phiI) (∀x : set, x ∈ D → apply_fun phiI x = 0) Hphi12).
We prove the intermediate claim HphiD0: ∀x : set, x ∈ D → apply_fun phiI x = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) phiI) (∀x : set, x ∈ D → apply_fun phiI x = 0) Hphi12).
We prove the intermediate claim HphiA1: ∀x : set, x ∈ A → apply_fun phiI x = 1.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) phiI ∧ (∀x : set, x ∈ D → apply_fun phiI x = 0)) (∀x : set, x ∈ A → apply_fun phiI x = 1) Hphi).
Set I01 to be the term closed_interval 0 1.
Set T01 to be the term closed_interval_topology 0 1.
We prove the intermediate claim HI01subR: I01 ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R 0 1).
Set inc01 to be the term {(y,y)|y ∈ I01}.
We prove the intermediate claim Hinc01: continuous_map I01 T01 R R_standard_topology inc01.
An exact proof term for the current goal is (subspace_inclusion_continuous R R_standard_topology I01 R_standard_topology_is_topology_local HI01subR).
Set phiR to be the term compose_fun X phiI inc01.
We prove the intermediate claim HphiRcont: continuous_map X Tx R R_standard_topology phiR.
An exact proof term for the current goal is (composition_continuous X Tx I01 T01 R R_standard_topology phiI inc01 HphiContI Hinc01).
Set hR to be the term compose_fun X (pair_map X phiR gR) mul_fun_R.
We prove the intermediate claim HhRcont: continuous_map X Tx R R_standard_topology hR.
An exact proof term for the current goal is (mul_two_continuous_R X Tx phiR gR HTx HphiRcont HgRcont).
We prove the intermediate claim HhRinU: ∀x : set, x ∈ X → apply_fun hR x ∈ U.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun hR x ∈ U.
Set p to be the term apply_fun phiR x.
Set t to be the term apply_fun gR x.
We prove the intermediate claim HpR: p ∈ R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology phiR HphiRcont x HxX).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology gR HgRcont x HxX).
We prove the intermediate claim HpS: SNo p.
An exact proof term for the current goal is (real_SNo p HpR).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
Set hval to be the term apply_fun hR x.
We prove the intermediate claim HpairRR: (p,t) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R p t HpR HtR).
We prove the intermediate claim HhvalEq: hval = mul_SNo p t.
rewrite the current goal using (compose_fun_apply X (pair_map X phiR gR) mul_fun_R x HxX) (from left to right).
rewrite the current goal using (pair_map_apply X R R phiR gR x HxX) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod R R) (λq : set ⇒ mul_SNo (q 0) (q 1)) (p,t) HpairRR) (from left to right).
rewrite the current goal using (tuple_2_0_eq p t) (from left to right).
rewrite the current goal using (tuple_2_1_eq p t) (from left to right).
Use reflexivity.
We prove the intermediate claim HmulR: mul_SNo p t ∈ R.
An exact proof term for the current goal is (real_mul_SNo p HpR t HtR).
Apply (xm (x ∈ D)) to the current goal.
Assume HxD: x ∈ D.
We will prove hval ∈ U.
We prove the intermediate claim HphiIx0: apply_fun phiI x = 0.
An exact proof term for the current goal is (HphiD0 x HxD).
We prove the intermediate claim HphiFun: function_on phiI X I01.
An exact proof term for the current goal is (continuous_map_function_on X Tx I01 T01 phiI HphiContI).
We prove the intermediate claim HphiIxI01: apply_fun phiI x ∈ I01.
An exact proof term for the current goal is (HphiFun x HxX).
We prove the intermediate claim HphiRval: p = apply_fun phiI x.
We will prove apply_fun phiR x = apply_fun phiI x.
rewrite the current goal using (compose_fun_apply X phiI inc01 x HxX) (from left to right).
rewrite the current goal using (identity_function_apply I01 (apply_fun phiI x) HphiIxI01) (from left to right).
Use reflexivity.
We prove the intermediate claim Hp0: p = 0.
rewrite the current goal using HphiRval (from left to right).
An exact proof term for the current goal is HphiIx0.
rewrite the current goal using HhvalEq (from left to right).
rewrite the current goal using Hp0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL t HtS) (from left to right).
We prove the intermediate claim HUdef: U = {y0 ∈ R|Rlt (minus_SNo 1) y0 ∧ Rlt y0 1}.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
Apply (SepI R (λy0 : set ⇒ Rlt (minus_SNo 1) y0 ∧ Rlt y0 1) 0 real_0) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (RltI (minus_SNo 1) 0 Hm1R real_0 minus_1_lt_0).
An exact proof term for the current goal is Rlt_0_1.
Assume HxNotD: ¬ (x ∈ D).
We will prove hval ∈ U.
We prove the intermediate claim HgIfun: function_on gI X I.
An exact proof term for the current goal is (continuous_map_function_on X Tx I Ti gI HgIcont).
We prove the intermediate claim HgIxI: apply_fun gI x ∈ I.
An exact proof term for the current goal is (HgIfun x HxX).
We prove the intermediate claim HgRval: t = apply_fun gI x.
We will prove apply_fun gR x = apply_fun gI x.
rewrite the current goal using (compose_fun_apply X gI incI x HxX) (from left to right).
rewrite the current goal using (identity_function_apply I (apply_fun gI x) HgIxI) (from left to right).
Use reflexivity.
We prove the intermediate claim HtI: t ∈ I.
rewrite the current goal using HgRval (from left to right).
An exact proof term for the current goal is HgIxI.
We prove the intermediate claim HtIdef: I = {y0 ∈ R|¬ (Rlt y0 (minus_SNo 1)) ∧ ¬ (Rlt 1 y0)}.
Use reflexivity.
We prove the intermediate claim HtIsep: t ∈ {y0 ∈ R|¬ (Rlt y0 (minus_SNo 1)) ∧ ¬ (Rlt 1 y0)}.
rewrite the current goal using HtIdef (from left to right).
An exact proof term for the current goal is HtI.
We prove the intermediate claim Htconj: ¬ (Rlt t (minus_SNo 1)) ∧ ¬ (Rlt 1 t).
An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ ¬ (Rlt y0 (minus_SNo 1)) ∧ ¬ (Rlt 1 y0)) t HtIsep).
We prove the intermediate claim Htge_m1: ¬ (Rlt t (minus_SNo 1)).
An exact proof term for the current goal is (andEL (¬ (Rlt t (minus_SNo 1))) (¬ (Rlt 1 t)) Htconj).
We prove the intermediate claim Htle_1: ¬ (Rlt 1 t).
An exact proof term for the current goal is (andER (¬ (Rlt t (minus_SNo 1))) (¬ (Rlt 1 t)) Htconj).
We prove the intermediate claim HtR2: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λy0 : set ⇒ ¬ (Rlt y0 (minus_SNo 1)) ∧ ¬ (Rlt 1 y0)) t HtIsep).
We prove the intermediate claim HxNotDm1: ¬ (x ∈ Dm1).
Assume HxDm1: x ∈ Dm1.
Apply HxNotD to the current goal.
An exact proof term for the current goal is (binunionI1 Dm1 D1 x HxDm1).
We prove the intermediate claim HxNotD1: ¬ (x ∈ D1).
Assume HxD1: x ∈ D1.
Apply HxNotD to the current goal.
An exact proof term for the current goal is (binunionI2 Dm1 D1 x HxD1).
We prove the intermediate claim Hneq_m1: ¬ (t = minus_SNo 1).
Assume Heq: t = minus_SNo 1.
Apply HxNotDm1 to the current goal.
We prove the intermediate claim HDm1def: Dm1 = {u ∈ X|apply_fun gR u ∈ {minus_SNo 1}}.
Use reflexivity.
rewrite the current goal using HDm1def (from left to right).
Apply (SepI X (λu : set ⇒ apply_fun gR u ∈ {minus_SNo 1}) x HxX) to the current goal.
We prove the intermediate claim Htdef: t = apply_fun gR x.
Use reflexivity.
rewrite the current goal using Htdef (from right to left).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SingI (minus_SNo 1)).
We prove the intermediate claim Hneq_1: ¬ (t = 1).
Assume Heq: t = 1.
Apply HxNotD1 to the current goal.
We prove the intermediate claim HD1def: D1 = {u ∈ X|apply_fun gR u ∈ {1}}.
Use reflexivity.
rewrite the current goal using HD1def (from left to right).
Apply (SepI X (λu : set ⇒ apply_fun gR u ∈ {1}) x HxX) to the current goal.
We prove the intermediate claim Htdef: t = apply_fun gR x.
Use reflexivity.
rewrite the current goal using Htdef (from right to left).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SingI 1).
We prove the intermediate claim Hm1le_t: Rle (minus_SNo 1) t.
Apply (RleI (minus_SNo 1) t Hm1R HtR2) to the current goal.
An exact proof term for the current goal is Htge_m1.
We prove the intermediate claim Ht_le1: Rle t 1.
Apply (RleI t 1 HtR2 real_1) to the current goal.
An exact proof term for the current goal is Htle_1.
We prove the intermediate claim Hm1lt_t: Rlt (minus_SNo 1) t.
We prove the intermediate claim HneqL: ¬ (minus_SNo 1 = t).
Assume Heq: minus_SNo 1 = t.
Apply Hneq_m1 to the current goal.
rewrite the current goal using Heq (from right to left).
Use reflexivity.
An exact proof term for the current goal is (Rle_neq_implies_Rlt (minus_SNo 1) t Hm1le_t HneqL).
We prove the intermediate claim Htlt1: Rlt t 1.
An exact proof term for the current goal is (Rle_neq_implies_Rlt t 1 Ht_le1 Hneq_1).
We prove the intermediate claim Hm1lt_tS: minus_SNo 1 < t.
An exact proof term for the current goal is (RltE_lt (minus_SNo 1) t Hm1lt_t).
We prove the intermediate claim Htlt1S: t < 1.
An exact proof term for the current goal is (RltE_lt t 1 Htlt1).
We prove the intermediate claim HpI01: p ∈ I01.
We prove the intermediate claim HphiFun: function_on phiI X I01.
An exact proof term for the current goal is (continuous_map_function_on X Tx I01 T01 phiI HphiContI).
We prove the intermediate claim HphiIxI01: apply_fun phiI x ∈ I01.
An exact proof term for the current goal is (HphiFun x HxX).
We prove the intermediate claim HphiRval: p = apply_fun phiI x.
We will prove apply_fun phiR x = apply_fun phiI x.
rewrite the current goal using (compose_fun_apply X phiI inc01 x HxX) (from left to right).
rewrite the current goal using (identity_function_apply I01 (apply_fun phiI x) HphiIxI01) (from left to right).
Use reflexivity.
rewrite the current goal using HphiRval (from left to right).
An exact proof term for the current goal is HphiIxI01.
We prove the intermediate claim HpI01def: I01 = {y0 ∈ R|¬ (Rlt y0 0) ∧ ¬ (Rlt 1 y0)}.
Use reflexivity.
We prove the intermediate claim HpI01sep: p ∈ {y0 ∈ R|¬ (Rlt y0 0) ∧ ¬ (Rlt 1 y0)}.
rewrite the current goal using HpI01def (from left to right).
An exact proof term for the current goal is HpI01.
We prove the intermediate claim Hpconj: ¬ (Rlt p 0) ∧ ¬ (Rlt 1 p).
An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ ¬ (Rlt y0 0) ∧ ¬ (Rlt 1 y0)) p HpI01sep).
We prove the intermediate claim Hpnotlt0: ¬ (Rlt p 0).
An exact proof term for the current goal is (andEL (¬ (Rlt p 0)) (¬ (Rlt 1 p)) Hpconj).
We prove the intermediate claim Hpnotgt1: ¬ (Rlt 1 p).
An exact proof term for the current goal is (andER (¬ (Rlt p 0)) (¬ (Rlt 1 p)) Hpconj).
rewrite the current goal using HhvalEq (from left to right).
We prove the intermediate claim HUdef: U = {y0 ∈ R|Rlt (minus_SNo 1) y0 ∧ Rlt y0 1}.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
Apply (SepI R (λy0 : set ⇒ Rlt (minus_SNo 1) y0 ∧ Rlt y0 1) (mul_SNo p t) HmulR) to the current goal.
Apply andI to the current goal.
Apply (SNoLt_trichotomy_or_impred p 0 HpS SNo_0 (Rlt (minus_SNo 1) (mul_SNo p t))) to the current goal.
Assume Hplt0: p < 0.
Apply FalseE to the current goal.
We prove the intermediate claim HpRlt0: Rlt p 0.
An exact proof term for the current goal is (RltI p 0 HpR real_0 Hplt0).
An exact proof term for the current goal is (Hpnotlt0 HpRlt0).
Assume Hpeq0: p = 0.
rewrite the current goal using Hpeq0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL t HtS) (from left to right).
An exact proof term for the current goal is (RltI (minus_SNo 1) 0 Hm1R real_0 minus_1_lt_0).
Assume H0ltp: 0 < p.
Apply (SNoLt_trichotomy_or_impred t 0 HtS SNo_0 (Rlt (minus_SNo 1) (mul_SNo p t))) to the current goal.
Assume Htlt0: t < 0.
Apply (SNoLt_trichotomy_or_impred p 1 HpS SNo_1 (Rlt (minus_SNo 1) (mul_SNo p t))) to the current goal.
Assume Hplt1: p < 1.
We prove the intermediate claim Hple1: p ≤ 1.
An exact proof term for the current goal is (SNoLtLe p 1 Hplt1).
We prove the intermediate claim HtLe0: t ≤ 0.
An exact proof term for the current goal is (SNoLtLe t 0 Htlt0).
We prove the intermediate claim Htpt_ge: t ≤ mul_SNo p t.
We prove the intermediate claim H1S: SNo 1.
An exact proof term for the current goal is SNo_1.
We prove the intermediate claim Hcomm: mul_SNo p t = mul_SNo t p.
An exact proof term for the current goal is (mul_SNo_com p t HpS HtS).
rewrite the current goal using Hcomm (from left to right).
We prove the intermediate claim Hineq: mul_SNo t 1 ≤ mul_SNo t p.
An exact proof term for the current goal is (nonpos_mul_SNo_Le t 1 p HtS HtLe0 H1S HpS Hple1).
We prove the intermediate claim Hineq2: t ≤ mul_SNo t p.
rewrite the current goal using (mul_SNo_oneR t HtS) (from right to left) at position 1.
An exact proof term for the current goal is Hineq.
An exact proof term for the current goal is Hineq2.
We prove the intermediate claim Hm1lt_tS2: minus_SNo 1 < t.
An exact proof term for the current goal is Hm1lt_tS.
We prove the intermediate claim Hm1lt_ptS: minus_SNo 1 < mul_SNo p t.
An exact proof term for the current goal is (SNoLtLe_tra (minus_SNo 1) t (mul_SNo p t) (SNo_minus_SNo 1 SNo_1) HtS (SNo_mul_SNo p t HpS HtS) Hm1lt_tS2 Htpt_ge).
An exact proof term for the current goal is (RltI (minus_SNo 1) (mul_SNo p t) Hm1R HmulR Hm1lt_ptS).
Assume Hpeq1: p = 1.
rewrite the current goal using Hpeq1 (from left to right).
rewrite the current goal using (mul_SNo_oneL t HtS) (from left to right).
An exact proof term for the current goal is Hm1lt_t.
Assume H1ltp: 1 < p.
Apply FalseE to the current goal.
We prove the intermediate claim H1ltpR: Rlt 1 p.
An exact proof term for the current goal is (RltI 1 p real_1 HpR H1ltp).
An exact proof term for the current goal is (Hpnotgt1 H1ltpR).
Assume Hteq0: t = 0.
rewrite the current goal using Hteq0 (from left to right).
rewrite the current goal using (mul_SNo_zeroR p HpS) (from left to right).
An exact proof term for the current goal is (RltI (minus_SNo 1) 0 Hm1R real_0 minus_1_lt_0).
Assume H0ltt: 0 < t.
We prove the intermediate claim H0le_pt: 0 ≤ mul_SNo p t.
An exact proof term for the current goal is (SNoLtLe 0 (mul_SNo p t) (mul_SNo_pos_pos p t HpS HtS H0ltp H0ltt)).
We prove the intermediate claim Hm10S: minus_SNo 1 < 0.
An exact proof term for the current goal is minus_1_lt_0.
We prove the intermediate claim Hm1lt_ptS: minus_SNo 1 < mul_SNo p t.
An exact proof term for the current goal is (SNoLtLe_tra (minus_SNo 1) 0 (mul_SNo p t) (SNo_minus_SNo 1 SNo_1) SNo_0 (SNo_mul_SNo p t HpS HtS) Hm10S H0le_pt).
An exact proof term for the current goal is (RltI (minus_SNo 1) (mul_SNo p t) Hm1R HmulR Hm1lt_ptS).
Apply (SNoLt_trichotomy_or_impred p 0 HpS SNo_0 (Rlt (mul_SNo p t) 1)) to the current goal.
Assume Hplt0: p < 0.
Apply FalseE to the current goal.
We prove the intermediate claim HpRlt0: Rlt p 0.
An exact proof term for the current goal is (RltI p 0 HpR real_0 Hplt0).
An exact proof term for the current goal is (Hpnotlt0 HpRlt0).
Assume Hpeq0: p = 0.
rewrite the current goal using Hpeq0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL t HtS) (from left to right).
An exact proof term for the current goal is Rlt_0_1.
Assume H0ltp: 0 < p.
Apply (SNoLt_trichotomy_or_impred t 0 HtS SNo_0 (Rlt (mul_SNo p t) 1)) to the current goal.
Assume Htlt0: t < 0.
We prove the intermediate claim Hptlt0: mul_SNo p t < 0.
An exact proof term for the current goal is (mul_SNo_pos_neg p t HpS HtS H0ltp Htlt0).
We prove the intermediate claim H0lt1: 0 < 1.
An exact proof term for the current goal is SNoLt_0_1.
We prove the intermediate claim Hptlt1: mul_SNo p t < 1.
An exact proof term for the current goal is (SNoLt_tra (mul_SNo p t) 0 1 (SNo_mul_SNo p t HpS HtS) SNo_0 SNo_1 Hptlt0 H0lt1).
An exact proof term for the current goal is (RltI (mul_SNo p t) 1 HmulR real_1 Hptlt1).
Assume Hteq0: t = 0.
rewrite the current goal using Hteq0 (from left to right).
rewrite the current goal using (mul_SNo_zeroR p HpS) (from left to right).
An exact proof term for the current goal is Rlt_0_1.
Assume H0ltt: 0 < t.
Apply (SNoLt_trichotomy_or_impred p 1 HpS SNo_1 (Rlt (mul_SNo p t) 1)) to the current goal.
Assume Hplt1: p < 1.
We prove the intermediate claim Hptlt_t: mul_SNo p t < t.
An exact proof term for the current goal is (mul_SNo_Lt1_pos_Lt p t HpS HtS Hplt1 H0ltt).
We prove the intermediate claim Hptlt1: mul_SNo p t < 1.
An exact proof term for the current goal is (SNoLt_tra (mul_SNo p t) t 1 (SNo_mul_SNo p t HpS HtS) HtS SNo_1 Hptlt_t Htlt1S).
An exact proof term for the current goal is (RltI (mul_SNo p t) 1 HmulR real_1 Hptlt1).
Assume Hpeq1: p = 1.
rewrite the current goal using Hpeq1 (from left to right).
rewrite the current goal using (mul_SNo_oneL t HtS) (from left to right).
An exact proof term for the current goal is Htlt1.
Assume H1ltp: 1 < p.
Apply FalseE to the current goal.
We prove the intermediate claim H1ltpR: Rlt 1 p.
An exact proof term for the current goal is (RltI 1 p real_1 HpR H1ltp).
An exact proof term for the current goal is (Hpnotgt1 H1ltpR).
Set g to be the term hR.
We use g to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (continuous_map_range_restrict X Tx R R_standard_topology g U HhRcont HUsubR HhRinU).
Let x be given.
Assume HxA: x ∈ A.
We will prove apply_fun g x = apply_fun f x.
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HA).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate claim Hcomp: apply_fun g x = apply_fun mul_fun_R (apply_fun (pair_map X phiR gR) x).
rewrite the current goal using (compose_fun_apply X (pair_map X phiR gR) mul_fun_R x HxX) (from left to right).
Use reflexivity.
rewrite the current goal using Hcomp (from left to right).
rewrite the current goal using (pair_map_apply X R R phiR gR x HxX) (from left to right).
We prove the intermediate claim HphiIx: apply_fun phiI x = 1.
An exact proof term for the current goal is (HphiA1 x HxA).
We prove the intermediate claim HphiFun: function_on phiI X I01.
An exact proof term for the current goal is (continuous_map_function_on X Tx I01 T01 phiI HphiContI).
We prove the intermediate claim HphiIxI01: apply_fun phiI x ∈ I01.
An exact proof term for the current goal is (HphiFun x HxX).
We prove the intermediate claim HphiRval: apply_fun phiR x = apply_fun phiI x.
rewrite the current goal using (compose_fun_apply X phiI inc01 x HxX) (from left to right).
rewrite the current goal using (identity_function_apply I01 (apply_fun phiI x) HphiIxI01) (from left to right).
Use reflexivity.
rewrite the current goal using HphiRval (from left to right).
rewrite the current goal using HphiIx (from left to right).
We prove the intermediate claim HgRxR: apply_fun gR x ∈ R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology gR HgRcont x HxX).
We prove the intermediate claim HpairRR: (1,apply_fun gR x) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R 1 (apply_fun gR x) real_1 HgRxR).
rewrite the current goal using (apply_fun_graph (setprod R R) (λp0 : set ⇒ mul_SNo (p0 0) (p0 1)) (1,apply_fun gR x) HpairRR) (from left to right).
rewrite the current goal using (tuple_2_0_eq 1 (apply_fun gR x)) (from left to right).
rewrite the current goal using (tuple_2_1_eq 1 (apply_fun gR x)) (from left to right).
We prove the intermediate claim HgRxS: SNo (apply_fun gR x).
An exact proof term for the current goal is (real_SNo (apply_fun gR x) HgRxR).
rewrite the current goal using (mul_SNo_oneL (apply_fun gR x) HgRxS) (from left to right).
An exact proof term for the current goal is (HgR_eq_on_A x HxA).
∎