feat(Tactic/FunProp): make fun_prop able to tag → and ∀ (leanprover-community#32888)

by representing forall as a function application internally. Also tag `Measurable.imp` and `Measurable.forall` which were rejected by `fun_prop`.

Author: staroperator

Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean

@@ -866,13 +866,15 @@ lemma Measurable.and (hp : Measurable p) (hq : Measurable q) : Measurable fun a
 lemma Measurable.or (hp : Measurable p) (hq : Measurable q) : Measurable fun a ↦ p a ∨ q a :=
   measurableSet_setOf.1 <| hp.setOf.union hq.setOf
 
+@[fun_prop]
 lemma Measurable.imp (hp : Measurable p) (hq : Measurable q) : Measurable fun a ↦ p a → q a :=
   measurableSet_setOf.1 <| hp.setOf.himp hq.setOf
 
 @[fun_prop]
 lemma Measurable.iff (hp : Measurable p) (hq : Measurable q) : Measurable fun a ↦ p a ↔ q a :=
   measurableSet_setOf.1 <| by simp_rw [iff_iff_implies_and_implies]; exact hq.setOf.bihimp hp.setOf
 
+@[fun_prop]
 lemma Measurable.forall [Countable ι] {p : ι → α → Prop} (hp : ∀ i, Measurable (p i)) :
     Measurable fun a ↦ ∀ i, p i a :=
   measurableSet_setOf.1 <| by rw [setOf_forall]; exact MeasurableSet.iInter fun i ↦ (hp i).setOf

Mathlib/Tactic/FunProp/Mor.lean

@@ -9,6 +9,8 @@ public import Mathlib.Init
 public meta import Lean.Meta.CoeAttr
 public import Lean.Meta.CoeAttr
 
+import Mathlib.Tactic.TypeStar
+
 /-!
 ## `funProp` Meta programming functions like in Lean.Expr.* but for working with bundled morphisms.
 
@@ -31,6 +33,10 @@ open Lean Meta
 
 namespace Meta.FunProp
 
+/-- An abbreviation of `∀ x, p x`. It is used by `fun_prop` to represent Pi types as function
+applications and should not occur in any place other than the implementation of `fun_prop`. -/
+abbrev Forall {α : Sort*} (p : α → Sort*) := ∀ x, p x
+
 namespace Mor
 
 /-- Is `name` a coercion from some function space to functions? -/
@@ -111,7 +117,9 @@ def app (f : Expr) (arg : Arg) : Expr :=
   | some coe => (coe.app f).app arg.expr
 
 
-/-- Given `e = f a₁ a₂ ... aₙ`, returns `k f #[a₁, ..., aₙ]` where `f` can be bundled morphism. -/
+/-- Given `e = f a₁ a₂ ... aₙ`, returns `k f #[a₁, ..., aₙ]` where `f` can be bundled morphism.
+
+`∀ x, p x` is represented as `Forall p`. -/
 partial def withApp {α} (e : Expr) (k : Expr → Array Arg → MetaM α) : MetaM α :=
   go e #[]
 where
@@ -132,6 +140,8 @@ where
 
       go (.app (.app c f) x) as
     | .app f a, as => go f (as.push { expr := a })
+    | .forallE x t b bi, _ => do
+      go (← mkAppM ``Forall #[.lam x t b bi]) #[]
     | f, as => k f as.reverse
 
 

MathlibTest/fun_prop.lean

@@ -220,3 +220,17 @@ If possible, `fun_prop` theorem about `DFunLike.coe` should be state in this way
 
 That should be all about `fun_prop`, I hope you will enjoy using it :)
 -/
+
+
+
+/-! Test that `fun_prop` should work on `→` and `∀` -/
+
+attribute [fun_prop] Measurable.imp Measurable.forall
+
+example {α : Type*} [MeasurableSpace α] {p q : α → Prop} (hp : Measurable p) (hq : Measurable q) :
+    Measurable fun x => p x → q x := by
+  fun_prop
+
+example {α ι : Type*} [MeasurableSpace α] [Countable ι] {p : ι → α → Prop}
+    (hp : ∀ i, Measurable (p i)) : Measurable fun x => ∀ i, p i x := by
+  fun_prop