feat(MeasureTheory): mass of count.real (leanprover-community#40367)

From MeanFourier

Author: YaelDillies

Mathlib.lean

@@ -7148,6 +7148,7 @@ public import Mathlib.SetTheory.Cardinal.Continuum
 public import Mathlib.SetTheory.Cardinal.CountableCover
 public import Mathlib.SetTheory.Cardinal.Defs
 public import Mathlib.SetTheory.Cardinal.Divisibility
+public import Mathlib.SetTheory.Cardinal.ENNReal
 public import Mathlib.SetTheory.Cardinal.ENat
 public import Mathlib.SetTheory.Cardinal.Embedding
 public import Mathlib.SetTheory.Cardinal.EventuallyConst

Mathlib/Data/Real/ENatENNReal.lean

@@ -87,6 +87,8 @@ theorem toENNReal_strictMono : StrictMono ((↑) : ℕ∞ → ℝ≥0∞) :=
 theorem toENNReal_zero : ((0 : ℕ∞) : ℝ≥0∞) = 0 :=
   map_zero toENNRealRingHom
 
+@[simp] lemma toENNReal_eq_zero : toENNReal n = 0 ↔ n = 0 := by rw [← toENNReal_zero, toENNReal_inj]
+
 @[simp, norm_cast]
 theorem toENNReal_add (m n : ℕ∞) : ↑(m + n) = (m + n : ℝ≥0∞) :=
   map_add toENNRealRingHom m n

Mathlib/MeasureTheory/Measure/Count.lean

@@ -7,6 +7,8 @@ module
 
 public import Mathlib.MeasureTheory.Measure.Dirac
 
+import Mathlib.SetTheory.Cardinal.ENNReal
+
 /-!
 # Counting measure
 
@@ -162,6 +164,11 @@ instance count.isFiniteMeasure [Finite α] :
 @[simp]
 lemma count_univ : count (univ : Set α) = ENat.card α := by simp [count_apply .univ, encard_univ]
 
+@[simp] lemma count_real_univ : count.real (.univ : Set α) = Nat.card α := by simp [Measure.real]
+
+instance neZero_count [Nonempty α] : NeZero (count : Measure α) where
+  out := by rintro h; simpa using congr($h .univ)
+
 lemma _root_.Subsingleton.count_eq_dirac [Subsingleton α] (i : α) :
     count = dirac i := by
   calc count

Mathlib/RingTheory/Length.lean

@@ -264,9 +264,7 @@ lemma Module.length_of_free [Module.Free R M] :
   nontriviality R
   nontriviality M
   by_cases H : Module.length R R = ⊤
-  · rw [b.repr.length_eq, Module.length_finsupp, H, ENat.mul_top', ENat.mul_top']
-    congr 1
-    simp [ENat.card_eq_zero_iff_empty, rank_pos_of_free.ne']
+  · simp [b.repr.length_eq, H, rank_pos_of_free.ne']
   rw [← ne_eq, Module.length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian] at H
   cases H
   let b := Module.Free.chooseBasis R M

Mathlib/SetTheory/Cardinal/ENNReal.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2026 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+module
+
+public import Mathlib.Data.Real.ENatENNReal
+public import Mathlib.SetTheory.Cardinal.NatCard
+
+/-!
+# Lemmas about `Nat.card` and `ENNReal`
+-/
+
+public section
+
+namespace ENNReal
+
+@[simp] lemma toReal_enatCard (α : Type*) : ENNReal.toReal (ENat.card α) = Nat.card α := by
+  cases finite_or_infinite α <;> simp [ENat.card_eq_coe_natCard]
+
+end ENNReal

Mathlib/SetTheory/Cardinal/Finite.lean

@@ -352,14 +352,15 @@ theorem card_eq_zero_iff_empty (α : Type*) : card α = 0 ↔ IsEmpty α := by
 theorem card_ne_zero_iff_nonempty (α : Type*) : card α ≠ 0 ↔ Nonempty α := by
   simp [card_eq_zero_iff_empty]
 
+@[simp] lemma card_ne_zero [Nonempty α] : card α ≠ 0 := (card_ne_zero_iff_nonempty _).2 ‹_›
+
 theorem card_pos_iff_nonempty (α : Type*) : 0 < card α ↔ Nonempty α := by
   rw [pos_iff_ne_zero, card_ne_zero_iff_nonempty]
 
 theorem one_le_card_iff_nonempty (α : Type*) : 1 ≤ card α ↔ Nonempty α := by
   simp [Order.one_le_iff_ne_zero, card_eq_zero_iff_empty]
 
-@[simp] lemma card_pos [Nonempty α] : 0 < card α := by
-  simpa [pos_iff_ne_zero, card_ne_zero_iff_nonempty]
+@[simp] lemma card_pos [Nonempty α] : 0 < card α := by simp [pos_iff_ne_zero]
 
 theorem card_le_one_iff_subsingleton (α : Type*) : card α ≤ 1 ↔ Subsingleton α := by
   rw [← le_one_iff_subsingleton]