We will prove compact_space (closed_interval (minus_SNo 1) 1) (closed_interval_topology (minus_SNo 1) 1).
Set I01 to be the term closed_interval 0 1.
Set T01 to be the term closed_interval_topology 0 1.
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 Hcomp01: compact_space I01 T01.
We prove the intermediate claim HIeq: I01 = unit_interval.
Use reflexivity.
We prove the intermediate claim HTeq: T01 = unit_interval_topology.
Use reflexivity.
rewrite the current goal using HIeq (from left to right).
rewrite the current goal using HTeq (from left to right).
An exact proof term for the current goal is unit_interval_compact_axiom.
We prove the intermediate claim Hab: 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 Hneq: ¬ (0 = 1).
Assume H01: 0 = 1.
An exact proof term for the current goal is (neq_0_1 H01).
We prove the intermediate claim HexAff: ∃h : set, ∃hinv : set, continuous_map I01 T01 Im1 Tm1 h ∧ (continuous_map Im1 Tm1 I01 T01 hinv ∧ ((∀t : set, t ∈ I01 → 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 0 1 Hab Hneq).
Apply HexAff to the current goal.
Let h be given.
Assume Hhexinv: ∃hinv : set, continuous_map I01 T01 Im1 Tm1 h ∧ (continuous_map Im1 Tm1 I01 T01 hinv ∧ ((∀t : set, t ∈ I01 → 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 I01 T01 Im1 Tm1 h ∧ (continuous_map Im1 Tm1 I01 T01 hinv ∧ ((∀t : set, t ∈ I01 → 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 Hhcont: continuous_map I01 T01 Im1 Tm1 h.
An exact proof term for the current goal is (andEL (continuous_map I01 T01 Im1 Tm1 h) (continuous_map Im1 Tm1 I01 T01 hinv ∧ ((∀t : set, t ∈ I01 → 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 Hmid: continuous_map Im1 Tm1 I01 T01 hinv ∧ ((∀t : set, t ∈ I01 → 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 I01 T01 Im1 Tm1 h) (continuous_map Im1 Tm1 I01 T01 hinv ∧ ((∀t : set, t ∈ I01 → 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 I01 T01 hinv.
An exact proof term for the current goal is (andEL (continuous_map Im1 Tm1 I01 T01 hinv) ((∀t : set, t ∈ I01 → 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 ∈ I01 → 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 I01 T01 hinv) ((∀t : set, t ∈ I01 → 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 Hh_after_hinv: ∀s : set, s ∈ Im1 → apply_fun h (apply_fun hinv s) = s.
An exact proof term for the current goal is (andER (∀t : set, t ∈ I01 → 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 h I01.
We prove the intermediate claim HImgEq: Img = Im1.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ Img.
We will prove y ∈ Im1.
Apply (ReplE_impred I01 (λt : set ⇒ apply_fun h t) y Hy (y ∈ Im1)) to the current goal.
Let t be given.
Assume HtI: t ∈ I01.
Assume HyEq: y = apply_fun h t.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate claim Hfunh: function_on h I01 Im1.
An exact proof term for the current goal is (continuous_map_function_on I01 T01 Im1 Tm1 h Hhcont).
An exact proof term for the current goal is (Hfunh t HtI).
Let y be given.
Assume Hy: y ∈ Im1.
We will prove y ∈ Img.
We prove the intermediate claim Hfunhinv: function_on hinv Im1 I01.
An exact proof term for the current goal is (continuous_map_function_on Im1 Tm1 I01 T01 hinv Hhinvcont).
Set t to be the term apply_fun hinv y.
We prove the intermediate claim HtI: t ∈ I01.
An exact proof term for the current goal is (Hfunhinv y Hy).
We prove the intermediate claim HyEq: apply_fun h t = y.
We prove the intermediate claim Htdef: t = apply_fun hinv y.
Use reflexivity.
rewrite the current goal using Htdef (from left to right).
An exact proof term for the current goal is (Hh_after_hinv y Hy).
rewrite the current goal using HyEq (from right to left).
An exact proof term for the current goal is (ReplI I01 (λu : set ⇒ apply_fun h u) t HtI).
We prove the intermediate claim HimgComp: compact_space Img (subspace_topology Im1 Tm1 Img).
An exact proof term for the current goal is (continuous_image_compact I01 T01 Im1 Tm1 h Hcomp01 Hhcont).
We prove the intermediate claim HTm1: topology_on Im1 Tm1.
An exact proof term for the current goal is (closed_interval_topology_on (minus_SNo 1) 1).
We prove the intermediate claim Hwhole: subspace_topology Im1 Tm1 Im1 = Tm1.
An exact proof term for the current goal is (subspace_topology_whole Im1 Tm1 HTm1).
We prove the intermediate claim Htmp: compact_space Im1 (subspace_topology Im1 Tm1 Im1).
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 HIm1def: Im1 = closed_interval (minus_SNo 1) 1.
Use reflexivity.
We prove the intermediate claim HTm1def: Tm1 = closed_interval_topology (minus_SNo 1) 1.
Use reflexivity.
rewrite the current goal using HIm1def (from right to left) at position 1.
rewrite the current goal using HTm1def (from right to left).
rewrite the current goal using Hwhole (from right to left).
An exact proof term for the current goal is Htmp.
∎