We prove the intermediate claim Hex1: ∃p : set, function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y.

An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ ∃p : set, function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y0) y HyPc).

We prove the intermediate claim Hex2: ∃q : set, function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q ∧ apply_fun q 0 = y ∧ apply_fun q 1 = z.

Apply Hex1 to the current goal.

Let p be given.

Assume Hp.

Apply Hex2 to the current goal.

Let q be given.

Assume Hq.

Set pf to be the term compose_fun unit_interval_left_half double_map_left_half p.

Set qf to be the term compose_fun unit_interval_right_half double_minus_one_map_right_half q.

We prove the intermediate claim Hp_fun: function_on p unit_interval X.

We prove the intermediate claim HpA: ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) ∧ apply_fun p 1 = y.

An exact proof term for the current goal is Hp.

We prove the intermediate claim HpB: (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x.

An exact proof term for the current goal is (andEL ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) (apply_fun p 1 = y) HpA).

We prove the intermediate claim HpC: function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p.

An exact proof term for the current goal is (andEL (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) (apply_fun p 0 = x) HpB).

An exact proof term for the current goal is (andEL (function_on p unit_interval X) (continuous_map unit_interval unit_interval_topology X Tx p) HpC).

We prove the intermediate claim Hp_cont: continuous_map unit_interval unit_interval_topology X Tx p.

We prove the intermediate claim HpA: ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) ∧ apply_fun p 1 = y.

An exact proof term for the current goal is Hp.

We prove the intermediate claim HpB: (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x.

An exact proof term for the current goal is (andEL ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) (apply_fun p 1 = y) HpA).

We prove the intermediate claim HpC: function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p.

An exact proof term for the current goal is (andEL (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) (apply_fun p 0 = x) HpB).

An exact proof term for the current goal is (andER (function_on p unit_interval X) (continuous_map unit_interval unit_interval_topology X Tx p) HpC).

We prove the intermediate claim Hp0: apply_fun p 0 = x.

We prove the intermediate claim HpA: ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) ∧ apply_fun p 1 = y.

An exact proof term for the current goal is Hp.

We prove the intermediate claim HpB: (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x.

An exact proof term for the current goal is (andEL ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) (apply_fun p 1 = y) HpA).

An exact proof term for the current goal is (andER (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) (apply_fun p 0 = x) HpB).

We prove the intermediate claim Hp1: apply_fun p 1 = y.

We prove the intermediate claim HpA: ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) ∧ apply_fun p 1 = y.

An exact proof term for the current goal is Hp.

An exact proof term for the current goal is (andER ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) (apply_fun p 1 = y) HpA).

We prove the intermediate claim Hq_fun: function_on q unit_interval X.

We prove the intermediate claim HqA: ((function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) ∧ apply_fun q 0 = y) ∧ apply_fun q 1 = z.

An exact proof term for the current goal is Hq.

We prove the intermediate claim HqB: (function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) ∧ apply_fun q 0 = y.

An exact proof term for the current goal is (andEL ((function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) ∧ apply_fun q 0 = y) (apply_fun q 1 = z) HqA).

We prove the intermediate claim HqC: function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q.

An exact proof term for the current goal is (andEL (function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) (apply_fun q 0 = y) HqB).

An exact proof term for the current goal is (andEL (function_on q unit_interval X) (continuous_map unit_interval unit_interval_topology X Tx q) HqC).

We prove the intermediate claim Hq_cont: continuous_map unit_interval unit_interval_topology X Tx q.

We prove the intermediate claim HqA: ((function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) ∧ apply_fun q 0 = y) ∧ apply_fun q 1 = z.

An exact proof term for the current goal is Hq.

We prove the intermediate claim HqB: (function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) ∧ apply_fun q 0 = y.

An exact proof term for the current goal is (andEL ((function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) ∧ apply_fun q 0 = y) (apply_fun q 1 = z) HqA).

We prove the intermediate claim HqC: function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q.

An exact proof term for the current goal is (andEL (function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) (apply_fun q 0 = y) HqB).

An exact proof term for the current goal is (andER (function_on q unit_interval X) (continuous_map unit_interval unit_interval_topology X Tx q) HqC).

We prove the intermediate claim Hq0: apply_fun q 0 = y.

We prove the intermediate claim HqA: ((function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) ∧ apply_fun q 0 = y) ∧ apply_fun q 1 = z.

An exact proof term for the current goal is Hq.

We prove the intermediate claim HqB: (function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) ∧ apply_fun q 0 = y.

