[Merged by Bors] - chore: tidy various files

Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean

@@ -99,7 +99,7 @@ open Nat
 theorem of_convergence_epsilon :
     ∀ ε > (0 : K), ∃ N : ℕ, ∀ n ≥ N, |v - (of v).convergents n| < ε := by
   intro ε ε_pos
-  -- use the archimedean property to obtian a suitable N
+  -- use the archimedean property to obtain a suitable N
   rcases (exists_nat_gt (1 / ε) : ∃ N' : ℕ, 1 / ε < N') with ⟨N', one_div_ε_lt_N'⟩
   let N := max N' 5
   -- set minimum to 5 to have N ≤ fib N work
@@ -115,7 +115,7 @@ theorem of_convergence_epsilon :
     let nB := g.denominators (n + 1)
     have abs_v_sub_conv_le : |v - g.convergents n| ≤ 1 / (B * nB) :=
       abs_sub_convergents_le not_terminated_at_n
-    suffices : 1 / (B * nB) < ε; exact lt_of_le_of_lt abs_v_sub_conv_le this
+    suffices 1 / (B * nB) < ε from lt_of_le_of_lt abs_v_sub_conv_le this
     -- show that `0 < (B * nB)` and then multiply by `B * nB` to get rid of the division
     have nB_ineq : (fib (n + 2) : K) ≤ nB :=
       haveI : ¬g.TerminatedAt (n + 1 - 1) := not_terminated_at_n
@@ -126,10 +126,10 @@ theorem of_convergence_epsilon :
     have zero_lt_B : 0 < B := B_ineq.trans_lt' $ mod_cast fib_pos.2 n.succ_pos
     have nB_pos : 0 < nB := nB_ineq.trans_lt' $ mod_cast fib_pos.2 $ succ_pos _
     have zero_lt_mul_conts : 0 < B * nB := by positivity
-    suffices : 1 < ε * (B * nB); exact (div_lt_iff zero_lt_mul_conts).mpr this
-    -- use that `N ≥ n` was obtained from the archimedean property to show the following
+    suffices 1 < ε * (B * nB) from (div_lt_iff zero_lt_mul_conts).mpr this
+    -- use that `N' ≥ n` was obtained from the archimedean property to show the following
     calc 1 < ε * (N' : K) := (div_lt_iff' ε_pos).mp one_div_ε_lt_N'
