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) (closed_interval (minus_SNo 1) 1) (closed_interval_topology (minus_SNo 1) 1) f.
We will prove ∃g : set, continuous_map X Tx (closed_interval (minus_SNo 1) 1) (closed_interval_topology (minus_SNo 1) 1) g ∧ (∀x : set, x ∈ A → apply_fun g x = apply_fun f x).
We prove the intermediate claim HA_cases: A = Empty ∨ ¬ (A = Empty).
An exact proof term for the current goal is (xm (A = Empty)).
Apply (HA_cases (∃g : set, continuous_map X Tx (closed_interval (minus_SNo 1) 1) (closed_interval_topology (minus_SNo 1) 1) g ∧ (∀x : set, x ∈ A → apply_fun g x = apply_fun f x))) to the current goal.
Assume HAemp: A = Empty.
We use (const_fun X 0) to witness the existential quantifier.
Apply andI to the current goal.
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 HCI_top: topology_on (closed_interval (minus_SNo 1) 1) (closed_interval_topology (minus_SNo 1) 1).
An exact proof term for the current goal is (closed_interval_topology_on (minus_SNo 1) 1).
We prove the intermediate claim H0I: 0 ∈ closed_interval (minus_SNo 1) 1.
An exact proof term for the current goal is zero_in_closed_interval_minus1_1.
An exact proof term for the current goal is (const_fun_continuous X Tx (closed_interval (minus_SNo 1) 1) (closed_interval_topology (minus_SNo 1) 1) 0 HTx HCI_top H0I).
Let x be given.
Assume HxA: x ∈ A.
We will prove apply_fun (const_fun X 0) x = apply_fun f x.
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HAemp (from right to left).
An exact proof term for the current goal is HxA.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE x) HxE).
Assume HAne: ¬ (A = Empty).
We prove the intermediate claim HstepI: ∃g0 : set, continuous_map X Tx (closed_interval (minus_SNo one_third) one_third) (closed_interval_topology (minus_SNo one_third) one_third) g0 ∧ (∀x : set, x ∈ preimage_of A f ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = minus_SNo one_third) ∧ (∀x : set, x ∈ preimage_of A f ((closed_interval one_third 1) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = one_third).
An exact proof term for the current goal is (Tietze_stepI_g_exists X Tx A f Hnorm HA Hf).
Apply HstepI to the current goal.
Let g0 be given.
Assume Hg0: continuous_map X Tx (closed_interval (minus_SNo one_third) one_third) (closed_interval_topology (minus_SNo one_third) one_third) g0 ∧ (∀x : set, x ∈ preimage_of A f ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = minus_SNo one_third) ∧ (∀x : set, x ∈ preimage_of A f ((closed_interval one_third 1) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = one_third).
We prove the intermediate claim Hcore: continuous_map X Tx (closed_interval (minus_SNo one_third) one_third) (closed_interval_topology (minus_SNo one_third) one_third) g0 ∧ (∀x : set, x ∈ preimage_of A f ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = minus_SNo one_third).
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval (minus_SNo one_third) one_third) (closed_interval_topology (minus_SNo one_third) one_third) g0 ∧ (∀x : set, x ∈ preimage_of A f ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = minus_SNo one_third)) (∀x : set, x ∈ preimage_of A f ((closed_interval one_third 1) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = one_third) Hg0).
We prove the intermediate claim Hg0cont: continuous_map X Tx (closed_interval (minus_SNo one_third) one_third) (closed_interval_topology (minus_SNo one_third) one_third) g0.
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval (minus_SNo one_third) one_third) (closed_interval_topology (minus_SNo one_third) one_third) g0) (∀x : set, x ∈ preimage_of A f ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = minus_SNo one_third) Hcore).
We prove the intermediate claim Hg0_on_B: ∀x : set, x ∈ preimage_of A f ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = minus_SNo one_third.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval (minus_SNo one_third) one_third) (closed_interval_topology (minus_SNo one_third) one_third) g0) (∀x : set, x ∈ preimage_of A f ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = minus_SNo one_third) Hcore).
We prove the intermediate claim Hg0_on_C: ∀x : set, x ∈ preimage_of A f ((closed_interval one_third 1) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = one_third.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval (minus_SNo one_third) one_third) (closed_interval_topology (minus_SNo one_third) one_third) g0 ∧ (∀x : set, x ∈ preimage_of A f ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = minus_SNo one_third)) (∀x : set, x ∈ preimage_of A f ((closed_interval one_third 1) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g0 x = one_third) Hg0).
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 HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HA).
Set f1 to be the term graph A (λx : set ⇒ add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x))).
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.
Set I0 to be the term closed_interval (minus_SNo one_third) one_third.
Set T0 to be the term closed_interval_topology (minus_SNo one_third) one_third.
We prove the intermediate claim Hfunf: function_on f A I.
An exact proof term for the current goal is (continuous_map_function_on A (subspace_topology X Tx A) I Ti f Hf).
We prove the intermediate claim Hfung0: function_on g0 X I0.
An exact proof term for the current goal is (continuous_map_function_on X Tx I0 T0 g0 Hg0cont).
We prove the intermediate claim Hf1_total: total_function_on f1 A R.
Apply (total_function_on_graph A R (λx : set ⇒ add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x)))) to the current goal.
Let x be given.
Assume HxA: x ∈ A.
We will prove add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x)) ∈ R.
We prove the intermediate claim HfxI: apply_fun f x ∈ I.
An exact proof term for the current goal is (Hfunf x HxA).
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo 1) 1 (apply_fun f x) HfxI).
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 Hg0xI0: apply_fun g0 x ∈ I0.
An exact proof term for the current goal is (Hfung0 x HxX).
We prove the intermediate claim Hg0xR: apply_fun g0 x ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo one_third) one_third (apply_fun g0 x) Hg0xI0).
We prove the intermediate claim HnegR: minus_SNo (apply_fun g0 x) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (apply_fun g0 x) Hg0xR).
An exact proof term for the current goal is (real_add_SNo (apply_fun f x) HfxR (minus_SNo (apply_fun g0 x)) HnegR).
We prove the intermediate claim Hf1fun: function_on f1 A R.
An exact proof term for the current goal is (andEL (function_on f1 A R) (∀a : set, a ∈ A → ∃y : set, y ∈ R ∧ (a,y) ∈ f1) Hf1_total).
We prove the intermediate claim Hf1_apply: ∀x : set, x ∈ A → apply_fun f1 x = add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x)).
Let x be given.
Assume HxA: x ∈ A.
rewrite the current goal using (apply_fun_graph A (λx0 : set ⇒ add_SNo (apply_fun f x0) (minus_SNo (apply_fun g0 x0))) x HxA) (from left to right).
Use reflexivity.
Set I1 to be the term closed_interval (minus_SNo 1) (minus_SNo one_third).
Set I3 to be the term closed_interval one_third 1.
Set I2 to be the term closed_interval (minus_SNo two_thirds) two_thirds.
Set B to be the term preimage_of A f (I1 ∩ I).
Set C to be the term preimage_of A f (I3 ∩ I).
We prove the intermediate claim Hf1_range: ∀x : set, x ∈ A → apply_fun f1 x ∈ I2.
Let x be given.
Assume HxA: x ∈ A.
We prove the intermediate claim HfxI: apply_fun f x ∈ I.
An exact proof term for the current goal is (Hfunf x HxA).
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 Hcase1: apply_fun f x ∈ I1 ∨ ¬ (apply_fun f x ∈ I1).
An exact proof term for the current goal is (xm (apply_fun f x ∈ I1)).
Apply (Hcase1 (apply_fun f1 x ∈ I2)) to the current goal.
Assume HfxI1: apply_fun f x ∈ I1.
We prove the intermediate claim HfxI1I: apply_fun f x ∈ I1 ∩ I.
An exact proof term for the current goal is (binintersectI I1 I (apply_fun f x) HfxI1 HfxI).
We prove the intermediate claim HxB: x ∈ B.
An exact proof term for the current goal is (SepI A (λx0 : set ⇒ apply_fun f x0 ∈ I1 ∩ I) x HxA HfxI1I).
We prove the intermediate claim Hg0eq: apply_fun g0 x = minus_SNo one_third.
An exact proof term for the current goal is (Hg0_on_B x HxB).
We prove the intermediate claim Hf1eq: apply_fun f1 x = add_SNo (apply_fun f x) one_third.
rewrite the current goal using (Hf1_apply x HxA) (from left to right).
rewrite the current goal using Hg0eq (from left to right) at position 1.
We prove the intermediate claim H13R: one_third ∈ R.
An exact proof term for the current goal is one_third_in_R.
rewrite the current goal using (minus_SNo_minus_SNo_real one_third H13R) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hf1eq (from left to right).
We prove the intermediate claim H13R: one_third ∈ R.
An exact proof term for the current goal is one_third_in_R.
We prove the intermediate claim H23R: two_thirds ∈ R.
An exact proof term for the current goal is two_thirds_in_R.
We prove the intermediate claim Hm23R: minus_SNo two_thirds ∈ R.
An exact proof term for the current goal is (real_minus_SNo two_thirds H23R).
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 Hm13R: minus_SNo one_third ∈ R.
An exact proof term for the current goal is (real_minus_SNo one_third H13R).
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo 1) (minus_SNo one_third) (apply_fun f x) HfxI1).
We prove the intermediate claim Hfx_bounds: Rle (minus_SNo 1) (apply_fun f x) ∧ Rle (apply_fun f x) (minus_SNo one_third).
An exact proof term for the current goal is (closed_interval_bounds (minus_SNo 1) (minus_SNo one_third) (apply_fun f x) Hm1R Hm13R HfxI1).
We prove the intermediate claim Hm1lefx: Rle (minus_SNo 1) (apply_fun f x).
An exact proof term for the current goal is (andEL (Rle (minus_SNo 1) (apply_fun f x)) (Rle (apply_fun f x) (minus_SNo one_third)) Hfx_bounds).
We prove the intermediate claim Hfxlem13: Rle (apply_fun f x) (minus_SNo one_third).
An exact proof term for the current goal is (andER (Rle (minus_SNo 1) (apply_fun f x)) (Rle (apply_fun f x) (minus_SNo one_third)) Hfx_bounds).
We prove the intermediate claim Hf1R: add_SNo (apply_fun f x) one_third ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun f x) HfxR one_third H13R).
We prove the intermediate claim Hlow_tmp: Rle (add_SNo (minus_SNo 1) one_third) (add_SNo (apply_fun f x) one_third).
An exact proof term for the current goal is (Rle_add_SNo_1 (minus_SNo 1) (apply_fun f x) one_third Hm1R HfxR H13R Hm1lefx).
We prove the intermediate claim Hlow: Rle (minus_SNo two_thirds) (add_SNo (apply_fun f x) one_third).
rewrite the current goal using minus_two_thirds_eq_minus1_plus_one_third (from left to right) at position 1.
An exact proof term for the current goal is Hlow_tmp.
We prove the intermediate claim Hup0_tmp: Rle (add_SNo (apply_fun f x) one_third) (add_SNo (minus_SNo one_third) one_third).
An exact proof term for the current goal is (Rle_add_SNo_1 (apply_fun f x) (minus_SNo one_third) one_third HfxR Hm13R H13R Hfxlem13).
We prove the intermediate claim H13S: SNo one_third.
An exact proof term for the current goal is (real_SNo one_third H13R).
We prove the intermediate claim Hup0: Rle (add_SNo (apply_fun f x) one_third) 0.
rewrite the current goal using (add_SNo_minus_SNo_linv one_third H13S) (from right to left) at position 1.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate claim H0le23: Rle 0 two_thirds.
An exact proof term for the current goal is Rle_0_two_thirds.
We prove the intermediate claim Hup: Rle (add_SNo (apply_fun f x) one_third) two_thirds.
An exact proof term for the current goal is (Rle_tra (add_SNo (apply_fun f x) one_third) 0 two_thirds Hup0 H0le23).
An exact proof term for the current goal is (closed_intervalI_of_Rle (minus_SNo two_thirds) two_thirds (add_SNo (apply_fun f x) one_third) Hm23R H23R Hf1R Hlow Hup).
Assume HnotI1: ¬ (apply_fun f x ∈ I1).
We prove the intermediate claim Hcase3: apply_fun f x ∈ I3 ∨ ¬ (apply_fun f x ∈ I3).
An exact proof term for the current goal is (xm (apply_fun f x ∈ I3)).
Apply (Hcase3 (apply_fun f1 x ∈ I2)) to the current goal.
Assume HfxI3: apply_fun f x ∈ I3.
We prove the intermediate claim HfxI3I: apply_fun f x ∈ I3 ∩ I.
An exact proof term for the current goal is (binintersectI I3 I (apply_fun f x) HfxI3 HfxI).
We prove the intermediate claim HxC: x ∈ C.
An exact proof term for the current goal is (SepI A (λx0 : set ⇒ apply_fun f x0 ∈ I3 ∩ I) x HxA HfxI3I).
We prove the intermediate claim Hg0eq: apply_fun g0 x = one_third.
An exact proof term for the current goal is (Hg0_on_C x HxC).
We prove the intermediate claim Hf1eq: apply_fun f1 x = add_SNo (apply_fun f x) (minus_SNo one_third).
rewrite the current goal using (Hf1_apply x HxA) (from left to right).
rewrite the current goal using Hg0eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hf1eq (from left to right).
We prove the intermediate claim H13R: one_third ∈ R.
An exact proof term for the current goal is one_third_in_R.
We prove the intermediate claim H23R: two_thirds ∈ R.
An exact proof term for the current goal is two_thirds_in_R.
We prove the intermediate claim Hm23R: minus_SNo two_thirds ∈ R.
An exact proof term for the current goal is (real_minus_SNo two_thirds H23R).
We prove the intermediate claim Hm13R: minus_SNo one_third ∈ R.
An exact proof term for the current goal is (real_minus_SNo one_third H13R).
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R one_third 1 (apply_fun f x) HfxI3).
We prove the intermediate claim Hfx_bounds: Rle one_third (apply_fun f x) ∧ Rle (apply_fun f x) 1.
An exact proof term for the current goal is (closed_interval_bounds one_third 1 (apply_fun f x) H13R real_1 HfxI3).
We prove the intermediate claim H13lefx: Rle one_third (apply_fun f x).
An exact proof term for the current goal is (andEL (Rle one_third (apply_fun f x)) (Rle (apply_fun f x) 1) Hfx_bounds).
We prove the intermediate claim Hfxle1: Rle (apply_fun f x) 1.
An exact proof term for the current goal is (andER (Rle one_third (apply_fun f x)) (Rle (apply_fun f x) 1) Hfx_bounds).
We prove the intermediate claim Hf1R: add_SNo (apply_fun f x) (minus_SNo one_third) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun f x) HfxR (minus_SNo one_third) Hm13R).
We prove the intermediate claim H0le_f1_tmp: Rle (add_SNo one_third (minus_SNo one_third)) (add_SNo (apply_fun f x) (minus_SNo one_third)).
An exact proof term for the current goal is (Rle_add_SNo_1 one_third (apply_fun f x) (minus_SNo one_third) H13R HfxR Hm13R H13lefx).
We prove the intermediate claim H13S: SNo one_third.
An exact proof term for the current goal is (real_SNo one_third H13R).
We prove the intermediate claim H0le_f1: Rle 0 (add_SNo (apply_fun f x) (minus_SNo one_third)).
rewrite the current goal using (add_SNo_minus_SNo_rinv one_third H13S) (from right to left) at position 1.
An exact proof term for the current goal is H0le_f1_tmp.
We prove the intermediate claim Hm23le0: Rle (minus_SNo two_thirds) 0.
An exact proof term for the current goal is Rle_minus_two_thirds_0.
We prove the intermediate claim Hlow: Rle (minus_SNo two_thirds) (add_SNo (apply_fun f x) (minus_SNo one_third)).
An exact proof term for the current goal is (Rle_tra (minus_SNo two_thirds) 0 (add_SNo (apply_fun f x) (minus_SNo one_third)) Hm23le0 H0le_f1).
We prove the intermediate claim Hup_tmp: Rle (add_SNo (apply_fun f x) (minus_SNo one_third)) (add_SNo 1 (minus_SNo one_third)).
An exact proof term for the current goal is (Rle_add_SNo_1 (apply_fun f x) 1 (minus_SNo one_third) HfxR real_1 Hm13R Hfxle1).
We prove the intermediate claim Hup: Rle (add_SNo (apply_fun f x) (minus_SNo one_third)) two_thirds.
rewrite the current goal using two_thirds_eq_1_minus_one_third (from left to right) at position 1.
An exact proof term for the current goal is Hup_tmp.
An exact proof term for the current goal is (closed_intervalI_of_Rle (minus_SNo two_thirds) two_thirds (add_SNo (apply_fun f x) (minus_SNo one_third)) Hm23R H23R Hf1R Hlow Hup).
Assume HnotI3: ¬ (apply_fun f x ∈ I3).
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo 1) 1 (apply_fun f x) HfxI).
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 H13R: one_third ∈ R.
An exact proof term for the current goal is one_third_in_R.
We prove the intermediate claim Hm13R: (minus_SNo one_third) ∈ R.
An exact proof term for the current goal is (real_minus_SNo one_third H13R).
We prove the intermediate claim Hfx_bounds: Rle (minus_SNo 1) (apply_fun f x) ∧ Rle (apply_fun f x) 1.
An exact proof term for the current goal is (closed_interval_bounds (minus_SNo 1) 1 (apply_fun f x) Hm1R real_1 HfxI).
We prove the intermediate claim Hnlt_fx_m1: ¬ (Rlt (apply_fun f x) (minus_SNo 1)).
An exact proof term for the current goal is (RleE_nlt (minus_SNo 1) (apply_fun f x) (andEL (Rle (minus_SNo 1) (apply_fun f x)) (Rle (apply_fun f x) 1) Hfx_bounds)).
We prove the intermediate claim Hnlt_1_fx: ¬ (Rlt 1 (apply_fun f x)).
An exact proof term for the current goal is (RleE_nlt (apply_fun f x) 1 (andER (Rle (minus_SNo 1) (apply_fun f x)) (Rle (apply_fun f x) 1) Hfx_bounds)).
We prove the intermediate claim HnotI1_cases: Rlt (apply_fun f x) (minus_SNo 1) ∨ Rlt (minus_SNo one_third) (apply_fun f x).
An exact proof term for the current goal is (closed_interval_not_mem_cases (minus_SNo 1) (minus_SNo one_third) (apply_fun f x) Hm1R Hm13R HfxR HnotI1).
We prove the intermediate claim Hm13lt_fx: Rlt (minus_SNo one_third) (apply_fun f x).
Apply (HnotI1_cases (Rlt (minus_SNo one_third) (apply_fun f x))) to the current goal.
Assume Hbad: Rlt (apply_fun f x) (minus_SNo 1).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
Assume Hok: Rlt (minus_SNo one_third) (apply_fun f x).
An exact proof term for the current goal is Hok.
We prove the intermediate claim Hnot_fx_lt_m13: ¬ (Rlt (apply_fun f x) (minus_SNo one_third)).
An exact proof term for the current goal is (not_Rlt_sym (minus_SNo one_third) (apply_fun f x) Hm13lt_fx).
We prove the intermediate claim HnotI3_cases: Rlt (apply_fun f x) one_third ∨ Rlt 1 (apply_fun f x).
An exact proof term for the current goal is (closed_interval_not_mem_cases one_third 1 (apply_fun f x) H13R real_1 HfxR HnotI3).
We prove the intermediate claim Hfx_lt_13: Rlt (apply_fun f x) one_third.
Apply (HnotI3_cases (Rlt (apply_fun f x) one_third)) to the current goal.
Assume Hok: Rlt (apply_fun f x) one_third.
An exact proof term for the current goal is Hok.
Assume Hbad: Rlt 1 (apply_fun f x).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate claim Hnot_13_lt_fx: ¬ (Rlt one_third (apply_fun f x)).
An exact proof term for the current goal is (not_Rlt_sym (apply_fun f x) one_third Hfx_lt_13).
We prove the intermediate claim HfxI0: apply_fun f x ∈ I0.
We prove the intermediate claim HI0_def: I0 = {t ∈ R|¬ (Rlt t (minus_SNo one_third)) ∧ ¬ (Rlt one_third t)}.
Use reflexivity.
We prove the intermediate claim HxSep: apply_fun f x ∈ {t ∈ R|¬ (Rlt t (minus_SNo one_third)) ∧ ¬ (Rlt one_third t)}.
An exact proof term for the current goal is (SepI R (λt : set ⇒ ¬ (Rlt t (minus_SNo one_third)) ∧ ¬ (Rlt one_third t)) (apply_fun f x) HfxR (andI (¬ (Rlt (apply_fun f x) (minus_SNo one_third))) (¬ (Rlt one_third (apply_fun f x))) Hnot_fx_lt_m13 Hnot_13_lt_fx)).
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
rewrite the current goal using (Hf1_apply x HxA) (from left to right).
We prove the intermediate claim Hg0xI0: apply_fun g0 x ∈ I0.
An exact proof term for the current goal is (Hfung0 x HxX).
We prove the intermediate claim Hg0xR: apply_fun g0 x ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo one_third) one_third (apply_fun g0 x) Hg0xI0).
We prove the intermediate claim Hm_g0x_R: minus_SNo (apply_fun g0 x) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (apply_fun g0 x) Hg0xR).
We prove the intermediate claim Hf1xR: add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x)) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun f x) HfxR (minus_SNo (apply_fun g0 x)) Hm_g0x_R).
We prove the intermediate claim H13R: one_third ∈ R.
An exact proof term for the current goal is one_third_in_R.
We prove the intermediate claim Hm13R: (minus_SNo one_third) ∈ R.
An exact proof term for the current goal is (real_minus_SNo one_third H13R).
We prove the intermediate claim H23R: two_thirds ∈ R.
An exact proof term for the current goal is two_thirds_in_R.
We prove the intermediate claim Hm23R: (minus_SNo two_thirds) ∈ R.
An exact proof term for the current goal is (real_minus_SNo two_thirds H23R).
We prove the intermediate claim Hfx0_bounds: Rle (minus_SNo one_third) (apply_fun f x) ∧ Rle (apply_fun f x) one_third.
An exact proof term for the current goal is (closed_interval_bounds (minus_SNo one_third) one_third (apply_fun f x) Hm13R H13R HfxI0).
We prove the intermediate claim Hg0x_bounds: Rle (minus_SNo one_third) (apply_fun g0 x) ∧ Rle (apply_fun g0 x) one_third.
An exact proof term for the current goal is (closed_interval_bounds (minus_SNo one_third) one_third (apply_fun g0 x) Hm13R H13R Hg0xI0).
We prove the intermediate claim Hm13_le_fx: Rle (minus_SNo one_third) (apply_fun f x).
An exact proof term for the current goal is (andEL (Rle (minus_SNo one_third) (apply_fun f x)) (Rle (apply_fun f x) one_third) Hfx0_bounds).
We prove the intermediate claim Hfx_le_13: Rle (apply_fun f x) one_third.
An exact proof term for the current goal is (andER (Rle (minus_SNo one_third) (apply_fun f x)) (Rle (apply_fun f x) one_third) Hfx0_bounds).
We prove the intermediate claim Hm13_le_g0x: Rle (minus_SNo one_third) (apply_fun g0 x).
An exact proof term for the current goal is (andEL (Rle (minus_SNo one_third) (apply_fun g0 x)) (Rle (apply_fun g0 x) one_third) Hg0x_bounds).
We prove the intermediate claim Hg0x_le_13: Rle (apply_fun g0 x) one_third.
An exact proof term for the current goal is (andER (Rle (minus_SNo one_third) (apply_fun g0 x)) (Rle (apply_fun g0 x) one_third) Hg0x_bounds).
We prove the intermediate claim Hm13_le_mg0x: Rle (minus_SNo one_third) (minus_SNo (apply_fun g0 x)).
An exact proof term for the current goal is (Rle_minus_contra (apply_fun g0 x) one_third Hg0x_le_13).
We prove the intermediate claim Hmg0x_le_13: Rle (minus_SNo (apply_fun g0 x)) one_third.
We prove the intermediate claim Htmp: Rle (minus_SNo (apply_fun g0 x)) (minus_SNo (minus_SNo one_third)).
An exact proof term for the current goal is (Rle_minus_contra (minus_SNo one_third) (apply_fun g0 x) Hm13_le_g0x).
We prove the intermediate claim H13R: one_third ∈ R.
An exact proof term for the current goal is one_third_in_R.
rewrite the current goal using (minus_SNo_minus_SNo_real one_third H13R) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hlo1: Rle (add_SNo (minus_SNo one_third) (minus_SNo one_third)) (add_SNo (apply_fun f x) (minus_SNo one_third)).
An exact proof term for the current goal is (Rle_add_SNo_1 (minus_SNo one_third) (apply_fun f x) (minus_SNo one_third) Hm13R HfxR Hm13R Hm13_le_fx).
We prove the intermediate claim Hlo2: Rle (add_SNo (apply_fun f x) (minus_SNo one_third)) (add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x))).
An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun f x) (minus_SNo one_third) (minus_SNo (apply_fun g0 x)) HfxR Hm13R Hm_g0x_R Hm13_le_mg0x).
We prove the intermediate claim Hlo': Rle (add_SNo (minus_SNo one_third) (minus_SNo one_third)) (add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x))).
An exact proof term for the current goal is (Rle_tra (add_SNo (minus_SNo one_third) (minus_SNo one_third)) (add_SNo (apply_fun f x) (minus_SNo one_third)) (add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x))) Hlo1 Hlo2).
We prove the intermediate claim Hlo: Rle (minus_SNo two_thirds) (add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x))).
rewrite the current goal using (minus_two_thirds_eq) (from left to right) at position 1.
An exact proof term for the current goal is Hlo'.
We prove the intermediate claim Hhi1: Rle (add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x))) (add_SNo one_third (minus_SNo (apply_fun g0 x))).
An exact proof term for the current goal is (Rle_add_SNo_1 (apply_fun f x) one_third (minus_SNo (apply_fun g0 x)) HfxR H13R Hm_g0x_R Hfx_le_13).
We prove the intermediate claim Hhi2: Rle (add_SNo one_third (minus_SNo (apply_fun g0 x))) (add_SNo one_third one_third).
An exact proof term for the current goal is (Rle_add_SNo_2 one_third (minus_SNo (apply_fun g0 x)) one_third H13R Hm_g0x_R H13R Hmg0x_le_13).
We prove the intermediate claim Hhi': Rle (add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x))) (add_SNo one_third one_third).
An exact proof term for the current goal is (Rle_tra (add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x))) (add_SNo one_third (minus_SNo (apply_fun g0 x))) (add_SNo one_third one_third) Hhi1 Hhi2).
We prove the intermediate claim Hhi: Rle (add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x))) two_thirds.
We prove the intermediate claim Hdef23: two_thirds = add_SNo one_third one_third.
Use reflexivity.
rewrite the current goal using Hdef23 (from left to right).
An exact proof term for the current goal is Hhi'.
An exact proof term for the current goal is (closed_intervalI_of_Rle (minus_SNo two_thirds) two_thirds (add_SNo (apply_fun f x) (minus_SNo (apply_fun g0 x))) Hm23R H23R Hf1xR Hlo Hhi).
We prove the intermediate claim HstepII: ∃g : set, continuous_map X Tx I Ti g ∧ (∀x : set, x ∈ A → apply_fun g x = apply_fun f x).
We prove the intermediate claim HstepII_R: ∃gR : set, continuous_map X Tx R R_standard_topology gR ∧ (∀x : set, x ∈ A → apply_fun gR x = apply_fun f x) ∧ (∀x : set, x ∈ X → apply_fun gR x ∈ I).
An exact proof term for the current goal is (Tietze_stepII_real_extension X Tx A f Hnorm HA Hf).
Apply HstepII_R to the current goal.
Let gR be given.
Assume HgR: continuous_map X Tx R R_standard_topology gR ∧ (∀x : set, x ∈ A → apply_fun gR x = apply_fun f x) ∧ (∀x : set, x ∈ X → apply_fun gR x ∈ I).
We use gR to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HgRcont: continuous_map X Tx R R_standard_topology gR.
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology gR) (∀x : set, x ∈ A → apply_fun gR x = apply_fun f x) (andEL (continuous_map X Tx R R_standard_topology gR ∧ (∀x : set, x ∈ A → apply_fun gR x = apply_fun f x)) (∀x : set, x ∈ X → apply_fun gR x ∈ I) HgR)).
We prove the intermediate claim HimgI: ∀x : set, x ∈ X → apply_fun gR x ∈ I.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology gR ∧ (∀x : set, x ∈ A → apply_fun gR x = apply_fun f x)) (∀x : set, x ∈ X → apply_fun gR x ∈ I) HgR).
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 HTiEq: Ti = subspace_topology R R_standard_topology I.
Use reflexivity.
rewrite the current goal using HTiEq (from left to right).
An exact proof term for the current goal is (continuous_map_range_restrict X Tx R R_standard_topology gR I HgRcont HISubR HimgI).
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology gR) (∀x : set, x ∈ A → apply_fun gR x = apply_fun f x) (andEL (continuous_map X Tx R R_standard_topology gR ∧ (∀x : set, x ∈ A → apply_fun gR x = apply_fun f x)) (∀x : set, x ∈ X → apply_fun gR x ∈ I) HgR)).
An exact proof term for the current goal is HstepII.
∎