An exact proof term for the current goal is (andEL ((function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) ∧ apply_fun q 0 = y) (apply_fun q 1 = z) HqA).

An exact proof term for the current goal is (andER (function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) (apply_fun q 0 = y) HqB).

We prove the intermediate claim Hq1: apply_fun q 1 = z.

We prove the intermediate claim HqA: ((function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) ∧ apply_fun q 0 = y) ∧ apply_fun q 1 = z.

An exact proof term for the current goal is Hq.

An exact proof term for the current goal is (andER ((function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q) ∧ apply_fun q 0 = y) (apply_fun q 1 = z) HqA).

We prove the intermediate claim Hpf_fun: function_on pf unit_interval_left_half X.

An exact proof term for the current goal is (function_on_compose_fun unit_interval_left_half unit_interval X double_map_left_half p double_map_function_on Hp_fun).

We prove the intermediate claim Hqf_fun: function_on qf unit_interval_right_half X.

An exact proof term for the current goal is (function_on_compose_fun unit_interval_right_half unit_interval X double_minus_one_map_right_half q double_minus_one_map_function_on Hq_fun).

We prove the intermediate claim Hpf_cont: continuous_map unit_interval_left_half (subspace_topology unit_interval unit_interval_topology unit_interval_left_half) X Tx pf.

An exact proof term for the current goal is (composition_continuous unit_interval_left_half (subspace_topology unit_interval unit_interval_topology unit_interval_left_half) unit_interval unit_interval_topology X Tx double_map_left_half p double_map_continuous Hp_cont).

We prove the intermediate claim Hqf_cont: continuous_map unit_interval_right_half (subspace_topology unit_interval unit_interval_topology unit_interval_right_half) X Tx qf.

An exact proof term for the current goal is (composition_continuous unit_interval_right_half (subspace_topology unit_interval unit_interval_topology unit_interval_right_half) unit_interval unit_interval_topology X Tx double_minus_one_map_right_half q double_minus_one_map_continuous Hq_cont).

We prove the intermediate claim Hleft_closed: closed_in unit_interval unit_interval_topology unit_interval_left_half.

An exact proof term for the current goal is (andEL (closed_in unit_interval unit_interval_topology unit_interval_left_half) (closed_in unit_interval unit_interval_topology unit_interval_right_half) unit_interval_halves_closed).

We prove the intermediate claim Hright_closed: closed_in unit_interval unit_interval_topology unit_interval_right_half.

An exact proof term for the current goal is (andER (closed_in unit_interval unit_interval_topology unit_interval_left_half) (closed_in unit_interval unit_interval_topology unit_interval_right_half) unit_interval_halves_closed).

We prove the intermediate claim Hagree: ∀t : set, t ∈ (unit_interval_left_half ∩ unit_interval_right_half) → apply_fun pf t = apply_fun qf t.

Let t be given.

Assume Ht: t ∈ (unit_interval_left_half ∩ unit_interval_right_half).

We prove the intermediate claim HtSing: t ∈ {eps_ 1}.

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

An exact proof term for the current goal is Ht.

We prove the intermediate claim Hteq: t = eps_ 1.

An exact proof term for the current goal is (SingE (eps_ 1) t HtSing).

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

We prove the intermediate claim Hpf: apply_fun pf (eps_ 1) = apply_fun p (apply_fun double_map_left_half (eps_ 1)).

An exact proof term for the current goal is (compose_fun_apply unit_interval_left_half double_map_left_half p (eps_ 1) eps_1_in_unit_interval_left_half).

We prove the intermediate claim Hqf: apply_fun qf (eps_ 1) = apply_fun q (apply_fun double_minus_one_map_right_half (eps_ 1)).

An exact proof term for the current goal is (compose_fun_apply unit_interval_right_half double_minus_one_map_right_half q (eps_ 1) eps_1_in_unit_interval_right_half).

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

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

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

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

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

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

Use reflexivity.

We prove the intermediate claim Hexh: ∃h : set, continuous_map unit_interval unit_interval_topology X Tx h ∧ ((∀t : set, t ∈ unit_interval_left_half → apply_fun h t = apply_fun pf t) ∧ (∀t : set, t ∈ unit_interval_right_half → apply_fun h t = apply_fun qf t)).

An exact proof term for the current goal is (pasting_lemma unit_interval unit_interval_left_half unit_interval_right_half X unit_interval_topology Tx pf qf unit_interval_topology_on Hleft_closed Hright_closed unit_interval_halves_cover Hpf_cont Hqf_cont Hagree).

