Merge pull request #478 from Seasawher/auto-update-branch

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `a9a54f808381b4bfb115c6206d75ffac1b0f1a79`
+Mathlib version: `f4506f7151c9057fd9f8714b2a1f13a647fe2352`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas
@@ -741,6 +741,10 @@ Register an Expr presenter. It must have the type `ProofWidgets.ExprPresenter`.
 ## extern
  builtin and foreign functions
 
+## field
+ Attribute grouping the simprocs associated to the field_simp tactic
+Initialize the attribute `field` grouping the simprocs associated to the field_simp tactic.
+
 ## fin_omega
  A simp set for the `fin_omega` wrapper around `omega`. 
 

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `a9a54f808381b4bfb115c6206d75ffac1b0f1a79`
+Mathlib version: `f4506f7151c9057fd9f8714b2a1f13a647fe2352`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `a9a54f808381b4bfb115c6206d75ffac1b0f1a79`
+Mathlib version: `f4506f7151c9057fd9f8714b2a1f13a647fe2352`
 
 ## Elab.async
 type: `Bool`

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `a9a54f808381b4bfb115c6206d75ffac1b0f1a79`
+Mathlib version: `f4506f7151c9057fd9f8714b2a1f13a647fe2352`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -2480,7 +2480,7 @@ Defined in: `Mathlib.Tactic.FieldSimp.fieldSimp`
 The goal of `field_simp` is to reduce an expression in a field to an expression of the form `n / d`
 where neither `n` nor `d` contains any division symbol.
 
-If the goal is an equality, this tactic will also clear the denominators, so that the proof
+If the goal is an (in)equality, this tactic will also clear the denominators, so that the proof
 can normally be concluded by an application of `ring`.
 
 For example,

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a9a54f808381b4bfb115c6206d75ffac1b0f1a79",
+   "rev": "f4506f7151c9057fd9f8714b2a1f13a647fe2352",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "345a958916d27982d4ecb4500fba0ebb21096651",
+   "rev": "2e582a44b0150db152bff1c8484eb557fb5340da",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",