-      _ ≤  ε * (B * nB) := ?_
+      _ ≤ ε * (B * nB) := ?_
     -- cancel `ε`
     gcongr
     calc

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -494,8 +494,7 @@ section
 theorem norm_ofSubsingleton [Subsingleton ι] (i : ι) (f : G →L[𝕜] G') :
     ‖ofSubsingleton 𝕜 G G' i f‖ = ‖f‖ := by
   letI : Unique ι := uniqueOfSubsingleton i
-  simp only [norm_def, ContinuousLinearMap.norm_def, (Equiv.funUnique _ _).symm.surjective.forall,
-    Fintype.prod_subsingleton _ i]; rfl
+  simp [norm_def, ContinuousLinearMap.norm_def, (Equiv.funUnique _ _).symm.surjective.forall]
 
 @[simp]
 theorem nnnorm_ofSubsingleton [Subsingleton ι] (i : ι) (f : G →L[𝕜] G') :

Mathlib/Condensed/Explicit.lean

@@ -21,7 +21,7 @@ We give the following three explicit descriptions of condensed sets:
 * `Condensed.ofSheafStonean`: A finite-product-preserving presheaf on `CompHaus`, satisfying
   `EqualizerCondition`.
 
-The property `EqualizerCondition` is defined in `Mathlib/CategoryTheory/Sites/RegularExtensive`
+The property `EqualizerCondition` is defined in `Mathlib/CategoryTheory/Sites/RegularExtensive.lean`
 and it says that for any effective epi `X ⟶ B` (in this case that is equivalent to being a
 continuous surjection), the presheaf `F` exhibits `F(B)` as the equalizer of the two maps
 `F(X) ⇉ F(X ×_B X)`

Mathlib/FieldTheory/RatFunc.lean

@@ -1284,7 +1284,7 @@ theorem num_denom_mul (x y : RatFunc K) :
 #align ratfunc.num_denom_mul RatFunc.num_denom_mul
 
 theorem num_dvd {x : RatFunc K} {p : K[X]} (hp : p ≠ 0) :
-    num x ∣ p ↔ ∃ (q : K[X]) (_ : q ≠ 0), x = algebraMap _ _ p / algebraMap _ _ q := by
+    num x ∣ p ↔ ∃ q : K[X], q ≠ 0 ∧ x = algebraMap _ _ p / algebraMap _ _ q := by
   constructor
   · rintro ⟨q, rfl⟩
     obtain ⟨_hx, hq⟩ := mul_ne_zero_iff.mp hp

Mathlib/Logic/Equiv/Defs.lean

@@ -630,7 +630,7 @@ def piUnique [Unique α] (β : α → Sort*) : (∀ i, β i) ≃ β default wher
   right_inv x := rfl
 
 /-- If `α` has a unique term, then the type of function `α → β` is equivalent to `β`. -/
-@[simps! (config := .asFn) apply]
+@[simps! (config := .asFn) apply symm_apply]
 def funUnique (α β) [Unique.{u} α] : (α → β) ≃ β := piUnique _
 #align equiv.fun_unique Equiv.funUnique
 #align equiv.fun_unique_apply Equiv.funUnique_apply

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -101,11 +101,11 @@ theorem TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom [TopologicalSp
   borel_eq_generateFrom_of_subbasis hs.eq_generateFrom
 #align topological_space.is_topological_basis.borel_eq_generate_from TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom
 
-theorem isPiSystem_isOpen [TopologicalSpace α] : IsPiSystem (IsOpen : Set α → Prop) :=
+theorem isPiSystem_isOpen [TopologicalSpace α] : IsPiSystem ({ s : Set α | IsOpen s }) :=
   fun _s hs _t ht _ => IsOpen.inter hs ht
 #align is_pi_system_is_open isPiSystem_isOpen
 
-lemma isPiSystem_isClosed [TopologicalSpace α] : IsPiSystem (IsClosed : Set α → Prop) :=
+lemma isPiSystem_isClosed [TopologicalSpace α] : IsPiSystem ({ s : Set α | IsClosed s }) :=
   fun _s hs _t ht _ ↦ IsClosed.inter hs ht
 
 theorem borel_eq_generateFrom_isClosed [TopologicalSpace α] :
@@ -130,7 +130,9 @@ theorem borel_eq_generateFrom_Iio : borel α = .generateFrom (range Iio) := by
     letI : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
     have H : ∀ a : α, MeasurableSet (Iio a) := fun a => GenerateMeasurable.basic _ ⟨_, rfl⟩
     refine' generateFrom_le _
-    rintro _ ⟨a, rfl | rfl⟩ <;> [skip; apply H]
+    rintro _ ⟨a, rfl | rfl⟩
+    swap
+    · apply H
     by_cases h : ∃ a', ∀ b, a < b ↔ a' ≤ b
     · rcases h with ⟨a', ha'⟩
       rw [(_ : Ioi a = (Iio a')ᶜ)]
@@ -149,7 +151,6 @@ theorem borel_eq_generateFrom_Iio : borel α = .generateFrom (range Iio) := by
             ⟨fun ab => le_of_not_lt fun h' => h ⟨b, ab, h'⟩, lt_of_lt_of_le ax⟩⟩) with ⟨a', h₁, h₂⟩
         · exact ⟨a', h₁, le_of_lt h₂⟩
       rw [this]
-      skip
       apply MeasurableSet.iUnion
       exact fun _ => (H _).compl
   · rw [forall_range_iff]
@@ -1270,7 +1271,7 @@ protected theorem Monotone.measurable [LinearOrder β] [OrderClosedTopology β]
 theorem aemeasurable_restrict_of_monotoneOn [LinearOrder β] [OrderClosedTopology β] {μ : Measure β}
     {s : Set β} (hs : MeasurableSet s) {f : β → α} (hf : MonotoneOn f s) :
     AEMeasurable f (μ.restrict s) :=
-  have : Monotone (f ∘ (↑) : s → α) := fun ⟨x, hx⟩ ⟨y, hy⟩=> fun (hxy : x ≤ y) => hf hx hy hxy
+  have : Monotone (f ∘ (↑) : s → α) := fun ⟨x, hx⟩ ⟨y, hy⟩ => fun (hxy : x ≤ y) => hf hx hy hxy
   aemeasurable_restrict_of_measurable_subtype hs this.measurable
 #align ae_measurable_restrict_of_monotone_on aemeasurable_restrict_of_monotoneOn
 

Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

@@ -694,7 +694,7 @@ theorem prodAssoc_prod [SFinite τ] :
         (sFiniteSeq μ p.1.1).prod ((sFiniteSeq ν p.1.2).prod (sFiniteSeq τ p.2))) := by
     ext s hs
     rw [sum_apply _ hs, sum_apply _ hs, ← (Equiv.prodAssoc _ _ _).tsum_eq]
-    rfl
+    simp only [Equiv.prodAssoc_apply]
   rw [← sum_sFiniteSeq μ, ← sum_sFiniteSeq ν, ← sum_sFiniteSeq τ, prod_sum, prod_sum,
     map_sum MeasurableEquiv.prodAssoc.measurable.aemeasurable, prod_sum, prod_sum, this]
   congr
@@ -820,8 +820,8 @@ theorem skew_product [SFinite μa] [SFinite μc] {f : α → β} (hf : MeasurePr
     ← hf.lintegral_comp (measurable_measure_prod_mk_left hs)]
   apply lintegral_congr_ae
   filter_upwards [hg] with a ha
-  rw [← ha, map_apply hgm.of_uncurry_left (measurable_prod_mk_left hs)]
-  rfl
+  rw [← ha, map_apply hgm.of_uncurry_left (measurable_prod_mk_left hs), preimage_preimage,
+    preimage_preimage]
 #align measure_theory.measure_preserving.skew_product MeasureTheory.MeasurePreserving.skew_product
 
 /-- If `f : α → β` sends the measure `μa` to `μb` and `g : γ → δ` sends the measure `μc` to `μd`,

Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean

@@ -130,8 +130,7 @@ theorem singularPart_mutuallySingular (s : SignedMeasure α) (μ : Measure α) :
     s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ
       s.toJordanDecomposition.negPart.singularPart μ := by
   by_cases hl : s.HaveLebesgueDecomposition μ
-  · haveI := hl
-    obtain ⟨i, hi, hpos, hneg⟩ := s.toJordanDecomposition.mutuallySingular
+  · obtain ⟨i, hi, hpos, hneg⟩ := s.toJordanDecomposition.mutuallySingular
     rw [s.toJordanDecomposition.posPart.haveLebesgueDecomposition_add μ] at hpos
     rw [s.toJordanDecomposition.negPart.haveLebesgueDecomposition_add μ] at hneg
     rw [add_apply, add_eq_zero_iff] at hpos hneg
@@ -153,16 +152,14 @@ theorem singularPart_totalVariation (s : SignedMeasure α) (μ : Measure α) :
       ⟨s.toJordanDecomposition.posPart.singularPart μ,
         s.toJordanDecomposition.negPart.singularPart μ, singularPart_mutuallySingular s μ⟩ := by
     refine' JordanDecomposition.toSignedMeasure_injective _
-    rw [toSignedMeasure_toJordanDecomposition]
-    rfl
+    rw [toSignedMeasure_toJordanDecomposition, singularPart, JordanDecomposition.toSignedMeasure]
   · rw [totalVariation, this]
 #align measure_theory.signed_measure.singular_part_total_variation MeasureTheory.SignedMeasure.singularPart_totalVariation
 
 nonrec theorem mutuallySingular_singularPart (s : SignedMeasure α) (μ : Measure α) :
     singularPart s μ ⟂ᵥ μ.toENNRealVectorMeasure := by
-  rw [mutuallySingular_ennreal_iff, singularPart_totalVariation]
-  change _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ)
-  rw [VectorMeasure.equivMeasure.right_inv μ]
+  rw [mutuallySingular_ennreal_iff, singularPart_totalVariation,
+    VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure]
   exact (mutuallySingular_singularPart _ _).add_left (mutuallySingular_singularPart _ _)
 #align measure_theory.signed_measure.mutually_singular_singular_part MeasureTheory.SignedMeasure.mutuallySingular_singularPart
 
@@ -208,8 +205,8 @@ variable (s μ)
 /-- **The Lebesgue Decomposition theorem between a signed measure and a measure**:
 Given a signed measure `s` and a σ-finite measure `μ`, there exist a signed measure `t` and a
 measurable and integrable function `f`, such that `t` is mutually singular with respect to `μ`
-and `s = t + μ.with_densityᵥ f`. In this case `t = s.singular_part μ` and
-`f = s.rn_deriv μ`. -/
+and `s = t + μ.withDensityᵥ f`. In this case `t = s.singularPart μ` and
+`f = s.rnDeriv μ`. -/
 theorem singularPart_add_withDensity_rnDeriv_eq [s.HaveLebesgueDecomposition μ] :
     s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s := by
   conv_rhs =>
@@ -239,11 +236,8 @@ theorem jordanDecomposition_add_withDensity_mutuallySingular {f : α → ℝ} (h
     (htμ : t ⟂ᵥ μ.toENNRealVectorMeasure) :
     (t.toJordanDecomposition.posPart + μ.withDensity fun x : α => ENNReal.ofReal (f x)) ⟂ₘ
       t.toJordanDecomposition.negPart + μ.withDensity fun x : α => ENNReal.ofReal (-f x) := by
-  rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff] at htμ
-  change
-    _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ) ∧
-      _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ) at htμ
-  rw [VectorMeasure.equivMeasure.right_inv] at htμ
+  rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff,
+    VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure] at htμ
   exact
     ((JordanDecomposition.mutuallySingular _).add_right
           (htμ.1.mono_ac (refl _) (withDensity_absolutelyContinuous _ _))).add_left
