chore(*): split long lines (#2883)

Also move docs for `control/fold` from a comment to a module docstring.

src/algebra/commute.lean

@@ -15,7 +15,8 @@ import ring_theory.subring
 * `centralizer a` : `{ x | commute a x }`
 * `set.centralizer s` : elements that commute with all `a ∈ s`
 
-We prove that `centralizer` and `set_centralilzer` are submonoid/subgroups/subrings depending on the available structures, and provide operations on `commute _ _`.
+We prove that `centralizer` and `set_centralilzer` are submonoid/subgroups/subrings depending on the
+available structures, and provide operations on `commute _ _`.
 
 E.g., if `a`, `b`, and c are elements of a semiring, and that `hb :
 commute a b` and `hc : commute a c`.  Then `hb.pow_left 5` proves

src/algebra/free.lean

@@ -165,13 +165,15 @@ end category
 end free_magma
 
 /-- `free_magma` is traversable. -/
-protected def free_magma.traverse {m : Type u → Type u} [applicative m] {α β : Type u} (F : α → m β) :
+protected def free_magma.traverse {m : Type u → Type u} [applicative m] {α β : Type u}
+  (F : α → m β) :
   free_magma α → m (free_magma β)
 | (free_magma.of x) := free_magma.of <$> F x
 | (x * y)           := (*) <$> x.traverse <*> y.traverse
 
 /-- `free_add_magma` is traversable. -/
-protected def free_add_magma.traverse {m : Type u → Type u} [applicative m] {α β : Type u} (F : α → m β) :
+protected def free_add_magma.traverse {m : Type u → Type u} [applicative m] {α β : Type u}
+  (F : α → m β) :
   free_add_magma α → m (free_add_magma β)
 | (free_add_magma.of x) := free_add_magma.of <$> F x
 | (x + y)               := (+) <$> x.traverse <*> y.traverse
@@ -328,8 +330,10 @@ section lift
 
 variables {β : Type v} [semigroup β] (f : α → β)
 
-/-- Lifts a magma homomorphism `α → β` to a semigroup homomorphism `magma.free_semigroup α → β` given a semigroup `β`. -/
-@[to_additive "Lifts an additive magma homomorphism `α → β` to an additive semigroup homomorphism `add_magma.free_add_semigroup α → β` given an additive semigroup `β`."]
+/-- Lifts a magma homomorphism `α → β` to a semigroup homomorphism `magma.free_semigroup α → β`
+given a semigroup `β`. -/
+@[to_additive "Lifts an additive magma homomorphism `α → β` to an additive semigroup homomorphism
+`add_magma.free_add_semigroup α → β` given an additive semigroup `β`."]
 def lift (hf : ∀ x y, f (x * y) = f x * f y) : free_semigroup α → β :=
 quot.lift f $ by rintros a b (⟨c, d, e⟩ | ⟨c, d, e, f⟩); simp only [hf, mul_assoc]
 
@@ -347,8 +351,10 @@ end lift
 
 variables {β : Type v} [has_mul β] (f : α → β)
 
-/-- From a magma homomorphism `α → β` to a semigroup homomorphism `magma.free_semigroup α → magma.free_semigroup β`. -/
-@[to_additive "From an additive magma homomorphism `α → β` to an additive semigroup homomorphism `add_magma.free_add_semigroup α → add_magma.free_add_semigroup β`."]
+/-- From a magma homomorphism `α → β` to a semigroup homomorphism
+`magma.free_semigroup α → magma.free_semigroup β`. -/
+@[to_additive "From an additive magma homomorphism `α → β` to an additive semigroup homomorphism
+`add_magma.free_add_semigroup α → add_magma.free_add_semigroup β`."]
 def map (hf : ∀ x y, f (x * y) = f x * f y) : free_semigroup α → free_semigroup β :=
 lift (of ∘ f) (λ x y, congr_arg of $ hf x y)
 
@@ -398,7 +404,8 @@ def free_semigroup.lift' {α : Type u} {β : Type v} [semigroup β] (f : α →
 | x (hd::tl) := f x * free_semigroup.lift' hd tl
 
 /-- Auxiliary function for `free_semigroup.lift`. -/
-def free_add_semigroup.lift' {α : Type u} {β : Type v} [add_semigroup β] (f : α → β) : α → list α → β
+def free_add_semigroup.lift' {α : Type u} {β : Type v} [add_semigroup β] (f : α → β) :
+  α → list α → β
 | x [] := f x
 | x (hd::tl) := f x + free_add_semigroup.lift' hd tl
 
@@ -412,8 +419,10 @@ section lift
 
 variables {β : Type v} [semigroup β] (f : α → β)
 
-/-- Lifts a function `α → β` to a semigroup homomorphism `free_semigroup α → β` given a semigroup `β`. -/
-@[to_additive "Lifts a function `α → β` to an additive semigroup homomorphism `free_add_semigroup α → β` given an additive semigroup `β`."]
+/-- Lifts a function `α → β` to a semigroup homomorphism `free_semigroup α → β` given
+a semigroup `β`. -/
+@[to_additive "Lifts a function `α → β` to an additive semigroup homomorphism
+`free_add_semigroup α → β` given an additive semigroup `β`."]
 def lift (x : free_semigroup α) : β :=
 lift' f x.1 x.2
 
@@ -505,8 +514,10 @@ instance : traversable free_semigroup := ⟨@free_semigroup.traverse⟩
 
 variables {m : Type u → Type u} [applicative m] (F : α → m β)
 
-@[simp, to_additive] lemma traverse_pure (x) : traverse F (pure x : free_semigroup α) = pure <$> F x := rfl
-@[simp, to_additive] lemma traverse_pure' : traverse F ∘ pure = λ x, (pure <$> F x : m (free_semigroup β)) := rfl
+@[simp, to_additive]
+lemma traverse_pure (x) :traverse F (pure x : free_semigroup α) = pure <$> F x := rfl
+@[simp, to_additive]
+lemma traverse_pure' : traverse F ∘ pure = λ x, (pure <$> F x : m (free_semigroup β)) := rfl
 
 section
 variables [is_lawful_applicative m]
@@ -551,7 +562,8 @@ instance [decidable_eq α] : decidable_eq (free_semigroup α) := prod.decidable_
 end free_semigroup
 
 /-- Isomorphism between `magma.free_semigroup (free_magma α)` and `free_semigroup α`. -/
-@[to_additive free_add_semigroup_free_add_magma "Isomorphism between `add_magma.free_add_semigroup (free_add_magma α)` and `free_add_semigroup α`."]
+@[to_additive free_add_semigroup_free_add_magma "Isomorphism between
+`add_magma.free_add_semigroup (free_add_magma α)` and `free_add_semigroup α`."]
 def free_semigroup_free_magma (α : Type u) :
   magma.free_semigroup (free_magma α) ≃ free_semigroup α :=
 { to_fun := magma.free_semigroup.lift (free_magma.lift free_semigroup.of) (free_magma.lift_mul _),

src/algebra/pi_instances.lean

@@ -85,22 +85,28 @@ instance semimodule (α) {r : semiring α} {m : ∀ i, add_comm_monoid $ f i} [
 
 variables {I f}
 
-instance left_cancel_semigroup [∀ i, left_cancel_semigroup $ f i] : left_cancel_semigroup (Π i : I, f i) :=
+instance left_cancel_semigroup [∀ i, left_cancel_semigroup $ f i] :
+  left_cancel_semigroup (Π i : I, f i) :=
 by pi_instance
 
-instance add_left_cancel_semigroup [∀ i, add_left_cancel_semigroup $ f i] : add_left_cancel_semigroup (Π i : I, f i) :=
+instance add_left_cancel_semigroup [∀ i, add_left_cancel_semigroup $ f i] :
+  add_left_cancel_semigroup (Π i : I, f i) :=
 by pi_instance
 
-instance right_cancel_semigroup [∀ i, right_cancel_semigroup $ f i] : right_cancel_semigroup (Π i : I, f i) :=
+instance right_cancel_semigroup [∀ i, right_cancel_semigroup $ f i] :
+  right_cancel_semigroup (Π i : I, f i) :=
 by pi_instance
 
-instance add_right_cancel_semigroup [∀ i, add_right_cancel_semigroup $ f i] : add_right_cancel_semigroup (Π i : I, f i) :=
+instance add_right_cancel_semigroup [∀ i, add_right_cancel_semigroup $ f i] :
+  add_right_cancel_semigroup (Π i : I, f i) :=
 by pi_instance
 
-instance ordered_cancel_comm_monoid [∀ i, ordered_cancel_add_comm_monoid $ f i] : ordered_cancel_add_comm_monoid (Π i : I, f i) :=
+instance ordered_cancel_comm_monoid [∀ i, ordered_cancel_add_comm_monoid $ f i] :
+  ordered_cancel_add_comm_monoid (Π i : I, f i) :=
 by pi_instance
 
-instance ordered_add_comm_group [∀ i, ordered_add_comm_group $ f i] : ordered_add_comm_group (Π i : I, f i) :=
+instance ordered_add_comm_group [∀ i, ordered_add_comm_group $ f i] :
+  ordered_add_comm_group (Π i : I, f i) :=
 { add_le_add_left := λ x y hxy c i, add_le_add_left (hxy i) _,
   ..pi.add_comm_group,
   ..pi.partial_order }
@@ -188,8 +194,10 @@ variable {I : Type u}     -- The indexing type
 variable (f : I → Type v) -- The family of types already equipped with instances
 variables [Π i, monoid (f i)]
 
-/-- Evaluation of functions into an indexed collection of monoids at a point is a monoid homomorphism. -/
-@[to_additive "Evaluation of functions into an indexed collection of additive monoids at a point is an additive monoid homomorphism."]
+/-- Evaluation of functions into an indexed collection of monoids at a point is a monoid
+homomorphism. -/
+@[to_additive "Evaluation of functions into an indexed collection of additive monoids at a point
+is an additive monoid homomorphism."]
 def monoid_hom.apply (i : I) : (Π i, f i) →* f i :=
 { to_fun := λ g, g i,
   map_one' := rfl,

src/algebraic_geometry/presheafed_space.lean

@@ -153,7 +153,8 @@ lemma id_c (X : PresheafedSpace.{v} C) :
 by { op_induction U, cases U, simp only [id_c], dsimp, simp, }
 
 @[simp] lemma comp_c_app {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) (U) :
-  (α ≫ β).c.app U = (β.c).app U ≫ (α.c).app (op ((opens.map (β.f)).obj (unop U))) ≫ (Top.presheaf.pushforward.comp _ _ _).inv.app U := rfl
+  (α ≫ β).c.app U = (β.c).app U ≫ (α.c).app (op ((opens.map (β.f)).obj (unop U))) ≫
+    (Top.presheaf.pushforward.comp _ _ _).inv.app U := rfl
 
 /-- The forgetful functor from `PresheafedSpace` to `Top`. -/
 def forget : PresheafedSpace.{v} C ⥤ Top :=

src/category_theory/connected.lean

@@ -88,7 +88,8 @@ This can be thought of as a local-to-global property.
 
 The converse is shown in `connected.of_constant_of_preserves_morphisms`
 -/
-lemma constant_of_preserves_morphisms [connected J] {α : Type v₂} (F : J → α) (h : ∀ (j₁ j₂ : J) (f : j₁ ⟶ j₂), F j₁ = F j₂) (j : J) :
+lemma constant_of_preserves_morphisms [connected J] {α : Type v₂} (F : J → α)
+  (h : ∀ (j₁ j₂ : J) (f : j₁ ⟶ j₂), F j₁ = F j₂) (j : J) :
   F j = F (default J) :=
 any_functor_const_on_obj { obj := F, map := λ _ _ f, eq_to_hom (h _ _ f) } j
 

src/category_theory/endomorphism.lean

@@ -13,7 +13,8 @@ universes v v' u u'
 
 namespace category_theory
 
-/-- Endomorphisms of an object in a category. Arguments order in multiplication agrees with `function.comp`, not with `category.comp`. -/
+/-- Endomorphisms of an object in a category. Arguments order in multiplication agrees with
+`function.comp`, not with `category.comp`. -/
 def End {C : Type u} [𝒞_struct : category_struct.{v} C] (X : C) := X ⟶ X
 
 namespace End

src/category_theory/natural_isomorphism.lean

@@ -8,12 +8,14 @@ import category_theory.isomorphism
 
 open category_theory
 
-universes v₁ v₂ v₃ v₄ u₁ 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₃ v₄ u₁ u₂ u₃ u₄
 
 namespace category_theory
 open nat_trans
 
-/-- The application of a natural isomorphism to an object. We put this definition in a different namespace, so that we can use α.app -/
+/-- The application of a natural isomorphism to an object. We put this definition in a different
+namespace, so that we can use `α.app` -/
 @[simp, reducible] def iso.app {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
   {F G : C ⥤ D} (α : F ≅ G) (X : C) : F.obj X ≅ G.obj X :=
 { hom := α.hom.app X,
@@ -36,11 +38,13 @@ lemma app_hom {F G : C ⥤ D} (α : F ≅ G) (X : C) : (α.app X).hom = α.hom.a
 lemma app_inv {F G : C ⥤ D} (α : F ≅ G) (X : C) : (α.app X).inv = α.inv.app X := rfl
 
 @[simp, reassoc]
-lemma hom_inv_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) : α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X) :=
+lemma hom_inv_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
+  α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X) :=
 congr_fun (congr_arg app α.hom_inv_id) X
 
 @[simp, reassoc]
-lemma inv_hom_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) : α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X) :=
+lemma inv_hom_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
+  α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X) :=
 congr_fun (congr_arg app α.inv_hom_id) X
 
 variables {F G : C ⥤ D}

src/category_theory/products/basic.lean

@@ -35,17 +35,20 @@ end
 section
 variables (C : Type u₁) [category.{v₁} C] (D : Type u₁) [category.{v₁} D]
 /--
-`prod.category.uniform C D` is an additional instance specialised so both factors have the same universe levels. This helps typeclass resolution.
+`prod.category.uniform C D` is an additional instance specialised so both factors have the same
+universe levels. This helps typeclass resolution.
 -/
 instance uniform_prod : category (C × D) := category_theory.prod C D
 end
 
--- Next we define the natural functors into and out of product categories. For now this doesn't address the universal properties.
+-- Next we define the natural functors into and out of product categories. For now this doesn't
+-- address the universal properties.
 namespace prod
 
 /-- `sectl C Z` is the functor `C ⥤ C × D` given by `X ↦ (X, Z)`. -/
 -- Here and below we specify explicitly the projections to generate `@[simp]` lemmas for,
--- as the default behaviour of `@[simps]` will generate projections all the way down to components of pairs.
+-- as the default behaviour of `@[simps]` will generate projections all the way down to components
+-- of pairs.
 @[simps obj map] def sectl
   (C : Type u₁) [category.{v₁} C] {D : Type u₂} [category.{v₂} D] (Z : D) : C ⥤ C × D :=
 { obj := λ X, (X, Z),