[Merged by Bors] - chore(*): split some long lines

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

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,

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
 

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
 

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,15 +301,17 @@ 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`,
 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],

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