feat: use measurability as auto-param in MeasurableEquiv (leanprover-community#34457)

... and remove as many explicit proofs as possible.

Author: YaelDillies

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -551,8 +551,6 @@ protected theorem Homeomorph.measurable (h : α ≃ₜ γ) : Measurable h :=
 
 /-- A homeomorphism between two Borel spaces is a measurable equivalence. -/
 def Homeomorph.toMeasurableEquiv (h : γ ≃ₜ γ₂) : γ ≃ᵐ γ₂ where
-  measurable_toFun := h.measurable
-  measurable_invFun := h.symm.measurable
   toEquiv := h.toEquiv
 
 lemma Homeomorph.measurableEmbedding (h : γ ≃ₜ γ₂) : MeasurableEmbedding h :=

Mathlib/MeasureTheory/Constructions/UnitInterval.lean

@@ -56,8 +56,6 @@ def symmMeasurableEquiv : I ≃ᵐ I where
   invFun := σ
   left_inv := symm_symm
   right_inv := symm_symm
-  measurable_toFun := measurable_symm
-  measurable_invFun := measurable_symm
 
 @[simp]
 lemma symm_symmMeasurableEquiv : symmMeasurableEquiv.symm = symmMeasurableEquiv := rfl

Mathlib/MeasureTheory/Group/MeasurableEquiv.lean

@@ -116,8 +116,6 @@ measurable automorphism of `G`. -/
       on the right is a measurable automorphism of `G`. -/]
 def mulRight (g : G) : G ≃ᵐ G where
   toEquiv := Equiv.mulRight g
-  measurable_toFun := measurable_mul_const g
-  measurable_invFun := measurable_mul_const g⁻¹
 
 @[to_additive]
 theorem _root_.measurableEmbedding_mulRight (g : G) : MeasurableEmbedding fun x => x * g :=
@@ -159,8 +157,6 @@ theorem toEquiv_mulLeft₀ {g : G₀} (hg : g ≠ 0) : (mulLeft₀ g hg).toEquiv
 nonzero element `g : G₀` is a measurable automorphism of `G₀`. -/
 def mulRight₀ (g : G₀) (hg : g ≠ 0) : G₀ ≃ᵐ G₀ where
   toEquiv := Equiv.mulRight₀ g hg
-  measurable_toFun := measurable_mul_const g
-  measurable_invFun := measurable_mul_const g⁻¹
 
 theorem _root_.measurableEmbedding_mulRight₀ {g : G₀} (hg : g ≠ 0) :
     MeasurableEmbedding fun x => x * g :=
@@ -186,8 +182,6 @@ end Mul
     /-- Negation as a measurable automorphism of an additive group. -/]
 def inv (G) [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] : G ≃ᵐ G where
   toEquiv := Equiv.inv G
-  measurable_toFun := measurable_inv
-  measurable_invFun := measurable_inv
 
 @[to_additive (attr := simp)]
 theorem symm_inv {G} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] :

Mathlib/MeasureTheory/Group/Prod.lean

@@ -58,18 +58,14 @@ variable (μ ν : Measure G) [SFinite ν] [SFinite μ] {s : Set G}
 
 /-- The map `(x, y) ↦ (x, xy)` as a `MeasurableEquiv`. -/
 @[to_additive /-- The map `(x, y) ↦ (x, x + y)` as a `MeasurableEquiv`. -/]
-protected def MeasurableEquiv.shearMulRight [MeasurableInv G] : G × G ≃ᵐ G × G :=
-  { Equiv.prodShear (Equiv.refl _) Equiv.mulLeft with
-    measurable_toFun := measurable_fst.prodMk measurable_mul
-    measurable_invFun := measurable_fst.prodMk <| measurable_fst.inv.mul measurable_snd }
+protected def MeasurableEquiv.shearMulRight [MeasurableInv G] : G × G ≃ᵐ G × G where
+  toEquiv := .prodShear (.refl _) .mulLeft
 
 /-- The map `(x, y) ↦ (x, y / x)` as a `MeasurableEquiv` with inverse `(x, y) ↦ (x, yx)` -/
 @[to_additive
 /-- The map `(x, y) ↦ (x, y - x)` as a `MeasurableEquiv` with inverse `(x, y) ↦ (x, y + x)`. -/]
