From dc1905bcf529e9ac22830fd0e8016e1e6ec2a3f3 Mon Sep 17 00:00:00 2001
From: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Date: Fri, 11 Dec 2020 23:53:31 -0500
Subject: [PATCH 1/9] ci(lint-copy-mod-doc.py): add reserved notation linter

---
 scripts/lint-copy-mod-doc.py | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/scripts/lint-copy-mod-doc.py b/scripts/lint-copy-mod-doc.py
index aafa3150e0dc9..286440d382a6a 100755
--- a/scripts/lint-copy-mod-doc.py
+++ b/scripts/lint-copy-mod-doc.py
@@ -9,6 +9,7 @@
 ERR_MOD = 2 # module docstring
 ERR_LIN = 3 # line length
 ERR_SAV = 4 # ᾰ
+ERR_RNT = 5 # reserved notation
 
 exceptions = []
 
@@ -25,12 +26,20 @@
             exceptions += [(ERR_LIN, fn)]
         if errno == "ERR_SAV":
             exceptions += [(ERR_SAV, fn)]
+        if errno == "ERR_RNT":
+            exceptions += [(ERR_RNT, fn)]
 
 new_exceptions = False
 
 def small_alpha_vrachy_check(lines, fn):
     return [ (ERR_SAV, line_nr, fn) for line_nr, line in enumerate(lines) if 'ᾰ' in line ]
 
+def reserved_notation_check(lines, fn):
+    if fn == 'src/tactic/core.lean':
+        return []
+    return [ (ERR_RNT, line_nr, fn) for line_nr, line in enumerate(lines)
+        if line.startswith('reserve') or line.startswith('precedence') ]
+
 def long_lines_check(lines, fn):
     errors = []
     for line_nr, line in enumerate(lines, 1):
@@ -121,6 +130,8 @@ def format_errors(errors):
             print("{} : line {} : ERR_LIN : Line has more than 100 characters".format(fn, line_nr))
         if errno == ERR_SAV:
             print("{} : line {} : ERR_SAV : File contains the character ᾰ".format(fn, line_nr))
+        if errno == ERR_RNT:
+            print("{} : line {} : ERR_RNT : Reserved notation outside tactic.core".format(fn, line_nr))
 
 def lint(fn):
     with open(fn) as f:
@@ -133,6 +144,10 @@ def lint(fn):
             return
         errs = regular_check(lines, fn)
         format_errors(errs)
+        errs = small_alpha_vrachy_check(lines, fn)
+        format_errors(errs)
+        errs = reserved_notation_check(lines, fn)
+        format_errors(errs)
 
 for fn in fns:
     lint(fn)

From 989232bdeccdf32424c83dc5944d70743fde4147 Mon Sep 17 00:00:00 2001
From: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Date: Sat, 12 Dec 2020 02:22:42 -0500
Subject: [PATCH 2/9] fix line numbers, skip comments

---
 scripts/lint-copy-mod-doc.py | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/scripts/lint-copy-mod-doc.py b/scripts/lint-copy-mod-doc.py
index 286440d382a6a..a132af24b87f5 100755
--- a/scripts/lint-copy-mod-doc.py
+++ b/scripts/lint-copy-mod-doc.py
@@ -32,13 +32,24 @@
 new_exceptions = False
 
 def small_alpha_vrachy_check(lines, fn):
-    return [ (ERR_SAV, line_nr, fn) for line_nr, line in enumerate(lines) if 'ᾰ' in line ]
+    return [ (ERR_SAV, line_nr, fn) for line_nr, line in enumerate(lines, 1) if 'ᾰ' in line ]
 
 def reserved_notation_check(lines, fn):
     if fn == 'src/tactic/core.lean':
         return []
-    return [ (ERR_RNT, line_nr, fn) for line_nr, line in enumerate(lines)
-        if line.startswith('reserve') or line.startswith('precedence') ]
+    errors = []
+    in_comment = False
+    for line_nr, line in enumerate(lines, 1):
+        if "/-" in line:
+            in_comment = True
+        if "-/" in line:
+            in_comment = False
+            continue
+        if line == "\n" or in_comment:
+            continue
+        if line.startswith('reserve') or line.startswith('precedence'):
+            errors += [(ERR_RNT, line_nr, fn)]
+    return errors
 
 def long_lines_check(lines, fn):
     errors = []

From a7fb35734a2da75e9c551f6c6000ccb451c5ad4e Mon Sep 17 00:00:00 2001
From: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Date: Sat, 12 Dec 2020 02:23:01 -0500
Subject: [PATCH 3/9] move notation, add exceptions

---
 scripts/copy-mod-doc-exceptions.txt | 48 ++++++++++++-----------------
 src/linear_algebra/basic.lean       | 29 +++++++++--------
 src/order/lattice.lean              |  5 ++-
 src/tactic/core.lean                | 36 ++++++++++++++++++++++
 src/tactic/lift.lean                | 14 ++++-----
 src/tactic/lint/frontend.lean       | 14 ++++-----
 src/tactic/localized.lean           |  2 --
 src/tactic/rcases.lean              |  6 ++--
 src/tactic/simps.lean               |  5 +--
 src/tactic/where.lean               | 14 +++++----
 10 files changed, 99 insertions(+), 74 deletions(-)

diff --git a/scripts/copy-mod-doc-exceptions.txt b/scripts/copy-mod-doc-exceptions.txt
index 53e7097121c5c..90ca178ee97e4 100644
--- a/scripts/copy-mod-doc-exceptions.txt
+++ b/scripts/copy-mod-doc-exceptions.txt
@@ -133,7 +133,7 @@ src/algebra/monoid_algebra.lean : line 850 : ERR_LIN : Line has more than 100 ch
 src/algebra/ordered_group.lean : line 369 : ERR_LIN : Line has more than 100 characters
 src/algebra/ordered_group.lean : line 371 : ERR_LIN : Line has more than 100 characters
 src/algebra/ordered_group.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/algebra/ordered_ring.lean : line 8 : ERR_MOD : Module docstring missing, or too late
+src/algebra/ordered_ring.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/algebra/polynomial/big_operators.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/algebra/punit_instances.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/algebra/quandle.lean : line 462 : ERR_LIN : Line has more than 100 characters
@@ -1117,15 +1117,6 @@ src/group_theory/subgroup.lean : line 803 : ERR_LIN : Line has more than 100 cha
 src/group_theory/subgroup.lean : line 838 : ERR_LIN : Line has more than 100 characters
 src/group_theory/submonoid/operations.lean : line 560 : ERR_LIN : Line has more than 100 characters
 src/group_theory/sylow.lean : line 13 : ERR_MOD : Module docstring missing, or too late
-src/linear_algebra/basic.lean : line 1520 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/basic.lean : line 1552 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/basic.lean : line 1928 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/basic.lean : line 2038 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/basic.lean : line 2044 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/basic.lean : line 2045 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/basic.lean : line 2052 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/basic.lean : line 2110 : ERR_LIN : Line has more than 100 characters
-src/linear_algebra/basic.lean : line 2178 : ERR_LIN : Line has more than 100 characters
 src/linear_algebra/basis.lean : line 93 : ERR_LIN : Line has more than 100 characters
 src/linear_algebra/char_poly/coeff.lean : line 190 : ERR_LIN : Line has more than 100 characters
 src/linear_algebra/char_poly/coeff.lean : line 24 : ERR_LIN : Line has more than 100 characters
@@ -1164,10 +1155,11 @@ src/logic/function/basic.lean : line 324 : ERR_LIN : Line has more than 100 char
 src/logic/function/basic.lean : line 498 : ERR_LIN : Line has more than 100 characters
 src/logic/function/basic.lean : line 538 : ERR_LIN : Line has more than 100 characters
 src/logic/relation.lean : line 10 : ERR_MOD : Module docstring missing, or too late
+src/logic/relator.lean : line 12 : ERR_RNT : Reserved notation outside tactic.core
 src/logic/relator.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/measure_theory/category/Meas.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/measure_theory/decomposition.lean : line 14 : ERR_MOD : Module docstring missing, or too late
-src/measure_theory/measure_space.lean : line 1721 : ERR_LIN : Line has more than 100 characters
+src/measure_theory/measure_space.lean : line 1720 : ERR_LIN : Line has more than 100 characters
 src/measure_theory/measure_space.lean : line 65 : ERR_LIN : Line has more than 100 characters
 src/meta/coinductive_predicates.lean : line 115 : ERR_LIN : Line has more than 100 characters
 src/meta/coinductive_predicates.lean : line 12 : ERR_LIN : Line has more than 100 characters
@@ -1180,6 +1172,15 @@ src/meta/coinductive_predicates.lean : line 488 : ERR_LIN : Line has more than 1
 src/meta/coinductive_predicates.lean : line 76 : ERR_LIN : Line has more than 100 characters
 src/meta/coinductive_predicates.lean : line 77 : ERR_LIN : Line has more than 100 characters
 src/meta/coinductive_predicates.lean : line 8 : ERR_MOD : Module docstring missing, or too late
+src/meta/expr.lean : line 165 : ERR_SAV : File contains the character ᾰ
+src/meta/expr.lean : line 168 : ERR_SAV : File contains the character ᾰ
+src/meta/expr.lean : line 171 : ERR_SAV : File contains the character ᾰ
+src/meta/expr.lean : line 179 : ERR_SAV : File contains the character ᾰ
+src/meta/expr.lean : line 185 : ERR_SAV : File contains the character ᾰ
+src/meta/expr.lean : line 191 : ERR_SAV : File contains the character ᾰ
+src/meta/expr.lean : line 195 : ERR_SAV : File contains the character ᾰ
+src/meta/expr.lean : line 197 : ERR_SAV : File contains the character ᾰ
+src/meta/expr.lean : line 204 : ERR_SAV : File contains the character ᾰ
 src/meta/expr.lean : line 460 : ERR_LIN : Line has more than 100 characters
 src/meta/expr.lean : line 715 : ERR_LIN : Line has more than 100 characters
 src/meta/expr.lean : line 750 : ERR_LIN : Line has more than 100 characters
