From 7734d3866b1bfd8ea39b474bee6d0918cd4e0f7a Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 4 Feb 2021 21:33:36 +0000 Subject: [PATCH] =?UTF-8?q?refactor(data/real/basic):=20make=20=E2=84=9D?= =?UTF-8?q?=20a=20structure=20(#6024)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Preparation for :four_leaf_clover:, which doesn't have irreducible. --- src/analysis/specific_limits.lean | 7 +- src/data/real/basic.lean | 214 ++++++++++++++++------- src/data/real/cardinality.lean | 6 +- src/measure_theory/lebesgue_measure.lean | 3 +- src/set_theory/cardinal.lean | 6 + src/topology/path_connected.lean | 2 +- 6 files changed, 169 insertions(+), 69 deletions(-) diff --git a/src/analysis/specific_limits.lean b/src/analysis/specific_limits.lean index 7e0406126ce0f..8c791081f70a8 100644 --- a/src/analysis/specific_limits.lean +++ b/src/analysis/specific_limits.lean @@ -188,8 +188,11 @@ metric.mk_uniformity_basis (λ i _, pow_pos h₀ _) $ λ ε ε0, lemma geom_lt {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) {n : ℕ} (hn : 0 < n) (h : ∀ k < n, c * u k < u (k + 1)) : c ^ n * u 0 < u n := -(monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_le_of_lt hn (by simp) - (λ k hk, by simp [pow_succ, mul_assoc]) h +begin + refine (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_le_of_lt hn _ _ h, + { simp }, + { simp [pow_succ, mul_assoc, le_refl] } +end lemma geom_le {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) (n : ℕ) (h : ∀ k < n, c * u k ≤ u (k + 1)) : c ^ n * u 0 ≤ u n := diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean index df2366b566761..f8694da15ba9c 100644 --- a/src/data/real/basic.lean +++ b/src/data/real/basic.lean @@ -13,17 +13,57 @@ import algebra.star.basic /-- The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers. -/ -def real := @cau_seq.completion.Cauchy ℚ _ _ _ abs _ +structure real := of_cauchy :: +(cauchy : @cau_seq.completion.Cauchy ℚ _ _ _ abs _) notation `ℝ` := real +attribute [pp_using_anonymous_constructor] real + namespace real open cau_seq cau_seq.completion variables {x y : ℝ} -def comm_ring_aux : comm_ring ℝ := Cauchy.comm_ring +lemma ext_cauchy_iff : ∀ {x y : real}, x = y ↔ x.cauchy = y.cauchy +| ⟨a⟩ ⟨b⟩ := by split; cc + +lemma ext_cauchy {x y : real} : x.cauchy = y.cauchy → x = y := +ext_cauchy_iff.2 + +/-- The real numbers are isomorphic to the quotient of Cauchy sequences on the rationals. -/ +def equiv_Cauchy : ℝ ≃ cau_seq.completion.Cauchy := +⟨real.cauchy, real.of_cauchy, λ ⟨_⟩, rfl, λ _, rfl⟩ + +-- irreducible doesn't work for instances: https://github.com/leanprover-community/lean/issues/511 +@[irreducible] private def zero : ℝ := ⟨0⟩ +@[irreducible] private def one : ℝ := ⟨1⟩ +@[irreducible] private def add : ℝ → ℝ → ℝ | ⟨a⟩ ⟨b⟩ := ⟨a + b⟩ +@[irreducible] private def neg : ℝ → ℝ | ⟨a⟩ := ⟨-a⟩ +@[irreducible] private def mul : ℝ → ℝ → ℝ | ⟨a⟩ ⟨b⟩ := ⟨a * b⟩ -instance : comm_ring ℝ := { ..comm_ring_aux } +instance : has_zero ℝ := ⟨zero⟩ +instance : has_one ℝ := ⟨one⟩ +instance : has_add ℝ := ⟨add⟩ +instance : has_neg ℝ := ⟨neg⟩ +instance : has_mul ℝ := ⟨mul⟩ + +lemma zero_cauchy : (⟨0⟩ : ℝ) = 0 := show _ = zero, by rw zero +lemma one_cauchy : (⟨1⟩ : ℝ) = 1 := show _ = one, by rw one +lemma add_cauchy {a b} : (⟨a⟩ + ⟨b⟩ : ℝ) = ⟨a + b⟩ := show add _ _ = _, by rw add +lemma neg_cauchy {a} : (-⟨a⟩ : ℝ) = ⟨-a⟩ := show neg _ = _, by rw neg +lemma mul_cauchy {a b} : (⟨a⟩ * ⟨b⟩ : ℝ) = ⟨a * b⟩ := show mul _ _ = _, by rw mul + +instance : comm_ring ℝ := +begin + refine_struct { zero := 0, one := 1, mul := (*), + add := (+), neg := @has_neg.neg ℝ _, sub := λ a b, a + (-b) }, + all_goals { + repeat { rintro ⟨_⟩, }, + simp [← zero_cauchy, ← one_cauchy, add_cauchy, neg_cauchy, mul_cauchy], + apply add_assoc <|> apply add_comm <|> apply mul_assoc <|> apply mul_comm <|> + apply left_distrib <|> apply right_distrib <|> apply sub_eq_add_neg <|> skip + }, +end /- Extra instances to short-circuit type class resolution -/ instance : ring ℝ := by apply_instance @@ -41,6 +81,7 @@ instance : comm_monoid ℝ := by apply_instance instance : monoid ℝ := by apply_instance instance : comm_semigroup ℝ := by apply_instance instance : semigroup ℝ := by apply_instance +instance : has_sub ℝ := by apply_instance instance : inhabited ℝ := ⟨0⟩ /-- The real numbers are a *-ring, with the trivial *-structure. -/ @@ -48,64 +89,104 @@ instance : star_ring ℝ := star_ring_of_comm /-- Coercion `ℚ` → `ℝ` as a `ring_hom`. Note that this is `cau_seq.completion.of_rat`, not `rat.cast`. -/ -def of_rat : ℚ →+* ℝ := ⟨of_rat, rfl, of_rat_mul, rfl, of_rat_add⟩ +def of_rat : ℚ →+* ℝ := +by refine_struct { to_fun := of_cauchy ∘ of_rat }; + simp [of_rat_one, of_rat_zero, of_rat_mul, of_rat_add, + one_cauchy, zero_cauchy, ← mul_cauchy, ← add_cauchy] + +lemma of_rat_apply (x : ℚ) : of_rat x = of_cauchy (cau_seq.completion.of_rat x) := rfl /-- Make a real number from a Cauchy sequence of rationals (by taking the equivalence class). -/ -def mk (x : cau_seq ℚ abs) : ℝ := cau_seq.completion.mk x +def mk (x : cau_seq ℚ abs) : ℝ := ⟨cau_seq.completion.mk x⟩ -theorem of_rat_sub (x y : ℚ) : of_rat (x - y) = of_rat x - of_rat y := -congr_arg mk (const_sub _ _) +theorem mk_eq {f g : cau_seq ℚ abs} : mk f = mk g ↔ f ≈ g := +ext_cauchy_iff.trans mk_eq -instance : has_lt ℝ := -⟨λ x y, quotient.lift_on₂ x y (<) $ +@[irreducible] +private def lt : ℝ → ℝ → Prop | ⟨x⟩ ⟨y⟩ := +quotient.lift_on₂ x y (<) $ λ f₁ g₁ f₂ g₂ hf hg, propext $ ⟨λ h, lt_of_eq_of_lt (setoid.symm hf) (lt_of_lt_of_eq h hg), - λ h, lt_of_eq_of_lt hf (lt_of_lt_of_eq h (setoid.symm hg))⟩⟩ + λ h, lt_of_eq_of_lt hf (lt_of_lt_of_eq h (setoid.symm hg))⟩ -@[simp] theorem mk_lt {f g : cau_seq ℚ abs} : mk f < mk g ↔ f < g := iff.rfl +instance : has_lt ℝ := ⟨lt⟩ -theorem mk_eq {f g : cau_seq ℚ abs} : mk f = mk g ↔ f ≈ g := mk_eq +lemma lt_cauchy {f g} : (⟨⟦f⟧⟩ : ℝ) < ⟨⟦g⟧⟩ ↔ f < g := show lt _ _ ↔ _, by rw lt; refl -theorem quotient_mk_eq_mk (f : cau_seq ℚ abs) : ⟦f⟧ = mk f := rfl +@[simp] theorem mk_lt {f g : cau_seq ℚ abs} : mk f < mk g ↔ f < g := +lt_cauchy -theorem mk_eq_mk {f : cau_seq ℚ abs} : cau_seq.completion.mk f = mk f := rfl +lemma mk_zero : mk 0 = 0 := by rw ← zero_cauchy; refl +lemma mk_one : mk 1 = 1 := by rw ← one_cauchy; refl +lemma mk_add {f g : cau_seq ℚ abs} : mk (f + g) = mk f + mk g := by simp [mk, add_cauchy] +lemma mk_mul {f g : cau_seq ℚ abs} : mk (f * g) = mk f * mk g := by simp [mk, mul_cauchy] +lemma mk_neg {f : cau_seq ℚ abs} : mk (-f) = -mk f := by simp [mk, neg_cauchy] @[simp] theorem mk_pos {f : cau_seq ℚ abs} : 0 < mk f ↔ pos f := -iff_of_eq (congr_arg pos (sub_zero f)) +by rw [← mk_zero, mk_lt]; exact iff_of_eq (congr_arg pos (sub_zero f)) -protected def le (x y : ℝ) : Prop := x < y ∨ x = y -instance : has_le ℝ := ⟨real.le⟩ +@[irreducible] private def le (x y : ℝ) : Prop := x < y ∨ x = y +instance : has_le ℝ := ⟨le⟩ +private lemma le_def {x y : ℝ} : x ≤ y ↔ x < y ∨ x = y := show le _ _ ↔ _, by rw le @[simp] theorem mk_le {f g : cau_seq ℚ abs} : mk f ≤ mk g ↔ f ≤ g := -or_congr iff.rfl quotient.eq +by simp [le_def, mk_eq]; refl + +@[elab_as_eliminator] +protected lemma ind_mk {C : real → Prop} (x : real) (h : ∀ y, C (mk y)) : C x := +begin + cases x with x, + induction x using quot.induction_on with x, + exact h x +end theorem add_lt_add_iff_left {a b : ℝ} (c : ℝ) : c + a < c + b ↔ a < b := -quotient.induction_on₃ a b c (λ f g h, - iff_of_eq (congr_arg pos $ by rw add_sub_add_left_eq_sub)) +begin + induction a using real.ind_mk, + induction b using real.ind_mk, + induction c using real.ind_mk, + simp only [mk_lt, ← mk_add], + show pos _ ↔ pos _, rw add_sub_add_left_eq_sub +end instance : partial_order ℝ := { le := (≤), lt := (<), - le_refl := λ a, or.inr rfl, - le_trans := λ a b c, quotient.induction_on₃ a b c $ - λ f g h, by simpa [quotient_mk_eq_mk] using le_trans, - lt_iff_le_not_le := λ a b, quotient.induction_on₂ a b $ - λ f g, by simpa [quotient_mk_eq_mk] using lt_iff_le_not_le, - le_antisymm := λ a b, quotient.induction_on₂ a b $ - λ f g, by simpa [mk_eq, quotient_mk_eq_mk] using @cau_seq.le_antisymm _ _ f g } + lt_iff_le_not_le := λ a b, real.ind_mk a $ λ a, real.ind_mk b $ λ b, + by simpa using lt_iff_le_not_le, + le_refl := λ a, a.ind_mk (by intro a; rw mk_le), + le_trans := λ a b c, real.ind_mk a $ λ a, real.ind_mk b $ λ b, real.ind_mk c $ λ c, + by simpa using le_trans, + lt_iff_le_not_le := λ a b, real.ind_mk a $ λ a, real.ind_mk b $ λ b, + by simpa using lt_iff_le_not_le, + le_antisymm := λ a b, real.ind_mk a $ λ a, real.ind_mk b $ λ b, + by simpa [mk_eq] using @cau_seq.le_antisymm _ _ a b } instance : preorder ℝ := by apply_instance -theorem of_rat_lt {x y : ℚ} : of_rat x < of_rat y ↔ x < y := const_lt +theorem of_rat_lt {x y : ℚ} : of_rat x < of_rat y ↔ x < y := +begin + rw [mk_lt] {md := tactic.transparency.semireducible}, + exact const_lt +end -protected theorem zero_lt_one : (0 : ℝ) < 1 := of_rat_lt.2 zero_lt_one +protected theorem zero_lt_one : (0 : ℝ) < 1 := +by convert of_rat_lt.2 zero_lt_one; simp protected theorem mul_pos {a b : ℝ} : 0 < a → 0 < b → 0 < a * b := -quotient.induction_on₂ a b $ λ f g, - show pos (f - 0) → pos (g - 0) → pos (f * g - 0), - by simpa using cau_seq.mul_pos +begin + induction a using real.ind_mk with a, + induction b using real.ind_mk with b, + simpa only [mk_lt, mk_pos, ← mk_mul] using cau_seq.mul_pos +end instance : ordered_ring ℝ := -{ add_le_add_left := λ a b h c, h.imp (real.add_lt_add_iff_left c).2 (λ h, h ▸ rfl), +{ add_le_add_left := + begin + simp only [le_iff_eq_or_lt], + rintros a b ⟨rfl, h⟩, + { simp }, + { exact λ c, or.inr ((add_lt_add_iff_left c).2 ‹_›) } + end, zero_le_one := le_of_lt real.zero_lt_one, mul_pos := @real.mul_pos, .. real.comm_ring, .. real.partial_order, .. real.semiring } @@ -114,18 +195,17 @@ instance : ordered_semiring ℝ := by apply_instance instance : ordered_add_comm_group ℝ := by apply_instance instance : ordered_cancel_add_comm_monoid ℝ := by apply_instance instance : ordered_add_comm_monoid ℝ := by apply_instance -instance : has_one ℝ := by apply_instance -instance : has_zero ℝ := by apply_instance -instance : has_mul ℝ := by apply_instance -instance : has_add ℝ := by apply_instance -instance : has_sub ℝ := by apply_instance instance : nontrivial ℝ := ⟨⟨0, 1, ne_of_lt real.zero_lt_one⟩⟩ open_locale classical noncomputable instance : linear_order ℝ := -{ le_total := λ a b, quotient.induction_on₂ a b $ - λ f g, by simpa [quotient_mk_eq_mk] using le_total f g, +{ le_total := begin + intros a b, + induction a using real.ind_mk with a, + induction b using real.ind_mk with b, + simpa using le_total a b, + end, decidable_le := by apply_instance, .. real.partial_order } @@ -138,10 +218,21 @@ noncomputable instance : linear_ordered_semiring ℝ := by apply_instance instance : domain ℝ := { .. real.nontrivial, .. real.comm_ring, .. linear_ordered_ring.to_domain } +@[irreducible] private noncomputable def inv' : ℝ → ℝ | ⟨a⟩ := ⟨a⁻¹⟩ +noncomputable instance : has_inv ℝ := ⟨inv'⟩ +lemma inv_cauchy {f} : (⟨f⟩ : ℝ)⁻¹ = ⟨f⁻¹⟩ := show inv' _ = _, by rw inv' + noncomputable instance : linear_ordered_field ℝ := -{ ..real.linear_ordered_comm_ring, - ..real.domain, - ..cau_seq.completion.field } +{ inv := has_inv.inv, + mul_inv_cancel := begin + rintros ⟨a⟩ h, + rw mul_comm, + simp only [inv_cauchy, mul_cauchy, ← one_cauchy, ← zero_cauchy, ne.def] at *, + exact cau_seq.completion.inv_mul_cancel h, + end, + inv_zero := by simp [← zero_cauchy, inv_cauchy], + ..real.linear_ordered_comm_ring, + ..real.domain } /- Extra instances to short-circuit type class resolution -/ @@ -166,23 +257,30 @@ of_rat.eq_rat_cast theorem le_mk_of_forall_le {f : cau_seq ℚ abs} : (∃ i, ∀ j ≥ i, x ≤ f j) → x ≤ mk f := -quotient.induction_on x $ λ g h, le_of_not_lt $ -λ ⟨K, K0, hK⟩, -let ⟨i, H⟩ := exists_forall_ge_and h $ - exists_forall_ge_and hK (f.cauchy₃ $ half_pos K0) in begin + intro h, + induction x using real.ind_mk with x, + apply le_of_not_lt, + rw mk_lt, + rintro ⟨K, K0, hK⟩, + obtain ⟨i, H⟩ := exists_forall_ge_and h + (exists_forall_ge_and hK (f.cauchy₃ $ half_pos K0)), apply not_lt_of_le (H _ (le_refl _)).1, rw ← of_rat_eq_cast, + rw [mk_lt] {md := tactic.transparency.semireducible}, refine ⟨_, half_pos K0, i, λ j ij, _⟩, have := add_le_add (H _ ij).2.1 (le_of_lt (abs_lt.1 $ (H _ (le_refl _)).2.2 _ ij).1), rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this end -theorem mk_le_of_forall_le {f : cau_seq ℚ abs} {x : ℝ} : - (∃ i, ∀ j ≥ i, (f j : ℝ) ≤ x) → mk f ≤ x -| ⟨i, H⟩ := by rw [← neg_le_neg_iff, ← mk_eq_mk, mk_neg]; exact - le_mk_of_forall_le ⟨i, λ j ij, by simp [H _ ij]⟩ +theorem mk_le_of_forall_le {f : cau_seq ℚ abs} {x : ℝ} + (h : ∃ i, ∀ j ≥ i, (f j : ℝ) ≤ x) : mk f ≤ x := +begin + cases h with i H, + rw [← neg_le_neg_iff, ← mk_neg], + exact le_mk_of_forall_le ⟨i, λ j ij, by simp [H _ ij]⟩ +end theorem mk_near_of_forall_near {f : cau_seq ℚ abs} {x : ℝ} {ε : ℝ} (H : ∃ i, ∀ j ≥ i, abs ((f j : ℝ) - x) ≤ ε) : abs (mk f - x) ≤ ε := @@ -193,17 +291,11 @@ abs_sub_le_iff.2 H.imp $ λ i h j ij, sub_le.1 (abs_sub_le_iff.1 $ h j ij).2⟩ instance : archimedean ℝ := -archimedean_iff_rat_le.2 $ λ x, quotient.induction_on x $ λ f, +archimedean_iff_rat_le.2 $ λ x, real.ind_mk x $ λ f, let ⟨M, M0, H⟩ := f.bounded' 0 in ⟨M, mk_le_of_forall_le ⟨0, λ i _, rat.cast_le.2 $ le_of_lt (abs_lt.1 (H i)).2⟩⟩ -/- mark `real` irreducible in order to prevent `auto_cases` unfolding reals, -since users rarely want to consider real numbers as Cauchy sequences. -Marking `comm_ring_aux` `irreducible` is done to ensure that there are no problems -with non definitionally equal instances, caused by making `real` irreducible-/ -attribute [irreducible] real comm_ring_aux - noncomputable instance : floor_ring ℝ := archimedean.floor_ring _ theorem is_cau_seq_iff_lift {f : ℕ → ℚ} : is_cau_seq abs f ↔ is_cau_seq abs (λ i, (f i : ℝ)) := @@ -296,13 +388,9 @@ theorem Sup_le (S : set ℝ) (h₁ : ∃ x, x ∈ S) (h₂ : ∃ x, ∀ y ∈ S, by simp [Sup_def, h₁, h₂]; exact classical.some_spec (exists_sup S h₁ h₂) y -section --- this proof times out without this -local attribute [instance, priority 1000] classical.prop_decidable theorem lt_Sup (S : set ℝ) (h₁ : ∃ x, x ∈ S) (h₂ : ∃ x, ∀ y ∈ S, y ≤ x) {y} : y < Sup S ↔ ∃ z ∈ S, y < z := by simpa [not_forall] using not_congr (@Sup_le S h₁ h₂ y) -end theorem le_Sup (S : set ℝ) (h₂ : ∃ x, ∀ y ∈ S, y ≤ x) {x} (xS : x ∈ S) : x ≤ Sup S := (Sup_le S ⟨_, xS⟩ h₂).1 (le_refl _) _ xS @@ -410,6 +498,4 @@ end noncomputable instance : cau_seq.is_complete ℝ abs := ⟨cau_seq_converges⟩ -attribute [irreducible] real.le - end real diff --git a/src/data/real/cardinality.lean b/src/data/real/cardinality.lean index eca413c7e62fb..c5227fbe27007 100644 --- a/src/data/real/cardinality.lean +++ b/src/data/real/cardinality.lean @@ -7,6 +7,7 @@ import set_theory.cardinal_ordinal import analysis.specific_limits import data.rat.denumerable import data.set.intervals.image_preimage + /-! # The cardinality of the reals @@ -34,9 +35,11 @@ We conclude that all intervals with distinct endpoints have cardinality continuu ## Tags continuum, cardinality, reals, cardinality of the reals -/ + open nat set open_locale cardinal noncomputable theory + namespace cardinal variables {c : ℝ} {f g : ℕ → bool} {n : ℕ} @@ -141,7 +144,8 @@ end lemma mk_real : #ℝ = 2 ^ omega.{0} := begin apply le_antisymm, - { dsimp [real], apply le_trans mk_quotient_le, apply le_trans (mk_subtype_le _), + { rw real.equiv_Cauchy.cardinal_eq, + apply mk_quotient_le.trans, apply (mk_subtype_le _).trans, rw [←power_def, mk_nat, mk_rat, power_self_eq (le_refl _)] }, { convert mk_le_of_injective (cantor_function_injective _ _), rw [←power_def, mk_bool, mk_nat], exact 1 / 3, norm_num, norm_num } diff --git a/src/measure_theory/lebesgue_measure.lean b/src/measure_theory/lebesgue_measure.lean index da1a5667cbe65..c43c3ad308b9d 100644 --- a/src/measure_theory/lebesgue_measure.lean +++ b/src/measure_theory/lebesgue_measure.lean @@ -365,7 +365,8 @@ by simpa only [mul_comm] using real.map_volume_mul_left h @[simp] lemma map_volume_neg : measure.map has_neg.neg (volume : measure ℝ) = volume := eq.symm $ real.measure_ext_Ioo_rat $ λ p q, - by simp [measure.map_apply measurable_neg measurable_set_Ioo] + by simp [show measure.map has_neg.neg volume (Ioo (p : ℝ) q) = _, + from measure.map_apply measurable_neg measurable_set_Ioo] end real diff --git a/src/set_theory/cardinal.lean b/src/set_theory/cardinal.lean index c1759eb9defda..7213301863fd4 100644 --- a/src/set_theory/cardinal.lean +++ b/src/set_theory/cardinal.lean @@ -93,6 +93,9 @@ theorem le_mk_iff_exists_set {c : cardinal} {α : Type u} : theorem out_embedding {c c' : cardinal} : c ≤ c' ↔ nonempty (c.out ↪ c'.out) := by { transitivity _, rw [←quotient.out_eq c, ←quotient.out_eq c'], refl } +protected lemma eq_congr : α ≃ β → # α = # β := +λ h, quot.sound ⟨h⟩ + noncomputable instance : linear_order cardinal.{u} := { le := (≤), le_refl := by rintros ⟨α⟩; exact ⟨embedding.refl _⟩, @@ -1081,3 +1084,6 @@ lemma powerlt_zero {a : cardinal} : a ^< 0 = 0 := by { apply sup_eq_zero, rintro ⟨x, hx⟩, rw [←not_le] at hx, apply hx, apply zero_le } end cardinal + +lemma equiv.cardinal_eq {α β} : α ≃ β → cardinal.mk α = cardinal.mk β := +cardinal.eq_congr diff --git a/src/topology/path_connected.lean b/src/topology/path_connected.lean index 080b0418a3763..ce8e1917e1527 100644 --- a/src/topology/path_connected.lean +++ b/src/topology/path_connected.lean @@ -168,7 +168,7 @@ begin simp only [ mem_range, path.symm, has_coe_to_fun.coe, coe_fn, I_symm, set_coe.exists, comp_app, subtype.coe_mk, subtype.val_eq_coe ], split; rintros ⟨y, hy, hxy⟩; refine ⟨1-y, Icc_zero_one_symm.mp hy, _⟩; convert hxy, - exact sub_sub_cancel _ _ + simp end /-- A continuous map extending a path to `ℝ`, constant before `0` and after `1`. -/