@@ -308,20 +302,17 @@ private theorem eq_singularPart' (t : SignedMeasure α) {f : α → ℝ} (hf : M
     (hfi : Integrable f μ) (htμ : t ⟂ᵥ μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :
     t = s.singularPart μ := by
   have htμ' := htμ
-  rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff] at htμ
-  change
-    _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ) ∧
-      _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ) at htμ
-  rw [VectorMeasure.equivMeasure.right_inv] at htμ
-  · rw [singularPart, ← t.toSignedMeasure_toJordanDecomposition,
-      JordanDecomposition.toSignedMeasure]
-    congr
-    · have hfpos : Measurable fun x => ENNReal.ofReal (f x) := by measurability
-      refine' eq_singularPart hfpos htμ.1 _
-      rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
-    · have hfneg : Measurable fun x => ENNReal.ofReal (-f x) := by measurability
-      refine' eq_singularPart hfneg htμ.2 _
-      rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
+  rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff,
+    VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure] at htμ
+  rw [singularPart, ← t.toSignedMeasure_toJordanDecomposition,
+    JordanDecomposition.toSignedMeasure]
+  congr
+  · have hfpos : Measurable fun x => ENNReal.ofReal (f x) := by measurability
+    refine' eq_singularPart hfpos htμ.1 _
+    rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
+  · have hfneg : Measurable fun x => ENNReal.ofReal (-f x) := by measurability
+    refine' eq_singularPart hfneg htμ.2 _
+    rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
 
 /-- Given a measure `μ`, signed measures `s` and `t`, and a function `f` such that `t` is
 mutually singular with respect to `μ` and `s = t + μ.withDensityᵥ f`, we have
