feat(measure_theory): allow measurability to prove ae_strongly_measur…

…able (#13427)

Adds `measurable.ae_strongly_measurable` to the `measurability` list



Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>

src/measure_theory/tactic.lean

@@ -137,15 +137,17 @@ meta def measurability_tactics (md : transparency := semireducible) : list (tact
   apply_measurable.comp_ae_measurable
                         >> pure "refine measurable.comp_ae_measurable _ _",
   `[ refine measurable.ae_measurable _ ]
-                        >> pure "refine measurable.ae_measurable _"
+                        >> pure "refine measurable.ae_measurable _",
+  `[ refine measurable.ae_strongly_measurable _ ]
+                        >> pure "refine measurable.ae_strongly_measurable _"
 ]
 
 namespace interactive
 setup_tactic_parser
 
 /--
-Solve goals of the form `measurable f`, `ae_measurable f μ` or `measurable_set s`.
-`measurability?` reports back the proof term it found.
+Solve goals of the form `measurable f`, `ae_measurable f μ`, `ae_strongly_measurable f μ` or
+`measurable_set s`. `measurability?` reports back the proof term it found.
 -/
 meta def measurability
   (bang : parse $ optional (tk "!")) (trace : parse $ optional (tk "?")) (cfg : tidy.cfg := {}) :
@@ -159,8 +161,9 @@ trace_fn measurability_core
 meta def measurability' : tactic unit := measurability none none {}
 
 /--
-`measurability` solves goals of the form `measurable f`, `ae_measurable f μ` or `measurable_set s`
-by applying lemmas tagged with the `measurability` user attribute.
+`measurability` solves goals of the form `measurable f`, `ae_measurable f μ`,
+`ae_strongly_measurable f μ` or `measurable_set s` by applying lemmas tagged with the
+`measurability` user attribute.
 
 You can also use `measurability!`, which applies lemmas with `{ md := semireducible }`.
 The default behaviour is more conservative, and only unfolds `reducible` definitions