From 7596552e8c9fea2beea53078ffc9d20db44e4d11 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 4 Oct 2024 15:49:06 +0000
Subject: [PATCH] chore: make `Integrable.of_finite` have no explicit argument
 (#17323)

This makes it really useful to fill in side conditions on the fly using anonymous dot notation. Also deprecate `Integrable.of_isEmpty` which is straightforwardly a special case of it (see eg `stronglyMeasurable_of_isEmpty` for a similar existing deprecation).

From PFR
---
 Mathlib/MeasureTheory/Function/L1Space.lean           | 11 ++++++-----
 .../Function/StronglyMeasurable/Basic.lean            |  6 +++---
 .../ProbabilityMassFunction/Integrals.lean            |  2 +-
 3 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/Mathlib/MeasureTheory/Function/L1Space.lean b/Mathlib/MeasureTheory/Function/L1Space.lean
index 9fb75e137b6c08..9994ae4d6e8b10 100644
--- a/Mathlib/MeasureTheory/Function/L1Space.lean
+++ b/Mathlib/MeasureTheory/Function/L1Space.lean
@@ -438,12 +438,13 @@ theorem integrable_const [IsFiniteMeasure μ] (c : β) : Integrable (fun _ : α
   integrable_const_iff.2 <| Or.inr <| measure_lt_top _ _
 
 @[simp]
-theorem Integrable.of_finite [Finite α] [MeasurableSpace α] [MeasurableSingletonClass α]
-    (μ : Measure α) [IsFiniteMeasure μ] (f : α → β) : Integrable (fun a ↦ f a) μ :=
-  ⟨(StronglyMeasurable.of_finite f).aestronglyMeasurable, .of_finite⟩
+lemma Integrable.of_finite [Finite α] [MeasurableSingletonClass α] [IsFiniteMeasure μ] {f : α → β} :
+    Integrable f μ := ⟨.of_finite, .of_finite⟩
 
-lemma Integrable.of_isEmpty [IsEmpty α] (f : α → β) (μ : Measure α) :
-    Integrable f μ := Integrable.of_finite μ f
+/-- This lemma is a special case of `Integrable.of_finite`. -/
+-- Eternal deprecation for discoverability, don't remove
+@[deprecated Integrable.of_finite, nolint deprecatedNoSince]
+lemma Integrable.of_isEmpty [IsEmpty α] {f : α → β} : Integrable f μ := .of_finite
 
 @[deprecated (since := "2024-02-05")] alias integrable_of_fintype := Integrable.of_finite
 
diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
index d4eafeb1777277..b9644215bcca28 100644
--- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
+++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
@@ -127,7 +127,7 @@ theorem SimpleFunc.stronglyMeasurable {α β} {_ : MeasurableSpace α} [Topologi
 @[nontriviality]
 theorem StronglyMeasurable.of_finite [Finite α] {_ : MeasurableSpace α}
     [MeasurableSingletonClass α] [TopologicalSpace β]
-    (f : α → β) : StronglyMeasurable f :=
+    {f : α → β} : StronglyMeasurable f :=
   ⟨fun _ => SimpleFunc.ofFinite f, fun _ => tendsto_const_nhds⟩
 
 @[deprecated (since := "2024-02-05")]
@@ -136,7 +136,7 @@ alias stronglyMeasurable_of_fintype := StronglyMeasurable.of_finite
 @[deprecated StronglyMeasurable.of_finite (since := "2024-02-06")]
 theorem stronglyMeasurable_of_isEmpty [IsEmpty α] {_ : MeasurableSpace α} [TopologicalSpace β]
     (f : α → β) : StronglyMeasurable f :=
-  .of_finite f
+  .of_finite
 
 theorem stronglyMeasurable_const {α β} {_ : MeasurableSpace α} [TopologicalSpace β] {b : β} :
     StronglyMeasurable fun _ : α => b :=
@@ -1108,7 +1108,7 @@ variable {m : MeasurableSpace α} {μ ν : Measure α} [TopologicalSpace β] [To
   {f g : α → β}
 
 lemma of_finite [DiscreteMeasurableSpace α] [Finite α] : AEStronglyMeasurable f μ :=
-  ⟨_, .of_finite _, ae_eq_rfl⟩
+  ⟨_, .of_finite, ae_eq_rfl⟩
 
 section Mk
 
diff --git a/Mathlib/Probability/ProbabilityMassFunction/Integrals.lean b/Mathlib/Probability/ProbabilityMassFunction/Integrals.lean
index 0803f711af0ab0..befbc17ee812fc 100644
--- a/Mathlib/Probability/ProbabilityMassFunction/Integrals.lean
+++ b/Mathlib/Probability/ProbabilityMassFunction/Integrals.lean
@@ -42,7 +42,7 @@ theorem integral_eq_tsum (p : PMF α) (f : α → E) (hf : Integrable f p.toMeas
 
 theorem integral_eq_sum [Fintype α] (p : PMF α) (f : α → E) :
     ∫ a, f a ∂(p.toMeasure) = ∑ a, (p a).toReal • f a := by
-  rw [integral_fintype _ (.of_finite _ f)]
+  rw [integral_fintype _ .of_finite]
   congr with x; congr 2
   exact PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)