chore({algebra, algebraic_geometry}/*): move 1 module doc and split l…

…ines (#6294)

This moves the module doc for `algebra/ordered_group` so that it gets recognised by the linter. Furthermore, several lines are split in the algebra and algebraic_geometry folder.

archive/miu_language/basic.lean

@@ -50,7 +50,8 @@ natural number' into the nonrecursive constructor `zero` of the inductive type `
 
 ## References
 
-* [Jeremy Avigad, Leonardo de Moura and Soonho Kong, _Theorem Proving in Lean_][avigad_moura_kong-2017]
+* [Jeremy Avigad, Leonardo de Moura and Soonho Kong, _Theorem Proving in Lean_]
+  [avigad_moura_kong-2017]
 * [Douglas R Hofstadter, _Gödel, Escher, Bach_][Hofstadter-1979]
 
 ## Tags

src/algebra/continued_fractions/convergents_equiv.lean

@@ -280,7 +280,7 @@ begin
           (continuants_recurrence_aux s_nth_eq zeroth_continuant_aux_eq_one_zero
           first_continuant_aux_eq_h_one)],
       calc
-        (b * g.h + a) / b = b * g.h / b + a / b  : by ring -- requires `field` rather than `division_ring`
+        (b * g.h + a) / b = b * g.h / b + a / b  : by ring -- requires `field`, not `division_ring`
                       ... = g.h + a / b          : by rw (mul_div_cancel_left _ b_ne_zero) },
     case nat.succ
     { obtain ⟨⟨pa, pb⟩, s_n'th_eq⟩ : ∃ gp_n', g.s.nth n' = some gp_n' :=

src/algebra/continued_fractions/terminated_stable.lean

@@ -25,7 +25,8 @@ variable [division_ring K]
 
 lemma continuants_aux_stable_step_of_terminated (terminated_at_n : g.terminated_at n) :
   g.continuants_aux (n + 2) = g.continuants_aux (n + 1) :=
-by { rw [terminated_at_iff_s_none] at terminated_at_n, simp only [terminated_at_n, continuants_aux] }
+by { rw [terminated_at_iff_s_none] at terminated_at_n,
+     simp only [terminated_at_n, continuants_aux] }
 
 lemma continuants_aux_stable_of_terminated (succ_n_le_m : (n + 1) ≤ m)
   (terminated_at_n : g.terminated_at n) :

src/algebra/free_monoid.lean

@@ -56,7 +56,8 @@ lemma of_injective : function.injective (@of α) :=
 λ a b, list.head_eq_of_cons_eq
 
 /-- Recursor for `free_monoid` using `1` and `of x * xs` instead of `[]` and `x :: xs`. -/
-@[to_additive "Recursor for `free_add_monoid` using `0` and `of x + xs` instead of `[]` and `x :: xs`."]
+@[to_additive
+  "Recursor for `free_add_monoid` using `0` and `of x + xs` instead of `[]` and `x :: xs`."]
 def rec_on {C : free_monoid α → Sort*} (xs : free_monoid α) (h0 : C 1)
   (ih : Π x xs, C xs → C (of x * xs)) : C xs := list.rec_on xs h0 ih
 

src/algebra/module/submodule.lean

@@ -11,8 +11,8 @@ import group_theory.group_action.sub_mul_action
 
 In this file we define
 
-* `submodule R M` : a subset of a `module` `M` that contains zero and is closed with respect to addition and
-  scalar multiplication.
+* `submodule R M` : a subset of a `module` `M` that contains zero and is closed with respect to
+  addition and scalar multiplication.
 
 * `subspace k M` : an abbreviation for `submodule` assuming that `k` is a `field`.
 

src/algebra/ordered_group.lean

@@ -5,8 +5,6 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import algebra.ordered_monoid
 
-set_option old_structure_cmd true
-
 /-!
 # Ordered groups
 
@@ -20,6 +18,8 @@ The reason is that we did not want to change existing names in the library.
 
 -/
 
+set_option old_structure_cmd true
+
 universe u
 variable {α : Type u}
 

src/algebraic_geometry/presheafed_space/has_colimits.lean

@@ -202,8 +202,8 @@ end
 lemma desc_c_naturality (F : J ⥤ PresheafedSpace C) (s : cocone F)
   {U V : (opens ↥(s.X.carrier))ᵒᵖ} (i : U ⟶ V) :
   s.X.presheaf.map i ≫ desc_c_app F s V =
-  desc_c_app F s U ≫
-    (colimit.desc (F ⋙ forget C) ((forget C).map_cocone s) _* (colimit_cocone F).X.presheaf).map i :=
+  desc_c_app F s U ≫ (colimit.desc (F ⋙ forget C)
+    ((forget C).map_cocone s) _* (colimit_cocone F).X.presheaf).map i :=
 begin
   dsimp [desc_c_app],
   ext,
@@ -249,7 +249,8 @@ def colimit_cocone_is_colimit (F : J ⥤ PresheafedSpace C) : is_colimit (colimi
   uniq' := λ s m w,
   begin
     -- We need to use the identity on the continuous maps twice, so we prepare that first:
-    have t : m.base = colimit.desc (F ⋙ PresheafedSpace.forget C) ((PresheafedSpace.forget C).map_cocone s),
+    have t : m.base = colimit.desc (F ⋙ PresheafedSpace.forget C)
+                        ((PresheafedSpace.forget C).map_cocone s),
     { ext,
       dsimp,
       simp only [colimit.ι_desc_apply, map_cocone_ι_app],

src/algebraic_geometry/sheafed_space.lean

@@ -47,7 +47,8 @@ def sheaf (X : SheafedSpace C) : sheaf C (X : Top.{v}) := ⟨X.presheaf, X.sheaf
 
 @[simp] lemma as_coe (X : SheafedSpace C) : X.carrier = (X : Top.{v}) := rfl
 @[simp] lemma mk_coe (carrier) (presheaf) (h) :
-  (({ carrier := carrier, presheaf := presheaf, sheaf_condition := h } : SheafedSpace.{v} C) : Top.{v}) = carrier :=
+  (({ carrier := carrier, presheaf := presheaf, sheaf_condition := h } : SheafedSpace.{v} C) :
+  Top.{v}) = carrier :=
 rfl
 
 instance (X : SheafedSpace.{v} C) : topological_space X := X.carrier.str

src/algebraic_geometry/stalks.lean

@@ -44,8 +44,9 @@ def stalk_map {X Y : PresheafedSpace C} (α : X ⟶ Y) (x : X) : Y.stalk (α.bas
 section restrict
 
 -- PROJECT: restriction preserves stalks.
--- We'll want to define cofinal functors, show precomposing with a cofinal functor preserves colimits,
--- and (easily) verify that "open neighbourhoods of x within U" is cofinal in "open neighbourhoods of x".
+-- We'll want to define cofinal functors, show precomposing with a cofinal functor preserves
+-- colimits, and (easily) verify that "open neighbourhoods of x within U" is cofinal in "open
+-- neighbourhoods of x".
 /-
 def restrict_stalk_iso {U : Top} (X : PresheafedSpace C)
   (f : U ⟶ (X : Top.{v})) (h : open_embedding f) (x : U) :