style: a linter for four spaces (#7283)

Includes an auto-fix feature with the `--fix` flag so that spacing suggestions will be automatically applied in review also.



Co-authored-by: Moritz Firsching <firsching@google.com>

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -154,7 +154,7 @@ theorem orderOf_eq_card_of_forall_mem_zpowers [Fintype α] {g : α} (hx : ∀ x,
 
 @[to_additive exists_nsmul_ne_zero_of_isAddCyclic]
 theorem exists_pow_ne_one_of_isCyclic {G : Type*} [Group G] [Fintype G] [G_cyclic : IsCyclic G]
-  {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Fintype.card G) : ∃ a : G, a ^ k ≠ 1 := by
+    {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Fintype.card G) : ∃ a : G, a ^ k ≠ 1 := by
   rcases G_cyclic with ⟨a, ha⟩
   use a
   contrapose! k_lt_card_G

Mathlib/LinearAlgebra/Prod.lean

@@ -607,7 +607,8 @@ def fst : Submodule R (M × M₂) :=
 
 /-- `M` as a submodule of `M × N` is isomorphic to `M`. -/
 @[simps]
-def fstEquiv : Submodule.fst R M M₂ ≃ₗ[R] M where -- Porting note: proofs were `tidy` or `simp`
+def fstEquiv : Submodule.fst R M M₂ ≃ₗ[R] M where
+  -- Porting note: proofs were `tidy` or `simp`
   toFun x := x.1.1
   invFun m := ⟨⟨m, 0⟩, by simp only [fst, comap_bot, mem_ker, snd_apply]⟩
   map_add' := by simp only [AddSubmonoid.coe_add, coe_toAddSubmonoid, Prod.fst_add, Subtype.forall,

Mathlib/NumberTheory/NumberField/Units.lean

@@ -368,7 +368,7 @@ theorem seq_norm_ne_zero (n : ℕ) : Algebra.norm ℤ (seq K w₁ hB n : 𝓞 K)
 
 /-- The sequence is strictly decreasing at infinite places distinct from `w₁`. -/
 theorem seq_decreasing {n m : ℕ} (h : n < m) (w : InfinitePlace K) (hw : w ≠ w₁) :
-     w (seq K w₁ hB m) < w (seq K w₁ hB n) := by
+    w (seq K w₁ hB m) < w (seq K w₁ hB n) := by
   induction m with
   | zero =>
       exfalso

Mathlib/Tactic/ToAdditive.lean

@@ -1096,7 +1096,7 @@ attribute is added to the generated lemma only, to additivize it again.
 This is useful for lemmas about `Pow` to generate both lemmas about `SMul` and `VAdd`. Example:
 ```
 @[to_additive (attr := to_additive VAdd_lemma, simp) SMul_lemma]
-lemma Pow_lemma ...
+lemma Pow_lemma ... :=
 ```
 In the above example, the `simp` is added to all 3 lemmas. All other options to `to_additive`
 (like the generated name or `(reorder := ...)`) are not passed down,

scripts/lint-style.py

@@ -47,8 +47,9 @@
 ERR_DOT = 12 # isolated or low focusing dot
 ERR_SEM = 13 # the substring " ;"
 ERR_WIN = 14 # Windows line endings "\r\n"
-ERR_TWS = 15 # Trailing whitespace
-ERR_CLN = 16 # Line starts with a colon
+ERR_TWS = 15 # trailing whitespace
+ERR_CLN = 16 # line starts with a colon
+ERR_IND = 17 # second line not correctly indented
 
 exceptions = []
 
@@ -160,6 +161,40 @@ def line_endings_check(lines, path):
         newlines.append((line_nr, line))
     return errors, newlines
 
+def four_spaces_in_second_line(lines, path):
+    # TODO: also fix the space for all lines before ":=", right now we only fix the line after
+    # the first line break
+    errors = []
+    # We never alter the first line, as it does not occur as next_line in the iteration over the
+    # zipped lines below, hence we add it here
+    newlines = [lines[0]]
+    annotated_lines = list(annotate_comments(lines))
+    for (_, line, is_comment), (next_line_nr, next_line, _) in zip(annotated_lines,
+                                                                   annotated_lines[1:]):
+        # Check if the current line matches "(lemma|theorem) .* :"
+        new_next_line = next_line
+        if (not is_comment) and re.search(r"^(protected )?(def|lemma|theorem) (?!.*:=).*(where)?$",
+                                          line):
+            # Calculate the number of spaces before the first non-space character in the next line
+            stripped_next_line = next_line.lstrip()
+            if not (next_line == '\n' or next_line.startswith("#") or stripped_next_line.startswith("--")):
+                num_spaces = len(next_line) - len(stripped_next_line)
+                # The match with "| " could potentially match with a different usage of the same
+                # symbol, e.g. some sort of norm. In that case a space is not necessary, so
+                # looking for "| " should be enough.
+                if stripped_next_line.startswith("| ") or line.endswith("where\n"):
+                    # Check and fix if the number of leading space is not 2
+                    if num_spaces != 2:
+                        errors += [(ERR_IND, next_line_nr, path)]
+                        new_next_line = ' ' * 2 + stripped_next_line
+                # Check and fix if the number of leading spaces is not 4
+                else:
+                    if num_spaces != 4:
+                        errors += [(ERR_IND, next_line_nr, path)]
+                        new_next_line = ' ' * 4 + stripped_next_line
+        newlines.append((next_line_nr, new_next_line))
+    return errors, newlines
+
 def long_lines_check(lines, path):
     errors = []
     # TODO: find a good way to break long lines
@@ -306,26 +341,28 @@ def format_errors(errors):
             output_message(path, line_nr, "ERR_TWS", "Trailing whitespace detected on line")
         if errno == ERR_CLN:
             output_message(path, line_nr, "ERR_CLN", "Put : and := before line breaks, not after")
+        if errno == ERR_IND:
+            output_message(path, line_nr, "ERR_IND", "If the theorem/def statement requires multiple lines, indent it correctly (4 spaces or 2 for `|`)")
 
 def lint(path, fix=False):
     with path.open(encoding="utf-8", newline="") as f:
         # We enumerate the lines so that we can report line numbers in the error messages correctly
         # we will modify lines as we go, so we need to keep track of the original line numbers
         lines = f.readlines()
         enum_lines = enumerate(lines, 1)
-        errs, newlines = line_endings_check(enum_lines, path)
-        format_errors(errs)
-
-        errs,newlines = long_lines_check(newlines, path)
-        format_errors(errs)
-        errs,newlines = isolated_by_dot_semicolon_check(newlines, path)
-        format_errors(errs)
-        errs,newlines = set_option_check(newlines, path)
-        format_errors(errs)
+        newlines = enum_lines
+        for error_check in [line_endings_check,
+                            four_spaces_in_second_line,
+                            long_lines_check,
+                            isolated_by_dot_semicolon_check,
+                            set_option_check]:
+            errs, newlines = error_check(newlines, path)
+            format_errors(errs)
+
         if not import_only_check(newlines, path):
-            errs,newlines = regular_check(newlines, path)
+            errs, newlines = regular_check(newlines, path)
             format_errors(errs)
-            errs,newlines = banned_import_check(newlines, path)
+            errs, newlines = banned_import_check(newlines, path)
             format_errors(errs)
     # if we haven't been asked to fix errors, or there are no errors or no fixes, we're done
     if fix and new_exceptions and enum_lines != newlines: