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

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `07f1b273c8871bec3f61440bb61babe43ae4d932`
+Mathlib version: `11d700a58e53f1903b9d99aacb82e03bdf4cca64`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `07f1b273c8871bec3f61440bb61babe43ae4d932`
+Mathlib version: `11d700a58e53f1903b9d99aacb82e03bdf4cca64`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `07f1b273c8871bec3f61440bb61babe43ae4d932`
+Mathlib version: `11d700a58e53f1903b9d99aacb82e03bdf4cca64`
 
 ## Elab.async
 type: `Bool`

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `07f1b273c8871bec3f61440bb61babe43ae4d932`
+Mathlib version: `11d700a58e53f1903b9d99aacb82e03bdf4cca64`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -3242,7 +3242,8 @@ Defined in: `Mathlib.Tactic.grwSeq`
 
 `grw [e]` works just like `rw [e]`, but `e` can be a relation other than `=` or `↔`.
 
-For example,
+For example:
+
 ```lean
 variable {a b c d n : ℤ}
 
@@ -3256,6 +3257,17 @@ example (h₁ : a ∣ b) (h₂ : b ∣ a ^ 2 * c) : a ∣ b ^ 2 * c := by
   grw [h₁] at *
   exact h₂
 ```
+
+To replace the RHS with the LHS of the given relation, use the `←` notation (just like in `rw`):
+
+```
+example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
+  grw [← h₂, ← h₁]
+```
+
+The strict inequality `a < b` is turned into the non-strict inequality `a ≤ b` to rewrite with it.
+A future version of `grw` may get special support for making better use of strict inequalities.
+
 To rewrite only in the `n`-th position, use `nth_grw n`.
 This is useful when `grw` tries to rewrite in a position that is not valid for the given relation.
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "07f1b273c8871bec3f61440bb61babe43ae4d932",
+   "rev": "11d700a58e53f1903b9d99aacb82e03bdf4cca64",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e2a2ee109182182dd0e347e8149d312d72bfbfb2",
+   "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "78129e1913fe4988ac238156ec5f223ec02d286c",
+   "rev": "6cae843edf5b3abc871c557614eaffdcb4492d89",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",