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

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `bc7f43e3827a034fa6f19803c7cedb9a9e86a15c`
+Mathlib version: `de7ac7cb70710498104300af3c811b05efbb48c6`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas
@@ -1081,6 +1081,9 @@ def isYellow (color : String) : Bool :=
   | _ => false
 ```
 
+## measurability
+ The `measurability` attribute used to tag measurability statements for the `measurability` tactic.
+
 ## method_specs
  generate method specification theorems
 

docs/commands.md

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

docs/options.md

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

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `bc7f43e3827a034fa6f19803c7cedb9a9e86a15c`
+Mathlib version: `de7ac7cb70710498104300af3c811b05efbb48c6`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -2788,7 +2788,7 @@ Defined in: `«tacticGeneralize'_:_=_»`
 Backwards compatibility shim for `generalize`.
 
 ## generalize_proofs
-Defined in: `Mathlib.Tactic.generalizeProofsElab`
+Defined in: `Batteries.Tactic.generalizeProofsElab`
 
 `generalize_proofs ids* [at locs]?` generalizes proofs in the current goal,
 turning them into new local hypotheses.
@@ -4409,8 +4409,10 @@ The tactic `measurability` solves goals of the form `Measurable f`, `AEMeasurabl
 `StronglyMeasurable f`, `AEStronglyMeasurable f μ`, or `MeasurableSet s` by applying lemmas tagged
 with the `measurability` user attribute.
 
-`fun_prop` is a (usually more powerful) alternative to `measurability`
-if your goal does not involve `MeasurableSet`.
+Note that `measurability` uses `fun_prop` for solving measurability of functions, so statements
+about `Measurable`, `AEMeasurable`, `StronglyMeasurable` and `AEStronglyMeasurable` should be tagged
+with `fun_prop` rather that `measurability`. The `measurability` attribute is equivalent to
+`fun_prop` in these cases for backward compatibility with the earlier implementation.
 
 ## measurability!
 Defined in: `measurability!`

lake-manifest.json

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