We will prove atleastp R (closed_interval 0 1).
We will prove ∃f : set → set, inj R (closed_interval 0 1) f.
Set I01 to be the term closed_interval 0 1.
Set Im1 to be the term closed_interval (minus_SNo 1) 1.
We prove the intermediate claim H0le1: 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 (closed_interval_topology 0 1) Im1 (closed_interval_topology (minus_SNo 1) 1) h ∧ (continuous_map Im1 (closed_interval_topology (minus_SNo 1) 1) I01 (closed_interval_topology 0 1) 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 H0le1 Hneq).
Apply HexAff to the current goal.
Let h be given.
Assume HexHinvs: ∃hinv : set, continuous_map I01 (closed_interval_topology 0 1) Im1 (closed_interval_topology (minus_SNo 1) 1) h ∧ (continuous_map Im1 (closed_interval_topology (minus_SNo 1) 1) I01 (closed_interval_topology 0 1) 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 HexHinvs to the current goal.
Let hinv be given.
Assume Hpack.
We prove the intermediate claim HhinvCont: continuous_map Im1 (closed_interval_topology (minus_SNo 1) 1) I01 (closed_interval_topology 0 1) hinv.
An exact proof term for the current goal is (andEL (continuous_map Im1 (closed_interval_topology (minus_SNo 1) 1) I01 (closed_interval_topology 0 1) 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)) (andER (continuous_map I01 (closed_interval_topology 0 1) Im1 (closed_interval_topology (minus_SNo 1) 1) h) (continuous_map Im1 (closed_interval_topology (minus_SNo 1) 1) I01 (closed_interval_topology 0 1) 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 Hinv2: ∀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) (andER (continuous_map Im1 (closed_interval_topology (minus_SNo 1) 1) I01 (closed_interval_topology 0 1) 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)) (andER (continuous_map I01 (closed_interval_topology 0 1) Im1 (closed_interval_topology (minus_SNo 1) 1) h) (continuous_map Im1 (closed_interval_topology (minus_SNo 1) 1) I01 (closed_interval_topology 0 1) 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 HhinvFun: function_on hinv Im1 I01.
An exact proof term for the current goal is (continuous_map_function_on Im1 (closed_interval_topology (minus_SNo 1) 1) I01 (closed_interval_topology 0 1) hinv HhinvCont).
Set f to be the term (λt : set ⇒ apply_fun hinv (apply_fun bounded_transform_phi t)).
We use f to witness the existential quantifier.
Apply (injI R I01 f) to the current goal.
Let t be given.
Assume HtR: t ∈ R.
We will prove f t ∈ I01.
We prove the intermediate claim HphiIn: apply_fun bounded_transform_phi t ∈ Im1.
An exact proof term for the current goal is (bounded_transform_phi_range_in_closed_interval_minus1_1 t HtR).
An exact proof term for the current goal is (HhinvFun (apply_fun bounded_transform_phi t) HphiIn).
Let t1 be given.
Assume Ht1R: t1 ∈ R.
Let t2 be given.
Assume Ht2R: t2 ∈ R.
Assume Heq: f t1 = f t2.
We will prove t1 = t2.
We prove the intermediate claim Hs1: apply_fun bounded_transform_phi t1 ∈ Im1.
An exact proof term for the current goal is (bounded_transform_phi_range_in_closed_interval_minus1_1 t1 Ht1R).
We prove the intermediate claim Hs2: apply_fun bounded_transform_phi t2 ∈ Im1.
An exact proof term for the current goal is (bounded_transform_phi_range_in_closed_interval_minus1_1 t2 Ht2R).
We prove the intermediate claim HphiEq: apply_fun bounded_transform_phi t1 = apply_fun bounded_transform_phi t2.
rewrite the current goal using (Hinv2 (apply_fun bounded_transform_phi t1) Hs1) (from right to left) at position 1.
rewrite the current goal using (Hinv2 (apply_fun bounded_transform_phi t2) Hs2) (from right to left) at position 1.
We prove the intermediate claim Hf1: f t1 = apply_fun hinv (apply_fun bounded_transform_phi t1).
Use reflexivity.
We prove the intermediate claim Hf2: f t2 = apply_fun hinv (apply_fun bounded_transform_phi t2).
Use reflexivity.
rewrite the current goal using Hf1 (from right to left) at position 1.
rewrite the current goal using Hf2 (from right to left) at position 1.
rewrite the current goal using Heq (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hpsi1: apply_fun bounded_transform_psi (apply_fun bounded_transform_phi t1) = t1.
An exact proof term for the current goal is (bounded_transform_psi_phi_cancel t1 Ht1R).
We prove the intermediate claim Hpsi2: apply_fun bounded_transform_psi (apply_fun bounded_transform_phi t2) = t2.
An exact proof term for the current goal is (bounded_transform_psi_phi_cancel t2 Ht2R).
rewrite the current goal using Hpsi1 (from right to left).
rewrite the current goal using Hpsi2 (from right to left).
rewrite the current goal using HphiEq (from left to right).
Use reflexivity.
∎