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

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `de7ac7cb70710498104300af3c811b05efbb48c6`
+Mathlib version: `ac48e6adc8b30cd28a5e3d428a25300457ae7243`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas
@@ -784,6 +784,11 @@ or more generally of the form `∀ i h h' j h'', f₁ i j ≈ f₂ i j` (say) fo
 pair `f₁`/`f₂`. (Other antecedents are considered to generate "side goals".) The index of the
 "varying argument" pair corresponding to each "main" antecedent is recorded.
 
+If a lemma such as `add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d` has been tagged with `gcongr`,
+then a direct consequence like `a ≤ b → a + c ≤ b + c` does *not* need to be tagged.
+However, if a more specific lemma has fewer side conditions, it should also be tagged with `gcongr`.
+For example, `mul_le_mul_of_nonneg_right` and `mul_le_mul_of_nonneg_left` are both tagged.
+
 Lemmas involving `<` or `≤` can also be marked `@[bound]` for use in the related `bound` tactic.
 
 ## gcongr_forward

docs/commands.md

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

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `de7ac7cb70710498104300af3c811b05efbb48c6`
+Mathlib version: `ac48e6adc8b30cd28a5e3d428a25300457ae7243`
 
 ## Elab.async
 type: `Bool`
@@ -1082,6 +1082,13 @@ default: `true`
 
 enable the tactic analysis framework
 
+## linter.tacticAnalysis.dummy
+type: `Bool`
+
+default: `false`
+
+
+
 ## linter.tacticAnalysis.introMerge
 type: `Bool`
 

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `de7ac7cb70710498104300af3c811b05efbb48c6`
+Mathlib version: `ac48e6adc8b30cd28a5e3d428a25300457ae7243`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -2888,24 +2888,8 @@ A macro for a common simplification when rewriting with ghost component equation
 ## grewrite
 Defined in: `Mathlib.Tactic.grewriteSeq`
 
-`grewrite [e]` works just like `rewrite [e]`, but `e` can be a relation other than `=` or `↔`.
-
-For example,
-```lean
-variable {a b c d n : ℤ}
-
-example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
-  grewrite [h₁, h₂]; rfl
-
-example (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
-  grewrite [h]; rfl
-
-example (h₁ : a ∣ b) (h₂ : b ∣ a ^ 2 * c) : a ∣ b ^ 2 * c := by
-  grewrite [h₁] at *
-  exact h₂
-```
-To be able to use `grewrite`, the relevant lemmas need to be tagged with `@[gcongr]`.
-To rewrite inside a transitive relation, you can also give it an `IsTrans` instance.
+`grewrite [e]` is like `grw [e]`, but it doesn't try to close the goal with `rfl`.
+This is analogous to `rw` and `rewrite`, where `rewrite` doesn't try to close the goal with `rfl`.
 
 ## grind
 Defined in: `Lean.Parser.Tactic.grind`
@@ -3228,6 +3212,9 @@ example (h₁ : a ∣ b) (h₂ : b ∣ a ^ 2 * c) : a ∣ b ^ 2 * c := by
   grw [h₁] at *
   exact h₂
 ```
+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.
+
 To be able to use `grw`, the relevant lemmas need to be tagged with `@[gcongr]`.
 To rewrite inside a transitive relation, you can also give it an `IsTrans` instance.
 
@@ -6053,6 +6040,9 @@ built in for `push Not`, so that it can preserve binder names, and so that `¬ (
 transformed to either `p → ¬ q` (the default) or `¬ p ∨ ¬ q`. To get `¬ p ∨ ¬ q`, use
 `set_option push_neg.use_distrib true`.
 
+Tactics that introduce a negation usually have a version that automatically calls `push_neg` on
+that negation. These include `by_cases!`, `contrapose!` and `by_contra!`.
+
 Another example: given a hypothesis
 ```lean
 h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "de7ac7cb70710498104300af3c811b05efbb48c6",
+   "rev": "ac48e6adc8b30cd28a5e3d428a25300457ae7243",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "754186a55901dcfdfd4a15f0e4217d8dce65ac37",
+   "rev": "091ff2379c7f0998aba1dc031a578810d44b9f3f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",