An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).

An exact proof term for the current goal is (closed_in_subset X Tx A HA).

An exact proof term for the current goal is (RleE_left a b Hab).

An exact proof term for the current goal is (left_endpoint_in_closed_interval a b Hab).

An exact proof term for the current goal is (closed_interval_topology_on a b).

An exact proof term for the current goal is (continuous_map_function_on A (subspace_topology X Tx A) (closed_interval a b) (closed_interval_topology a b) f Hf).

An exact proof term for the current goal is (xm (A = Empty)).

Assume HAemp: A = Empty.

We use (const_fun X a) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (const_fun_continuous X Tx (closed_interval a b) (closed_interval_topology a b) a HTx HCI_top HaIab).

Let x be given.

Assume HxA: x ∈ A.

We will prove apply_fun (const_fun X a) 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 Hab_cases: a = b ∨ ¬ (a = b).

An exact proof term for the current goal is (xm (a = b)).

Apply (Hab_cases (∃g : set, continuous_map X Tx (closed_interval a b) (closed_interval_topology a b) g ∧ (∀x : set, x ∈ A → apply_fun g x = apply_fun f x))) to the current goal.

Assume Heq: a = b.

We use (const_fun X a) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (const_fun_continuous X Tx (closed_interval a b) (closed_interval_topology a b) a HTx HCI_top HaIab).

Let x be given.

Assume HxA: x ∈ A.

We will prove apply_fun (const_fun X a) x = apply_fun f x.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HAsubX x HxA).

rewrite the current goal using (const_fun_apply X a x HxX) (from left to right).

Set y to be the term apply_fun f x.

We will prove a = y.

We prove the intermediate claim HyIab: y ∈ closed_interval a b.

An exact proof term for the current goal is (Hfunf x HxA).

We prove the intermediate claim HeqCI: closed_interval a b = closed_interval a a.

rewrite the current goal using Heq (from right to left).

Use reflexivity.

We prove the intermediate claim HyIaa: y ∈ closed_interval a a.

rewrite the current goal using HeqCI (from right to left).

An exact proof term for the current goal is HyIab.

We prove the intermediate claim Hyeq: y = a.

An exact proof term for the current goal is (closed_interval_degenerate a y HaR HyIaa).

rewrite the current goal using Hyeq (from left to right).

Use reflexivity.

Assume Hneq: ¬ (a = b).

Set I to be the term closed_interval a b.

Set Ti to be the term closed_interval_topology a b.

Set I01 to be the term closed_interval (minus_SNo 1) 1.

Set T01 to be the term closed_interval_topology (minus_SNo 1) 1.

We prove the intermediate claim Hh: ∃h : set, ∃hinv : set, continuous_map I Ti I01 T01 h ∧ (continuous_map I01 T01 I Ti hinv ∧ ((∀t : set, t ∈ I → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ I01 → apply_fun h (apply_fun hinv s) = s))).

An exact proof term for the current goal is (closed_interval_affine_equiv_minus1_1 a b Hab Hneq).

Apply Hh to the current goal.

Let h be given.

Assume Hhex: ∃hinv : set, continuous_map I Ti I01 T01 h ∧ (continuous_map I01 T01 I Ti hinv ∧ ((∀t : set, t ∈ I → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ I01 → apply_fun h (apply_fun hinv s) = s))).

Apply Hhex to the current goal.

Let hinv be given.

Assume Hhcore: continuous_map I Ti I01 T01 h ∧ (continuous_map I01 T01 I Ti hinv ∧ ((∀t : set, t ∈ I → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ I01 → apply_fun h (apply_fun hinv s) = s))).

We prove the intermediate claim Hhcont: continuous_map I Ti I01 T01 h.

An exact proof term for the current goal is (andEL (continuous_map I Ti I01 T01 h) (continuous_map I01 T01 I Ti hinv ∧ ((∀t : set, t ∈ I → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ I01 → apply_fun h (apply_fun hinv s) = s))) Hhcore).