@@ -1261,7 +1262,7 @@ src/order/filter/basic.lean : line 1497 : ERR_LIN : Line has more than 100 chara
 src/order/filter/basic.lean : line 1783 : ERR_LIN : Line has more than 100 characters
 src/order/filter/basic.lean : line 1935 : ERR_LIN : Line has more than 100 characters
 src/order/filter/basic.lean : line 2063 : ERR_LIN : Line has more than 100 characters
-src/order/filter/basic.lean : line 2303 : ERR_LIN : Line has more than 100 characters
+src/order/filter/basic.lean : line 2308 : ERR_LIN : Line has more than 100 characters
 src/order/filter/basic.lean : line 669 : ERR_LIN : Line has more than 100 characters
 src/order/filter/basic.lean : line 679 : ERR_LIN : Line has more than 100 characters
 src/order/filter/extr.lean : line 301 : ERR_LIN : Line has more than 100 characters
@@ -1289,7 +1290,6 @@ src/order/galois_connection.lean : line 514 : ERR_LIN : Line has more than 100 c
 src/order/galois_connection.lean : line 524 : ERR_LIN : Line has more than 100 characters
 src/order/galois_connection.lean : line 534 : ERR_LIN : Line has more than 100 characters
 src/order/lattice.lean : line 10 : ERR_MOD : Module docstring missing, or too late
-src/order/lattice.lean : line 370 : ERR_LIN : Line has more than 100 characters
 src/order/lexicographic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/order/lexicographic.lean : line 169 : ERR_LIN : Line has more than 100 characters
 src/order/lexicographic.lean : line 172 : ERR_LIN : Line has more than 100 characters
@@ -1540,7 +1540,6 @@ src/tactic/interval_cases.lean : line 241 : ERR_LIN : Line has more than 100 cha
 src/tactic/interval_cases.lean : line 32 : ERR_MOD : Module docstring missing, or too late
 src/tactic/lean_core_docs.lean : line 733 : ERR_LIN : Line has more than 100 characters
 src/tactic/lean_core_docs.lean : line 766 : ERR_LIN : Line has more than 100 characters
-src/tactic/lift.lean : line 176 : ERR_LIN : Line has more than 100 characters
 src/tactic/lift.lean : line 78 : ERR_LIN : Line has more than 100 characters
 src/tactic/linarith/datatypes.lean : line 118 : ERR_LIN : Line has more than 100 characters
 src/tactic/linarith/datatypes.lean : line 233 : ERR_LIN : Line has more than 100 characters
@@ -1574,10 +1573,7 @@ src/tactic/lint/default.lean : line 42 : ERR_LIN : Line has more than 100 charac
 src/tactic/lint/default.lean : line 44 : ERR_LIN : Line has more than 100 characters
 src/tactic/lint/default.lean : line 45 : ERR_LIN : Line has more than 100 characters
 src/tactic/lint/default.lean : line 46 : ERR_LIN : Line has more than 100 characters
-src/tactic/lint/frontend.lean : line 157 : ERR_LIN : Line has more than 100 characters
-src/tactic/lint/frontend.lean : line 228 : ERR_LIN : Line has more than 100 characters
-src/tactic/lint/frontend.lean : line 232 : ERR_LIN : Line has more than 100 characters
-src/tactic/lint/frontend.lean : line 79 : ERR_LIN : Line has more than 100 characters
+src/tactic/lint/frontend.lean : line 153 : ERR_LIN : Line has more than 100 characters
 src/tactic/lint/misc.lean : line 78 : ERR_LIN : Line has more than 100 characters
 src/tactic/lint/simp.lean : line 116 : ERR_LIN : Line has more than 100 characters
 src/tactic/lint/simp.lean : line 122 : ERR_LIN : Line has more than 100 characters
@@ -1632,7 +1628,6 @@ src/tactic/push_neg.lean : line 180 : ERR_LIN : Line has more than 100 character
 src/tactic/push_neg.lean : line 181 : ERR_LIN : Line has more than 100 characters
 src/tactic/push_neg.lean : line 183 : ERR_LIN : Line has more than 100 characters
 src/tactic/push_neg.lean : line 184 : ERR_LIN : Line has more than 100 characters
-src/tactic/rcases.lean : line 741 : ERR_LIN : Line has more than 100 characters
 src/tactic/restate_axiom.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/rewrite.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/rewrite_all/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
@@ -1646,9 +1641,8 @@ src/tactic/simp_result.lean : line 94 : ERR_LIN : Line has more than 100 charact
 src/tactic/simp_rw.lean : line 44 : ERR_LIN : Line has more than 100 characters
 src/tactic/simpa.lean : line 38 : ERR_LIN : Line has more than 100 characters
 src/tactic/simpa.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/tactic/simps.lean : line 401 : ERR_LIN : Line has more than 100 characters
-src/tactic/simps.lean : line 432 : ERR_LIN : Line has more than 100 characters
-src/tactic/simps.lean : line 440 : ERR_LIN : Line has more than 100 characters
+src/tactic/simps.lean : line 400 : ERR_LIN : Line has more than 100 characters
+src/tactic/simps.lean : line 431 : ERR_LIN : Line has more than 100 characters
 src/tactic/slice.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/slim_check.lean : line 186 : ERR_LIN : Line has more than 100 characters
 src/tactic/slim_check.lean : line 188 : ERR_LIN : Line has more than 100 characters
@@ -1691,10 +1685,6 @@ src/tactic/transform_decl.lean : line 43 : ERR_LIN : Line has more than 100 char
 src/tactic/transform_decl.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/transport.lean : line 44 : ERR_LIN : Line has more than 100 characters
 src/tactic/trunc_cases.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-src/tactic/where.lean : line 40 : ERR_LIN : Line has more than 100 characters
-src/tactic/where.lean : line 47 : ERR_LIN : Line has more than 100 characters
-src/tactic/where.lean : line 54 : ERR_LIN : Line has more than 100 characters
-src/tactic/where.lean : line 58 : ERR_LIN : Line has more than 100 characters
 src/tactic/wlog.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/tactic/wlog.lean : line 181 : ERR_LIN : Line has more than 100 characters
 src/tactic/wlog.lean : line 198 : ERR_LIN : Line has more than 100 characters
@@ -1762,9 +1752,9 @@ src/topology/algebra/continuous_functions.lean : line 87 : ERR_LIN : Line has mo
 src/topology/algebra/floor_ring.lean : line 12 : ERR_MOD : Module docstring missing, or too late
 src/topology/algebra/floor_ring.lean : line 183 : ERR_LIN : Line has more than 100 characters
 src/topology/algebra/floor_ring.lean : line 187 : ERR_LIN : Line has more than 100 characters
-src/topology/algebra/group.lean : line 440 : ERR_LIN : Line has more than 100 characters
-src/topology/algebra/group.lean : line 450 : ERR_LIN : Line has more than 100 characters
-src/topology/algebra/group.lean : line 469 : ERR_LIN : Line has more than 100 characters
+src/topology/algebra/group.lean : line 516 : ERR_LIN : Line has more than 100 characters
+src/topology/algebra/group.lean : line 526 : ERR_LIN : Line has more than 100 characters
+src/topology/algebra/group.lean : line 545 : ERR_LIN : Line has more than 100 characters
 src/topology/algebra/group_completion.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/topology/algebra/group_completion.lean : line 53 : ERR_LIN : Line has more than 100 characters
 src/topology/algebra/group_completion.lean : line 55 : ERR_LIN : Line has more than 100 characters
diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean
index 788d195a997fa..48411d454ae1e 100644
--- a/src/linear_algebra/basic.lean
+++ b/src/linear_algebra/basic.lean
@@ -57,8 +57,6 @@ linear algebra, vector space, module
 open function
 open_locale big_operators
 