-protected def MeasurableEquiv.shearDivRight [MeasurableInv G] : G × G ≃ᵐ G × G :=
-  { Equiv.prodShear (Equiv.refl _) Equiv.divRight with
-    measurable_toFun := measurable_fst.prodMk <| measurable_snd.div measurable_fst
-    measurable_invFun := measurable_fst.prodMk <| measurable_snd.mul measurable_fst }
+protected def MeasurableEquiv.shearDivRight [MeasurableInv G] : G × G ≃ᵐ G × G where
+  toEquiv := .prodShear (.refl _) .divRight
 
 variable {G}
 

Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

@@ -168,9 +168,9 @@ theorem MeasurableSet.exists_measurable_proj {_ : MeasurableSpace α}
 statements along measurable equivalences. -/
 structure MeasurableEquiv (α β : Type*) [MeasurableSpace α] [MeasurableSpace β] extends α ≃ β where
   /-- The forward function of a measurable equivalence is measurable. -/
-  measurable_toFun : Measurable toEquiv
+  measurable_toFun : Measurable toEquiv := by measurability
   /-- The inverse function of a measurable equivalence is measurable. -/
-  measurable_invFun : Measurable toEquiv.symm
+  measurable_invFun : Measurable toEquiv.symm := by measurability
 
 @[inherit_doc]
 infixl:25 " ≃ᵐ " => MeasurableEquiv
@@ -206,8 +206,6 @@ theorem coe_mk (e : α ≃ β) (h1 : Measurable e) (h2 : Measurable e.symm) :
 /-- Any measurable space is equivalent to itself. -/
 def refl (α : Type*) [MeasurableSpace α] : α ≃ᵐ α where
   toEquiv := Equiv.refl α
-  measurable_toFun := measurable_id
-  measurable_invFun := measurable_id
 
 instance instInhabited : Inhabited (α ≃ᵐ α) := ⟨refl α⟩
 
@@ -223,7 +221,6 @@ theorem coe_trans (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) : ⇑(ab.trans bc) = b
 def symm (ab : α ≃ᵐ β) : β ≃ᵐ α where
   toEquiv := ab.toEquiv.symm
   measurable_toFun := ab.measurable_invFun
-  measurable_invFun := ab.measurable_toFun
 
 @[simp]
 theorem coe_toEquiv_symm (e : α ≃ᵐ β) : (e.toEquiv.symm : β → α) = e.symm :=
@@ -338,14 +335,6 @@ protected theorem measurableEmbedding (e : α ≃ᵐ β) : MeasurableEmbedding e
 protected def cast {α β} [i₁ : MeasurableSpace α] [i₂ : MeasurableSpace β] (h : α = β)
     (hi : i₁ ≍ i₂) : α ≃ᵐ β where
   toEquiv := Equiv.cast h
-  measurable_toFun := by
-    subst h
-    subst hi
-    exact measurable_id
-  measurable_invFun := by
-    subst h
-    subst hi
-    exact measurable_id
 
 /-- Measurable equivalence between `ULift α` and `α`. -/
 def ulift.{u, v} {α : Type u} [MeasurableSpace α] : ULift.{v, u} α ≃ᵐ α :=
@@ -363,43 +352,29 @@ protected theorem measurable_comp_iff {f : β → γ} (e : α ≃ᵐ β) :
 def ofUniqueOfUnique (α β : Type*) [MeasurableSpace α] [MeasurableSpace β] [Unique α] [Unique β] :
     α ≃ᵐ β where
   toEquiv := ofUnique α β
-  measurable_toFun := Subsingleton.measurable
-  measurable_invFun := Subsingleton.measurable
 
 variable [MeasurableSpace δ] in
 /-- Products of equivalent measurable spaces are equivalent. -/
 def prodCongr (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) : α × γ ≃ᵐ β × δ where
   toEquiv := .prodCongr ab.toEquiv cd.toEquiv
-  measurable_toFun :=
-    (ab.measurable_toFun.comp measurable_id.fst).prodMk
-      (cd.measurable_toFun.comp measurable_id.snd)
-  measurable_invFun :=
-    (ab.measurable_invFun.comp measurable_id.fst).prodMk
-      (cd.measurable_invFun.comp measurable_id.snd)
 
 /-- Products of measurable spaces are symmetric. -/
 def prodComm : α × β ≃ᵐ β × α where
   toEquiv := .prodComm α β
