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

src/algebra/category/CommRing/colimits.lean

@@ -290,9 +290,14 @@ instance : comm_ring (colimit_type F) :=
 
 @[simp] lemma quot_zero : quot.mk setoid.r zero = (0 : colimit_type F) := rfl
 @[simp] lemma quot_one : quot.mk setoid.r one = (1 : colimit_type F) := rfl
-@[simp] lemma quot_neg (x) : quot.mk setoid.r (neg x) = (-(quot.mk setoid.r x) : colimit_type F) := rfl
-@[simp] lemma quot_add (x y) : quot.mk setoid.r (add x y) = ((quot.mk setoid.r x) + (quot.mk setoid.r y) : colimit_type F) := rfl
-@[simp] lemma quot_mul (x y) : quot.mk setoid.r (mul x y) = ((quot.mk setoid.r x) * (quot.mk setoid.r y) : colimit_type F) := rfl
+
+@[simp] lemma quot_neg (x) : quot.mk setoid.r (neg x) = (-(quot.mk setoid.r x) : colimit_type F) :=
+rfl
+
+@[simp] lemma quot_add (x y) :
+  quot.mk setoid.r (add x y) = ((quot.mk setoid.r x) + (quot.mk setoid.r y) : colimit_type F) := rfl
+@[simp] lemma quot_mul (x y) :
+  quot.mk setoid.r (mul x y) = ((quot.mk setoid.r x) * (quot.mk setoid.r y) : colimit_type F) := rfl
 
 /-- The bundled commutative ring giving the colimit of a diagram. -/
 def colimit : CommRing := CommRing.of (colimit_type F)
@@ -301,7 +306,8 @@ def colimit : CommRing := CommRing.of (colimit_type F)
 def cocone_fun (j : J) (x : F.obj j) : colimit_type F :=
 quot.mk _ (of j x)
 
-/-- The ring homomorphism from a given commutative ring in the diagram to the colimit commutative ring. -/
+/-- The ring homomorphism from a given commutative ring in the diagram to the colimit commutative
+ring. -/
 def cocone_morphism (j : J) : F.obj j ⟶ colimit F :=
 { to_fun := cocone_fun F j,
   map_one' := by apply quot.sound; apply relation.one,
@@ -327,7 +333,8 @@ def colimit_cocone : cocone F :=
   ι :=
   { app := cocone_morphism F } }.
 
-/-- The function from the free commutative ring on the diagram to the cone point of any other cocone. -/
+/-- The function from the free commutative ring on the diagram to the cone point of any other
+cocone. -/
 @[simp] def desc_fun_lift (s : cocone F) : prequotient F → s.X
 | (of j x)  := (s.ι.app j) x
 | zero      := 0
@@ -396,7 +403,8 @@ begin
   }
 end
 