-reserve infix ` ≃ₗ `:25
-
 universes u v w x y z u' v' w' y'
 variables {R : Type u} {K : Type u'} {M : Type v} {V : Type v'} {M₂ : Type w} {V₂ : Type w'}
 variables {M₃ : Type y} {V₃ : Type y'} {M₄ : Type z} {ι : Type x}
@@ -1517,8 +1515,8 @@ end field
 
 end linear_map
 
-lemma submodule.sup_eq_range [semiring R] [add_comm_monoid M] [semimodule R M] (p q : submodule R M) :
-  p ⊔ q = (p.subtype.coprod q.subtype).range :=
+lemma submodule.sup_eq_range [semiring R] [add_comm_monoid M] [semimodule R M]
+  (p q : submodule R M) : p ⊔ q = (p.subtype.coprod q.subtype).range :=
 submodule.ext $ λ x, by simp [submodule.mem_sup, submodule.exists]
 
 namespace is_linear_map
@@ -1549,7 +1547,8 @@ namespace submodule
 
 section add_comm_monoid
 
-variables {T : semiring R} [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂]
+variables {T : semiring R} [add_comm_monoid M] [add_comm_monoid M₂]
+variables [semimodule R M] [semimodule R M₂]
 variables (p p' : submodule R M) (q : submodule R M₂)
 include T
 open linear_map
@@ -1925,7 +1924,8 @@ end add_comm_monoid
 
 section add_comm_group
 
-variables [semiring R] [add_comm_group M] [add_comm_group M₂] [add_comm_group M₃] [add_comm_group M₄]
+variables [semiring R]
+variables [add_comm_group M] [add_comm_group M₂] [add_comm_group M₃] [add_comm_group M₄]
 variables {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂}
 variables {semimodule_M₃ : semimodule R M₃} {semimodule_M₄ : semimodule R M₄}
 variables (e e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄)
@@ -2035,21 +2035,24 @@ rfl
 rfl
 
 lemma arrow_congr_comp {N N₂ N₃ : Sort*}
-  [add_comm_group N] [add_comm_group N₂] [add_comm_group N₃] [module R N] [module R N₂] [module R N₃]
+  [add_comm_group N] [add_comm_group N₂] [add_comm_group N₃]
+  [module R N] [module R N₂] [module R N₃]
   (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃) (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
   arrow_congr e₁ e₃ (g.comp f) = (arrow_congr e₂ e₃ g).comp (arrow_congr e₁ e₂ f) :=
 by { ext, simp only [symm_apply_apply, arrow_congr_apply, linear_map.comp_apply], }
 
 lemma arrow_congr_trans {M₁ M₂ M₃ N₁ N₂ N₃ : Sort*}
-  [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] [add_comm_group M₃] [module R M₃]
-  [add_comm_group N₁] [module R N₁] [add_comm_group N₂] [module R N₂] [add_comm_group N₃] [module R N₃]
+  [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂]
+  [add_comm_group M₃] [module R M₃] [add_comm_group N₁] [module R N₁]
+  [add_comm_group N₂] [module R N₂] [add_comm_group N₃] [module R N₃]
   (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) :
   (arrow_congr e₁ e₂).trans (arrow_congr e₃ e₄) = arrow_congr (e₁.trans e₃) (e₂.trans e₄) :=
 rfl
 
 /-- If `M₂` and `M₃` are linearly isomorphic then the two spaces of linear maps from `M` into `M₂`
 and `M` into `M₃` are linearly isomorphic. -/
-def congr_right (f : M₂ ≃ₗ[R] M₃) : (M →ₗ[R] M₂) ≃ₗ (M →ₗ M₃) := arrow_congr (linear_equiv.refl R M) f
+def congr_right (f : M₂ ≃ₗ[R] M₃) : (M →ₗ[R] M₂) ≃ₗ (M →ₗ M₃) :=
+arrow_congr (linear_equiv.refl R M) f
 
 /-- If `M` and `M₂` are linearly isomorphic then the two spaces of linear maps from `M` and `M₂` to
 themselves are linearly isomorphic. -/
@@ -2107,7 +2110,8 @@ end
 def to_span_nonzero_singleton (x : M) (h : x ≠ 0) : K ≃ₗ[K] (submodule.span K ({x} : set M)) :=
 linear_equiv.trans
   (linear_equiv.of_injective (to_span_singleton K M x) (ker_to_span_singleton K M h))
-  (of_eq (to_span_singleton K M x).range (submodule.span K {x}) (span_singleton_eq_range K M x).symm)
+  (of_eq (to_span_singleton K M x).range (submodule.span K {x})
+    (span_singleton_eq_range K M x).symm)
 
 lemma to_span_nonzero_singleton_one (x : M) (h : x ≠ 0) : to_span_nonzero_singleton K M x h 1
   = (⟨x, submodule.mem_span_singleton_self x⟩ : submodule.span K ({x} : set M)) :=
@@ -2175,7 +2179,8 @@ variables (q : submodule R M)
 /-- Quotienting by equal submodules gives linearly equivalent quotients. -/
 def quot_equiv_of_eq (h : p = q) : p.quotient ≃ₗ[R] q.quotient :=
 { map_add' := by { rintros ⟨x⟩ ⟨y⟩, refl }, map_smul' := by { rintros x ⟨y⟩, refl },
-  ..@quotient.congr _ _ (quotient_rel p) (quotient_rel q) (equiv.refl _) $ λ a b, by { subst h, refl } }
+  ..@quotient.congr _ _ (quotient_rel p) (quotient_rel q) (equiv.refl _) $
+    λ a b, by { subst h, refl } }
 
 end submodule
 
diff --git a/src/order/lattice.lean b/src/order/lattice.lean
index 58b8376125ac6..63123b9b6386e 100644
--- a/src/order/lattice.lean
+++ b/src/order/lattice.lean
@@ -23,8 +23,6 @@ section
 end
 
 /- TODO: automatic construction of dual definitions / theorems -/
-reserve infixl ` ⊓ `:70
-reserve infixl ` ⊔ `:65
 
 /-- Typeclass for the `⊔` (`\lub`) notation -/
 class has_sup (α : Type u) := (sup : α → α → α)
@@ -367,7 +365,8 @@ by simp only [sup_inf_left, λy:α, @sup_comm α _ y x, eq_self_iff_true]
 
 theorem inf_sup_left : x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z) :=
 calc x ⊓ (y ⊔ z) = (x ⊓ (x ⊔ z)) ⊓ (y ⊔ z)       : by rw [inf_sup_self]
-             ... = x ⊓ ((x ⊓ y) ⊔ z)             : by simp only [inf_assoc, sup_inf_right, eq_self_iff_true]
+             ... = x ⊓ ((x ⊓ y) ⊔ z)             : by simp only [inf_assoc, sup_inf_right,
+                                                                 eq_self_iff_true]
              ... = (x ⊔ (x ⊓ y)) ⊓ ((x ⊓ y) ⊔ z) : by rw [sup_inf_self]
              ... = ((x ⊓ y) ⊔ x) ⊓ ((x ⊓ y) ⊔ z) : by rw [sup_comm]
              ... = (x ⊓ y) ⊔ (x ⊓ z)             : by rw [sup_inf_left]
diff --git a/src/tactic/core.lean b/src/tactic/core.lean
index 1f64026968997..78259a91bba27 100644
--- a/src/tactic/core.lean
+++ b/src/tactic/core.lean
@@ -2306,3 +2306,39 @@ Otherwise, it fails.
 meta def list.find_defeq (red : tactic.transparency) {v} (m : list (expr × v)) (e : expr) :
   tactic (expr × v) :=
 m.mfind $ λ ⟨e', val⟩, tactic.is_def_eq e e' red
+
+/-!
+### Reserved notation
+
+We place all `mathlib`'s reserved notation here so that users will know not to
+use them as e.g. variable names without needing to import the specific file where they
+are defined.
+-/
+
+-- used in `tactic/localized.lean`
+reserve notation `localized`
+
+-- used in `tactic/lint/frontend.lean`
+reserve notation `#lint`
+reserve notation `#lint_mathlib`
+reserve notation `#lint_all`
+reserve notation `#list_linters`
+
+-- used in `tactic/where.lean`
+reserve prefix `#where`:max
+
+-- used in `tactic/simps.lean`
+reserve notation `initialize_simps_projections`
+
+-- used in `tactic/lift.lean`
+reserve notation `to`
+
+-- used in `tactic/rcases.lean`
+precedence `?`:max
+
+-- used in `order/lattice.lean`
+reserve infixl ` ⊓ `:70
+reserve infixl ` ⊔ `:65
+
+-- used in `linear_algebra/basic.lean`
+reserve infix ` ≃ₗ `:25
diff --git a/src/tactic/lift.lean b/src/tactic/lift.lean
index c6d761db90021..8b5e0f46bd5b9 100644
--- a/src/tactic/lift.lean
+++ b/src/tactic/lift.lean
@@ -7,7 +7,7 @@ import tactic.rcases
 /-!
 # lift tactic
 
-This file defines the lift tactic, allowing the user to lift elements from one type to another
+This file defines the `lift` tactic, allowing the user to lift elements from one type to another
 under a specified condition.
 
 ## Tags
@@ -121,7 +121,8 @@ do
   dsimp_hyp temp_e s to_unfold {},
   /- We case on the existential. We use `rcases` because `eq_nm` could be `rfl`. -/
   rcases none (pexpr.of_expr temp_e) $ rcases_patt.tuple ([new_nm, eq_nm].map rcases_patt.one),
-  /- If the lifted variable is not a local constant, try to rewrite it away using the new equality-/
+  /- If the lifted variable is not a local constant,
+    try to rewrite it away using the new equality. -/
   when (¬ e.is_local_constant) (get_local eq_nm >>=
     λ e, interactive.rw ⟨[⟨⟨0, 0⟩, tt, (pexpr.of_expr e)⟩], none⟩ interactive.loc.wildcard),
   /- If the proof `prf_cond` is a local constant, remove it from the context,
@@ -131,8 +132,6 @@ do
 
 open lean.parser interactive interactive.types
 
-reserve notation `to`
-
 local postfix `?`:9001 := optional
 /-- Parses an optional token "using" followed by a trailing `pexpr`. -/
 meta def using_texpr := (tk "using" *> texpr)?
@@ -142,8 +141,7 @@ meta def to_texpr := (tk "to" *> texpr)
 
 namespace interactive
 
-/-- Lift an expression to another type.
-
+/--
 Lift an expression to another type.
 * Usage: `'lift' expr 'to' expr ('using' expr)? ('with' id (id id?)?)?`.
 * If `n : ℤ` and `hn : n ≥ 0` then the tactic `lift n to ℕ using hn` creates a new
@@ -173,8 +171,8 @@ Lift an expression to another type.
 * More generally, this can lift an expression from `α` to `β` assuming that there is an instance
   of `can_lift α β`. In this case the proof obligation is specified by `can_lift.cond`.
 * Given an instance `can_lift β γ`, it can also lift `α → β` to `α → γ`; more generally, given
-  `β : Π a : α, Type*`, `γ : Π a : α, Type*`, and `[Π a : α, can_lift (β a) (γ a)]`, it automatically
-  generates an instance `can_lift (Π a, β a) (Π a, γ a)`.
+  `β : Π a : α, Type*`, `γ : Π a : α, Type*`, and `[Π a : α, can_lift (β a) (γ a)]`, it
+  automatically generates an instance `can_lift (Π a, β a) (Π a, γ a)`.
 
 `lift` is in some sense dual to the `zify` tactic. `lift (z : ℤ) to ℕ` will change the type of an
 integer `z` (in the supertype) to `ℕ` (the subtype), given a proof that `z ≥ 0`;
diff --git a/src/tactic/lint/frontend.lean b/src/tactic/lint/frontend.lean
index a8f362d1bbcb8..800d8c6d7d900 100644
--- a/src/tactic/lint/frontend.lean
+++ b/src/tactic/lint/frontend.lean
@@ -47,11 +47,6 @@ omits it from only the specified linter checks.
 sanity check, lint, cleanup, command, tactic
 -/
 
-reserve notation `#lint`
-reserve notation `#lint_mathlib`
-reserve notation `#lint_all`
-reserve notation `#list_linters`
-
 open tactic expr native
 setup_tactic_parser
 
@@ -76,7 +71,8 @@ meta def get_checks (slow : bool) (extra : list name) (use_only : bool) :
   list.append default <$> get_linters extra
 
 /--
-`lint_core all_decls non_auto_decls checks` applies the linters `checks` to the list of declarations.
+`lint_core all_decls non_auto_decls checks` applies the linters `checks` to the list of
+declarations.
 If `auto_decls` is false for a linter (default) the linter is applied to `non_auto_decls`.
 If `auto_decls` is true, then it is applied to `all_decls`.
 The resulting list has one element for each linter, containing the linter as
@@ -225,11 +221,13 @@ tk "+" >> return lint_verbosity.high <|>
 return none
 
 /-- The common denominator of `lint_cmd`, `lint_mathlib_cmd`, `lint_all_cmd` -/
-private meta def lint_cmd_aux (scope : bool → lint_verbosity → list name → bool → tactic (name_set × format)) :
+private meta def lint_cmd_aux
+  (scope : bool → lint_verbosity → list name → bool → tactic (name_set × format)) :
   parser unit :=
 do verbosity ← parse_verbosity,
    fast_only ← optional (tk "*"),
-   verbosity ← if verbosity.is_some then return verbosity else parse_verbosity, -- allow either order of *-
+   -- allow either order of *-
+   verbosity ← if verbosity.is_some then return verbosity else parse_verbosity,
    let verbosity := verbosity.get_or_else lint_verbosity.medium,
    (use_only, extra) ← parse_lint_additions,
    (failed, s) ← scope fast_only.is_none verbosity extra use_only,
diff --git a/src/tactic/localized.lean b/src/tactic/localized.lean
index 8284d793c60a8..3a88cfbbcec7b 100644
--- a/src/tactic/localized.lean
+++ b/src/tactic/localized.lean
@@ -36,8 +36,6 @@ The code is inspired by code from Gabriel Ebner from the
 
 open lean lean.parser interactive tactic native
 
-reserve notation `localized`
-
 @[user_attribute]
 meta def localized_attr : user_attribute (rb_lmap name string) unit := {
   name := "_localized",
diff --git a/src/tactic/rcases.lean b/src/tactic/rcases.lean
index fbf736b3b56f0..51569d6c39293 100644
--- a/src/tactic/rcases.lean
+++ b/src/tactic/rcases.lean
@@ -614,8 +614,6 @@ with rcases_patt_parse_list_rest : rcases_patt → parser (listΣ rcases_patt)
 meta def rcases_parse_depth : parser nat :=
 do o ← (tk ":" *> small_nat)?, pure $ o.get_or_else 5
 
-precedence `?`:max
-
 /-- The arguments to `rcases`, which in fact dispatch to several other tactics.
 * `rcases? expr (: n)?` or `rcases? ⟨expr, ...⟩ (: n)?` calls `rcases_hint`
 * `rcases? ⟨expr, ...⟩ (: n)?` calls `rcases_hint_many`
@@ -738,8 +736,8 @@ parameter as necessary.
 `rcases` also has special support for quotient types: quotient induction into Prop works like
 matching on the constructor `quot.mk`.
 
-`rcases h : e with PAT` will do the same as `rcases e with PAT` with the exception that an assumption
-`h : e = PAT` will be added to the context.
+`rcases h : e with PAT` will do the same as `rcases e with PAT` with the exception that an
+assumption `h : e = PAT` will be added to the context.
 
 `rcases? e` will perform case splits on `e` in the same way as `rcases e`,
 but rather than accepting a pattern, it does a maximal cases and prints the
diff --git a/src/tactic/simps.lean b/src/tactic/simps.lean
index f5f23513670a0..7332d92a93d8d 100644
--- a/src/tactic/simps.lean
+++ b/src/tactic/simps.lean
@@ -34,7 +34,6 @@ structures, projections, simp, simplifier, generates declarations
 open tactic expr
 
 setup_tactic_parser
-reserve notation `initialize_simps_projections`
 declare_trace simps.verbose
 
 /--
@@ -437,7 +436,9 @@ Projection {(todo_next.head.split_on '_').tail.head} doesn't exist, because targ
 /-- `simps_tac` derives simp-lemmas for all (nested) non-Prop projections of the declaration.
   If `todo` is non-empty, it will generate exactly the names in `todo`.
   If `short_nm` is true, the generated names will only use the last projection name. -/
-meta def simps_tac (nm : name) (cfg : simps_cfg := {}) (todo : list string := []) : tactic unit := do
+meta def simps_tac (nm : name) (cfg : simps_cfg := {}) (todo : list string := []) :
+  tactic unit :=
+do
   e ← get_env,
   d ← e.get nm,
   let lhs : expr := const d.to_name (d.univ_params.map level.param),
diff --git a/src/tactic/where.lean b/src/tactic/where.lean
index 4cacb318add10..dd16cecaf6f7c 100644
--- a/src/tactic/where.lean
+++ b/src/tactic/where.lean
@@ -37,25 +37,29 @@ meta def binder_less_important (u v : binder_info) : bool :=
 /-- Selects the elements of the given `list α` which under the image of `p : α → β × γ` have `β`
 component equal to `b'`. Returns the `γ` components of the selected elements under the image of `p`,
 and the elements of the original `list α` which were not selected. -/
-def select_for_which {α β γ : Type} (p : α → β × γ) [decidable_eq β] (b' : β) : list α → list γ × list α
+def select_for_which {α β γ : Type} (p : α → β × γ) [decidable_eq β] (b' : β) :
+  list α → list γ × list α
 | [] := ([], [])
 | (a :: rest) :=
   let (cs, others) := select_for_which rest, (b, c) := p a in
   if b = b' then (c :: cs, others) else (cs, a :: others)
 
 /-- Helper function for `collect_by`. -/
-private meta def collect_by_aux {α β γ : Type} (p : α → β × γ) [decidable_eq β] : list β → list α → list (β × list γ)
+private meta def collect_by_aux {α β γ : Type} (p : α → β × γ) [decidable_eq β] :
+  list β → list α → list (β × list γ)
 | [] [] := []
 | [] _ := undefined_core "didn't find every key entry!"
 | (b :: rest) as := let (cs, as) := select_for_which p b as in (b, cs) :: collect_by_aux rest as
 
 /-- Returns the elements of `l` under the image of `p`, collecting together elements with the same
 `β` component, deleting duplicates. -/
-meta def collect_by {α β γ : Type} (l : list α) (p : α → β × γ) [decidable_eq β] : list (β × list γ) :=
+meta def collect_by {α β γ : Type} (l : list α) (p : α → β × γ) [decidable_eq β] :
+  list (β × list γ) :=
 collect_by_aux p (l.map $ prod.fst ∘ p).erase_dup l
 
 /-- Sort the variables by their priority as defined by `where.binder_priority`. -/
-meta def sort_variable_list (l : list (name × binder_info × expr)) : list (expr × binder_info × list name) :=
+meta def sort_variable_list (l : list (name × binder_info × expr)) :
+  list (expr × binder_info × list name) :=
 let l := collect_by l $ λ v, (v.2.2, (v.1, v.2.1)) in
 let l := l.map $ λ el, (el.1, collect_by el.2 $ λ v, (v.2, v.1)) in
 (list.join $ l.map $ λ e, prod.mk e.1 <$> e.2).qsort (λ v u, binder_less_important v.2.1 u.2.1)
@@ -151,8 +155,6 @@ do let msg := "",
 
 open interactive
 
-reserve prefix `#where`:max
-
 /--
 When working in a Lean file with namespaces, parameters, and variables, it can be confusing to
 identify what the current "parser context" is. The command `#where` identifies and prints

From 5799cbcad5fc2a30535856c0bf0f6f2571f35232 Mon Sep 17 00:00:00 2001
From: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Date: Sat, 12 Dec 2020 03:46:27 -0500
Subject: [PATCH 4/9] fix?

---
 src/algebra/module/linear_map.lean | 2 +-
 src/tactic/core.lean               | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/algebra/module/linear_map.lean b/src/algebra/module/linear_map.lean
index 67929a2485c6e..c86442aed5b08 100644
--- a/src/algebra/module/linear_map.lean
+++ b/src/algebra/module/linear_map.lean
@@ -303,7 +303,7 @@ end
 attribute [nolint doc_blame] linear_equiv.to_linear_map
 attribute [nolint doc_blame] linear_equiv.to_add_equiv
 
-infix ` ≃ₗ `:25 := linear_equiv _
+infix ` ≃ₗ ` := linear_equiv _
 notation M ` ≃ₗ[`:50 R `] ` M₂ := linear_equiv R M M₂
 
 namespace linear_equiv
diff --git a/src/tactic/core.lean b/src/tactic/core.lean
index 78259a91bba27..5db61db4dc546 100644
--- a/src/tactic/core.lean
+++ b/src/tactic/core.lean
@@ -2340,5 +2340,5 @@ precedence `?`:max
 reserve infixl ` ⊓ `:70
 reserve infixl ` ⊔ `:65
 
--- used in `linear_algebra/basic.lean`
+-- used in `algebra/module/linear_map.lean`
 reserve infix ` ≃ₗ `:25

From d73dda66a6db11a81eb32ae21aca176e100bebe9 Mon Sep 17 00:00:00 2001
From: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Date: Sat, 12 Dec 2020 17:25:36 -0500
Subject: [PATCH 5/9] add set_option_check, factor out skip_comment and add
 skip_string functions

---
 scripts/copy-mod-doc-exceptions.txt |  9 ----
 scripts/lint-copy-mod-doc.py        | 77 ++++++++++++++++++++++-------
 2 files changed, 60 insertions(+), 26 deletions(-)

diff --git a/scripts/copy-mod-doc-exceptions.txt b/scripts/copy-mod-doc-exceptions.txt
index 90ca178ee97e4..283b13d9a1af5 100644
--- a/scripts/copy-mod-doc-exceptions.txt
+++ b/scripts/copy-mod-doc-exceptions.txt
@@ -1172,15 +1172,6 @@ src/meta/coinductive_predicates.lean : line 488 : ERR_LIN : Line has more than 1
 src/meta/coinductive_predicates.lean : line 76 : ERR_LIN : Line has more than 100 characters
 src/meta/coinductive_predicates.lean : line 77 : ERR_LIN : Line has more than 100 characters
 src/meta/coinductive_predicates.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/meta/expr.lean : line 165 : ERR_SAV : File contains the character ᾰ
-src/meta/expr.lean : line 168 : ERR_SAV : File contains the character ᾰ
-src/meta/expr.lean : line 171 : ERR_SAV : File contains the character ᾰ
-src/meta/expr.lean : line 179 : ERR_SAV : File contains the character ᾰ
-src/meta/expr.lean : line 185 : ERR_SAV : File contains the character ᾰ
-src/meta/expr.lean : line 191 : ERR_SAV : File contains the character ᾰ
-src/meta/expr.lean : line 195 : ERR_SAV : File contains the character ᾰ
-src/meta/expr.lean : line 197 : ERR_SAV : File contains the character ᾰ
-src/meta/expr.lean : line 204 : ERR_SAV : File contains the character ᾰ
 src/meta/expr.lean : line 460 : ERR_LIN : Line has more than 100 characters
 src/meta/expr.lean : line 715 : ERR_LIN : Line has more than 100 characters
 src/meta/expr.lean : line 750 : ERR_LIN : Line has more than 100 characters
diff --git a/scripts/lint-copy-mod-doc.py b/scripts/lint-copy-mod-doc.py
index a132af24b87f5..c17b6d0b14b46 100755
--- a/scripts/lint-copy-mod-doc.py
+++ b/scripts/lint-copy-mod-doc.py
@@ -10,6 +10,7 @@
 ERR_LIN = 3 # line length
 ERR_SAV = 4 # ᾰ
 ERR_RNT = 5 # reserved notation
+ERR_OPT = 6 # set_option
 
 exceptions = []
 
@@ -28,18 +29,14 @@
             exceptions += [(ERR_SAV, fn)]
         if errno == "ERR_RNT":
             exceptions += [(ERR_RNT, fn)]
+        if errno == "ERR_OPT":
+            exceptions += [(ERR_OPT, fn)]
 
 new_exceptions = False
 
-def small_alpha_vrachy_check(lines, fn):
-    return [ (ERR_SAV, line_nr, fn) for line_nr, line in enumerate(lines, 1) if 'ᾰ' in line ]
-
-def reserved_notation_check(lines, fn):
-    if fn == 'src/tactic/core.lean':
-        return []
-    errors = []
+def skip_comments(enumerate_lines):
     in_comment = False
-    for line_nr, line in enumerate(lines, 1):
+    for line_nr, line in enumerate_lines:
         if "/-" in line:
             in_comment = True
         if "-/" in line:
@@ -47,12 +44,62 @@ def reserved_notation_check(lines, fn):
             continue
         if line == "\n" or in_comment:
             continue
+        yield line_nr, line
+
+def skip_string(enumerate_lines):
+    in_string = False
+    in_comment = False
+    for line_nr, line in enumerate_lines:
+        # ignore comment markers inside string literals
+        if not in_string:
+            if "/-" in line:
+                in_comment = True
+            if "-/" in line:
+                in_comment = False
+        # ignore quotes inside comments
+        if not in_comment:
+            # crude heuristic: if the number of non-escaped quote signs is odd,
+            # we're starting / ending a string literal
+            if line.count("\"") - line.count("\\\"") % 2 == 1:
+                in_string = not in_string
+            # if there are quote signs in this line,
+            # a string literal probably begins and / or ends here,
+            # so we skip this line
+            if line.count("\"") > 0:
+                continue
+            if in_string:
+                continue
+        yield line_nr, line
+
+def small_alpha_vrachy_check(lines, fn):
+    errors = []
+    for line_nr, line in skip_string(skip_comments(enumerate(lines, 1))):
+        if 'ᾰ' in line:
+            errors += [(ERR_SAV, line_nr, fn)]
+    return errors
+
+def reserved_notation_check(lines, fn):
+    if fn == 'src/tactic/core.lean':
+        return []
+    errors = []
+    for line_nr, line in skip_string(skip_comments(enumerate(lines, 1))):
         if line.startswith('reserve') or line.startswith('precedence'):
             errors += [(ERR_RNT, line_nr, fn)]
     return errors
 
+def set_option_check(lines, fn):
+    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]
+            # 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, fn)]
+    return errors
+
 def long_lines_check(lines, fn):
     errors = []
+    # TODO: some string literals (in e.g. tactic output messages) can be excepted from this rule
     for line_nr, line in enumerate(lines, 1):
         if "http" in line:
             continue
@@ -63,15 +110,7 @@ def long_lines_check(lines, fn):
 def import_only_check(lines, fn):
     import_only_file = True
     errors = []
-    in_comment = False
-    for line_nr, line in enumerate(lines, 1):
-        if "/-" in line:
-            in_comment = True
-        if "-/" in line:
-            in_comment = False
-            continue
-        if line == "\n" or in_comment:
-            continue
+    for line_nr, line in skip_comments(enumerate(lines, 1)):
         imports = line.split()
         if imports[0] == "--":
             continue
@@ -143,6 +182,8 @@ def format_errors(errors):
             print("{} : line {} : ERR_SAV : File contains the character ᾰ".format(fn, line_nr))
         if errno == ERR_RNT:
             print("{} : line {} : ERR_RNT : Reserved notation outside tactic.core".format(fn, line_nr))
+        if errno == ERR_OPT:
+            print("{} : line {} : ERR_OPT : Forbidden set_option command".format(fn, line_nr))
 
 def lint(fn):
     with open(fn) as f:
@@ -159,6 +200,8 @@ def lint(fn):
         format_errors(errs)
         errs = reserved_notation_check(lines, fn)
         format_errors(errs)
+        errs = set_option_check(lines, fn)
+        format_errors(errs)
 
 for fn in fns:
     lint(fn)

From 7b0444785f9e192086bbc6603d56d52b3c876148 Mon Sep 17 00:00:00 2001
From: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Date: Mon, 14 Dec 2020 22:55:14 -0500
Subject: [PATCH 6/9] move notation to tactic/reserved_notation.lean

---
 scripts/lint-copy-mod-doc.py      |  2 +-
 src/logic/basic.lean              | 10 +++++--
 src/logic/relator.lean            |  4 +--
 src/tactic/core.lean              | 36 -----------------------
 src/tactic/reserved_notation.lean | 48 +++++++++++++++++++++++++++++++
 5 files changed, 58 insertions(+), 42 deletions(-)
 create mode 100644 src/tactic/reserved_notation.lean

diff --git a/scripts/lint-copy-mod-doc.py b/scripts/lint-copy-mod-doc.py
index c17b6d0b14b46..312b96313303b 100755
--- a/scripts/lint-copy-mod-doc.py
+++ b/scripts/lint-copy-mod-doc.py
@@ -79,7 +79,7 @@ def small_alpha_vrachy_check(lines, fn):
     return errors
 
 def reserved_notation_check(lines, fn):
-    if fn == 'src/tactic/core.lean':
+    if fn == 'src/tactic/reserved_notation.lean':
         return []
     errors = []
     for line_nr, line in skip_string(skip_comments(enumerate(lines, 1))):
diff --git a/src/logic/basic.lean b/src/logic/basic.lean
index 73ba7bca130d2..7d8a1255931ab 100644
--- a/src/logic/basic.lean
+++ b/src/logic/basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 -/
 import tactic.doc_commands
+import tactic.reserved_notation
 
 /-!
 # Basic logic properties
@@ -498,7 +499,8 @@ by rw [@iff_def a, @iff_def b]; exact and_congr imp_not_comm decidable.not_imp_c
 theorem iff_not_comm : (a ↔ ¬ b) ↔ (b ↔ ¬ a) := decidable.iff_not_comm
 
 -- See Note [decidable namespace]
-protected theorem decidable.iff_iff_and_or_not_and_not [decidable b] : (a ↔ b) ↔ (a ∧ b) ∨ (¬ a ∧ ¬ b) :=
+protected theorem decidable.iff_iff_and_or_not_and_not [decidable b] :
+  (a ↔ b) ↔ (a ∧ b) ∨ (¬ a ∧ ¬ b) :=
 by { split; intro h,
      { rw h; by_cases b; [left,right]; split; assumption },
      { cases h with h h; cases h; split; intro; { contradiction <|> assumption } } }
@@ -575,7 +577,8 @@ by rw [← not_or_distrib, decidable.not_not]
 theorem or_iff_not_and_not : a ∨ b ↔ ¬ (¬a ∧ ¬b) := decidable.or_iff_not_and_not
 
 -- See Note [decidable namespace]
-protected theorem decidable.and_iff_not_or_not [decidable a] [decidable b] : a ∧ b ↔ ¬ (¬ a ∨ ¬ b) :=
+protected theorem decidable.and_iff_not_or_not [decidable a] [decidable b] :
+  a ∧ b ↔ ¬ (¬ a ∨ ¬ b) :=
 by rw [← decidable.not_and_distrib, decidable.not_not]
 
 theorem and_iff_not_or_not : a ∧ b ↔ ¬ (¬ a ∨ ¬ b) := decidable.and_iff_not_or_not
@@ -875,7 +878,8 @@ theorem Exists.snd {p : b → Prop} : ∀ h : Exists p, p h.fst
 @[simp] theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∃ h' : p, q h') ↔ q h :=
 @exists_const (q h) p ⟨h⟩
 
-@[simp] theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬ p) : (∀ h' : p, q h') ↔ true :=
+@[simp] theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬ p) :
+  (∀ h' : p, q h') ↔ true :=
 iff_true_intro $ λ h, hn.elim h
 
 @[simp] theorem exists_prop_of_false {p : Prop} {q : p → Prop} : ¬ p → ¬ (∃ h' : p, q h') :=
diff --git a/src/logic/relator.lean b/src/logic/relator.lean
index 5b4c783126e03..fbb82ef74841f 100644
--- a/src/logic/relator.lean
+++ b/src/logic/relator.lean
@@ -6,11 +6,11 @@ Authors: Johannes Hölzl
 Relator for functions, pairs, sums, and lists.
 -/
 
+import tactic.reserved_notation
+
 namespace relator
 universe variables u₁ u₂ v₁ v₂
 
-reserve infixr ` ⇒ `:40
-
 /- TODO(johoelzl):
  * should we introduce relators of datatypes as recursive function or as inductive
 predicate? For now we stick to the recursor approach.
diff --git a/src/tactic/core.lean b/src/tactic/core.lean
index 5db61db4dc546..1f64026968997 100644
--- a/src/tactic/core.lean
+++ b/src/tactic/core.lean
@@ -2306,39 +2306,3 @@ Otherwise, it fails.
 meta def list.find_defeq (red : tactic.transparency) {v} (m : list (expr × v)) (e : expr) :
   tactic (expr × v) :=
 m.mfind $ λ ⟨e', val⟩, tactic.is_def_eq e e' red
-
-/-!
-### Reserved notation
-
-We place all `mathlib`'s reserved notation here so that users will know not to
-use them as e.g. variable names without needing to import the specific file where they
-are defined.
--/
-
--- used in `tactic/localized.lean`
-reserve notation `localized`
-
--- used in `tactic/lint/frontend.lean`
-reserve notation `#lint`
-reserve notation `#lint_mathlib`
-reserve notation `#lint_all`
-reserve notation `#list_linters`
-
--- used in `tactic/where.lean`
-reserve prefix `#where`:max
-
--- used in `tactic/simps.lean`
-reserve notation `initialize_simps_projections`
-
--- used in `tactic/lift.lean`
-reserve notation `to`
-
--- used in `tactic/rcases.lean`
-precedence `?`:max
-
--- used in `order/lattice.lean`
-reserve infixl ` ⊓ `:70
-reserve infixl ` ⊔ `:65
-
--- used in `algebra/module/linear_map.lean`
-reserve infix ` ≃ₗ `:25
diff --git a/src/tactic/reserved_notation.lean b/src/tactic/reserved_notation.lean
new file mode 100644
index 0000000000000..82f2a5a58c569
--- /dev/null
+++ b/src/tactic/reserved_notation.lean
@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2020 Bryan Gin-ge Chen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bryan Gin-ge Chen
+-/
+
+/-!
+# Reserved notation
+
+This file is imported by `logic.basic` and `logic.relator` to place it at the top of the
+import graph.
+
+We place all of `mathlib`'s reserved notation in this file so that users will know not to
+use them as e.g. variable names without needing to import the specific file where they
+are defined.
+
+-/
+
+-- used in `logic/relator.lean`
+reserve infixr ` ⇒ `:40
+
+-- used in `tactic/localized.lean`
+reserve notation `localized`
+
+-- used in `tactic/lint/frontend.lean`
+reserve notation `#lint`
+reserve notation `#lint_mathlib`
+reserve notation `#lint_all`
+reserve notation `#list_linters`
+
+-- used in `tactic/where.lean`
+reserve prefix `#where`:max
+
+-- used in `tactic/simps.lean`
+reserve notation `initialize_simps_projections`
+
+-- used in `tactic/lift.lean`
+reserve notation `to`
+
+-- used in `tactic/rcases.lean`
+precedence `?`:max
+
+-- used in `order/lattice.lean`
+reserve infixl ` ⊓ `:70
+reserve infixl ` ⊔ `:65
+
+-- used in `algebra/module/linear_map.lean`
+reserve infix ` ≃ₗ `:25

From 95b31e2f375622b5a31d7ca9dd784ca0c9917ce5 Mon Sep 17 00:00:00 2001
From: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Date: Mon, 14 Dec 2020 22:58:26 -0500
Subject: [PATCH 7/9] fix

---
 scripts/copy-mod-doc-exceptions.txt | 34 ++++++++++++++---------------
 src/tactic/core.lean                |  5 -----
 src/tactic/reserved_notation.lean   |  5 +++++
 3 files changed, 22 insertions(+), 22 deletions(-)

diff --git a/scripts/copy-mod-doc-exceptions.txt b/scripts/copy-mod-doc-exceptions.txt
index 403386be48293..548ac46a520d9 100644
--- a/scripts/copy-mod-doc-exceptions.txt
+++ b/scripts/copy-mod-doc-exceptions.txt
@@ -106,12 +106,12 @@ src/algebra/invertible.lean : line 216 : ERR_LIN : Line has more than 100 charac
 src/algebra/invertible.lean : line 224 : ERR_LIN : Line has more than 100 characters
 src/algebra/invertible.lean : line 233 : ERR_LIN : Line has more than 100 characters
 src/algebra/invertible.lean : line 84 : ERR_LIN : Line has more than 100 characters
+src/algebra/lie/basic.lean : line 1059 : ERR_LIN : Line has more than 100 characters
 src/algebra/lie/basic.lean : line 241 : ERR_LIN : Line has more than 100 characters
 src/algebra/lie/basic.lean : line 245 : ERR_LIN : Line has more than 100 characters
 src/algebra/lie/basic.lean : line 385 : ERR_LIN : Line has more than 100 characters
 src/algebra/lie/basic.lean : line 68 : ERR_LIN : Line has more than 100 characters
 src/algebra/lie/basic.lean : line 83 : ERR_LIN : Line has more than 100 characters
-src/algebra/lie/basic.lean : line 948 : ERR_LIN : Line has more than 100 characters
 src/algebra/lie/classical.lean : line 124 : ERR_LIN : Line has more than 100 characters
 src/algebra/lie/classical.lean : line 215 : ERR_LIN : Line has more than 100 characters
 src/algebra/lie/classical.lean : line 363 : ERR_LIN : Line has more than 100 characters
@@ -282,7 +282,7 @@ src/analysis/special_functions/trigonometric.lean : line 2326 : ERR_LIN : Line h
 src/analysis/special_functions/trigonometric.lean : line 2329 : ERR_LIN : Line has more than 100 characters
 src/analysis/special_functions/trigonometric.lean : line 2425 : ERR_LIN : Line has more than 100 characters
 src/analysis/special_functions/trigonometric.lean : line 2469 : ERR_LIN : Line has more than 100 characters
-src/analysis/specific_limits.lean : line 575 : ERR_LIN : Line has more than 100 characters
+src/analysis/specific_limits.lean : line 567 : ERR_LIN : Line has more than 100 characters
 src/category_theory/abelian/exact.lean : line 70 : ERR_LIN : Line has more than 100 characters
 src/category_theory/abelian/exact.lean : line 76 : ERR_LIN : Line has more than 100 characters
 src/category_theory/abelian/non_preadditive.lean : line 190 : ERR_LIN : Line has more than 100 characters
@@ -1058,8 +1058,7 @@ src/geometry/manifold/times_cont_mdiff.lean : line 523 : ERR_LIN : Line has more
 src/geometry/manifold/times_cont_mdiff.lean : line 900 : ERR_LIN : Line has more than 100 characters
 src/group_theory/abelianization.lean : line 13 : ERR_MOD : Module docstring missing, or too late
 src/group_theory/archimedean.lean : line 43 : ERR_LIN : Line has more than 100 characters
-src/group_theory/coset.lean : line 173 : ERR_LIN : Line has more than 100 characters
-src/group_theory/coset.lean : line 260 : ERR_LIN : Line has more than 100 characters
+src/group_theory/coset.lean : line 259 : ERR_LIN : Line has more than 100 characters
 src/group_theory/coset.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/group_theory/eckmann_hilton.lean : line 98 : ERR_LIN : Line has more than 100 characters
 src/group_theory/free_abelian_group.lean : line 14 : ERR_MOD : Module docstring missing, or too late
@@ -1083,12 +1082,12 @@ src/group_theory/free_group.lean : line 180 : ERR_LIN : Line has more than 100 c
 src/group_theory/free_group.lean : line 672 : ERR_LIN : Line has more than 100 characters
 src/group_theory/free_group.lean : line 737 : ERR_LIN : Line has more than 100 characters
 src/group_theory/order_of_element.lean : line 12 : ERR_MOD : Module docstring missing, or too late
-src/group_theory/order_of_element.lean : line 396 : ERR_LIN : Line has more than 100 characters
-src/group_theory/order_of_element.lean : line 436 : ERR_LIN : Line has more than 100 characters
-src/group_theory/order_of_element.lean : line 446 : ERR_LIN : Line has more than 100 characters
-src/group_theory/order_of_element.lean : line 476 : ERR_LIN : Line has more than 100 characters
-src/group_theory/order_of_element.lean : line 521 : ERR_LIN : Line has more than 100 characters
-src/group_theory/order_of_element.lean : line 523 : ERR_LIN : Line has more than 100 characters
+src/group_theory/order_of_element.lean : line 392 : ERR_LIN : Line has more than 100 characters
+src/group_theory/order_of_element.lean : line 432 : ERR_LIN : Line has more than 100 characters
+src/group_theory/order_of_element.lean : line 442 : ERR_LIN : Line has more than 100 characters
+src/group_theory/order_of_element.lean : line 472 : ERR_LIN : Line has more than 100 characters
+src/group_theory/order_of_element.lean : line 517 : ERR_LIN : Line has more than 100 characters
+src/group_theory/order_of_element.lean : line 519 : ERR_LIN : Line has more than 100 characters
 src/group_theory/perm/cycles.lean : line 124 : ERR_LIN : Line has more than 100 characters
 src/group_theory/perm/cycles.lean : line 127 : ERR_LIN : Line has more than 100 characters
 src/group_theory/perm/cycles.lean : line 138 : ERR_LIN : Line has more than 100 characters
@@ -1149,15 +1148,11 @@ src/linear_algebra/multilinear.lean : line 517 : ERR_LIN : Line has more than 10
 src/linear_algebra/multilinear.lean : line 63 : ERR_LIN : Line has more than 100 characters
 src/linear_algebra/multilinear.lean : line 78 : ERR_LIN : Line has more than 100 characters
 src/linear_algebra/special_linear_group.lean : line 53 : ERR_LIN : Line has more than 100 characters
-src/logic/basic.lean : line 501 : ERR_LIN : Line has more than 100 characters
-src/logic/basic.lean : line 578 : ERR_LIN : Line has more than 100 characters
-src/logic/basic.lean : line 878 : ERR_LIN : Line has more than 100 characters
 src/logic/function/basic.lean : line 324 : ERR_LIN : Line has more than 100 characters
 src/logic/function/basic.lean : line 498 : ERR_LIN : Line has more than 100 characters
 src/logic/function/basic.lean : line 538 : ERR_LIN : Line has more than 100 characters
 src/logic/relation.lean : line 10 : ERR_MOD : Module docstring missing, or too late
-src/logic/relator.lean : line 12 : ERR_RNT : Reserved notation outside tactic.core
-src/logic/relator.lean : line 9 : ERR_MOD : Module docstring missing, or too late
+src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/measure_theory/category/Meas.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/measure_theory/decomposition.lean : line 14 : ERR_MOD : Module docstring missing, or too late
 src/measure_theory/measure_space.lean : line 1720 : ERR_LIN : Line has more than 100 characters
@@ -1406,8 +1401,8 @@ src/ring_theory/polynomial/scale_roots.lean : line 89 : ERR_LIN : Line has more
 src/ring_theory/polynomial/scale_roots.lean : line 92 : ERR_LIN : Line has more than 100 characters
 src/ring_theory/power_series.lean : line 189 : ERR_LIN : Line has more than 100 characters
 src/ring_theory/power_series.lean : line 194 : ERR_LIN : Line has more than 100 characters
+src/ring_theory/power_series.lean : line 690 : ERR_LIN : Line has more than 100 characters
 src/ring_theory/power_series.lean : line 693 : ERR_LIN : Line has more than 100 characters
-src/ring_theory/power_series.lean : line 696 : ERR_LIN : Line has more than 100 characters
 src/ring_theory/principal_ideal_domain.lean : line 121 : ERR_LIN : Line has more than 100 characters
 src/ring_theory/principal_ideal_domain.lean : line 124 : ERR_LIN : Line has more than 100 characters
 src/ring_theory/roots_of_unity.lean : line 148 : ERR_LIN : Line has more than 100 characters
@@ -1470,8 +1465,12 @@ src/tactic/converter/old_conv.lean : line 272 : ERR_LIN : Line has more than 100
 src/tactic/converter/old_conv.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/core.lean : line 17 : ERR_MOD : Module docstring missing, or too late
 src/tactic/core.lean : line 1802 : ERR_LIN : Line has more than 100 characters
+src/tactic/core.lean : line 1805 : ERR_RNT : Reserved notation outside tactic.core
 src/tactic/core.lean : line 1890 : ERR_LIN : Line has more than 100 characters
+src/tactic/core.lean : line 2075 : ERR_RNT : Reserved notation outside tactic.core
 src/tactic/core.lean : line 2085 : ERR_LIN : Line has more than 100 characters
+src/tactic/core.lean : line 2103 : ERR_RNT : Reserved notation outside tactic.core
+src/tactic/core.lean : line 2113 : ERR_RNT : Reserved notation outside tactic.core
 src/tactic/core.lean : line 2148 : ERR_LIN : Line has more than 100 characters
 src/tactic/core.lean : line 2156 : ERR_LIN : Line has more than 100 characters
 src/tactic/core.lean : line 2180 : ERR_LIN : Line has more than 100 characters
@@ -1509,6 +1508,7 @@ src/tactic/generalizes.lean : line 118 : ERR_LIN : Line has more than 100 charac
 src/tactic/group.lean : line 36 : ERR_LIN : Line has more than 100 characters
 src/tactic/hint.lean : line 57 : ERR_LIN : Line has more than 100 characters
 src/tactic/hint.lean : line 9 : ERR_MOD : Module docstring missing, or too late
+src/tactic/induction.lean : line 1252 : ERR_RNT : Reserved notation outside tactic.core
 src/tactic/interactive.lean : line 1117 : ERR_LIN : Line has more than 100 characters
 src/tactic/interactive.lean : line 379 : ERR_LIN : Line has more than 100 characters
 src/tactic/interactive.lean : line 703 : ERR_LIN : Line has more than 100 characters
@@ -1755,7 +1755,7 @@ src/topology/algebra/group_completion.lean : line 69 : ERR_LIN : Line has more t
 src/topology/algebra/group_completion.lean : line 75 : ERR_LIN : Line has more than 100 characters
 src/topology/algebra/group_completion.lean : line 82 : ERR_LIN : Line has more than 100 characters
 src/topology/algebra/group_completion.lean : line 84 : ERR_LIN : Line has more than 100 characters
-src/topology/algebra/infinite_sum.lean : line 697 : ERR_LIN : Line has more than 100 characters
+src/topology/algebra/infinite_sum.lean : line 713 : ERR_LIN : Line has more than 100 characters
 src/topology/algebra/module.lean : line 1078 : ERR_LIN : Line has more than 100 characters
 src/topology/algebra/module.lean : line 1088 : ERR_LIN : Line has more than 100 characters
 src/topology/algebra/module.lean : line 300 : ERR_LIN : Line has more than 100 characters
diff --git a/src/tactic/core.lean b/src/tactic/core.lean
index 1500618ac80de..b2e7b6a0605cf 100644
--- a/src/tactic/core.lean
+++ b/src/tactic/core.lean
@@ -2072,8 +2072,6 @@ do (e, s) ← with_input (lean.parser.pexpr 0) s.as_string,
    pure ``(to_pfmt %%(reflect acc) ++ to_pfmt %%e ++ %%f)
 | acc (c::s) := parse_pformat (acc.str c) s
 
-reserve prefix `pformat! `:100
-
 /-- See `format!` in `init/meta/interactive_base.lean`.
 
 The main differences are that `pp` is called instead of `to_fmt` and that we can use
@@ -2100,8 +2098,6 @@ meta def pformat_macro (_ : parse $ tk "pformat!") (s : string) : parser pexpr :
 do e ← parse_pformat "" s.to_list,
    return ``(%%e : pformat)
 
-reserve prefix `fail! `:100
-
 /--
 The combination of `pformat` and `fail`.
 -/
@@ -2110,7 +2106,6 @@ meta def fail_macro (_ : parse $ tk "fail!") (s : string) : parser pexpr :=
 do e ← pformat_macro () s,
    pure ``((%%e : pformat) >>= fail)
 
-reserve prefix `trace! `:100
 /--
 The combination of `pformat` and `trace`.
 -/
diff --git a/src/tactic/reserved_notation.lean b/src/tactic/reserved_notation.lean
index 82f2a5a58c569..d309051650d91 100644
--- a/src/tactic/reserved_notation.lean
+++ b/src/tactic/reserved_notation.lean
@@ -19,6 +19,11 @@ are defined.
 -- used in `logic/relator.lean`
 reserve infixr ` ⇒ `:40
 
+-- used in `tactic/core.lean`
+reserve prefix `pformat! `:100
+reserve prefix `fail! `:100
+reserve prefix `trace! `:100
+
 -- used in `tactic/localized.lean`
 reserve notation `localized`
 

From 5eee23b647bf5f257da122e6b07579c17f94118a Mon Sep 17 00:00:00 2001
From: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Date: Mon, 14 Dec 2020 23:07:52 -0500
Subject: [PATCH 8/9] lint tactic/core.lean again

---
 scripts/copy-mod-doc-exceptions.txt | 25 ++------------
 src/tactic/core.lean                | 53 +++++++++++++++++------------
 src/tactic/reserved_notation.lean   |  1 +
 3 files changed, 35 insertions(+), 44 deletions(-)

diff --git a/scripts/copy-mod-doc-exceptions.txt b/scripts/copy-mod-doc-exceptions.txt
index 548ac46a520d9..5d498b5d8aaaf 100644
--- a/scripts/copy-mod-doc-exceptions.txt
+++ b/scripts/copy-mod-doc-exceptions.txt
@@ -1464,28 +1464,9 @@ src/tactic/converter/interactive.lean : line 53 : ERR_LIN : Line has more than 1
 src/tactic/converter/old_conv.lean : line 272 : ERR_LIN : Line has more than 100 characters
 src/tactic/converter/old_conv.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/core.lean : line 17 : ERR_MOD : Module docstring missing, or too late
-src/tactic/core.lean : line 1802 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 1805 : ERR_RNT : Reserved notation outside tactic.core
-src/tactic/core.lean : line 1890 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 2075 : ERR_RNT : Reserved notation outside tactic.core
-src/tactic/core.lean : line 2085 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 2103 : ERR_RNT : Reserved notation outside tactic.core
-src/tactic/core.lean : line 2113 : ERR_RNT : Reserved notation outside tactic.core
-src/tactic/core.lean : line 2148 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 2156 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 2180 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 2181 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 2207 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 2300 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 2304 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 2305 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 624 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 639 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 640 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 647 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 649 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 819 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 820 : ERR_LIN : Line has more than 100 characters
+src/tactic/core.lean : line 2147 : ERR_LIN : Line has more than 100 characters
+src/tactic/core.lean : line 2308 : ERR_LIN : Line has more than 100 characters
+src/tactic/core.lean : line 2309 : ERR_LIN : Line has more than 100 characters
 src/tactic/delta_instance.lean : line 56 : ERR_LIN : Line has more than 100 characters
 src/tactic/delta_instance.lean : line 66 : ERR_LIN : Line has more than 100 characters
 src/tactic/delta_instance.lean : line 8 : ERR_MOD : Module docstring missing, or too late
diff --git a/src/tactic/core.lean b/src/tactic/core.lean
index b2e7b6a0605cf..fce85e2783083 100644
--- a/src/tactic/core.lean
+++ b/src/tactic/core.lean
@@ -621,7 +621,8 @@ retrieve $ do revert e, expr.elet _ _ _ _ ← target, skip
 whereas `split_on_p p xs` removes the matches, `partition_local_deps_aux vs xs acc` includes
 them in the following partition. Also, `partition_local_deps_aux vs xs acc` discards the partition
 running up to the first match. -/
-private def partition_local_deps_aux {α} [decidable_eq α] (vs : list α) : list α → list α → list (list α)
+private def partition_local_deps_aux {α} [decidable_eq α] (vs : list α) :
+  list α → list α → list (list α)
 | [] acc := [acc.reverse]
 | (l :: ls) acc :=
   if l ∈ vs then acc.reverse :: partition_local_deps_aux ls [l]
@@ -636,17 +637,19 @@ meta def partition_local_deps (vs : list expr) : tactic (list (list expr)) :=
 do ls ← local_context,
    pure (partition_local_deps_aux vs ls []).tail.reverse
 
-/-- `clear_value [e₀, e₁, e₂, ...]` clears the body of the local definitions `e₀`, `e₁`, `e₂`, ... changing them into regular
-hypotheses. A hypothesis `e : α := t` is changed to `e : α`. The order of locals `e₀`, `e₁`, `e₂` does not
-matter as a permutation will be chosen so as to preserve type correctness.
-This tactic is called `clearbody` in Coq. -/
+/-- `clear_value [e₀, e₁, e₂, ...]` clears the body of the local definitions `e₀`, `e₁`, `e₂`, ...
+changing them into regular hypotheses. A hypothesis `e : α := t` is changed to `e : α`. The order of
+locals `e₀`, `e₁`, `e₂` does not matter as a permutation will be chosen so as to preserve type
+correctness. This tactic is called `clearbody` in Coq. -/
 meta def clear_value (vs : list expr) : tactic unit := do
   ls ← partition_local_deps vs,
   ls.mmap' $ λ vs, do
   { revert_lst vs,
-    (expr.elet v t d b) ← target | fail format!"Cannot clear the body of {vs.head}. It is not a local definition.",
+    (expr.elet v t d b) ← target |
+      fail format!"Cannot clear the body of {vs.head}. It is not a local definition.",
     let e := expr.pi v binder_info.default t b,
-    type_check e <|> fail format!"Cannot clear the body of {vs.head}. The resulting goal is not type correct.",
+    type_check e <|>
+      fail format!"Cannot clear the body of {vs.head}. The resulting goal is not type correct.",
     g ← mk_meta_var e,
     h ← note `h none g,
     tactic.exact $ h d,
@@ -815,10 +818,10 @@ attribute.get_instances `class >>= list.mfilter (λ n,
   succeeds $ mk_app n [e] >>= mk_instance)
 
 /--
-  Finds an instance of an implication `cond → tgt`.
-  Returns a pair of a local constant `e` of type `cond`, and an instance of `tgt` that can mention `e`.
-  The local constant `e` is added as an hypothesis to the tactic state, but should not be used, since
-  it has been "proven" by a metavariable.
+Finds an instance of an implication `cond → tgt`.
+Returns a pair of a local constant `e` of type `cond`, and an instance of `tgt` that can mention
+`e`. The local constant `e` is added as an hypothesis to the tactic state, but should not be used,
+since it has been "proven" by a metavariable.
 -/
 meta def mk_conditional_instance (cond tgt : expr) : tactic (expr × expr) := do
 f ← mk_meta_var cond,
@@ -1799,11 +1802,10 @@ do tgt   ← infer_type h,
    match env.symm_for (const_name r) with
    | (some symm) := do s ← mk_const symm,
                        apply_at s h
-   | none        := fail "symmetry tactic failed, target is not a relation application with the expected property."
+   | none        := fail
+      "symmetry tactic failed, target is not a relation application with the expected property."
    end
 
-precedence `setup_tactic_parser`:0
-
 /-- `setup_tactic_parser` is a user command that opens the namespaces used in writing
 interactive tactics, and declares the local postfix notation `?` for `optional` and `*` for `many`.
 It does *not* use the `namespace` command, so it will typically be used after
@@ -1887,7 +1889,8 @@ of `t`. -/
 meta def trace_error (msg : string) (t : tactic α) : tactic α
 | s := match t s with
        | (result.success r s') := result.success r s'
-       | (result.exception (some msg') p s') := (trace msg >> trace (msg' ()) >> result.exception (some msg') p) s'
+       | (result.exception (some msg') p s') := (trace msg >> trace (msg' ()) >> result.exception
+            (some msg') p) s'
        | (result.exception none p s') := result.exception none p s'
        end
 
@@ -2080,7 +2083,8 @@ arguments of type `tactic α` in the quotations.
 Now, consider the following:
 ```lean
 e ← to_expr ``(3 + 7),
-trace format!"{e}"  -- outputs `has_add.add.{0} nat nat.has_add (bit1.{0} nat nat.has_one nat.has_add (has_one.one.{0} nat nat.has_one)) ...`
+trace format!"{e}"  -- outputs `has_add.add.{0} nat nat.has_add
+                    -- (bit1.{0} nat nat.has_one nat.has_add (has_one.one.{0} nat nat.has_one)) ...`
 trace pformat!"{e}" -- outputs `3 + 7`
 ```
 
@@ -2148,7 +2152,8 @@ private meta def apply_under_n_pis_aux (func arg : pexpr) : ℕ → ℕ → expr
   let vars := ((list.range n).reverse.map (@expr.var ff)),
       bd := vars.foldl expr.app arg.mk_explicit in
   func bd
-| n (k+1) (expr.pi nm bi tp bd) := expr.pi nm bi (pexpr.of_expr tp) (apply_under_n_pis_aux (n+1) k bd)
+| n (k+1) (expr.pi nm bi tp bd) := expr.pi nm bi (pexpr.of_expr tp)
+  (apply_under_n_pis_aux (n+1) k bd)
 | n (k+1) t := apply_under_n_pis_aux n 0 t
 
 /--
@@ -2172,10 +2177,12 @@ When `tgt` is a `pi` expr, `func` is elaborated in a context
 with the domain of `tgt`.
 
 Examples:
-* ```get_pexpr_arg_arity ``(ring) `(true)``` returns 0, since `ring` takes one non-function argument.
-* ```get_pexpr_arg_arity_with_tgt ``(monad) `(true)``` returns 1, since `monad` takes one argument of type `α → α`.
+* ```get_pexpr_arg_arity ``(ring) `(true)``` returns 0, since `ring` takes one non-function
+  argument.
+* ```get_pexpr_arg_arity_with_tgt ``(monad) `(true)``` returns 1, since `monad` takes one argument
+  of type `α → α`.
 * ```get_pexpr_arg_arity_with_tgt ``(module R) `(Π (R : Type), comm_ring R → true)``` returns 0
- -/
+-/
 meta def get_pexpr_arg_arity_with_tgt (func : pexpr) (tgt : expr) : tactic ℕ :=
 lock_tactic_state $ do
   mv ← mk_mvar,
@@ -2199,7 +2206,8 @@ do env ← get_env,
      end,
    let xs := env.decl_filter_map (λ d,
      do fn ← env.decl_olean d.to_name,
-        guard ((`_private).is_prefix_of d.to_name ∧ p fn ∧ d.to_name.update_prefix name.anonymous = n),
+        guard ((`_private).is_prefix_of d.to_name ∧ p fn ∧
+          d.to_name.update_prefix name.anonymous = n),
         pure d.to_name),
    match xs with
    | [n] := pure n
@@ -2292,7 +2300,8 @@ meta def set_attribute (attr_name : name) (c_name : name) (persistent := tt)
 get_decl c_name <|> fail!"unknown declaration {c_name}",
 s ← try_or_report_error (set_basic_attribute attr_name c_name persistent prio),
 sum.inr msg ← return s | skip,
-if msg = (format!"set_basic_attribute tactic failed, '{attr_name}' is not a basic attribute").to_string
+if msg =
+  (format!"set_basic_attribute tactic failed, '{attr_name}' is not a basic attribute").to_string
 then do
   user_attr_nm ← get_user_attribute_name attr_name,
   user_attr_const ← mk_const user_attr_nm,
diff --git a/src/tactic/reserved_notation.lean b/src/tactic/reserved_notation.lean
index d309051650d91..1f5870bd584f4 100644
--- a/src/tactic/reserved_notation.lean
+++ b/src/tactic/reserved_notation.lean
@@ -20,6 +20,7 @@ are defined.
 reserve infixr ` ⇒ `:40
 
 -- used in `tactic/core.lean`
+precedence `setup_tactic_parser`:0
 reserve prefix `pformat! `:100
 reserve prefix `fail! `:100
 reserve prefix `trace! `:100

From fafeec33b793e0392ffea1f8d614b161b2efe52e Mon Sep 17 00:00:00 2001
From: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Date: Tue, 15 Dec 2020 02:22:55 -0500
Subject: [PATCH 9/9] Update scripts/lint-copy-mod-doc.py

Co-authored-by: Johan Commelin <johan@commelin.net>
---
 scripts/lint-copy-mod-doc.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/lint-copy-mod-doc.py b/scripts/lint-copy-mod-doc.py
index 312b96313303b..b97b96175b87d 100755
--- a/scripts/lint-copy-mod-doc.py
+++ b/scripts/lint-copy-mod-doc.py
@@ -181,7 +181,7 @@ def format_errors(errors):
         if errno == ERR_SAV:
             print("{} : line {} : ERR_SAV : File contains the character ᾰ".format(fn, line_nr))
         if errno == ERR_RNT:
-            print("{} : line {} : ERR_RNT : Reserved notation outside tactic.core".format(fn, line_nr))
+            print("{} : line {} : ERR_RNT : Reserved notation outside tactic.reserved_notation".format(fn, line_nr))
         if errno == ERR_OPT:
             print("{} : line {} : ERR_OPT : Forbidden set_option command".format(fn, line_nr))