-  measurable_toFun := measurable_id.snd.prodMk measurable_id.fst
-  measurable_invFun := measurable_id.snd.prodMk measurable_id.fst
 
 /-- Products of measurable spaces are associative. -/
 def prodAssoc : (α × β) × γ ≃ᵐ α × β × γ where
   toEquiv := .prodAssoc α β γ
-  measurable_toFun := measurable_fst.fst.prodMk <| measurable_fst.snd.prodMk measurable_snd
-  measurable_invFun := (measurable_fst.prodMk measurable_snd.fst).prodMk measurable_snd.snd
 
 /-- `PUnit` is a left identity for product of measurable spaces up to a measurable equivalence. -/
 def punitProd : PUnit × α ≃ᵐ α where
   toEquiv := Equiv.punitProd α
   measurable_toFun := measurable_snd
-  measurable_invFun := measurable_prodMk_left
 
 /-- `PUnit` is a right identity for product of measurable spaces up to a measurable equivalence. -/
 def prodPUnit : α × PUnit ≃ᵐ α where
   toEquiv := Equiv.prodPUnit α
   measurable_toFun := measurable_fst
-  measurable_invFun := measurable_prodMk_right
 
 variable [MeasurableSpace δ] in
 /-- Sums of measurable spaces are symmetric. -/
@@ -411,8 +386,6 @@ def sumCongr (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) : α ⊕ γ ≃ᵐ β ⊕ 
 /-- `s ×ˢ t ≃ (s × t)` as measurable spaces. -/
 def Set.prod (s : Set α) (t : Set β) : ↥(s ×ˢ t) ≃ᵐ s × t where
   toEquiv := Equiv.Set.prod s t
-  measurable_toFun :=
-    measurable_id.subtype_val.fst.subtype_mk.prodMk measurable_id.subtype_val.snd.subtype_mk
   measurable_invFun :=
     Measurable.subtype_mk <| measurable_id.fst.subtype_val.prodMk measurable_id.snd.subtype_val
 
@@ -425,8 +398,6 @@ def Set.univ (α : Type*) [MeasurableSpace α] : (univ : Set α) ≃ᵐ α where
 /-- `{a} ≃ Unit` as measurable spaces. -/
 def Set.singleton (a : α) : ({a} : Set α) ≃ᵐ Unit where
   toEquiv := Equiv.Set.singleton a
-  measurable_toFun := measurable_const
-  measurable_invFun := measurable_const
 
 /-- `α` is equivalent to its image in `α ⊕ β` as measurable spaces. -/
 def Set.rangeInl : (range Sum.inl : Set (α ⊕ β)) ≃ᵐ α where
