Assume Habeq: a = b.

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

Set I to be the term closed_interval b b.

Set Ti to be the term closed_interval_topology b b.

We prove the intermediate claim HTi: topology_on I Ti.

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

We prove the intermediate claim HbR: b ∈ R.

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

We prove the intermediate claim HIeq: I = {b}.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ I.

We prove the intermediate claim HxEq: x = b.

An exact proof term for the current goal is (closed_interval_degenerate b x HbR Hx).

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

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

Let x be given.

Assume Hx: x ∈ {b}.

We prove the intermediate claim HxEq: x = b.

An exact proof term for the current goal is (SingE b x Hx).

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

We prove the intermediate claim Hbb: Rle b b.

An exact proof term for the current goal is (Rle_refl b HbR).

An exact proof term for the current goal is (closed_intervalI_of_Rle b b b HbR HbR HbR Hbb Hbb).

An exact proof term for the current goal is (compact_space_singleton I Ti b HIeq HTi).

Assume Hneq: ¬ (a = b).

Set Iab to be the term closed_interval a b.

Set Tiab to be the term closed_interval_topology a b.

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

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

We prove the intermediate claim Hcompm1: compact_space Im1 Tm1.

An exact proof term for the current goal is closed_interval_minus1_1_compact.

We prove the intermediate claim HexAff: ∃h : set, ∃hinv : set, continuous_map Iab Tiab Im1 Tm1 h ∧ (continuous_map Im1 Tm1 Iab Tiab hinv ∧ ((∀t : set, t ∈ Iab → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ Im1 → 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 HexAff to the current goal.

Let h be given.

Assume Hhexinv: ∃hinv : set, continuous_map Iab Tiab Im1 Tm1 h ∧ (continuous_map Im1 Tm1 Iab Tiab hinv ∧ ((∀t : set, t ∈ Iab → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ Im1 → apply_fun h (apply_fun hinv s) = s))).

Apply Hhexinv to the current goal.

Let hinv be given.

Assume Hpack: continuous_map Iab Tiab Im1 Tm1 h ∧ (continuous_map Im1 Tm1 Iab Tiab hinv ∧ ((∀t : set, t ∈ Iab → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ Im1 → apply_fun h (apply_fun hinv s) = s))).

We prove the intermediate claim Hmid: continuous_map Im1 Tm1 Iab Tiab hinv ∧ ((∀t : set, t ∈ Iab → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ Im1 → apply_fun h (apply_fun hinv s) = s)).

An exact proof term for the current goal is (andER (continuous_map Iab Tiab Im1 Tm1 h) (continuous_map Im1 Tm1 Iab Tiab hinv ∧ ((∀t : set, t ∈ Iab → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ Im1 → apply_fun h (apply_fun hinv s) = s))) Hpack).

We prove the intermediate claim Hhinvcont: continuous_map Im1 Tm1 Iab Tiab hinv.

An exact proof term for the current goal is (andEL (continuous_map Im1 Tm1 Iab Tiab hinv) ((∀t : set, t ∈ Iab → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ Im1 → apply_fun h (apply_fun hinv s) = s)) Hmid).

We prove the intermediate claim Hinvprops: (∀t : set, t ∈ Iab → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ Im1 → apply_fun h (apply_fun hinv s) = s).

An exact proof term for the current goal is (andER (continuous_map Im1 Tm1 Iab Tiab hinv) ((∀t : set, t ∈ Iab → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ Im1 → apply_fun h (apply_fun hinv s) = s)) Hmid).

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

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

Set Img to be the term image_of_fun hinv Im1.

We prove the intermediate claim HImgEq: Img = Iab.

Apply set_ext to the current goal.

Let y be given.

Assume Hy: y ∈ Img.

We will prove y ∈ Iab.

Apply (ReplE_impred Im1 (λs : set ⇒ apply_fun hinv s) y Hy (y ∈ Iab)) to the current goal.

Let s be given.

Assume Hs: s ∈ Im1.

Assume HyEq: y = apply_fun hinv s.

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

We prove the intermediate claim Hfunhinv: function_on hinv Im1 Iab.

An exact proof term for the current goal is (continuous_map_function_on Im1 Tm1 Iab Tiab hinv Hhinvcont).

An exact proof term for the current goal is (Hfunhinv s Hs).

Let y be given.

Assume Hy: y ∈ Iab.

We will prove y ∈ Img.

We prove the intermediate claim Hfunh: function_on h Iab Im1.

An exact proof term for the current goal is (continuous_map_function_on Iab Tiab Im1 Tm1 h (andEL (continuous_map Iab Tiab Im1 Tm1 h) (continuous_map Im1 Tm1 Iab Tiab hinv ∧ ((∀t : set, t ∈ Iab → apply_fun hinv (apply_fun h t) = t) ∧ (∀s : set, s ∈ Im1 → apply_fun h (apply_fun hinv s) = s))) Hpack)).

Set s to be the term apply_fun h y.

We prove the intermediate claim Hs: s ∈ Im1.

An exact proof term for the current goal is (Hfunh y Hy).

We prove the intermediate claim HyEq: apply_fun hinv s = y.

We prove the intermediate claim Hsdef: s = apply_fun h y.

Use reflexivity.

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

An exact proof term for the current goal is (Hhinv_after_h y Hy).

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

An exact proof term for the current goal is (ReplI Im1 (λu : set ⇒ apply_fun hinv u) s Hs).

We prove the intermediate claim HimgComp: compact_space Img (subspace_topology Iab Tiab Img).

An exact proof term for the current goal is (continuous_image_compact Im1 Tm1 Iab Tiab hinv Hcompm1 Hhinvcont).

We prove the intermediate claim HTiab: topology_on Iab Tiab.

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

We prove the intermediate claim Hwhole: subspace_topology Iab Tiab Iab = Tiab.

An exact proof term for the current goal is (subspace_topology_whole Iab Tiab HTiab).

We prove the intermediate claim Htmp: compact_space Iab (subspace_topology Iab Tiab Iab).

rewrite the current goal using HImgEq (from right to left) at position 1.

rewrite the current goal using HImgEq (from right to left) at position 2.

An exact proof term for the current goal is HimgComp.

We prove the intermediate claim HIabdef: Iab = closed_interval a b.

Use reflexivity.

We prove the intermediate claim HTiabdef: Tiab = closed_interval_topology a b.

Use reflexivity.

rewrite the current goal using HIabdef (from right to left) at position 1.

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

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

An exact proof term for the current goal is Htmp.