[GOAL]
t : ℝ
⊢ t ∈ I ↔ 1 - t ∈ I
[PROOFSTEP]
rw [mem_Icc, mem_Icc]
[GOAL]
t : ℝ
⊢ 0 ≤ t ∧ t ≤ 1 ↔ 0 ≤ 1 - t ∧ 1 - t ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case mp
t : ℝ
⊢ 0 ≤ t ∧ t ≤ 1 → 0 ≤ 1 - t ∧ 1 - t ≤ 1
[PROOFSTEP]
intro
[GOAL]
case mpr
t : ℝ
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1 → 0 ≤ t ∧ t ≤ 1
[PROOFSTEP]
intro
[GOAL]
case mp
t : ℝ
a✝ : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case mpr
t : ℝ
a✝ : 0 ≤ 1 - t ∧ 1 - t ≤ 1
⊢ 0 ≤ t ∧ t ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case mp.left
t : ℝ
a✝ : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t
[PROOFSTEP]
linarith
[GOAL]
case mp.right
t : ℝ
a✝ : 0 ≤ t ∧ t ≤ 1
⊢ 1 - t ≤ 1
[PROOFSTEP]
linarith
[GOAL]
case mpr.left
t : ℝ
a✝ : 0 ≤ 1 - t ∧ 1 - t ≤ 1
⊢ 0 ≤ t
[PROOFSTEP]
linarith
[GOAL]
case mpr.right
t : ℝ
a✝ : 0 ≤ 1 - t ∧ 1 - t ≤ 1
⊢ t ≤ 1
[PROOFSTEP]
linarith
[GOAL]
⊢ 1 ∈ I
[PROOFSTEP]
constructor
[GOAL]
case left
⊢ 0 ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case right
⊢ 1 ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
⊢ ↑(σ 0) = ↑1
[PROOFSTEP]
simp [symm]
[GOAL]
⊢ ↑(σ 1) = ↑0
[PROOFSTEP]
simp [symm]
[GOAL]
x : ↑I
⊢ ↑(σ (σ x)) = ↑x
[PROOFSTEP]
simp [symm]
[GOAL]
⊢ CompactSpace ↑I
[PROOFSTEP]
infer_instance
[GOAL]
x : ↑I
⊢ 0 ≤ 1 - ↑x
[PROOFSTEP]
simpa using x.2.2
[GOAL]
x : ↑I
⊢ 1 - ↑x ≤ 1
[PROOFSTEP]
simpa using x.2.1
[GOAL]
a t : ℝ
ha : 0 < a
⊢ a * t ∈ I ↔ t ∈ Icc 0 (1 / a)
[PROOFSTEP]
constructor
[GOAL]
case mp
a t : ℝ
ha : 0 < a
⊢ a * t ∈ I → t ∈ Icc 0 (1 / a)
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mpr
a t : ℝ
ha : 0 < a
⊢ t ∈ Icc 0 (1 / a) → a * t ∈ I
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mp.intro
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ∈ Icc 0 (1 / a)
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ∈ I
[PROOFSTEP]
constructor
[GOAL]
case mp.intro.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ 0 ≤ t
[PROOFSTEP]
exact nonneg_of_mul_nonneg_right h₁ ha
[GOAL]
case mp.intro.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ≤ 1 / a
[PROOFSTEP]
rwa [le_div_iff ha, mul_comm]
[GOAL]
case mpr.intro.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ 0 ≤ a * t
[PROOFSTEP]
exact mul_nonneg ha.le h₁
[GOAL]
case mpr.intro.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ≤ 1
[PROOFSTEP]
rwa [le_div_iff ha, mul_comm] at h₂ 
[GOAL]
t : ℝ
⊢ 2 * t - 1 ∈ I ↔ t ∈ Icc (1 / 2) 1
[PROOFSTEP]
constructor
[GOAL]
case mp
t : ℝ
⊢ 2 * t - 1 ∈ I → t ∈ Icc (1 / 2) 1
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mpr
t : ℝ
⊢ t ∈ Icc (1 / 2) 1 → 2 * t - 1 ∈ I
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mp.intro
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
⊢ t ∈ Icc (1 / 2) 1
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
⊢ 2 * t - 1 ∈ I
[PROOFSTEP]
constructor
[GOAL]
case mp.intro.left
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
⊢ 1 / 2 ≤ t
[PROOFSTEP]
linarith
[GOAL]
case mp.intro.right
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
⊢ t ≤ 1
[PROOFSTEP]
linarith
[GOAL]
case mpr.intro.left
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
⊢ 0 ≤ 2 * t - 1
[PROOFSTEP]
linarith
[GOAL]
case mpr.intro.right
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
⊢ 2 * t - 1 ≤ 1
[PROOFSTEP]
linarith
[GOAL]
x : ↑unitInterval
⊢ 0 ≤ ↑x
[PROOFSTEP]
unit_interval
[GOAL]
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : 0 < a
⊢ ↑(affineHomeomorph a b (_ : a ≠ 0)) '' Icc 0 1 = Icc b (a + b)
[PROOFSTEP]
simp [h]
[GOAL]
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a < b
⊢ ↑(Icc a b) ≃ₜ ↑(Icc 0 1)
[PROOFSTEP]
let e := Homeomorph.image (affineHomeomorph (b - a) a (sub_pos.mpr h).ne.symm) (Set.Icc 0 1)
[GOAL]
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(↑(affineHomeomorph (b - a) a (_ : b - a ≠ 0)) '' Icc 0 1) :=
  Homeomorph.image (affineHomeomorph (b - a) a (_ : b - a ≠ 0)) (Icc 0 1)
⊢ ↑(Icc a b) ≃ₜ ↑(Icc 0 1)
[PROOFSTEP]
refine' (e.trans _).symm
[GOAL]
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(↑(affineHomeomorph (b - a) a (_ : b - a ≠ 0)) '' Icc 0 1) :=
  Homeomorph.image (affineHomeomorph (b - a) a (_ : b - a ≠ 0)) (Icc 0 1)
⊢ ↑(↑(affineHomeomorph (b - a) a (_ : b - a ≠ 0)) '' Icc 0 1) ≃ₜ ↑(Icc a b)
[PROOFSTEP]
apply Homeomorph.setCongr
[GOAL]
case h
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(↑(affineHomeomorph (b - a) a (_ : b - a ≠ 0)) '' Icc 0 1) :=
  Homeomorph.image (affineHomeomorph (b - a) a (_ : b - a ≠ 0)) (Icc 0 1)
⊢ ↑(affineHomeomorph (b - a) a (_ : b - a ≠ 0)) '' Icc 0 1 = Icc a b
[PROOFSTEP]
rw [affineHomeomorph_image_I _ _ (sub_pos.2 h)]
[GOAL]
case h
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(↑(affineHomeomorph (b - a) a (_ : b - a ≠ 0)) '' Icc 0 1) :=
  Homeomorph.image (affineHomeomorph (b - a) a (_ : b - a ≠ 0)) (Icc 0 1)
⊢ Icc a (b - a + a) = Icc a b
[PROOFSTEP]
simp