@@ -489,7 +460,6 @@ variable (π) in
 /-- Moving a dependent type along an equivalence of coordinates, as a measurable equivalence. -/
 def piCongrLeft (f : δ ≃ δ') : (∀ b, π (f b)) ≃ᵐ ∀ a, π a where
   __ := Equiv.piCongrLeft π f
-  measurable_toFun := measurable_piCongrLeft f
   measurable_invFun := by
     rw [measurable_pi_iff]
     exact fun i => measurable_pi_apply (f i)
@@ -538,8 +508,6 @@ variable (π) in
 @[simps! -fullyApplied]
 def piUnique [Unique δ'] : (∀ i, π i) ≃ᵐ π default where
   toEquiv := Equiv.piUnique π
-  measurable_toFun := measurable_pi_apply _
-  measurable_invFun := measurable_uniqueElim
 
 /-- If `α` has a unique term, then the type of function `α → β` is measurably equivalent to `β`. -/
 @[simps! -fullyApplied]
@@ -550,7 +518,6 @@ def funUnique (α β : Type*) [Unique α] [MeasurableSpace β] : (α → β) ≃
 @[simps! -fullyApplied]
 def piFinTwo (α : Fin 2 → Type*) [∀ i, MeasurableSpace (α i)] : (∀ i, α i) ≃ᵐ α 0 × α 1 where
   toEquiv := piFinTwoEquiv α
-  measurable_toFun := Measurable.prod (measurable_pi_apply _) (measurable_pi_apply _)
   measurable_invFun := measurable_pi_iff.2 <| Fin.forall_fin_two.2 ⟨measurable_fst, measurable_snd⟩
 
 /-- The space `Fin 2 → α` is measurably equivalent to `α × α`. -/
@@ -579,16 +546,12 @@ variable (π)
 def piEquivPiSubtypeProd (p : δ' → Prop) [DecidablePred p] :
     (∀ i, π i) ≃ᵐ (∀ i : Subtype p, π i) × ∀ i : { i // ¬p i }, π i where
   toEquiv := .piEquivPiSubtypeProd p π
-  measurable_toFun := measurable_piEquivPiSubtypeProd π p
-  measurable_invFun := measurable_piEquivPiSubtypeProd_symm π p
 
 /-- The measurable equivalence between the pi type over a sum type and a product of pi-types.
 This is similar to `MeasurableEquiv.piEquivPiSubtypeProd`. -/
 def sumPiEquivProdPi (α : δ ⊕ δ' → Type*) [∀ i, MeasurableSpace (α i)] :
     (∀ i, α i) ≃ᵐ (∀ i, α (.inl i)) × ∀ i', α (.inr i') where
   __ := Equiv.sumPiEquivProdPi α
-  measurable_toFun := by
-    apply Measurable.prod <;> rw [measurable_pi_iff] <;> rintro i <;> apply measurable_pi_apply
   measurable_invFun := by
     rw [measurable_pi_iff]; rintro (i | i)
     · exact measurable_pi_iff.1 measurable_fst _
@@ -637,8 +600,6 @@ def sumCompl {s : Set α} [DecidablePred (· ∈ s)] (hs : MeasurableSet s) :
 @[simps toEquiv]
 def ofInvolutive (f : α → α) (hf : Involutive f) (hf' : Measurable f) : α ≃ᵐ α where
   toEquiv := hf.toPerm
-  measurable_toFun := hf'
-  measurable_invFun := hf'
 
 @[simp] theorem ofInvolutive_apply (f : α → α) (hf : Involutive f) (hf' : Measurable f) (a : α) :
     ofInvolutive f hf hf' a = f a := rfl
@@ -651,8 +612,6 @@ def ofInvolutive (f : α → α) (hf : Involutive f) (hf' : Measurable f) : α 
 protected def setOf {α : Type*} : (α → Prop) ≃ᵐ Set α where
   toFun p := {a | p a}
   invFun s a := a ∈ s
-  measurable_toFun := measurable_id
-  measurable_invFun := measurable_id
 
 @[simp, norm_cast] lemma coe_setOf {α : Type*} : ⇑MeasurableEquiv.setOf = setOf (α := α) := rfl
 
@@ -812,8 +771,6 @@ def piCurry {ι : Type*} {κ : ι → Type*} (X : (i : ι) → κ i → Type*)
     [∀ i j, MeasurableSpace (X i j)] :
     ((p : (i : ι) × κ i) → X p.1 p.2) ≃ᵐ ((i : ι) → (j : κ i) → X i j) where
   toEquiv := Equiv.piCurry X
-  measurable_toFun := by fun_prop
-  measurable_invFun := by fun_prop
 
 lemma coe_piCurry {ι : Type*} {κ : ι → Type*} (X : (i : ι) → κ i → Type*)
     [∀ i j, MeasurableSpace (X i j)] : ⇑(piCurry X) = Sigma.curry := rfl
@@ -826,8 +783,6 @@ See `MeasurableEquiv.piCurry` for the dependent version. -/
 @[simps!]
 def curry (ι κ X : Type*) [MeasurableSpace X] : (ι × κ → X) ≃ᵐ (ι → κ → X) where
   toEquiv := Equiv.curry ι κ X
-  measurable_toFun := by fun_prop
-  measurable_invFun := by fun_prop
 
 lemma coe_curry (ι κ X : Type*) [MeasurableSpace X] : ⇑(curry ι κ X) = Function.curry := rfl
 

Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

@@ -34,10 +34,7 @@ namespace LinearIsometryEquiv
 variable (f : E ≃ₗᵢ[ℝ] F)
 
 /-- Every linear isometry equivalence is a measurable equivalence. -/
-def toMeasurableEquiv : E ≃ᵐ F where
-  toEquiv := f
-  measurable_toFun := f.continuous.measurable
-  measurable_invFun := f.symm.continuous.measurable
+def toMeasurableEquiv : E ≃ᵐ F := f.toHomeomorph.toMeasurableEquiv
 
 @[simp] theorem coe_toMeasurableEquiv : (f.toMeasurableEquiv : E → F) = f := rfl
 

Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean

@@ -212,9 +212,7 @@ lemma ext_of_integral_prod_mul_boundedContinuousFunction {μ ν : Measure ((Π i
     { toFun p := ⟨fun i ↦ p.1 i, fun _ ↦ p.2⟩
       invFun p := ⟨fun i ↦ p.1 i, p.2 ()⟩
       left_inv p := by simp
-      right_inv p := by simp
-      measurable_toFun := by simp; fun_prop
-      measurable_invFun := by simp; fun_prop }
+      right_inv p := by simp }
   rw [← e.map_measurableEquiv_injective.eq_iff]
   refine ext_of_integral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_
   rw [integral_map_equiv, integral_map_equiv]
@@ -233,10 +231,7 @@ lemma ext_of_integral_mul_prod_boundedContinuousFunction {μ ν : Measure (Z ×
     (h : ∀ (f : Z →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
       ∫ p, f p.1 * ∏ j, g j (p.2 j) ∂μ = ∫ p, f p.1 * ∏ j, g j (p.2 j) ∂ν) :
     μ = ν := by
-  let e : (Z × (Π i, Y i)) ≃ᵐ ((Π i, Y i) × Z) :=
-    { toEquiv := Equiv.prodComm _ _
-      measurable_toFun := measurable_swap
-      measurable_invFun := measurable_swap }
+  let e : (Z × (Π i, Y i)) ≃ᵐ ((Π i, Y i) × Z) := .prodComm
   rw [← e.map_measurableEquiv_injective.eq_iff]
   refine ext_of_integral_prod_mul_boundedContinuousFunction fun f g ↦ ?_
   rw [integral_map_equiv, integral_map_equiv]
@@ -258,12 +253,7 @@ lemma ext_of_integral_mul_boundedContinuousFunction {μ ν : Measure (Z × T)}
     (h : ∀ (f : Z →ᵇ ℝ) (g : T →ᵇ ℝ), ∫ p, f p.1 * g p.2 ∂μ = ∫ p, f p.1 * g p.2 ∂ν) :
     μ = ν := by
   let e : (Z × T) ≃ᵐ ((Unit → Z) × (Unit → T)) :=
-    { toFun p := ⟨fun _ ↦ p.1, fun _ ↦ p.2⟩
-      invFun p := ⟨p.1 (), p.2 ()⟩
-      left_inv p := by simp
-      right_inv p := by simp
-      measurable_toFun := by simp; fun_prop
-      measurable_invFun := by simp; fun_prop }
+    .symm <| .prodCongr (.funUnique ..) (.funUnique ..)
   rw [← e.map_measurableEquiv_injective.eq_iff]
   refine ext_of_integral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_
   rw [integral_map_equiv, integral_map_equiv]

Mathlib/Probability/Kernel/IonescuTulcea/Maps.lean

@@ -107,7 +107,6 @@ def IicProdIoc {a b : ι} (hab : a ≤ b) :
     by_cases h : x ≤ a
     · simpa [h] using measurable_fst.eval
     · simpa [h] using measurable_snd.eval
-  measurable_invFun := by dsimp; fun_prop
 
 lemma coe_IicProdIoc {a b : ι} (hab : a ≤ b) :
     ⇑(IicProdIoc (X := X) hab) = _root_.IicProdIoc a b := rfl
@@ -134,7 +133,6 @@ def IicProdIoi (a : ι) :
     by_cases hi : i ≤ a <;> simp only [Equiv.coe_fn_mk, hi, ↓reduceDIte]
     · exact measurable_fst.eval
     · exact measurable_snd.eval
-  measurable_invFun := Measurable.prodMk (measurable_restrict _) (Set.measurable_restrict _)
 
 end MeasurableEquiv
 
@@ -154,7 +152,6 @@ def MeasurableEquiv.piSingleton (a : ℕ) : X (a + 1) ≃ᵐ Π i : Ioc a (a + 1
     simp_rw [eqRec_eq_cast]
     refine measurable_pi_lambda _ (fun i ↦ (MeasurableEquiv.cast _ ?_).measurable)
     cases Nat.mem_Ioc_succ' i; rfl
-  measurable_invFun := measurable_pi_apply _
 
 end Nat