Apply Hexh to the current goal.

Let h be given.

Assume Hh: continuous_map unit_interval unit_interval_topology X Tx h ∧ ((∀t : set, t ∈ unit_interval_left_half → apply_fun h t = apply_fun pf t) ∧ (∀t : set, t ∈ unit_interval_right_half → apply_fun h t = apply_fun qf t)).

We will prove ∃p0 : set, function_on p0 unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p0 ∧ apply_fun p0 0 = x ∧ apply_fun p0 1 = z.

We use h to witness the existential quantifier.

We will prove function_on h unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx h ∧ apply_fun h 0 = x ∧ apply_fun h 1 = z.

Apply andI to the current goal.

An exact proof term for the current goal is (continuous_map_function_on unit_interval unit_interval_topology X Tx h (andEL (continuous_map unit_interval unit_interval_topology X Tx h) ((∀t : set, t ∈ unit_interval_left_half → apply_fun h t = apply_fun pf t) ∧ (∀t : set, t ∈ unit_interval_right_half → apply_fun h t = apply_fun qf t)) Hh)).

An exact proof term for the current goal is (andEL (continuous_map unit_interval unit_interval_topology X Tx h) ((∀t : set, t ∈ unit_interval_left_half → apply_fun h t = apply_fun pf t) ∧ (∀t : set, t ∈ unit_interval_right_half → apply_fun h t = apply_fun qf t)) Hh).

We prove the intermediate claim H0I: 0 ∈ unit_interval.

An exact proof term for the current goal is zero_in_unit_interval.

We prove the intermediate claim H0left: 0 ∈ unit_interval_left_half.

An exact proof term for the current goal is (SepI unit_interval (λt0 : set ⇒ ¬ (Rlt (eps_ 1) t0)) 0 H0I (not_Rlt_sym 0 (eps_ 1) eps_1_pos_R)).

We prove the intermediate claim Hleft: ∀t : set, t ∈ unit_interval_left_half → apply_fun h t = apply_fun pf t.

An exact proof term for the current goal is (andEL (∀t : set, t ∈ unit_interval_left_half → apply_fun h t = apply_fun pf t) (∀t : set, t ∈ unit_interval_right_half → apply_fun h t = apply_fun qf t) (andER (continuous_map unit_interval unit_interval_topology X Tx h) ((∀t : set, t ∈ unit_interval_left_half → apply_fun h t = apply_fun pf t) ∧ (∀t : set, t ∈ unit_interval_right_half → apply_fun h t = apply_fun qf t)) Hh)).

rewrite the current goal using (Hleft 0 H0left) (from left to right).

We prove the intermediate claim Hpf0: apply_fun pf 0 = apply_fun p (apply_fun double_map_left_half 0).

An exact proof term for the current goal is (compose_fun_apply unit_interval_left_half double_map_left_half p 0 zero_in_unit_interval_left_half).

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

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

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

Use reflexivity.

We prove the intermediate claim H1I: 1 ∈ unit_interval.

An exact proof term for the current goal is one_in_unit_interval.

We prove the intermediate claim H1right: 1 ∈ unit_interval_right_half.

An exact proof term for the current goal is (SepI unit_interval (λt0 : set ⇒ ¬ (Rlt t0 (eps_ 1))) 1 H1I (not_Rlt_sym (eps_ 1) 1 eps_1_lt1_R)).

We prove the intermediate claim Hright: ∀t : set, t ∈ unit_interval_right_half → apply_fun h t = apply_fun qf t.

An exact proof term for the current goal is (andER (∀t : set, t ∈ unit_interval_left_half → apply_fun h t = apply_fun pf t) (∀t : set, t ∈ unit_interval_right_half → apply_fun h t = apply_fun qf t) (andER (continuous_map unit_interval unit_interval_topology X Tx h) ((∀t : set, t ∈ unit_interval_left_half → apply_fun h t = apply_fun pf t) ∧ (∀t : set, t ∈ unit_interval_right_half → apply_fun h t = apply_fun qf t)) Hh)).

rewrite the current goal using (Hright 1 H1right) (from left to right).

We prove the intermediate claim Hqf1: apply_fun qf 1 = apply_fun q (apply_fun double_minus_one_map_right_half 1).

An exact proof term for the current goal is (compose_fun_apply unit_interval_right_half double_minus_one_map_right_half q 1 one_in_unit_interval_right_half).

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

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

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

Use reflexivity.