-/-- The ring homomorphism from the colimit commutative ring to the cone point of any other cocone. -/
+/-- The ring homomorphism from the colimit commutative ring to the cone point of any other
+cocone. -/
 def desc_morphism (s : cocone F) : colimit F ⟶ s.X :=
 { to_fun := desc_fun F s,
   map_one' := rfl,

src/algebra/category/Group/limits.lean

@@ -80,15 +80,17 @@ creates_limit_of_reflects_iso (λ c' t,
 A choice of limit cone for a functor into `Group`.
 (Generally, you'll just want to use `limit F`.)
 -/
-@[to_additive "A choice of limit cone for a functor into `Group`. (Generally, you'll just want to use `limit F`.)"]
+@[to_additive "A choice of limit cone for a functor into `Group`.
+(Generally, you'll just want to use `limit F`.)"]
 def limit_cone (F : J ⥤ Group) : cone F :=
 lift_limit (limit.is_limit (F ⋙ (forget₂ Group Mon.{u})))
 
 /--
 The chosen cone is a limit cone.
 (Generally, you'll just want to use `limit.cone F`.)
 -/
-@[to_additive "The chosen cone is a limit cone. (Generally, you'll just want to use `limit.cone F`.)"]
+@[to_additive "The chosen cone is a limit cone.
+(Generally, you'll just want to use `limit.cone F`.)"]
 def limit_cone_is_limit (F : J ⥤ Group) : is_limit (limit_cone F) :=
 lifted_limit_is_limit _
 
@@ -100,7 +102,8 @@ instance has_limits : has_limits Group :=
 
 /--
 The forgetful functor from groups to monoids preserves all limits.
-(That is, the underlying monoid could have been computed instead as limits in the category of monoids.)
+(That is, the underlying monoid could have been computed instead as limits in the category
+of monoids.)
 -/
 @[to_additive AddGroup.forget₂_AddMon_preserves_limits]
 instance forget₂_Mon_preserves_limits : preserves_limits (forget₂ Group Mon) :=
@@ -146,22 +149,24 @@ creates_limit_of_reflects_iso (λ c' t,
     { app := Mon.limit_π_monoid_hom (F ⋙ forget₂ CommGroup Group.{u} ⋙ forget₂ Group Mon),
       naturality' := (Mon.has_limits.limit_cone _).π.naturality, } },
   valid_lift := is_limit.unique_up_to_iso (Group.limit_cone_is_limit _) t,
-  makes_limit := is_limit.of_faithful (forget₂ _ Group.{u} ⋙ forget₂ _ Mon.{u}) (Mon.has_limits.limit_cone_is_limit _)
-    (λ s, _) (λ s, rfl) })
+  makes_limit := is_limit.of_faithful (forget₂ _ Group.{u} ⋙ forget₂ _ Mon.{u})
+    (Mon.has_limits.limit_cone_is_limit _) (λ s, _) (λ s, rfl) })
 
 /--
 A choice of limit cone for a functor into `CommGroup`.
 (Generally, you'll just want to use `limit F`.)
 -/
-@[to_additive "A choice of limit cone for a functor into `CommGroup`. (Generally, you'll just want to use `limit F`.)"]
+@[to_additive "A choice of limit cone for a functor into `CommGroup`.
+(Generally, you'll just want to use `limit F`.)"]
 def limit_cone (F : J ⥤ CommGroup) : cone F :=
 lift_limit (limit.is_limit (F ⋙ (forget₂ CommGroup Group.{u})))
 
 /--
 The chosen cone is a limit cone.
 (Generally, you'll just want to use `limit.cone F`.)
 -/
-@[to_additive "The chosen cone is a limit cone. (Generally, you'll just want to use `limit.cone F`.)"]
+@[to_additive "The chosen cone is a limit cone.
+(Generally, you'll just wantto use `limit.cone F`.)"]
 def limit_cone_is_limit (F : J ⥤ CommGroup) : is_limit (limit_cone F) :=
 lifted_limit_is_limit _
 
@@ -173,7 +178,8 @@ instance has_limits : has_limits CommGroup :=
 
 /--
 The forgetful functor from commutative groups to groups preserves all limits.
-(That is, the underlying group could have been computed instead as limits in the category of groups.)
+(That is, the underlying group could have been computed instead as limits in the category
+of groups.)
 -/
 @[to_additive AddCommGroup.forget₂_AddGroup_preserves_limits]
 instance forget₂_Group_preserves_limits : preserves_limits (forget₂ CommGroup Group) :=
@@ -201,8 +207,8 @@ instance forget₂_CommMon_preserves_limits : preserves_limits (forget₂ CommGr
     (limit_cone_is_limit F) (forget₂_CommMon_preserves_limits_aux F) } }
 
 /--
-The forgetful functor from commutative groups to types preserves all limits. (That is, the underlying
-types could have been computed instead as limits in the category of types.)
+The forgetful functor from commutative groups to types preserves all limits. (That is, the
+underlying types could have been computed instead as limits in the category of types.)
 -/
 @[to_additive AddCommGroup.forget_preserves_limits]
 instance forget_preserves_limits : preserves_limits (forget CommGroup) :=

src/algebra/group_with_zero/basic.lean

@@ -233,7 +233,8 @@ end units
 
 namespace is_unit
 
-lemma ne_zero [nontrivial M₀] {a : M₀} (ha : is_unit a) : a ≠ 0 := let ⟨u, hu⟩ := ha in hu ▸ u.ne_zero
+lemma ne_zero [nontrivial M₀] {a : M₀} (ha : is_unit a) : a ≠ 0 := let ⟨u, hu⟩ :=
+ha in hu ▸ u.ne_zero
 
 lemma mul_right_eq_zero {a b : M₀} (ha : is_unit a) : a * b = 0 ↔ b = 0 :=
 let ⟨u, hu⟩ := ha in hu ▸ u.mul_right_eq_zero
@@ -254,7 +255,8 @@ All other elements will be provably equal to it, but not necessarily definitiona
 def unique_of_zero_eq_one (h : (0 : M₀) = 1) : unique M₀ :=
 { default := 0, uniq := eq_zero_of_zero_eq_one h }
 
-/-- In a monoid with zero, zero equals one if and only if all elements of that semiring are equal. -/
+/-- In a monoid with zero, zero equals one if and only if all elements of that semiring
+are equal. -/
 theorem subsingleton_iff_zero_eq_one : (0 : M₀) = 1 ↔ subsingleton M₀ :=
 ⟨λ h, @unique.subsingleton _ (unique_of_zero_eq_one h), λ h, @subsingleton.elim _ h _ _⟩
 

src/algebra/ordered_group.lean

@@ -370,9 +370,11 @@ lemma div_le_div_iff' : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b :=
 begin
   split ; intro h,
   have := mul_le_mul_right' (mul_le_mul_right' h b) d,
-  rwa [inv_mul_cancel_right, mul_assoc _ _ b, mul_comm _ b, ← mul_assoc, inv_mul_cancel_right] at this,
+  rwa [inv_mul_cancel_right, mul_assoc _ _ b, mul_comm _ b, ← mul_assoc, inv_mul_cancel_right]
+    at this,
   have := mul_le_mul_right' (mul_le_mul_right' h d⁻¹) b⁻¹,
-  rwa [mul_inv_cancel_right, _root_.mul_assoc, _root_.mul_comm d⁻¹ b⁻¹, ← mul_assoc, mul_inv_cancel_right] at this,
+  rwa [mul_inv_cancel_right, _root_.mul_assoc, _root_.mul_comm d⁻¹ b⁻¹, ← mul_assoc,
+    mul_inv_cancel_right] at this,
 end
 
 end ordered_comm_group

src/topology/uniform_space/basic.lean

@@ -217,7 +217,8 @@ def uniform_space.core.to_topological_space {α : Type u} (u : uniform_space.cor
   is_open_sUnion :=
     assume s hs x ⟨t, ts, xt⟩, by filter_upwards [hs t ts x xt] assume p ph h, ⟨t, ts, ph h⟩ }
 
-lemma uniform_space.core_eq : ∀{u₁ u₂ : uniform_space.core α}, u₁.uniformity = u₂.uniformity → u₁ = u₂
+lemma uniform_space.core_eq :
+  ∀{u₁ u₂ : uniform_space.core α}, u₁.uniformity = u₂.uniformity → u₁ = u₂
 | ⟨u₁, _, _, _⟩  ⟨u₂, _, _, _⟩ h := by { congr, exact h }
 
 /-- Suppose that one can put two mathematical structures on a type, a rich one `R` and a poor one
@@ -382,7 +383,7 @@ tendsto_diag_uniformity (λ _, a) f
 lemma symm_of_uniformity {s : set (α × α)} (hs : s ∈ 𝓤 α) :
   ∃ t ∈ 𝓤 α, (∀a b, (a, b) ∈ t → (b, a) ∈ t) ∧ t ⊆ s :=
 have preimage prod.swap s ∈ 𝓤 α, from symm_le_uniformity hs,
-⟨s ∩ preimage prod.swap s, inter_mem_sets hs this, assume a b ⟨h₁, h₂⟩, ⟨h₂, h₁⟩, inter_subset_left _ _⟩
+⟨s ∩ preimage prod.swap s, inter_mem_sets hs this, λ a b ⟨h₁, h₂⟩, ⟨h₂, h₁⟩, inter_subset_left _ _⟩
 
 lemma comp_symm_of_uniformity {s : set (α × α)} (hs : s ∈ 𝓤 α) :
   ∃ t ∈ 𝓤 α, (∀{a b}, (a, b) ∈ t → (b, a) ∈ t) ∧ t ○ t ⊆ s :=
@@ -571,7 +572,8 @@ begin
   exact iff.rfl,
 end
 
-lemma nhds_basis_uniformity' {p : β → Prop} {s : β → set (α × α)} (h : (𝓤 α).has_basis p s) {x : α} :
+lemma nhds_basis_uniformity' {p : β → Prop} {s : β → set (α × α)} (h : (𝓤 α).has_basis p s)
+  {x : α} :
   (𝓝 x).has_basis p (λ i, {y | (x, y) ∈ s i}) :=
 by { rw [nhds_eq_comap_uniformity], exact h.comap (prod.mk x) }
 
@@ -652,7 +654,8 @@ eq.trans
 lemma lift_nhds_right {x : α} {g : set α → filter β} (hg : monotone g) :
   (𝓝 x).lift g = (𝓤 α).lift (λs:set (α×α), g {y | (y, x) ∈ s}) :=
 calc (𝓝 x).lift g = (𝓤 α).lift (λs:set (α×α), g {y | (x, y) ∈ s}) : lift_nhds_left hg
-  ... = ((@prod.swap α α) <$> (𝓤 α)).lift (λs:set (α×α), g {y | (x, y) ∈ s}) : by rw [←uniformity_eq_symm]
+  ... = ((@prod.swap α α) <$> (𝓤 α)).lift (λs:set (α×α), g {y | (x, y) ∈ s}) :
+    by rw [←uniformity_eq_symm]
   ... = (𝓤 α).lift (λs:set (α×α), g {y | (x, y) ∈ image prod.swap s}) :
     map_lift_eq2 $ hg.comp monotone_preimage
   ... = _ : by simp [image_swap_eq_preimage_swap]
@@ -811,12 +814,13 @@ lemma uniformity_eq_uniformity_interior : 𝓤 α = (𝓤 α).lift' interior :=
 le_antisymm
   (le_infi $ assume d, le_infi $ assume hd,
     let ⟨s, hs, hs_comp⟩ := (mem_lift'_sets $
-      monotone_comp_rel monotone_id $ monotone_comp_rel monotone_id monotone_id).mp (comp_le_uniformity3 hd) in
+      monotone_comp_rel monotone_id $ monotone_comp_rel monotone_id monotone_id).mp
+        (comp_le_uniformity3 hd) in
     let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs in
     have s ⊆ interior d, from
       calc s ⊆ t : hst
        ... ⊆ interior d : (subset_interior_iff_subset_of_open ht).mpr $
-        assume x, assume : x ∈ t, let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp this in hs_comp ⟨x, h₁, y, h₂, h₃⟩,
+        λ x (hx : x ∈ t), let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx in hs_comp ⟨x, h₁, y, h₂, h₃⟩,
     have interior d ∈ 𝓤 α, by filter_upwards [hs] this,
     by simp [this])
   (assume s hs, ((𝓤 α).lift' interior).sets_of_superset (mem_lift' hs) interior_subset)
@@ -913,10 +917,11 @@ lemma filter.has_basis.uniform_continuous_iff [uniform_space β] {p : γ → Pro
   uniform_continuous f ↔ ∀ i (hi : q i), ∃ j (hj : p j), ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ t i :=
 (ha.tendsto_iff hb).trans $ by simp only [prod.forall]
 
-lemma filter.has_basis.uniform_continuous_on_iff [uniform_space β] {p : γ → Prop} {s : γ → set (α×α)}
-  (ha : (𝓤 α).has_basis p s) {q : δ → Prop} {t : δ → set (β×β)} (hb : (𝓤 β).has_basis q t)
-  {f : α → β} {S : set α} :
-  uniform_continuous_on f S ↔ ∀ i (hi : q i), ∃ j (hj : p j), ∀ x y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i :=
+lemma filter.has_basis.uniform_continuous_on_iff [uniform_space β] {p : γ → Prop}
+  {s : γ → set (α×α)} (ha : (𝓤 α).has_basis p s) {q : δ → Prop} {t : δ → set (β×β)}
+  (hb : (𝓤 β).has_basis q t) {f : α → β} {S : set α} :
+  uniform_continuous_on f S ↔
+    ∀ i (hi : q i), ∃ j (hj : p j), ∀ x y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i :=
 ((ha.inf_principal (S.prod S)).tendsto_iff hb).trans $ by finish [prod.forall]
 
 end uniform_space
@@ -1011,7 +1016,8 @@ def uniform_space.comap (f : α → β) (u : uniform_space β) : uniform_space 
 { uniformity := u.uniformity.comap (λp:α×α, (f p.1, f p.2)),
   to_topological_space := u.to_topological_space.induced f,
   refl := le_trans (by simp; exact assume ⟨a, b⟩ (h : a = b), h ▸ rfl) (comap_mono u.refl),
-  symm := by simp [tendsto_comap_iff, prod.swap, (∘)]; exact tendsto_swap_uniformity.comp tendsto_comap,
+  symm := by simp [tendsto_comap_iff, prod.swap, (∘)];
+            exact tendsto_swap_uniformity.comp tendsto_comap,
   comp := le_trans
     begin
       rw [comap_lift'_eq, comap_lift'_eq2],
@@ -1123,7 +1129,8 @@ lemma uniform_continuous_subtype_mk {p : α → Prop} [uniform_space α] [unifor
   uniform_continuous (λx, ⟨f x, h x⟩ : β → subtype p) :=
 uniform_continuous_comap' hf
 
-lemma uniform_continuous_on_iff_restrict [uniform_space α] [uniform_space β] {f : α → β} {s : set α} :
+lemma uniform_continuous_on_iff_restrict [uniform_space α] [uniform_space β] {f : α → β}
+  {s : set α} :
   uniform_continuous_on f s ↔ uniform_continuous (s.restrict f) :=
 begin
   unfold uniform_continuous_on set.restrict uniform_continuous tendsto,
@@ -1192,8 +1199,8 @@ begin
   refl
 end
 
-lemma mem_uniform_prod [t₁ : uniform_space α] [t₂ : uniform_space β] {a : set (α × α)} {b : set (β × β)}
-  (ha : a ∈ 𝓤 α) (hb : b ∈ 𝓤 β) :
+lemma mem_uniform_prod [t₁ : uniform_space α] [t₂ : uniform_space β] {a : set (α × α)}
+  {b : set (β × β)} (ha : a ∈ 𝓤 α) (hb : b ∈ 𝓤 β) :
   {p:(α×β)×(α×β) | (p.1.1, p.2.1) ∈ a ∧ (p.1.2, p.2.2) ∈ b } ∈ (@uniformity (α × β) _) :=
 by rw [uniformity_prod]; exact inter_mem_inf_sets (preimage_mem_comap ha) (preimage_mem_comap hb)
 
@@ -1205,10 +1212,12 @@ lemma tendsto_prod_uniformity_snd [uniform_space α] [uniform_space β] :
   tendsto (λp:(α×β)×(α×β), (p.1.2, p.2.2)) (𝓤 (α × β)) (𝓤 β) :=
 le_trans (map_mono (@inf_le_right (uniform_space (α×β)) _ _ _)) map_comap_le
 
-lemma uniform_continuous_fst [uniform_space α] [uniform_space β] : uniform_continuous (λp:α×β, p.1) :=
+lemma uniform_continuous_fst [uniform_space α] [uniform_space β] :
+  uniform_continuous (λp:α×β, p.1) :=
 tendsto_prod_uniformity_fst
 
-lemma uniform_continuous_snd [uniform_space α] [uniform_space β] : uniform_continuous (λp:α×β, p.2) :=
+lemma uniform_continuous_snd [uniform_space α] [uniform_space β] :
+  uniform_continuous (λp:α×β, p.2) :=
 tendsto_prod_uniformity_snd
 
 variables [uniform_space α] [uniform_space β] [uniform_space γ]
@@ -1305,7 +1314,8 @@ lemma union_mem_uniformity_sum
   {a : set (α × α)} (ha : a ∈ 𝓤 α) {b : set (β × β)} (hb : b ∈ 𝓤 β) :
   ((λ p : (α × α), (inl p.1, inl p.2)) '' a ∪ (λ p : (β × β), (inr p.1, inr p.2)) '' b) ∈
     (@uniform_space.core.sum α β _ _).uniformity :=
-⟨mem_map_sets_iff.2 ⟨_, ha, subset_union_left _ _⟩, mem_map_sets_iff.2 ⟨_, hb, subset_union_right _ _⟩⟩
+⟨mem_map_sets_iff.2 ⟨_, ha, subset_union_left _ _⟩,
+  mem_map_sets_iff.2 ⟨_, hb, subset_union_right _ _⟩⟩
 
 /- To prove that the topology defined by the uniform structure on the disjoint union coincides with
 the disjoint union topology, we need two lemmas saying that open sets can be characterized by
@@ -1315,19 +1325,22 @@ lemma uniformity_sum_of_open_aux {s : set (α ⊕ β)} (hs : is_open s) {x : α
 begin
   cases x,
   { refine mem_sets_of_superset
-      (union_mem_uniformity_sum (mem_nhds_uniformity_iff_right.1 (mem_nhds_sets hs.1 xs)) univ_mem_sets)
+      (union_mem_uniformity_sum (mem_nhds_uniformity_iff_right.1 (mem_nhds_sets hs.1 xs))
+        univ_mem_sets)
       (union_subset _ _);
     rintro _ ⟨⟨_, b⟩, h, ⟨⟩⟩ ⟨⟩,
     exact h rfl },
   { refine mem_sets_of_superset
-      (union_mem_uniformity_sum univ_mem_sets (mem_nhds_uniformity_iff_right.1 (mem_nhds_sets hs.2 xs)))
+      (union_mem_uniformity_sum univ_mem_sets (mem_nhds_uniformity_iff_right.1
+        (mem_nhds_sets hs.2 xs)))
       (union_subset _ _);
     rintro _ ⟨⟨a, _⟩, h, ⟨⟩⟩ ⟨⟩,
     exact h rfl },
 end
 
 lemma open_of_uniformity_sum_aux {s : set (α ⊕ β)}
-  (hs : ∀x ∈ s, { p : ((α ⊕ β) × (α ⊕ β)) | p.1 = x → p.2 ∈ s } ∈ (@uniform_space.core.sum α β _ _).uniformity) :
+  (hs : ∀x ∈ s, { p : ((α ⊕ β) × (α ⊕ β)) | p.1 = x → p.2 ∈ s } ∈
+    (@uniform_space.core.sum α β _ _).uniformity) :
   is_open s :=
 begin
   split,