@@ -371,21 +362,22 @@ theorem singularPart_smul_nnreal (s : SignedMeasure α) (μ : Measure α) (r : 
 
 nonrec theorem singularPart_smul (s : SignedMeasure α) (μ : Measure α) (r : ℝ) :
     (r • s).singularPart μ = r • s.singularPart μ := by
-  by_cases hr : 0 ≤ r
-  · lift r to ℝ≥0 using hr
+  cases le_or_lt 0 r with
+  | inl hr =>
+    lift r to ℝ≥0 using hr
     exact singularPart_smul_nnreal s μ r
-  · rw [singularPart, singularPart]
+  | inr hr =>
+    rw [singularPart, singularPart]
     conv_lhs =>
       congr
       · congr
         · rw [toJordanDecomposition_smul_real,
-            JordanDecomposition.real_smul_posPart_neg _ _ (not_le.1 hr), singularPart_smul]
+            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]
       · congr
         · rw [toJordanDecomposition_smul_real,
-            JordanDecomposition.real_smul_negPart_neg _ _ (not_le.1 hr), singularPart_smul]
-    rw [toSignedMeasure_smul, toSignedMeasure_smul, ← neg_sub, ← smul_sub]
-    change -(((-r).toNNReal : ℝ) • (_ : SignedMeasure α)) = _
-    rw [← neg_smul, Real.coe_toNNReal _ (le_of_lt (neg_pos.mpr (not_le.1 hr))), neg_neg]
+            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]
+    rw [toSignedMeasure_smul, toSignedMeasure_smul, ← neg_sub, ← smul_sub, NNReal.smul_def,
+      ← neg_smul, Real.coe_toNNReal _ (le_of_lt (neg_pos.mpr hr)), neg_neg]
 #align measure_theory.signed_measure.singular_part_smul MeasureTheory.SignedMeasure.singularPart_smul
 
 theorem singularPart_add (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ]
