From d6fe605f4f028b34543a9394037a8c497ab9c588 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sat, 30 Jan 2021 14:50:34 +0000 Subject: [PATCH] chore(*): split some long lines (#5959) --- src/category_theory/elements.lean | 12 ++-- src/category_theory/equivalence.lean | 33 ++++++---- src/category_theory/is_connected.lean | 9 +-- src/category_theory/limits/cones.lean | 22 ++++--- .../limits/preserves/basic.lean | 39 ++++++++---- src/data/bitvec/basic.lean | 11 ++-- src/data/complex/exponential.lean | 9 ++- src/data/equiv/mul_add.lean | 9 ++- src/data/holor.lean | 11 ++-- src/data/matrix/pequiv.lean | 7 ++- src/data/multiset/basic.lean | 62 ++++++++++++------- src/group_theory/free_abelian_group.lean | 39 ++++++++---- src/ring_theory/polynomial/basic.lean | 19 ++++-- src/topology/algebra/group.lean | 4 +- src/topology/algebra/module.lean | 14 +++-- src/topology/metric_space/emetric_space.lean | 22 ++++--- .../gromov_hausdorff_realized.lean | 36 +++++++---- test/general_recursion.lean | 27 +++++--- 18 files changed, 244 insertions(+), 141 deletions(-) diff --git a/src/category_theory/elements.lean b/src/category_theory/elements.lean index 91489d5da2e6a..b73e5d4ef434a 100644 --- a/src/category_theory/elements.lean +++ b/src/category_theory/elements.lean @@ -10,14 +10,17 @@ import category_theory.punit /-! # The category of elements -This file defines the category of elements, also known as (a special case of) the Grothendieck construction. +This file defines the category of elements, also known as (a special case of) the Grothendieck +construction. Given a functor `F : C ⥤ Type`, an object of `F.elements` is a pair `(X : C, x : F.obj X)`. A morphism `(X, x) ⟶ (Y, y)` is a morphism `f : X ⟶ Y` in `C`, so `F.map f` takes `x` to `y`. ## Implementation notes -This construction is equivalent to a special case of a comma construction, so this is mostly just -a more convenient API. We prove the equivalence in `category_theory.category_of_elements.comma_equivalence`. + +This construction is equivalent to a special case of a comma construction, so this is mostly just a +more convenient API. We prove the equivalence in +`category_theory.category_of_elements.comma_equivalence`. ## References * [Emily Riehl, *Category Theory in Context*, Section 2.4][riehl2017] @@ -61,7 +64,8 @@ subtype.ext_val w end category_of_elements -instance groupoid_of_elements {G : Type u} [groupoid.{v} G] (F : G ⥤ Type w) : groupoid F.elements := +instance groupoid_of_elements {G : Type u} [groupoid.{v} G] (F : G ⥤ Type w) : + groupoid F.elements := { inv := λ p q f, ⟨inv f.val, calc F.map (inv f.val) q.2 = F.map (inv f.val) (F.map f.val p.2) : by rw f.2 ... = (F.map f.val ≫ F.map (inv f.val)) p.2 : by simp diff --git a/src/category_theory/equivalence.lean b/src/category_theory/equivalence.lean index 858c18457e203..478645c08ada9 100644 --- a/src/category_theory/equivalence.lean +++ b/src/category_theory/equivalence.lean @@ -54,7 +54,8 @@ We write `C ≌ D` (`\backcong`, not to be confused with `≅`/`\cong`) for a bu namespace category_theory open category_theory.functor nat_iso category -universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation +-- declare the `v`'s first; see `category_theory.category` for an explanation +universes v₁ v₂ v₃ u₁ u₂ u₃ /-- We define an equivalence as a (half)-adjoint equivalence, a pair of functors with a unit and counit which are natural isomorphisms and the triangle law `Fη ≫ εF = 1`, or in other @@ -238,16 +239,19 @@ variables {E : Type u₃} [category.{v₃} E] exact iso_whisker_left f.inverse (iso_whisker_right e.counit_iso f.functor) end, -- We wouldn't have needed to give this proof if we'd used `equivalence.mk`, - -- but we choose to avoid using that here, for the sake of good structure projection `simp` lemmas. + -- but we choose to avoid using that here, for the sake of good structure projection `simp` + -- lemmas. functor_unit_iso_comp' := λ X, begin dsimp, rw [← f.functor.map_comp_assoc, e.functor.map_comp, ←counit_inv_app_functor, fun_inv_map, - iso.inv_hom_id_app_assoc, assoc, iso.inv_hom_id_app, counit_app_functor, ← functor.map_comp], + iso.inv_hom_id_app_assoc, assoc, iso.inv_hom_id_app, counit_app_functor, + ← functor.map_comp], erw [comp_id, iso.hom_inv_id_app, functor.map_id], end } -/-- Composing a functor with both functors of an equivalence yields a naturally isomorphic functor. -/ +/-- Composing a functor with both functors of an equivalence yields a naturally isomorphic +functor. -/ def fun_inv_id_assoc (e : C ≌ D) (F : C ⥤ E) : e.functor ⋙ e.inverse ⋙ F ≅ F := (functor.associator _ _ _).symm ≪≫ iso_whisker_right e.unit_iso.symm F ≪≫ F.left_unitor @@ -259,7 +263,8 @@ by { dsimp [fun_inv_id_assoc], tidy } (fun_inv_id_assoc e F).inv.app X = F.map (e.unit.app X) := by { dsimp [fun_inv_id_assoc], tidy } -/-- Composing a functor with both functors of an equivalence yields a naturally isomorphic functor. -/ +/-- Composing a functor with both functors of an equivalence yields a naturally isomorphic +functor. -/ def inv_fun_id_assoc (e : C ≌ D) (F : D ⥤ E) : e.inverse ⋙ e.functor ⋙ F ≅ F := (functor.associator _ _ _).symm ≪≫ iso_whisker_right e.counit_iso F ≪≫ F.left_unitor @@ -296,11 +301,11 @@ equivalence.mk section cancellation_lemmas variables (e : C ≌ D) --- We need special forms of `cancel_nat_iso_hom_right(_assoc)` and `cancel_nat_iso_inv_right(_assoc)` --- for units and counits, because neither `simp` or `rw` will apply those lemmas in this --- setting without providing `e.unit_iso` (or similar) as an explicit argument. --- We also provide the lemmas for length four compositions, since they're occasionally useful. --- (e.g. in proving that equivalences take monos to monos) +/- We need special forms of `cancel_nat_iso_hom_right(_assoc)` and +`cancel_nat_iso_inv_right(_assoc)` for units and counits, because neither `simp` or `rw` will apply +those lemmas in this setting without providing `e.unit_iso` (or similar) as an explicit argument. +We also provide the lemmas for length four compositions, since they're occasionally useful. +(e.g. in proving that equivalences take monos to monos) -/ @[simp] lemma cancel_unit_right {X Y : C} (f f' : X ⟶ Y) : @@ -521,10 +526,12 @@ See https://stacks.math.columbia.edu/tag/02C3. @[priority 100] -- see Note [lower instance priority] instance full_of_equivalence (F : C ⥤ D) [is_equivalence F] : full F := { preimage := λ X Y f, F.fun_inv_id.inv.app X ≫ F.inv.map f ≫ F.fun_inv_id.hom.app Y, - witness' := λ X Y f, F.inv.map_injective - (by simpa only [is_equivalence.inv_fun_map, assoc, iso.hom_inv_id_app_assoc, iso.hom_inv_id_app] using comp_id _) } + witness' := λ X Y f, F.inv.map_injective $ + by simpa only [is_equivalence.inv_fun_map, assoc, iso.hom_inv_id_app_assoc, iso.hom_inv_id_app] + using comp_id _ } -@[simps] private noncomputable def equivalence_inverse (F : C ⥤ D) [full F] [faithful F] [ess_surj F] : D ⥤ C := +@[simps] private noncomputable def equivalence_inverse (F : C ⥤ D) [full F] [faithful F] + [ess_surj F] : D ⥤ C := { obj := λ X, F.obj_preimage X, map := λ X Y f, F.preimage ((F.obj_obj_preimage_iso X).hom ≫ f ≫ (F.obj_obj_preimage_iso Y).inv), map_id' := λ X, begin apply F.map_injective, tidy end, diff --git a/src/category_theory/is_connected.lean b/src/category_theory/is_connected.lean index 126b4e3c3de34..bec73cf91a359 100644 --- a/src/category_theory/is_connected.lean +++ b/src/category_theory/is_connected.lean @@ -121,7 +121,8 @@ This can be thought of as a local-to-global property. The converse of `constant_of_preserves_morphisms`. -/ lemma is_connected.of_constant_of_preserves_morphisms [nonempty J] - (h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (f : j₁ ⟶ j₂), F j₁ = F j₂) → (∀ j j' : J, F j = F j')) : + (h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (f : j₁ ⟶ j₂), F j₁ = F j₂) → + (∀ j j' : J, F j = F j')) : is_connected J := is_connected.of_any_functor_const_on_obj (λ _ F, h F.obj (λ _ _ f, (F.map f).down.1)) @@ -147,8 +148,8 @@ If any maximal connected component containing some element j₀ of J is all of J The converse of `induct_on_objects`. -/ -lemma is_connected.of_induct [nonempty J] - {j₀ : J} (h : ∀ (p : set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (f : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p) : +lemma is_connected.of_induct [nonempty J] {j₀ : J} + (h : ∀ (p : set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (f : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p) : is_connected J := is_connected.of_constant_of_preserves_morphisms (λ α F a, begin @@ -247,7 +248,7 @@ lemma equiv_relation [is_connected J] (r : J → J → Prop) (hr : _root_.equiva begin have z : ∀ (j : J), r (classical.arbitrary J) j := induct_on_objects (λ k, r (classical.arbitrary J) k) - (hr.1 (classical.arbitrary J)) (λ _ _ f, ⟨λ t, hr.2.2 t (h f), λ t, hr.2.2 t (hr.2.1 (h f))⟩), + (hr.1 (classical.arbitrary J)) (λ _ _ f, ⟨λ t, hr.2.2 t (h f), λ t, hr.2.2 t (hr.2.1 (h f))⟩), intros, apply hr.2.2 (hr.2.1 (z _)) (z _) end diff --git a/src/category_theory/limits/cones.lean b/src/category_theory/limits/cones.lean index 9ca595e1bc850..bb78c4a32a87b 100644 --- a/src/category_theory/limits/cones.lean +++ b/src/category_theory/limits/cones.lean @@ -327,7 +327,8 @@ instance reflects_cone_isomorphism (F : C ⥤ D) [reflects_isomorphisms F] (K : begin constructor, introsI, - haveI : is_iso (F.map f.hom) := (cones.forget (K ⋙ F)).map_is_iso ((cones.functoriality K F).map f), + haveI : is_iso (F.map f.hom) := + (cones.forget (K ⋙ F)).map_is_iso ((cones.functoriality K F).map f), haveI := reflects_isomorphisms.reflects F f.hom, apply cone_iso_of_hom_iso end @@ -373,9 +374,8 @@ def cocone_iso_of_hom_iso {K : J ⥤ C} {c d : cocone K} (f : c ⟶ d) [i : is_i { hom := i.inv, w' := λ j, (as_iso f.hom).comp_inv_eq.2 (f.w j).symm } } -/-- -Functorially precompose a cocone for `F` by a natural transformation `G ⟶ F` to give a cocone for `G`. --/ +/-- Functorially precompose a cocone for `F` by a natural transformation `G ⟶ F` to give a cocone +for `G`. -/ @[simps] def precompose {G : J ⥤ C} (α : G ⟶ F) : cocone F ⥤ cocone G := { obj := λ c, { X := c.X, ι := α ≫ c.ι }, map := λ c₁ c₂ f, { hom := f.hom } } @@ -417,7 +417,8 @@ def whiskering_equivalence {K : Type v} [small_category K] (e : K ≌ J) : cocone F ≌ cocone (e.functor ⋙ F) := { functor := whiskering e.functor, inverse := whiskering e.inverse ⋙ - precompose ((functor.left_unitor F).inv ≫ (whisker_right (e.counit_iso).inv F) ≫ (functor.associator _ _ _).inv), + precompose ((functor.left_unitor F).inv ≫ (whisker_right (e.counit_iso).inv F) ≫ + (functor.associator _ _ _).inv), unit_iso := nat_iso.of_components (λ s, cocones.ext (iso.refl _) (by tidy)) (by tidy), counit_iso := nat_iso.of_components (λ s, cocones.ext (iso.refl _) (begin @@ -483,8 +484,8 @@ let f : (F ⋙ e.functor) ⋙ e.inverse ≅ F := -- In this configuration `simp` reaches a dead-end and needs help. intros j, dsimp, - simp only [←equivalence.counit_inv_app_functor, iso.inv_hom_id_app, map_comp, equivalence.fun_inv_map, - assoc, id_comp, iso.inv_hom_id_app_assoc], + simp only [←equivalence.counit_inv_app_functor, iso.inv_hom_id_app, map_comp, + equivalence.fun_inv_map, assoc, id_comp, iso.inv_hom_id_app_assoc], dsimp, simp, -- See note [dsimp, simp]. end) (by tidy), } @@ -497,7 +498,8 @@ instance reflects_cocone_isomorphism (F : C ⥤ D) [reflects_isomorphisms F] (K begin constructor, introsI, - haveI : is_iso (F.map f.hom) := (cocones.forget (K ⋙ F)).map_is_iso ((cocones.functoriality K F).map f), + haveI : is_iso (F.map f.hom) := + (cocones.forget (K ⋙ F)).map_is_iso ((cocones.functoriality K F).map f), haveI := reflects_isomorphisms.reflects F f.hom, apply cocone_iso_of_hom_iso end @@ -524,7 +526,9 @@ def map_cocone (c : cocone F) : cocone (F ⋙ H) := (cocones.functoriality F H). /-- Given a cone morphism `c ⟶ c'`, construct a cone morphism on the mapped cones functorially. -/ def map_cone_morphism {c c' : cone F} (f : c ⟶ c') : H.map_cone c ⟶ H.map_cone c' := (cones.functoriality F H).map f -/-- Given a cocone morphism `c ⟶ c'`, construct a cocone morphism on the mapped cocones functorially. -/ + +/-- Given a cocone morphism `c ⟶ c'`, construct a cocone morphism on the mapped cocones +functorially. -/ def map_cocone_morphism {c c' : cocone F} (f : c ⟶ c') : H.map_cocone c ⟶ H.map_cocone c' := (cocones.functoriality F H).map f diff --git a/src/category_theory/limits/preserves/basic.lean b/src/category_theory/limits/preserves/basic.lean index b7a2780fcf2e1..18761bcd3f116 100644 --- a/src/category_theory/limits/preserves/basic.lean +++ b/src/category_theory/limits/preserves/basic.lean @@ -64,16 +64,19 @@ class preserves_limits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) : (preserves_limit : Π {K : J ⥤ C}, preserves_limit K F) /-- We say that `F` preserves colimits of shape `J` if `F` preserves colimits for every diagram `K : J ⥤ C`, i.e., `F` maps colimit cocones over `K` to colimit cocones. -/ -class preserves_colimits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) : Type (max u₁ u₂ v) := +class preserves_colimits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) : + Type (max u₁ u₂ v) := (preserves_colimit : Π {K : J ⥤ C}, preserves_colimit K F) /-- We say that `F` preserves limits if it sends limit cones over any diagram to limit cones. -/ class preserves_limits (F : C ⥤ D) : Type (max u₁ u₂ (v+1)) := -(preserves_limits_of_shape : Π {J : Type v} [𝒥 : small_category J], by exactI preserves_limits_of_shape J F) +(preserves_limits_of_shape : Π {J : Type v} [𝒥 : small_category J], + by exactI preserves_limits_of_shape J F) /-- We say that `F` preserves colimits if it sends colimit cocones over any diagram to colimit cocones.-/ class preserves_colimits (F : C ⥤ D) : Type (max u₁ u₂ (v+1)) := -(preserves_colimits_of_shape : Π {J : Type v} [𝒥 : small_category J], by exactI preserves_colimits_of_shape J F) +(preserves_colimits_of_shape : Π {J : Type v} [𝒥 : small_category J], + by exactI preserves_colimits_of_shape J F) attribute [instance, priority 100] -- see Note [lower instance priority] preserves_limits_of_shape.preserves_limit preserves_limits.preserves_limits_of_shape @@ -96,9 +99,11 @@ def is_colimit_of_preserves (F : C ⥤ D) {c : cocone K} (t : is_colimit c) is_colimit (F.map_cocone c) := preserves_colimit.preserves t -instance preserves_limit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : subsingleton (preserves_limit K F) := +instance preserves_limit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : + subsingleton (preserves_limit K F) := by split; rintros ⟨a⟩ ⟨b⟩; congr -instance preserves_colimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : subsingleton (preserves_colimit K F) := +instance preserves_colimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : + subsingleton (preserves_colimit K F) := by split; rintros ⟨a⟩ ⟨b⟩; congr instance preserves_limits_of_shape_subsingleton (J : Type v) [small_category J] (F : C ⥤ D) : @@ -118,14 +123,16 @@ instance id_preserves_limits : preserves_limits (𝟭 C) := { preserves_limit := λ K, by exactI ⟨λ c h, ⟨λ s, h.lift ⟨s.X, λ j, s.π.app j, λ j j' f, s.π.naturality f⟩, by cases K; rcases c with ⟨_, _, _⟩; intros s j; cases s; exact h.fac _ j, - by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; exact h.uniq _ m w⟩⟩ } } + by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; + exact h.uniq _ m w⟩⟩ } } instance id_preserves_colimits : preserves_colimits (𝟭 C) := { preserves_colimits_of_shape := λ J 𝒥, { preserves_colimit := λ K, by exactI ⟨λ c h, ⟨λ s, h.desc ⟨s.X, λ j, s.ι.app j, λ j j' f, s.ι.naturality f⟩, by cases K; rcases c with ⟨_, _, _⟩; intros s j; cases s; exact h.fac _ j, - by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; exact h.uniq _ m w⟩⟩ } } + by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; + exact h.uniq _ m w⟩⟩ } } section variables {E : Type u₃} [ℰ : category.{v} E] @@ -294,7 +301,8 @@ the cone was already a limit cone in `C`. Note that we do not assume a priori that `D` actually has any limits. -/ class reflects_limits (F : C ⥤ D) : Type (max u₁ u₂ (v+1)) := -(reflects_limits_of_shape : Π {J : Type v} {𝒥 : small_category J}, by exactI reflects_limits_of_shape J F) +(reflects_limits_of_shape : Π {J : Type v} {𝒥 : small_category J}, + by exactI reflects_limits_of_shape J F) /-- A functor `F : C ⥤ D` reflects colimits if whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit cocone in `D`, @@ -302,7 +310,8 @@ the cocone was already a colimit cocone in `C`. Note that we do not assume a priori that `D` actually has any colimits. -/ class reflects_colimits (F : C ⥤ D) : Type (max u₁ u₂ (v+1)) := -(reflects_colimits_of_shape : Π {J : Type v} {𝒥 : small_category J}, by exactI reflects_colimits_of_shape J F) +(reflects_colimits_of_shape : Π {J : Type v} {𝒥 : small_category J}, + by exactI reflects_colimits_of_shape J F) /-- A convenience function for `reflects_limit`, which takes the functor as an explicit argument to @@ -323,7 +332,8 @@ reflects_colimit.reflects t instance reflects_limit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : subsingleton (reflects_limit K F) := by split; rintros ⟨a⟩ ⟨b⟩; congr -instance reflects_colimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : subsingleton (reflects_colimit K F) := +instance reflects_colimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : + subsingleton (reflects_colimit K F) := by split; rintros ⟨a⟩ ⟨b⟩; congr instance reflects_limits_of_shape_subsingleton (J : Type v) [small_category J] (F : C ⥤ D) : @@ -361,14 +371,16 @@ instance id_reflects_limits : reflects_limits (𝟭 C) := { reflects_limit := λ K, by exactI ⟨λ c h, ⟨λ s, h.lift ⟨s.X, λ j, s.π.app j, λ j j' f, s.π.naturality f⟩, by cases K; rcases c with ⟨_, _, _⟩; intros s j; cases s; exact h.fac _ j, - by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; exact h.uniq _ m w⟩⟩ } } + by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; + exact h.uniq _ m w⟩⟩ } } instance id_reflects_colimits : reflects_colimits (𝟭 C) := { reflects_colimits_of_shape := λ J 𝒥, { reflects_colimit := λ K, by exactI ⟨λ c h, ⟨λ s, h.desc ⟨s.X, λ j, s.ι.app j, λ j j' f, s.ι.naturality f⟩, by cases K; rcases c with ⟨_, _, _⟩; intros s j; cases s; exact h.fac _ j, - by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; exact h.uniq _ m w⟩⟩ } } + by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; + exact h.uniq _ m w⟩⟩ } } section variables {E : Type u₃} [ℰ : category.{v} E] @@ -569,7 +581,8 @@ def fully_faithful_reflects_colimits [full F] [faithful F] : reflects_colimits F { reflects_colimits_of_shape := λ J 𝒥₁, by exactI { reflects_colimit := λ K, { reflects := λ c t, - is_colimit.mk_cocone_morphism (λ s, (cocones.functoriality K F).preimage (t.desc_cocone_morphism _)) $ + is_colimit.mk_cocone_morphism + (λ s, (cocones.functoriality K F).preimage (t.desc_cocone_morphism _)) $ begin apply (λ s m, (cocones.functoriality K F).map_injective _), rw [functor.image_preimage], diff --git a/src/data/bitvec/basic.lean b/src/data/bitvec/basic.lean index 3e77ff7c390c5..d586a2f9bff92 100644 --- a/src/data/bitvec/basic.lean +++ b/src/data/bitvec/basic.lean @@ -55,8 +55,8 @@ by cases b; simp only [nat.add_mul_div_left, add_lsb, ←two_mul, add_comm, nat. nat.mul_div_right, gt_iff_lt, zero_add, cond]; norm_num lemma to_bool_add_lsb_mod_two {x b} : to_bool (add_lsb x b % 2 = 1) = b := -by cases b; simp only [to_bool_iff, nat.add_mul_mod_self_left, add_lsb, ←two_mul, add_comm, bool.to_bool_false, - nat.mul_mod_right, zero_add, cond, zero_ne_one]; norm_num +by cases b; simp only [to_bool_iff, nat.add_mul_mod_self_left, add_lsb, ←two_mul, add_comm, + bool.to_bool_false, nat.mul_mod_right, zero_add, cond, zero_ne_one]; norm_num lemma of_nat_to_nat {n : ℕ} (v : bitvec n) : bitvec.of_nat _ v.to_nat = v := begin @@ -69,9 +69,10 @@ begin generalize_hyp : xs.reverse = ys at ⊢ h, clear xs, induction ys generalizing n, { cases h, simp [bitvec.of_nat] }, - { simp only [←nat.succ_eq_add_one, list.length] at h, - cases h, simp only [bitvec.of_nat, vector.to_list_cons, vector.to_list_nil, list.reverse_cons, vector.to_list_append, list.foldr], - erw [add_lsb_div_two,to_bool_add_lsb_mod_two], + { simp only [←nat.succ_eq_add_one, list.length] at h, subst n, + simp only [bitvec.of_nat, vector.to_list_cons, vector.to_list_nil, list.reverse_cons, + vector.to_list_append, list.foldr], + erw [add_lsb_div_two, to_bool_add_lsb_mod_two], congr, apply ys_ih, refl } end diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index 6201e1df23b61..5948ff9194e58 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -163,7 +163,8 @@ lemma series_ratio_test {f : ℕ → β} (n : ℕ) (r : α) is_cau_seq abv (λ m, ∑ n in range m, f n) := have har1 : abs r < 1, by rwa abs_of_nonneg hr0, begin - refine is_cau_series_of_abv_le_cau n.succ _ (is_cau_geo_series_const (abv (f n.succ) * r⁻¹ ^ n.succ) har1), + refine is_cau_series_of_abv_le_cau n.succ _ + (is_cau_geo_series_const (abv (f n.succ) * r⁻¹ ^ n.succ) har1), assume m hmn, cases classical.em (r = 0) with r_zero r_ne_zero, { have m_pos := lt_of_lt_of_le (nat.succ_pos n) hmn, @@ -542,7 +543,8 @@ lemma cosh_sub : cosh (x - y) = cosh x * cosh y - sinh x * sinh y := by simp [sub_eq_add_neg, cosh_add, sinh_neg, cosh_neg] lemma sinh_conj : sinh (conj x) = conj (sinh x) := -by rw [sinh, ← conj.map_neg, exp_conj, exp_conj, ← conj.map_sub, sinh, conj.map_div, conj_bit0, conj.map_one] +by rw [sinh, ← conj.map_neg, exp_conj, exp_conj, ← conj.map_sub, sinh, conj.map_div, conj_bit0, + conj.map_one] @[simp] lemma of_real_sinh_of_real_re (x : ℝ) : ((sinh x).re : ℂ) = sinh x := eq_conj_iff_re.1 $ by rw [← sinh_conj, conj_of_real] @@ -875,7 +877,8 @@ lemma exp_eq_exp_re_mul_sin_add_cos : exp x = exp x.re * (cos x.im + sin x.im * by rw [← exp_add_mul_I, re_add_im] /-- De Moivre's formula -/ -theorem cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) : (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I := +theorem cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) : + (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I := begin rw [← exp_mul_I, ← exp_mul_I], induction n with n ih, diff --git a/src/data/equiv/mul_add.lean b/src/data/equiv/mul_add.lean index 83f6b2e48905a..bd7473766e2b5 100644 --- a/src/data/equiv/mul_add.lean +++ b/src/data/equiv/mul_add.lean @@ -391,7 +391,8 @@ section type_tags /-- Reinterpret `G ≃+ H` as `multiplicative G ≃* multiplicative H`. -/ def add_equiv.to_multiplicative [add_monoid G] [add_monoid H] : (G ≃+ H) ≃ (multiplicative G ≃* multiplicative H) := -{ to_fun := λ f, ⟨f.to_add_monoid_hom.to_multiplicative, f.symm.to_add_monoid_hom.to_multiplicative, f.3, f.4, f.5⟩, +{ to_fun := λ f, ⟨f.to_add_monoid_hom.to_multiplicative, + f.symm.to_add_monoid_hom.to_multiplicative, f.3, f.4, f.5⟩, inv_fun := λ f, ⟨f.to_monoid_hom, f.symm.to_monoid_hom, f.3, f.4, f.5⟩, left_inv := λ x, by { ext, refl, }, right_inv := λ x, by { ext, refl, }, } @@ -407,7 +408,8 @@ def mul_equiv.to_additive [monoid G] [monoid H] : /-- Reinterpret `additive G ≃+ H` as `G ≃* multiplicative H`. -/ def add_equiv.to_multiplicative' [monoid G] [add_monoid H] : (additive G ≃+ H) ≃ (G ≃* multiplicative H) := -{ to_fun := λ f, ⟨f.to_add_monoid_hom.to_multiplicative', f.symm.to_add_monoid_hom.to_multiplicative'', f.3, f.4, f.5⟩, +{ to_fun := λ f, ⟨f.to_add_monoid_hom.to_multiplicative', + f.symm.to_add_monoid_hom.to_multiplicative'', f.3, f.4, f.5⟩, inv_fun := λ f, ⟨f.to_monoid_hom, f.symm.to_monoid_hom, f.3, f.4, f.5⟩, left_inv := λ x, by { ext, refl, }, right_inv := λ x, by { ext, refl, }, } @@ -420,7 +422,8 @@ add_equiv.to_multiplicative'.symm /-- Reinterpret `G ≃+ additive H` as `multiplicative G ≃* H`. -/ def add_equiv.to_multiplicative'' [add_monoid G] [monoid H] : (G ≃+ additive H) ≃ (multiplicative G ≃* H) := -{ to_fun := λ f, ⟨f.to_add_monoid_hom.to_multiplicative'', f.symm.to_add_monoid_hom.to_multiplicative', f.3, f.4, f.5⟩, +{ to_fun := λ f, ⟨f.to_add_monoid_hom.to_multiplicative'', + f.symm.to_add_monoid_hom.to_multiplicative', f.3, f.4, f.5⟩, inv_fun := λ f, ⟨f.to_monoid_hom, f.symm.to_monoid_hom, f.3, f.4, f.5⟩, left_inv := λ x, by { ext, refl, }, right_inv := λ x, by { ext, refl, }, } diff --git a/src/data/holor.lean b/src/data/holor.lean index 9e23effb51f64..8d1be3c4daa77 100644 --- a/src/data/holor.lean +++ b/src/data/holor.lean @@ -36,7 +36,8 @@ open list open_locale big_operators -/-- `holor_index ds` is the type of valid index tuples to identify an entry of a holor of dimensions `ds` -/ +/-- `holor_index ds` is the type of valid index tuples used to identify an entry of a holor +of dimensions `ds`. -/ def holor_index (ds : list ℕ) : Type := { is : list ℕ // forall₂ (<) is ds} namespace holor_index @@ -63,7 +64,8 @@ cast (congr_arg holor_index (append_assoc ds₁ ds₂ ds₃).symm) lemma take_take : ∀ t : holor_index (ds₁ ++ ds₂ ++ ds₃), t.assoc_right.take = t.take.take -| ⟨ is , h ⟩ := subtype.eq (by simp [assoc_right,take, cast_type, list.take_take, nat.le_add_right, min_eq_left]) +| ⟨ is , h ⟩ := subtype.eq $ by simp [assoc_right,take, cast_type, list.take_take, + nat.le_add_right, min_eq_left] lemma drop_take : ∀ t : holor_index (ds₁ ++ ds₂ ++ ds₃), @@ -149,7 +151,7 @@ funext (λt, left_distrib (x (holor_index.take t)) (y (holor_index.drop t)) (z ( lemma mul_right_distrib [distrib α] (x : holor α ds₁) (y : holor α ds₁) (z : holor α ds₂) : (x + y) ⊗ z = x ⊗ z + y ⊗ z := -funext (λt, right_distrib (x (holor_index.take t)) (y (holor_index.take t)) (z (holor_index.drop t))) +funext $ λt, add_mul (x (holor_index.take t)) (y (holor_index.take t)) (z (holor_index.drop t)) @[simp] lemma zero_mul {α : Type} [ring α] (x : holor α ds₂) : (0 : holor α ds₁) ⊗ x = 0 := @@ -215,7 +217,8 @@ begin rw [finset.sum_insert h_not_in, ih, slice_add, finset.sum_insert h_not_in] } end -/-- The original holor can be recovered from its slices by multiplying with unit vectors and summing up. -/ +/-- The original holor can be recovered from its slices by multiplying with unit vectors and +summing up. -/ @[simp] lemma sum_unit_vec_mul_slice [ring α] (x : holor α (d :: ds)) : ∑ i in (finset.range d).attach, unit_vec d i ⊗ slice x i (nat.succ_le_of_lt (finset.mem_range.1 i.prop)) = x := diff --git a/src/data/matrix/pequiv.lean b/src/data/matrix/pequiv.lean index 1d3ae2fa76d4c..a685fd159ddd8 100644 --- a/src/data/matrix/pequiv.lean +++ b/src/data/matrix/pequiv.lean @@ -134,13 +134,14 @@ by rw [← to_matrix_trans, single_trans_single_of_ne hb, to_matrix_bot] /-- Restatement of `single_mul_single`, which will simplify expressions in `simp` normal form, when associativity may otherwise need to be carefully applied. -/ -@[simp] lemma single_mul_single_right [decidable_eq k] [decidable_eq m] [decidable_eq n] [semiring α] - (a : m) (b : n) (c : k) (M : matrix k l α) : +@[simp] lemma single_mul_single_right [decidable_eq k] [decidable_eq m] [decidable_eq n] + [semiring α] (a : m) (b : n) (c : k) (M : matrix k l α) : (single a b).to_matrix ⬝ ((single b c).to_matrix ⬝ M) = (single a c).to_matrix ⬝ M := by rw [← matrix.mul_assoc, single_mul_single] /-- We can also define permutation matrices by permuting the rows of the identity matrix. -/ -lemma equiv_to_pequiv_to_matrix [decidable_eq n] [has_zero α] [has_one α] (σ : equiv n n) (i j : n) : +lemma equiv_to_pequiv_to_matrix [decidable_eq n] [has_zero α] [has_one α] (σ : equiv n n) + (i j : n) : σ.to_pequiv.to_matrix i j = (1 : matrix n n α) (σ i) j := if_congr option.some_inj rfl rfl diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean index f774e2106a317..412e593c18ca1 100644 --- a/src/data/multiset/basic.lean +++ b/src/data/multiset/basic.lean @@ -113,7 +113,8 @@ overflow in `whnf`. protected def rec (C_0 : C 0) (C_cons : Πa m, C m → C (a ::ₘ m)) - (C_cons_heq : ∀a a' m b, C_cons a (a' ::ₘ m) (C_cons a' m b) == C_cons a' (a ::ₘ m) (C_cons a m b)) + (C_cons_heq : ∀ a a' m b, C_cons a (a' ::ₘ m) (C_cons a' m b) == + C_cons a' (a ::ₘ m) (C_cons a m b)) (m : multiset α) : C m := quotient.hrec_on m (@list.rec α (λl, C ⟦l⟧) C_0 (λa l b, C_cons a ⟦l⟧ b)) $ assume l l' h, @@ -125,12 +126,14 @@ quotient.hrec_on m (@list.rec α (λl, C ⟦l⟧) C_0 (λa l b, C_cons a ⟦l⟧ protected def rec_on (m : multiset α) (C_0 : C 0) (C_cons : Πa m, C m → C (a ::ₘ m)) - (C_cons_heq : ∀a a' m b, C_cons a (a' ::ₘ m) (C_cons a' m b) == C_cons a' (a ::ₘ m) (C_cons a m b)) : + (C_cons_heq : ∀a a' m b, C_cons a (a' ::ₘ m) (C_cons a' m b) == + C_cons a' (a ::ₘ m) (C_cons a m b)) : C m := multiset.rec C_0 C_cons C_cons_heq m variables {C_0 : C 0} {C_cons : Πa m, C m → C (a ::ₘ m)} - {C_cons_heq : ∀a a' m b, C_cons a (a' ::ₘ m) (C_cons a' m b) == C_cons a' (a ::ₘ m) (C_cons a m b)} + {C_cons_heq : ∀a a' m b, C_cons a (a' ::ₘ m) (C_cons a' m b) == + C_cons a' (a ::ₘ m) (C_cons a m b)} @[simp] lemma rec_on_0 : @multiset.rec_on α C (0:multiset α) C_0 C_cons C_cons_heq = C_0 := rfl @@ -540,7 +543,8 @@ quot.lift_on s (λ l, (l.erase a : multiset α)) quot.induction_on s $ λ l, congr_arg coe $ erase_cons_head a l @[simp, priority 990] -theorem erase_cons_tail {a b : α} (s : multiset α) (h : b ≠ a) : (b ::ₘ s).erase a = b ::ₘ s.erase a := +theorem erase_cons_tail {a b : α} (s : multiset α) (h : b ≠ a) : + (b ::ₘ s).erase a = b ::ₘ s.erase a := quot.induction_on s $ λ l, congr_arg coe $ erase_cons_tail l h @[simp, priority 980] @@ -664,7 +668,8 @@ theorem mem_map_of_injective {f : α → β} (H : function.injective f) {a : α} f a ∈ map f s ↔ a ∈ s := quot.induction_on s $ λ l, mem_map_of_injective H -@[simp] theorem map_map (g : β → γ) (f : α → β) (s : multiset α) : map g (map f s) = map (g ∘ f) s := +@[simp] theorem map_map (g : β → γ) (f : α → β) (s : multiset α) : + map g (map f s) = map (g ∘ f) s := quot.induction_on s $ λ l, congr_arg coe $ list.map_map _ _ _ theorem map_id (s : multiset α) : map id s = s := @@ -675,14 +680,16 @@ quot.induction_on s $ λ l, congr_arg coe $ map_id _ @[simp] theorem map_const (s : multiset α) (b : β) : map (function.const α b) s = repeat b s.card := quot.induction_on s $ λ l, congr_arg coe $ map_const _ _ -@[congr] theorem map_congr {f g : α → β} {s : multiset α} : (∀ x ∈ s, f x = g x) → map f s = map g s := +@[congr] theorem map_congr {f g : α → β} {s : multiset α} : + (∀ x ∈ s, f x = g x) → map f s = map g s := quot.induction_on s $ λ l H, congr_arg coe $ map_congr H lemma map_hcongr {β' : Type*} {m : multiset α} {f : α → β} {f' : α → β'} (h : β = β') (hf : ∀a∈m, f a == f' a) : map f m == map f' m := begin subst h, simp at hf, simp [map_congr hf] end -theorem eq_of_mem_map_const {b₁ b₂ : β} {l : list α} (h : b₁ ∈ map (function.const α b₂) l) : b₁ = b₂ := +theorem eq_of_mem_map_const {b₁ b₂ : β} {l : list α} (h : b₁ ∈ map (function.const α b₂) l) : + b₁ = b₂ := eq_of_mem_repeat $ by rwa map_const at h @[simp] theorem map_le_map {f : α → β} {s t : multiset α} (h : s ≤ t) : map f s ≤ map f t := @@ -702,10 +709,12 @@ quot.lift_on s (λ l, foldl f b l) @[simp] theorem foldl_zero (f : β → α → β) (H b) : foldl f H b 0 = b := rfl -@[simp] theorem foldl_cons (f : β → α → β) (H b a s) : foldl f H b (a ::ₘ s) = foldl f H (f b a) s := +@[simp] theorem foldl_cons (f : β → α → β) (H b a s) : + foldl f H b (a ::ₘ s) = foldl f H (f b a) s := quot.induction_on s $ λ l, rfl -@[simp] theorem foldl_add (f : β → α → β) (H b s t) : foldl f H b (s + t) = foldl f H (foldl f H b s) t := +@[simp] theorem foldl_add (f : β → α → β) (H b s t) : + foldl f H b (s + t) = foldl f H (foldl f H b s) t := quotient.induction_on₂ s t $ λ l₁ l₂, foldl_append _ _ _ _ /-- `foldr f H b s` is the lift of the list operation `foldr f b l`, @@ -717,10 +726,12 @@ quot.lift_on s (λ l, foldr f b l) @[simp] theorem foldr_zero (f : α → β → β) (H b) : foldr f H b 0 = b := rfl -@[simp] theorem foldr_cons (f : α → β → β) (H b a s) : foldr f H b (a ::ₘ s) = f a (foldr f H b s) := +@[simp] theorem foldr_cons (f : α → β → β) (H b a s) : + foldr f H b (a ::ₘ s) = f a (foldr f H b s) := quot.induction_on s $ λ l, rfl -@[simp] theorem foldr_add (f : α → β → β) (H b s t) : foldr f H b (s + t) = foldr f H (foldr f H b t) s := +@[simp] theorem foldr_add (f : α → β → β) (H b s t) : + foldr f H b (s + t) = foldr f H (foldr f H b t) s := quotient.induction_on₂ s t $ λ l₁ l₂, foldr_append _ _ _ _ @[simp] theorem coe_foldr (f : α → β → β) (H : left_commutative f) (b : β) (l : list α) : @@ -971,7 +982,8 @@ by simp [bind]; simp [-exists_and_distrib_right, exists_and_distrib_right.symm]; @[simp] theorem card_bind (s) (f : α → multiset β) : card (bind s f) = sum (map (card ∘ f) s) := by simp [bind] -lemma bind_congr {f g : α → multiset β} {m : multiset α} : (∀a∈m, f a = g a) → bind m f = bind m g := +lemma bind_congr {f g : α → multiset β} {m : multiset α} : + (∀a∈m, f a = g a) → bind m f = bind m g := by simp [bind] {contextual := tt} lemma bind_hcongr {β' : Type*} {m : multiset α} {f : α → multiset β} {f' : α → multiset β'} @@ -1034,7 +1046,8 @@ multiset.induction_on s (λ t u, rfl) $ λ a s IH t u, @[simp] theorem mem_product {s t} : ∀ {p : α × β}, p ∈ @product α β s t ↔ p.1 ∈ s ∧ p.2 ∈ t | (a, b) := by simp [product, and.left_comm] -@[simp] theorem card_product (s : multiset α) (t : multiset β) : card (product s t) = card s * card t := +@[simp] theorem card_product (s : multiset α) (t : multiset β) : + card (product s t) = card s * card t := by simp [product, repeat, (∘), mul_comm] /-! ### Sigma multiset -/ @@ -1288,7 +1301,8 @@ by rw ← eq_union_left h₂; exact union_le_union_right h₁ t ⟨λ h, (mem_add.1 h).imp_left (mem_of_le $ sub_le_self _ _), or.rec (mem_of_le $ le_union_left _ _) (mem_of_le $ le_union_right _ _)⟩ -@[simp] theorem map_union [decidable_eq β] {f : α → β} (finj : function.injective f) {s t : multiset α} : +@[simp] theorem map_union [decidable_eq β] {f : α → β} (finj : function.injective f) + {s t : multiset α} : map f (s ∪ t) = map f s ∪ map f t := quotient.induction_on₂ s t $ λ l₁ l₂, congr_arg coe (by rw [list.map_append f, list.map_diff finj]) @@ -1725,7 +1739,8 @@ begin apply mt eq_of_mem_repeat h₁ }, end -@[simp] theorem count_erase_self (a : α) (s : multiset α) : count a (erase s a) = pred (count a s) := +@[simp] theorem count_erase_self (a : α) (s : multiset α) : + count a (erase s a) = pred (count a s) := begin by_cases a ∈ s, { rw [(by rw cons_erase h : count a s = count a (a ::ₘ erase s a)), @@ -1733,8 +1748,8 @@ begin { rw [erase_of_not_mem h, count_eq_zero.2 h]; refl } end -@[simp, priority 980] -theorem count_erase_of_ne {a b : α} (ab : a ≠ b) (s : multiset α) : count a (erase s b) = count a s := +@[simp, priority 980] theorem count_erase_of_ne {a b : α} (ab : a ≠ b) (s : multiset α) : + count a (erase s b) = count a s := begin by_cases b ∈ s, { rw [← count_cons_of_ne ab, cons_erase h] }, @@ -1750,10 +1765,12 @@ begin { rw [count_erase_of_ne ab, count_cons_of_ne ab] } end -@[simp] theorem count_union (a : α) (s t : multiset α) : count a (s ∪ t) = max (count a s) (count a t) := +@[simp] theorem count_union (a : α) (s t : multiset α) : + count a (s ∪ t) = max (count a s) (count a t) := by simp [(∪), union, sub_add_eq_max, -add_comm] -@[simp] theorem count_inter (a : α) (s t : multiset α) : count a (s ∩ t) = min (count a s) (count a t) := +@[simp] theorem count_inter (a : α) (s t : multiset α) : + count a (s ∩ t) = min (count a s) (count a t) := begin apply @nat.add_left_cancel (count a (s - t)), rw [← count_add, sub_add_inter, count_sub, sub_add_min], @@ -1942,7 +1959,8 @@ lemma card_eq_card_of_rel {r : α → β → Prop} {s : multiset α} {t : multis card s = card t := by induction h; simp [*] -lemma exists_mem_of_rel_of_mem {r : α → β → Prop} {s : multiset α} {t : multiset β} (h : rel r s t) : +lemma exists_mem_of_rel_of_mem {r : α → β → Prop} {s : multiset α} {t : multiset β} + (h : rel r s t) : ∀ {a : α} (ha : a ∈ s), ∃ b ∈ t, r a b := begin induction h with x y s t hxy hst ih, @@ -2061,7 +2079,8 @@ lemma disjoint_map_map {f : α → γ} {g : β → γ} {s : multiset α} {t : mu disjoint (s.map f) (t.map g) ↔ (∀a∈s, ∀b∈t, f a ≠ g b) := by { simp [disjoint, @eq_comm _ (f _) (g _)], refl } -/-- `pairwise r m` states that there exists a list of the elements s.t. `r` holds pairwise on this list. -/ +/-- `pairwise r m` states that there exists a list of the elements s.t. `r` holds pairwise on this +list. -/ def pairwise (r : α → α → Prop) (m : multiset α) : Prop := ∃l:list α, m = l ∧ l.pairwise r @@ -2071,7 +2090,6 @@ iff.intro (assume ⟨l', eq, h⟩, ((quotient.exact eq).pairwise_iff hr).2 h) (assume h, ⟨l, rfl, h⟩) - end multiset namespace multiset diff --git a/src/group_theory/free_abelian_group.lean b/src/group_theory/free_abelian_group.lean index 1db44c31e518d..c3a192fa4f0b0 100644 --- a/src/group_theory/free_abelian_group.lean +++ b/src/group_theory/free_abelian_group.lean @@ -31,7 +31,8 @@ def of (x : α) : free_abelian_group α := abelianization.of $ free_group.of x def lift {β : Type v} [add_comm_group β] (f : α → β) : free_abelian_group α →+ β := -(@abelianization.lift _ _ (multiplicative β) _ (monoid_hom.of (@free_group.to_group _ (multiplicative β) _ f))).to_additive +(@abelianization.lift _ _ (multiplicative β) _ + (monoid_hom.of (@free_group.to_group _ (multiplicative β) _ f))).to_additive namespace lift variables {β : Type v} [add_comm_group β] (f : α → β) @@ -172,13 +173,15 @@ lift.of _ _ @[simp] lemma map_zero (f : α → β) : f <$> (0 : free_abelian_group α) = 0 := lift.zero (of ∘ f) -@[simp] lemma map_add (f : α → β) (x y : free_abelian_group α) : f <$> (x + y) = f <$> x + f <$> y := +@[simp] lemma map_add (f : α → β) (x y : free_abelian_group α) : + f <$> (x + y) = f <$> x + f <$> y := lift.add _ _ _ @[simp] lemma map_neg (f : α → β) (x : free_abelian_group α) : f <$> (-x) = -(f <$> x) := lift.neg _ _ -@[simp] lemma map_sub (f : α → β) (x y : free_abelian_group α) : f <$> (x - y) = f <$> x - f <$> y := +@[simp] lemma map_sub (f : α → β) (x y : free_abelian_group α) : + f <$> (x - y) = f <$> x - f <$> y := lift.sub _ _ _ @[simp] lemma map_of (f : α → β) (y : α) : f <$> of y = of (f y) := rfl @@ -205,13 +208,16 @@ lift.of _ _ @[simp] lemma zero_bind (f : α → free_abelian_group β) : 0 >>= f = 0 := lift.zero f -@[simp] lemma add_bind (f : α → free_abelian_group β) (x y : free_abelian_group α) : x + y >>= f = (x >>= f) + (y >>= f) := +@[simp] lemma add_bind (f : α → free_abelian_group β) (x y : free_abelian_group α) : + x + y >>= f = (x >>= f) + (y >>= f) := lift.add _ _ _ -@[simp] lemma neg_bind (f : α → free_abelian_group β) (x : free_abelian_group α) : -x >>= f = -(x >>= f) := +@[simp] lemma neg_bind (f : α → free_abelian_group β) (x : free_abelian_group α) : + -x >>= f = -(x >>= f) := lift.neg _ _ -@[simp] lemma sub_bind (f : α → free_abelian_group β) (x y : free_abelian_group α) : x - y >>= f = (x >>= f) - (y >>= f) := +@[simp] lemma sub_bind (f : α → free_abelian_group β) (x y : free_abelian_group α) : + x - y >>= f = (x >>= f) - (y >>= f) := lift.sub _ _ _ @[simp] lemma pure_seq (f : α → β) (x : free_abelian_group α) : pure f <*> x = f <$> x := @@ -220,29 +226,36 @@ pure_bind _ _ @[simp] lemma zero_seq (x : free_abelian_group α) : (0 : free_abelian_group (α → β)) <*> x = 0 := zero_bind _ -@[simp] lemma add_seq (f g : free_abelian_group (α → β)) (x : free_abelian_group α) : f + g <*> x = (f <*> x) + (g <*> x) := +@[simp] lemma add_seq (f g : free_abelian_group (α → β)) (x : free_abelian_group α) : + f + g <*> x = (f <*> x) + (g <*> x) := add_bind _ _ _ -@[simp] lemma neg_seq (f : free_abelian_group (α → β)) (x : free_abelian_group α) : -f <*> x = -(f <*> x) := +@[simp] lemma neg_seq (f : free_abelian_group (α → β)) (x : free_abelian_group α) : + -f <*> x = -(f <*> x) := neg_bind _ _ -@[simp] lemma sub_seq (f g : free_abelian_group (α → β)) (x : free_abelian_group α) : f - g <*> x = (f <*> x) - (g <*> x) := +@[simp] lemma sub_seq (f g : free_abelian_group (α → β)) (x : free_abelian_group α) : + f - g <*> x = (f <*> x) - (g <*> x) := sub_bind _ _ _ instance is_add_group_hom_seq (f : free_abelian_group (α → β)) : is_add_group_hom ((<*>) f) := { map_add := λ x y, show lift (<$> (x+y)) _ = _, by simp only [map_add]; exact -@@is_add_hom.map_add _ _ _ (@@free_abelian_group.is_add_group_hom_lift' (free_abelian_group β) _ _).to_is_add_hom _ _ } +@@is_add_hom.map_add _ _ _ + (@@free_abelian_group.is_add_group_hom_lift' (free_abelian_group β) _ _).to_is_add_hom _ _ } @[simp] lemma seq_zero (f : free_abelian_group (α → β)) : f <*> 0 = 0 := is_add_group_hom.map_zero _ -@[simp] lemma seq_add (f : free_abelian_group (α → β)) (x y : free_abelian_group α) : f <*> (x + y) = (f <*> x) + (f <*> y) := +@[simp] lemma seq_add (f : free_abelian_group (α → β)) (x y : free_abelian_group α) : + f <*> (x + y) = (f <*> x) + (f <*> y) := is_add_hom.map_add _ _ _ -@[simp] lemma seq_neg (f : free_abelian_group (α → β)) (x : free_abelian_group α) : f <*> (-x) = -(f <*> x) := +@[simp] lemma seq_neg (f : free_abelian_group (α → β)) (x : free_abelian_group α) : + f <*> (-x) = -(f <*> x) := is_add_group_hom.map_neg _ _ -@[simp] lemma seq_sub (f : free_abelian_group (α → β)) (x y : free_abelian_group α) : f <*> (x - y) = (f <*> x) - (f <*> y) := +@[simp] lemma seq_sub (f : free_abelian_group (α → β)) (x y : free_abelian_group α) : + f <*> (x - y) = (f <*> x) - (f <*> y) := is_add_group_hom.map_sub _ _ _ instance : is_lawful_monad free_abelian_group.{u} := diff --git a/src/ring_theory/polynomial/basic.lean b/src/ring_theory/polynomial/basic.lean index c7ec6a38cf9b9..893be84ba80ae 100644 --- a/src/ring_theory/polynomial/basic.lean +++ b/src/ring_theory/polynomial/basic.lean @@ -66,7 +66,8 @@ begin finset.mem_image.2 ⟨_, finset.mem_range.2 (nat.lt_succ_of_le this), rfl⟩) }, rw [submodule.span_le, finset.coe_image, set.image_subset_iff], intros k hk, apply mem_degree_le.2, - apply le_trans (degree_X_pow_le _) (with_bot.coe_le_coe.2 $ nat.le_of_lt_succ $ finset.mem_range.1 hk) + exact (degree_X_pow_le _).trans + (with_bot.coe_le_coe.2 $ nat.le_of_lt_succ $ finset.mem_range.1 hk) end theorem mem_degree_lt {n : ℕ} {f : polynomial R} : @@ -132,9 +133,11 @@ def restriction (p : polynomial R) : polynomial (ring.closure (↑p.frange : set else ring.subset_closure $ finsupp.mem_frange.2 ⟨H, i, rfl⟩⟩, λ i, finsupp.mem_support_iff.trans (not_iff_not_of_iff ⟨λ H, subtype.eq H, subtype.mk.inj⟩)⟩ -@[simp] theorem coeff_restriction {p : polynomial R} {n : ℕ} : ↑(coeff (restriction p) n) = coeff p n := rfl +@[simp] theorem coeff_restriction {p : polynomial R} {n : ℕ} : + ↑(coeff (restriction p) n) = coeff p n := rfl -@[simp] theorem coeff_restriction' {p : polynomial R} {n : ℕ} : (coeff (restriction p) n).1 = coeff p n := rfl +@[simp] theorem coeff_restriction' {p : polynomial R} {n : ℕ} : + (coeff (restriction p) n).1 = coeff p n := rfl section local attribute [instance] algebra.of_is_subring subring.domain subset.comm_ring @@ -144,7 +147,8 @@ end @[simp] theorem degree_restriction {p : polynomial R} : (restriction p).degree = p.degree := rfl -@[simp] theorem nat_degree_restriction {p : polynomial R} : (restriction p).nat_degree = p.nat_degree := rfl +@[simp] theorem nat_degree_restriction {p : polynomial R} : + (restriction p).nat_degree = p.nat_degree := rfl @[simp] theorem monic_restriction {p : polynomial R} : monic (restriction p) ↔ monic p := ⟨λ H, congr_arg subtype.val H, λ H, subtype.eq H⟩ @@ -517,7 +521,9 @@ have hm2 : ∀ k, I.leading_coeff_nth k ≤ M := λ k, or.cases_on (le_or_lt k N have hs2 : ∀ {x}, x ∈ I.degree_le N → x ∈ ideal.span (↑s : set (polynomial R)), from hs ▸ λ x hx, submodule.span_induction hx (λ _ hx, ideal.subset_span hx) (ideal.zero_mem _) (λ _ _, ideal.add_mem _) (λ c f hf, f.C_mul' c ▸ ideal.mul_mem_left _ _ hf), -⟨s, le_antisymm (ideal.span_le.2 $ λ x hx, have x ∈ I.degree_le N, from hs ▸ submodule.subset_span hx, this.2) $ begin +⟨s, le_antisymm + (ideal.span_le.2 $ λ x hx, have x ∈ I.degree_le N, from hs ▸ submodule.subset_span hx, this.2) $ +begin change I ≤ ideal.span ↑s, intros p hp, generalize hn : p.nat_degree = k, induction k using nat.strong_induction_on with k ih generalizing p, @@ -718,7 +724,8 @@ protected theorem eq_zero_or_eq_zero_of_mul_eq_zero {R : Type u} [integral_domai begin obtain ⟨s, p, rfl⟩ := exists_finset_rename p, obtain ⟨t, q, rfl⟩ := exists_finset_rename q, - have : rename (subtype.map id (finset.subset_union_left s t) : {x // x ∈ s} → {x // x ∈ s ∪ t}) p * + have : + rename (subtype.map id (finset.subset_union_left s t) : {x // x ∈ s} → {x // x ∈ s ∪ t}) p * rename (subtype.map id (finset.subset_union_right s t) : {x // x ∈ t} → {x // x ∈ s ∪ t}) q = 0, { apply rename_injective _ subtype.val_injective, simpa using h }, letI := mv_polynomial.integral_domain_fintype R {x // x ∈ (s ∪ t)}, diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean index 5835dd19d0c13..99e9f60e7a708 100644 --- a/src/topology/algebra/group.lean +++ b/src/topology/algebra/group.lean @@ -535,8 +535,8 @@ variables [topological_space G] [group G] [topological_group G] /-- Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of `1` such that `KV ⊆ U`. -/ -@[to_additive "Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of `0` - such that `K + V ⊆ U`."] +@[to_additive "Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of +`0` such that `K + V ⊆ U`."] lemma compact_open_separated_mul {K U : set G} (hK : is_compact K) (hU : is_open U) (hKU : K ⊆ U) : ∃ V : set G, is_open V ∧ (1 : G) ∈ V ∧ K * V ⊆ U := begin diff --git a/src/topology/algebra/module.lean b/src/topology/algebra/module.lean index 9872a3fa3595c..727d214b74114 100644 --- a/src/topology/algebra/module.lean +++ b/src/topology/algebra/module.lean @@ -350,7 +350,7 @@ instance : has_add (M →L[R] M₂) := ⟨λ f g, ⟨f + g, f.2.add g.2⟩⟩ @[simp] lemma add_apply : (f + g) x = f x + g x := rfl -@[simp, norm_cast] lemma coe_add : (((f + g) : M →L[R] M₂) : M →ₗ[R] M₂) = (f : M →ₗ[R] M₂) + g := rfl +@[simp, norm_cast] lemma coe_add : (((f + g) : M →L[R] M₂) : M →ₗ[R] M₂) = f + g := rfl @[norm_cast] lemma coe_add' : (((f + g) : M →L[R] M₂) : M → M₂) = (f : M → M₂) + g := rfl instance : add_comm_monoid (M →L[R] M₂) := @@ -572,7 +572,8 @@ variables {R : Type*} [semiring R] {M : Type*} [topological_space M] [add_comm_monoid M] [semimodule R M] {M₂ : Type*} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M₂] - {ι : Type*} {φ : ι → Type*} [∀i, topological_space (φ i)] [∀i, add_comm_monoid (φ i)] [∀i, semimodule R (φ i)] + {ι : Type*} {φ : ι → Type*} [∀i, topological_space (φ i)] [∀i, add_comm_monoid (φ i)] + [∀i, semimodule R (φ i)] /-- `pi` construction for continuous linear functions. From a family of continuous linear functions it produces a continuous linear function into a family of topological modules. -/ @@ -604,8 +605,8 @@ linear_map.infi_ker_proj variables (R φ) -/-- If `I` and `J` are complementary index sets, the product of the kernels of the `J`th projections of -`φ` is linearly equivalent to the product over `I`. -/ +/-- If `I` and `J` are complementary index sets, the product of the kernels of the `J`th projections +of `φ` is linearly equivalent to the product over `I`. -/ def infi_ker_proj_equiv {I J : set ι} [decidable_pred (λi, i ∈ I)] (hd : disjoint I J) (hu : set.univ ⊆ I ∪ J) : (⨅i ∈ J, ker (proj i) : submodule R (Πi, φ i)) ≃L[R] (Πi:I, φ i) := @@ -658,7 +659,7 @@ by refine {zero := 0, add := (+), neg := has_neg.neg, sub := has_sub.sub, sub_eq intros; ext; apply_rules [zero_add, add_assoc, add_zero, add_left_neg, add_comm, sub_eq_add_neg] lemma sub_apply (x : M) : (f - g) x = f x - g x := rfl -@[simp, norm_cast] lemma coe_sub : (((f - g) : M →L[R] M₂) : M →ₗ[R] M₂) = (f : M →ₗ[R] M₂) - g := rfl +@[simp, norm_cast] lemma coe_sub : (((f - g) : M →L[R] M₂) : M →ₗ[R] M₂) = f - g := rfl @[simp, norm_cast] lemma coe_sub' : (((f - g) : M →L[R] M₂) : M → M₂) = (f : M → M₂) - g := rfl end @@ -1130,7 +1131,8 @@ variables [add_comm_monoid M] [semimodule R M] but one needs a fully (rather than partially) defined inverse function for some purposes, including for calculus. -/ noncomputable def inverse : (M →L[R] M₂) → (M₂ →L[R] M) := -λ f, if h : ∃ (e : M ≃L[R] M₂), (e : M →L[R] M₂) = f then ((classical.some h).symm : M₂ →L[R] M) else 0 +λ f, if h : ∃ (e : M ≃L[R] M₂), (e : M →L[R] M₂) = f then ((classical.some h).symm : M₂ →L[R] M) +else 0 /-- By definition, if `f` is invertible then `inverse f = f.symm`. -/ @[simp] lemma inverse_equiv (e : M ≃L[R] M₂) : inverse (e : M →L[R] M₂) = e.symm := diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean index 3fcaba07143d7..ddbe13eca6a3a 100644 --- a/src/topology/metric_space/emetric_space.lean +++ b/src/topology/metric_space/emetric_space.lean @@ -16,9 +16,9 @@ This file is devoted to the definition and study of `emetric_spaces`, i.e., metr spaces in which the distance is allowed to take the value ∞. This extended distance is called `edist`, and takes values in `ennreal`. -Many definitions and theorems expected on emetric spaces are already introduced on uniform spaces and -topological spaces. For example: - open and closed sets, compactness, completeness, continuity and uniform continuity +Many definitions and theorems expected on emetric spaces are already introduced on uniform spaces +and topological spaces. For example: open and closed sets, compactness, completeness, continuity and +uniform continuity. The class `emetric_space` therefore extends `uniform_space` (and `topological_space`). -/ @@ -33,8 +33,8 @@ variables {α : Type u} {β : Type v} {γ : Type w} /-- Characterizing uniformities associated to a (generalized) distance function `D` in terms of the elements of the uniformity. -/ -theorem uniformity_dist_of_mem_uniformity [linear_order β] {U : filter (α × α)} (z : β) (D : α → α → β) - (H : ∀ s, s ∈ U ↔ ∃ε>z, ∀{a b:α}, D a b < ε → (a, b) ∈ s) : +theorem uniformity_dist_of_mem_uniformity [linear_order β] {U : filter (α × α)} (z : β) + (D : α → α → β) (H : ∀ s, s ∈ U ↔ ∃ε>z, ∀{a b:α}, D a b < ε → (a, b) ∈ s) : U = ⨅ ε>z, 𝓟 {p:α×α | D p.1 p.2 < ε} := le_antisymm (le_infi $ λ ε, le_infi $ λ ε0, le_principal_iff.2 $ (H _).2 ⟨ε, ε0, λ a b, id⟩) @@ -90,7 +90,8 @@ class emetric_space (α : Type u) extends has_edist α : Type u := (eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y) (edist_comm : ∀ x y : α, edist x y = edist y x) (edist_triangle : ∀ x y z : α, edist x z ≤ edist x y + edist y z) -(to_uniform_space : uniform_space α := uniform_space_of_edist edist edist_self edist_comm edist_triangle) +(to_uniform_space : uniform_space α := + uniform_space_of_edist edist edist_self edist_comm edist_triangle) (uniformity_edist : 𝓤 α = ⨅ ε>0, 𝓟 {p:α×α | edist p.1 p.2 < ε} . control_laws_tac) /- emetric spaces are less common than metric spaces. Therefore, we work in a dedicated @@ -315,7 +316,8 @@ converging. This is often applied for `B N = 2^{-N}`, i.e., with a very fast con `0`, which makes it possible to use arguments of converging series, while this is impossible to do in general for arbitrary Cauchy sequences. -/ theorem complete_of_convergent_controlled_sequences (B : ℕ → ennreal) (hB : ∀n, 0 < B n) - (H : ∀u : ℕ → α, (∀N n m : ℕ, N ≤ n → N ≤ m → edist (u n) (u m) < B N) → ∃x, tendsto u at_top (𝓝 x)) : + (H : ∀u : ℕ → α, (∀N n m : ℕ, N ≤ n → N ≤ m → edist (u n) (u m) < B N) → + ∃x, tendsto u at_top (𝓝 x)) : complete_space α := uniform_space.complete_of_convergent_controlled_sequences uniformity_has_countable_basis @@ -765,7 +767,8 @@ diam_le_of_forall_edist_le $ λ x hx y hy, edist_le_diam_of_mem (h hx) (h hy) /-- The diameter of a union is controlled by the diameter of the sets, and the edistance between two points in the sets. -/ -lemma diam_union {t : set α} (xs : x ∈ s) (yt : y ∈ t) : diam (s ∪ t) ≤ diam s + edist x y + diam t := +lemma diam_union {t : set α} (xs : x ∈ s) (yt : y ∈ t) : + diam (s ∪ t) ≤ diam s + edist x y + diam t := begin have A : ∀a ∈ s, ∀b ∈ t, edist a b ≤ diam s + edist x y + diam t := λa ha b hb, calc edist a b ≤ edist a x + edist x y + edist y b : edist_triangle4 _ _ _ _ @@ -775,7 +778,8 @@ begin cases (mem_union _ _ _).1 ha with h'a h'a; cases (mem_union _ _ _).1 hb with h'b h'b, { calc edist a b ≤ diam s : edist_le_diam_of_mem h'a h'b ... ≤ diam s + (edist x y + diam t) : le_add_right (le_refl _) - ... = diam s + edist x y + diam t : by simp only [add_comm, eq_self_iff_true, add_left_comm] }, + ... = diam s + edist x y + diam t : + by simp only [add_comm, eq_self_iff_true, add_left_comm] }, { exact A a h'a b h'b }, { have Z := A b h'b a h'a, rwa [edist_comm] at Z }, { calc edist a b ≤ diam t : edist_le_diam_of_mem h'a h'b diff --git a/src/topology/metric_space/gromov_hausdorff_realized.lean b/src/topology/metric_space/gromov_hausdorff_realized.lean index fdb5ce684fa68..ac96ec50e766f 100644 --- a/src/topology/metric_space/gromov_hausdorff_realized.lean +++ b/src/topology/metric_space/gromov_hausdorff_realized.lean @@ -72,9 +72,11 @@ private lemma max_var_bound : dist x y ≤ max_var α β := calc dist_le_diam_of_mem (bounded_of_compact compact_univ) (mem_univ _) (mem_univ _) ... = diam (inl '' (univ : set α) ∪ inr '' (univ : set β)) : by apply congr_arg; ext x y z; cases x; simp [mem_univ, mem_range_self] - ... ≤ diam (inl '' (univ : set α)) + dist (inl (default α)) (inr (default β)) + diam (inr '' (univ : set β)) : + ... ≤ diam (inl '' (univ : set α)) + dist (inl (default α)) (inr (default β)) + + diam (inr '' (univ : set β)) : diam_union (mem_image_of_mem _ (mem_univ _)) (mem_image_of_mem _ (mem_univ _)) - ... = diam (univ : set α) + (dist (default α) (default α) + 1 + dist (default β) (default β)) + diam (univ : set β) : + ... = diam (univ : set α) + (dist (default α) (default α) + 1 + dist (default β) (default β)) + + diam (univ : set β) : by { rw [isometry_on_inl.diam_image, isometry_on_inr.diam_image], refl } ... = 1 * diam (univ : set α) + 1 + 1 * diam (univ : set β) : by simp ... ≤ 2 * diam (univ : set α) + 1 + 2 * diam (univ : set β) : @@ -100,10 +102,12 @@ begin by linarith end -private lemma candidates_dist_inl (fA : f ∈ candidates α β) (x y: α) : f (inl x, inl y) = dist x y := +private lemma candidates_dist_inl (fA : f ∈ candidates α β) (x y: α) : + f (inl x, inl y) = dist x y := fA.1.1.1.1.1 x y -private lemma candidates_dist_inr (fA : f ∈ candidates α β) (x y : β) : f (inr x, inr y) = dist x y := +private lemma candidates_dist_inr (fA : f ∈ candidates α β) (x y : β) : + f (inr x, inr y) = dist x y := fA.1.1.1.1.2 x y private lemma candidates_le_max_var (fA : f ∈ candidates α β) : f (x, y) ≤ max_var α β := @@ -136,7 +140,8 @@ private lemma candidates_dist_bound (fA : f ∈ candidates α β) : mul_le_mul_of_nonneg_right (one_le_max_var α β) dist_nonneg /-- Technical lemma to prove that candidates are Lipschitz -/ -private lemma candidates_lipschitz_aux (fA : f ∈ candidates α β) : f (x, y) - f (z, t) ≤ 2 * max_var α β * dist (x, y) (z, t) := +private lemma candidates_lipschitz_aux (fA : f ∈ candidates α β) : + f (x, y) - f (z, t) ≤ 2 * max_var α β * dist (x, y) (z, t) := calc f (x, y) - f(z, t) ≤ f (x, t) + f (t, y) - f (z, t) : sub_le_sub_right (candidates_triangle fA) _ ... ≤ (f (x, z) + f (z, t) + f(t, y)) - f (z, t) : @@ -147,8 +152,10 @@ calc ... ≤ max_var α β * max (dist x z) (dist t y) + max_var α β * max (dist x z) (dist t y) : begin apply add_le_add, - apply mul_le_mul_of_nonneg_left (le_max_left (dist x z) (dist t y)) (le_trans zero_le_one (one_le_max_var α β)), - apply mul_le_mul_of_nonneg_left (le_max_right (dist x z) (dist t y)) (le_trans zero_le_one (one_le_max_var α β)), + apply mul_le_mul_of_nonneg_left (le_max_left (dist x z) (dist t y)) + (zero_le_one.trans (one_le_max_var α β)), + apply mul_le_mul_of_nonneg_left (le_max_right (dist x z) (dist t y)) + (zero_le_one.trans (one_le_max_var α β)), end ... = 2 * max_var α β * max (dist x z) (dist y t) : by { simp [dist_comm], ring } @@ -185,7 +192,8 @@ begin end def candidates_b_dist (α : Type u) (β : Type v) [metric_space α] [compact_space α] [inhabited α] - [metric_space β] [compact_space β] [inhabited β] : Cb α β := candidates_b_of_candidates _ dist_mem_candidates + [metric_space β] [compact_space β] [inhabited β] : Cb α β := +candidates_b_of_candidates _ dist_mem_candidates lemma candidates_b_dist_mem_candidates_b : candidates_b_dist α β ∈ candidates_b α β := candidates_b_of_candidates_mem _ _ @@ -193,8 +201,8 @@ candidates_b_of_candidates_mem _ _ private lemma candidates_b_nonempty : (candidates_b α β).nonempty := ⟨_, candidates_b_dist_mem_candidates_b⟩ -/-- To apply Arzela-Ascoli, we need to check that the set of candidates is closed and equicontinuous. -Equicontinuity follows from the Lipschitz control, we check closedness -/ +/-- To apply Arzela-Ascoli, we need to check that the set of candidates is closed and +equicontinuous. Equicontinuity follows from the Lipschitz control, we check closedness. -/ private lemma closed_candidates_b : is_closed (candidates_b α β) := begin have I1 : ∀x y, is_closed {f : Cb α β | f (inl x, inl y) = dist x y} := @@ -228,10 +236,11 @@ begin <|> assume x }, end -/-- Compactness of candidates (in bounded_continuous_functions) follows -/ +/-- Compactness of candidates (in bounded_continuous_functions) follows. -/ private lemma compact_candidates_b : is_compact (candidates_b α β) := begin - refine arzela_ascoli₂ (Icc 0 (max_var α β)) compact_Icc (candidates_b α β) closed_candidates_b _ _, + refine arzela_ascoli₂ (Icc 0 (max_var α β)) compact_Icc (candidates_b α β) + closed_candidates_b _ _, { rintros f ⟨x1, x2⟩ hf, simp only [set.mem_Icc], exact ⟨candidates_nonneg hf, candidates_le_max_var hf⟩ }, @@ -401,7 +410,8 @@ private definition optimal_GH_dist : Cb α β := classical.some (exists_minimize private lemma optimal_GH_dist_mem_candidates_b : optimal_GH_dist α β ∈ candidates_b α β := by cases (classical.some_spec (exists_minimizer α β)); assumption -private lemma HD_optimal_GH_dist_le (g : Cb α β) (hg : g ∈ candidates_b α β) : HD (optimal_GH_dist α β) ≤ HD g := +private lemma HD_optimal_GH_dist_le (g : Cb α β) (hg : g ∈ candidates_b α β) : + HD (optimal_GH_dist α β) ≤ HD g := let ⟨Z1, Z2⟩ := classical.some_spec (exists_minimizer α β) in Z2 g hg /-- With the optimal candidate, construct a premetric space structure on α ⊕ β, on which the diff --git a/test/general_recursion.lean b/test/general_recursion.lean index 7662475bc9142..5a1d17b148397 100644 --- a/test/general_recursion.lean +++ b/test/general_recursion.lean @@ -52,8 +52,10 @@ pi.omega_complete_partial_order.flip₂_continuous' div.intl (λ (x_1 : ℕ), (continuous_hom.ite_continuous' (λ (x_2 : ℕ → ℕ → roption ℕ), x_2 (x - x_1) x_1) (λ (x_1 : ℕ → ℕ → roption ℕ), pure x) - (pi.omega_complete_partial_order.flip₁_continuous' (λ (v_1 : ℕ) (x_2 : ℕ → ℕ → roption ℕ), x_2 (x - x_1) v_1) _ - $ pi.omega_complete_partial_order.flip₁_continuous' (λ (v : ℕ) (g : ℕ → ℕ → roption ℕ) (x : ℕ), g v x) _ id_continuous') + (pi.omega_complete_partial_order.flip₁_continuous' + (λ (v_1 : ℕ) (x_2 : ℕ → ℕ → roption ℕ), x_2 (x - x_1) v_1) _ $ + pi.omega_complete_partial_order.flip₁_continuous' + (λ (v : ℕ) (g : ℕ → ℕ → roption ℕ) (x : ℕ), g v x) _ id_continuous') (const_continuous' (pure x))))) -- automation coming soon @@ -67,7 +69,8 @@ inductive tree (α : Type*) open roption.examples.tree /-! `map` on a `tree` using monadic notation -/ -def tree_map.intl {α β : Type*} (f : α → β) (tree_map : tree α → roption (tree β)) : tree α → roption (tree β) +def tree_map.intl {α β : Type*} (f : α → β) (tree_map : tree α → roption (tree β)) : + tree α → roption (tree β) | nil := pure nil | (node x t₀ t₁) := do tt₀ ← tree_map t₀, @@ -79,7 +82,8 @@ def tree_map {α : Type u_1} {β : Type u_2} (f : α → β) : tree α → ropti fix (tree_map.intl f) -- automation coming soon -theorem tree_map.cont : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), continuous' (tree_map.intl f) := +theorem tree_map.cont : + ∀ {α : Type u_1} {β : Type u_2} (f : α → β), continuous' (tree_map.intl f) := λ {α : Type u_1} {β : Type u_2} (f : α → β), pi.omega_complete_partial_order.flip₂_continuous' (tree_map.intl f) (λ (x : tree α), @@ -102,17 +106,21 @@ theorem tree_map.cont : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), con (λ (x_1 : tree β), const_continuous' (pure (node (f x_x) x x_1))))))))) -- automation coming soon -theorem tree_map.equations.eqn_1 {α : Type u_1} {β : Type u_2} (f : α → β) : tree_map f nil = pure nil := +theorem tree_map.equations.eqn_1 {α : Type u_1} {β : Type u_2} (f : α → β) : + tree_map f nil = pure nil := by rw [tree_map,lawful_fix.fix_eq' (tree_map.cont f)]; refl -- automation coming soon -theorem tree_map.equations.eqn_2 {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) (t₀ t₁ : tree α) : - tree_map f (node x t₀ t₁) = tree_map f t₀ >>= λ (tt₀ : tree β), tree_map f t₁ >>= λ (tt₁ : tree β), pure (node (f x) tt₀ tt₁) := +theorem tree_map.equations.eqn_2 {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) + (t₀ t₁ : tree α) : + tree_map f (node x t₀ t₁) = tree_map f t₀ >>= λ (tt₀ : tree β), tree_map f t₁ >>= + λ (tt₁ : tree β), pure (node (f x) tt₀ tt₁) := by conv_lhs { rw [tree_map,lawful_fix.fix_eq' (tree_map.cont f)] }; refl /-! `map` on a `tree` using applicative notation -/ -def tree_map'.intl {α β} (f : α → β) (tree_map : tree α → roption (tree β)) : tree α → roption (tree β) +def tree_map'.intl {α β} (f : α → β) (tree_map : tree α → roption (tree β)) : + tree α → roption (tree β) | nil := pure nil | (node x t₀ t₁) := node (f x) <$> tree_map t₀ <*> tree_map t₁ @@ -122,7 +130,8 @@ def tree_map' {α : Type u_1} {β : Type u_2} (f : α → β) : tree α → ropt fix (tree_map'.intl f) -- automation coming soon -theorem tree_map'.cont : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), continuous' (tree_map'.intl f) := +theorem tree_map'.cont : + ∀ {α : Type u_1} {β : Type u_2} (f : α → β), continuous' (tree_map'.intl f) := λ {α : Type u_1} {β : Type u_2} (f : α → β), pi.omega_complete_partial_order.flip₂_continuous' (tree_map'.intl f) (λ (x : tree α),