We prove the intermediate claim Hrest: continuous_map I01 T01 I Ti hinv ∧ ((∀t : set, t ∈ I → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ I01 → apply_fun h (apply_fun hinv s) = s)).

An exact proof term for the current goal is (andER (continuous_map I Ti I01 T01 h) (continuous_map I01 T01 I Ti hinv ∧ ((∀t : set, t ∈ I → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ I01 → apply_fun h (apply_fun hinv s) = s))) Hhcore).

We prove the intermediate claim Hhinvcont: continuous_map I01 T01 I Ti hinv.

An exact proof term for the current goal is (andEL (continuous_map I01 T01 I Ti hinv) ((∀t : set, t ∈ I → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ I01 → apply_fun h (apply_fun hinv s) = s)) Hrest).

We prove the intermediate claim Hhrest2: (∀t : set, t ∈ I → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ I01 → apply_fun h (apply_fun hinv s) = s).

An exact proof term for the current goal is (andER (continuous_map I01 T01 I Ti hinv) ((∀t : set, t ∈ I → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ I01 → apply_fun h (apply_fun hinv s) = s)) Hrest).

We prove the intermediate claim Hhinv_after_h: ∀t : set, t ∈ I → apply_fun hinv (apply_fun h t) = t.

An exact proof term for the current goal is (andEL (∀t : set, t ∈ I → apply_fun hinv (apply_fun h t) = t) (∀s : set, s ∈ I01 → apply_fun h (apply_fun hinv s) = s) Hhrest2).

Set f01 to be the term compose_fun A f h.

We prove the intermediate claim Hf01cont: continuous_map A (subspace_topology X Tx A) I01 T01 f01.

An exact proof term for the current goal is (composition_continuous A (subspace_topology X Tx A) I Ti I01 T01 f h Hf Hhcont).

We prove the intermediate claim Hext01: ∃g01 : set, continuous_map X Tx I01 T01 g01 ∧ (∀x : set, x ∈ A → apply_fun g01 x = apply_fun f01 x).

An exact proof term for the current goal is (Tietze_extension_minus1_1 X Tx A f01 Hnorm HA Hf01cont).

Apply Hext01 to the current goal.

Let g01 be given.

Assume Hg01: continuous_map X Tx I01 T01 g01 ∧ (∀x : set, x ∈ A → apply_fun g01 x = apply_fun f01 x).

We prove the intermediate claim Hg01cont: continuous_map X Tx I01 T01 g01.

An exact proof term for the current goal is (andEL (continuous_map X Tx I01 T01 g01) (∀x : set, x ∈ A → apply_fun g01 x = apply_fun f01 x) Hg01).

We prove the intermediate claim Hg01eq: ∀x : set, x ∈ A → apply_fun g01 x = apply_fun f01 x.

An exact proof term for the current goal is (andER (continuous_map X Tx I01 T01 g01) (∀x : set, x ∈ A → apply_fun g01 x = apply_fun f01 x) Hg01).

Set g to be the term compose_fun X g01 hinv.

We use g to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (composition_continuous X Tx I01 T01 I Ti g01 hinv Hg01cont Hhinvcont).

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 Hcompg: apply_fun g x = apply_fun hinv (apply_fun g01 x).

rewrite the current goal using (compose_fun_apply X g01 hinv x HxX) (from left to right).

Use reflexivity.

rewrite the current goal using Hcompg (from left to right).

rewrite the current goal using (Hg01eq x HxA) (from left to right).

We prove the intermediate claim Hcompf01: apply_fun f01 x = apply_fun h (apply_fun f x).

rewrite the current goal using (compose_fun_apply A f h x HxA) (from left to right).

Use reflexivity.

rewrite the current goal using Hcompf01 (from left to right).

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 HfxI: apply_fun f x ∈ I.

An exact proof term for the current goal is (Hfunf x HxA).

rewrite the current goal using (Hhinv_after_h (apply_fun f x) HfxI) (from left to right).

Use reflexivity.