@@ -395,8 +387,8 @@ theorem singularPart_add (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebes
     (eq_singularPart _ (s.rnDeriv μ + t.rnDeriv μ)
         ((mutuallySingular_singularPart s μ).add_left (mutuallySingular_singularPart t μ))
         _).symm
-  erw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ)]
-  rw [add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
+  rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), add_assoc,
+    add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
     singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
     singularPart_add_withDensity_rnDeriv_eq]
 #align measure_theory.signed_measure.singular_part_add MeasureTheory.SignedMeasure.singularPart_add
@@ -417,7 +409,7 @@ theorem eq_rnDeriv (t : SignedMeasure α) (f : α → ℝ) (hfi : Integrable f 
   have hadd' : s = t + μ.withDensityᵥ f' := by
     convert hadd using 2
     exact WithDensityᵥEq.congr_ae hfi.1.ae_eq_mk.symm
-  haveI := haveLebesgueDecomposition_mk μ hfi.1.measurable_mk htμ hadd'
+  have := haveLebesgueDecomposition_mk μ hfi.1.measurable_mk htμ hadd'
   refine' (Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) hfi _).symm
   rw [← add_right_inj t, ← hadd, eq_singularPart _ f htμ hadd,
     singularPart_add_withDensity_rnDeriv_eq]
@@ -437,11 +429,9 @@ theorem rnDeriv_smul (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDec
   refine'
     Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
       ((integrable_rnDeriv _ _).smul r) _
-  change _ = μ.withDensityᵥ ((r : ℝ) • s.rnDeriv μ)
-  rw [withDensityᵥ_smul (rnDeriv s μ) (r : ℝ), ← add_right_inj ((r • s).singularPart μ),
-    singularPart_add_withDensity_rnDeriv_eq, singularPart_smul]
-  change _ = _ + r • _
-  rw [← smul_add, singularPart_add_withDensity_rnDeriv_eq]
+  rw [withDensityᵥ_smul (rnDeriv s μ) r, ← add_right_inj ((r • s).singularPart μ),
+    singularPart_add_withDensity_rnDeriv_eq, singularPart_smul, ← smul_add,
+    singularPart_add_withDensity_rnDeriv_eq]
 #align measure_theory.signed_measure.rn_deriv_smul MeasureTheory.SignedMeasure.rnDeriv_smul
 
 theorem rnDeriv_add (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ]

Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean

@@ -210,10 +210,11 @@ theorem measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure {Ω : Type
     (h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ x, f x ∂μ = ∫⁻ x, f x ∂ν) {F : Set Ω} (F_closed : IsClosed F) :
     μ F = ν F := by
   have ν_finite : IsFiniteMeasure ν := by
+    constructor
     have whole := h 1
     simp only [BoundedContinuousFunction.coe_one, Pi.one_apply, coe_one, lintegral_const, one_mul]
       at whole
-    refine ⟨by simpa [← whole] using IsFiniteMeasure.measure_univ_lt_top⟩
+    simpa [← whole] using IsFiniteMeasure.measure_univ_lt_top
   have obs_μ := HasOuterApproxClosed.tendsto_lintegral_apprSeq F_closed μ
   have obs_ν := HasOuterApproxClosed.tendsto_lintegral_apprSeq F_closed ν
   simp_rw [h] at obs_μ
@@ -231,7 +232,6 @@ theorem ext_of_forall_lintegral_eq_of_IsFiniteMeasure {Ω : Type*}
   · exact fun F F_closed ↦ key F_closed
   · exact key isClosed_univ
   · rw [BorelSpace.measurable_eq (α := Ω), borel_eq_generateFrom_isClosed]
-    rfl
 
 end MeasureTheory -- namespace
 

Mathlib/MeasureTheory/Measure/VectorMeasure.lean

@@ -521,17 +521,26 @@ theorem ennrealToMeasure_apply {m : MeasurableSpace α} {v : VectorMeasure α 
   rw [ennrealToMeasure, ofMeasurable_apply _ hs]
 #align measure_theory.vector_measure.ennreal_to_measure_apply MeasureTheory.VectorMeasure.ennrealToMeasure_apply
 
+@[simp]
+theorem _root_.MeasureTheory.Measure.toENNRealVectorMeasure_ennrealToMeasure
+    (μ : VectorMeasure α ℝ≥0∞) :
+    toENNRealVectorMeasure (ennrealToMeasure μ) = μ := ext fun s hs => by
+  rw [toENNRealVectorMeasure_apply_measurable hs, ennrealToMeasure_apply hs]
+
+@[simp]
+theorem ennrealToMeasure_toENNRealVectorMeasure (μ : Measure α) :
+    ennrealToMeasure (toENNRealVectorMeasure μ) = μ := Measure.ext fun s hs => by
+  rw [ennrealToMeasure_apply hs, toENNRealVectorMeasure_apply_measurable hs]
+
 /-- The equiv between `VectorMeasure α ℝ≥0∞` and `Measure α` formed by
 `MeasureTheory.VectorMeasure.ennrealToMeasure` and
 `MeasureTheory.Measure.toENNRealVectorMeasure`. -/
 @[simps]
 def equivMeasure [MeasurableSpace α] : VectorMeasure α ℝ≥0∞ ≃ Measure α where
   toFun := ennrealToMeasure
   invFun := toENNRealVectorMeasure
-  left_inv _ := ext fun s hs => by
-    rw [toENNRealVectorMeasure_apply_measurable hs, ennrealToMeasure_apply hs]
-  right_inv _ := Measure.ext fun s hs => by
-    rw [ennrealToMeasure_apply hs, toENNRealVectorMeasure_apply_measurable hs]
+  left_inv := toENNRealVectorMeasure_ennrealToMeasure
+  right_inv := ennrealToMeasure_toENNRealVectorMeasure
 #align measure_theory.vector_measure.equiv_measure MeasureTheory.VectorMeasure.equivMeasure
 
 end