feat(scripts): make style lint script more robust to lines starting w…

…ith spaces (#13317)

Currently some banned commands aren't caught if the line is indented.

Because of this I previously snuck in a `set_option pp.all true` by accident

scripts/lint-style.py

@@ -132,15 +132,15 @@ def reserved_notation_check(lines, path):
         return []
     errors = []
     for line_nr, line in skip_string(skip_comments(enumerate(lines, 1))):
-        if line.startswith('reserve') or line.startswith('precedence'):
+        if line.strip().startswith('reserve') or line.strip().startswith('precedence'):
             errors += [(ERR_RNT, line_nr, path)]
     return errors
 
 def set_option_check(lines, path):
     errors = []
     for line_nr, line in skip_string(skip_comments(enumerate(lines, 1))):
-        if line.startswith('set_option'):
-            next_two_chars = line.split(' ')[1][:2]
+        if line.strip().startswith('set_option'):
+            next_two_chars = line.strip().split(' ')[1][:2]
             # forbidden options: pp, profiler, trace
             if next_two_chars == 'pp' or next_two_chars == 'pr' or next_two_chars == 'tr':
                 errors += [(ERR_OPT, line_nr, path)]

src/group_theory/order_of_element.lean

@@ -383,7 +383,6 @@ calc x ^ i = x ^ (i % order_of x + order_of x * (i / order_of x)) :
     by rw [int.mod_add_div]
        ... = x ^ (i % order_of x) :
     by simp [zpow_add, zpow_mul, pow_order_of_eq_one]
-    set_option pp.all true
 
 @[to_additive nsmul_inj_iff_of_add_order_of_eq_zero]
 lemma pow_inj_iff_of_order_of_eq_zero (h : order_of x = 0) {n m : ℕ} :