NNReal.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 981 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

64 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Carleson.ToMathlib.MeasureTheory.Integral.Lebesgue

Imported by 5 files

instance NNReal.MeasureSpace line 10 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, NNReal
Proof uses: MeasureTheory.MeasureSpace.mk, MeasureTheory.Measure.comap, Real, LE.le, OfNat.ofNat, MeasureTheory.MeasureSpace.volume
7 instances, coercions and auxiliary constants left out.
lemma NNReal.volume_val line 16 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, NNReal, Eq, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Real, Set.image, Subtype, LE.le, OfNat.ofNat
Proof uses: comap_subtype_coe_apply, Set.Ici, measurableSet_Ici
25 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
example (example at line 20) line 20 source
Source comment
sanity check: this measure is what you expect
```
example : volume (Ioo (3 : ℝ≥0) 5) = 2 := by
…
```
instance (instance at line 27) line 27 source
lemma ENNReal.ofNNReal_preimage TODO: move these lemmas somewhere else? line 31 source
Source comment
TODO: move these lemmas somewhere else?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, ENNReal, Eq, NNReal, Set.preimage, Set.image, ENNReal.toNNReal, SDiff.sdiff, Singleton.singleton, Top.top
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, Not, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, Exists.intro, True, False, not_false_eq_true, and_true, eq_self and 4 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma ENNReal.ofNNReal_preimage {s : Set ℝ≥0∞} :
    ENNReal.ofNNReal ⁻¹' s = ENNReal.toNNReal '' (s \ {⊤}) := by
…
```
Mentions: s
lemma ENNReal.map_toReal_eq_map_toReal_comap_ofReal TODO: move these lemmas somewhere else? line 44 source
Source comment
TODO: move these lemmas somewhere else?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, ENNReal, Not, Membership.mem, Top.top, Eq, Real, Set.image, ENNReal.toReal, NNReal, Set.preimage
Proof uses: Eq.mpr, ENNReal.toNNReal, SDiff.sdiff, Singleton.singleton, id, congrArg, ENNReal.ofNNReal_preimage, Set.image_image, Set.sdiff_singleton_eq_self, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma ENNReal.map_toReal_eq_map_toReal_comap_ofReal {s : Set ℝ≥0∞} (h : ∞ ∉ s) :
    ENNReal.toReal '' s = NNReal.toReal '' (ENNReal.ofNNReal ⁻¹' s) := by
…
```
Mentions: s
lemma ENNReal.map_toReal_eq_map_toReal_comap_ofReal' line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, ENNReal, Membership.mem, Top.top, Eq, Real, Set.image, ENNReal.toReal, Union.union, NNReal, Set.preimage, Singleton.singleton, OfNat.ofNat
Proof uses: Set.ext, Eq.mpr, Iff, Exists, And, id, congrFun', congrArg, Iff.intro, dite, Eq.symm, of_eq_true, Eq.trans, Or, True, Insert.insert, Set.union_singleton, congr, eq_self, funext and 8 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.map_toReal_ae_eq_map_toReal_comap_ofReal line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, ENNReal, Filter.EventuallyEq, Real, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Set.image, ENNReal.toReal, NNReal, Set.preimage
Proof uses: dite, Membership.mem, Top.top, Classical.propDecidable, Eq.mpr, Union.union, Singleton.singleton, OfNat.ofNat, id, Eq, congrArg, ENNReal.map_toReal_eq_map_toReal_comap_ofReal', Insert.insert, Set.union_singleton, MeasureTheory.insert_ae_eq_self, Not, ENNReal.map_toReal_eq_map_toReal_comap_ofReal, Filter.EventuallyEq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.volume_val line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, ENNReal, MeasurableSet, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Real, Set.image, ENNReal.toReal
Proof uses: Trans.trans, NNReal, Set.preimage, rfl, MeasureTheory.Measure.map_apply_of_aemeasurable, AEMeasurable.coe_nnreal_ennreal, aemeasurable_id, NNReal.volume_val, Eq.symm, MeasureTheory.measure_congr, ENNReal.map_toReal_ae_eq_map_toReal_comap_ofReal
18 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
instance (instance at line 85) line 85 source
lemma Measure.Subtype.noAtoms TODO: move this general result to an appropriate place TODO: maybe generalize further to general measures restricted to a subtype line 93 source
Source comment
TODO: move this general result to an appropriate place TODO: maybe generalize further to general measures restricted to a subtype

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasureTheory.NullSingletonClass, MeasureTheory.MeasureSpace.volume, MeasurableSet, Subtype, MeasureTheory.Measure.Subtype.measureSpace
Proof uses: MeasureTheory.NullSingletonClass.mk, Trans.trans, ENNReal, Eq, MeasureTheory.Measure, Set, Singleton.singleton, Set.image, OfNat.ofNat, rfl, comap_subtype_coe_apply, of_eq_true, Eq.trans, True, congrFun', congrArg, Set.image_singleton, MeasureTheory.NullSingletonClass.measure_singleton, eq_self
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma Measure.Subtype.noAtoms {δ : Type*} [MeasureSpace δ] [NullSingletonClass (volume : Measure δ)]
    {p : δ → Prop} (hp : MeasurableSet p) :
    NullSingletonClass (Measure.Subtype.measureSpace.volume : Measure (Subtype p)) where
…
```
instance (instance at line 104) line 104 source
lemma Measure.Subtype.sigmaFinite TODO: move this general result to an appropriate place TODO: maybe generalize further to general measures restricted to a subtype line 108 source
Source comment
TODO: move this general result to an appropriate place TODO: maybe generalize further to general measures restricted to a subtype

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasureTheory.SigmaFinite, MeasureTheory.MeasureSpace.volume, MeasurableSet, Subtype, MeasureTheory.Measure.Subtype.measureSpace
Proof uses: MeasureTheory.SigmaFinite.mk, Nonempty.intro, MeasureTheory.Measure.FiniteSpanningSetsIn, Set.univ, Set, Classical.choice, Eq.mp, Nonempty, congrArg, propext, MeasureTheory.sigmaFinite_iff, Nat, Membership.mem, LT.lt, ENNReal, MeasureTheory.Measure, Top.top, Eq, Set.iUnion, Set.preimage and 21 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma Measure.Subtype.sigmaFinite {δ : Type*} [MeasureSpace δ] [sf : SigmaFinite (@volume δ _)] {p : δ → Prop} (hp : MeasurableSet p) :
    SigmaFinite (Measure.Subtype.measureSpace.volume : Measure (Subtype p)) where
…
```
instance (instance at line 132) line 132 source
lemma measurableEmbedding_ofNNReal TODO: move? line 135 source
Source comment
TODO: move?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableEmbedding, NNReal, ENNReal
Proof uses: MeasurableEmbedding.of_measurable_inverse, ENNReal.toNNReal, measurable_coe_nnreal_ennreal, Eq.mpr, MeasurableSet, Set.range, Set.Iio, Top.top, id, Eq, congrArg, Set, ENNReal.range_coe', measurableSet_Iio, ENNReal.measurable_toNNReal, Function.RightInverse.leftInverse, congrFun, rfl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma measurableEmbedding_ofNNReal : MeasurableEmbedding ENNReal.ofNNReal := by
…
```
instance (instance at line 142) line 142 source
lemma NNReal.volume_eq_volume_ennreal line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, NNReal, MeasurableSet, ENNReal, Set.image, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume
Proof uses: Eq.mpr, Real, ENNReal.toReal, id, congrArg, ENNReal.volume_val, Subtype, LE.le, OfNat.ofNat, NNReal.volume_val, eq_of_heq, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Eq.symm, Set.image_image
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem NNReal.smul_map_volume_mul_left line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Ne, OfNat.ofNat, Eq, MeasureTheory.Measure, HSMul.hSMul, ENNReal, MeasureTheory.Measure.map, HMul.hMul, MeasureTheory.MeasureSpace.volume
Proof uses: MeasureTheory.Measure.ext, Set, MeasurableSet, Eq.mpr, Real, Set.image, Subtype, LE.le, id, congrArg, NNReal.volume_val, ENNReal.ofReal, abs, Eq.symm, Real.smul_map_volume_mul_left, Not, congr, congrFun', Eq.trans, NNReal.abs_eq and 37 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
theorem NNReal.map_volume_mul_left line 177 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Ne, OfNat.ofNat, Eq, MeasureTheory.Measure, MeasureTheory.Measure.map, HMul.hMul, MeasureTheory.MeasureSpace.volume, HSMul.hSMul, ENNReal, Inv.inv
Proof uses: Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, NNReal.smul_map_volume_mul_left, smul_assoc, smul_eq_mul, inv_mul_cancel₀, MeasureTheory.Measure.ext, Set, MeasurableSet, of_eq_true, True, congrFun', one_smul, eq_self
59 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.volume_eq_volume_preimage line 185 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, ENNReal, MeasurableSet, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Real, Inter.inter, Set.preimage, ENNReal.ofReal, Set.Ici, OfNat.ofNat
Proof uses: Eq.mpr, Set.image, ENNReal.toReal, id, congrArg, ENNReal.volume_val, NNReal, MeasureTheory.measure_congr, ENNReal.map_toReal_ae_eq_map_toReal_comap_ofReal, eq_of_heq, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Set.ext, Iff, Membership.mem, Exists, And and 15 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Ioo_zero_top_ae_eq_univ line 193 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.EventuallyEq, ENNReal, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Set.Ioo, OfNat.ofNat, Top.top, Set.univ
Proof uses: Eq.mpr, Eq, Set, Compl.compl, id, Real, Set.image, ENNReal.toReal, congrArg, ENNReal.volume_val, of_eq_true, MeasurableSet, Eq.trans, True, Insert.insert, Singleton.singleton, Set.ofPred, Not, Membership.mem, Set.compl_def and 31 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma ae_in_Ioo_zero_top line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Eventually, ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Top.top, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume
Proof uses: Filter.mp_mem, Set.ofPred, Eq, Set.univ, Ioo_zero_top_ae_eq_univ, Filter.univ_mem', id, Iff.mpr, Eq.mp, Iff, trivial
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma map_restrict_Ioi_eq_restrict_Ioi line 206 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, MeasureTheory.Measure, ENNReal, MeasureTheory.Measure.map, Real, ENNReal.ofReal, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat
Proof uses: MeasureTheory.Measure.ext, Set, MeasurableSet, Eq.mpr, Set.preimage, id, congrArg, MeasureTheory.Measure.map_apply, ENNReal.measurable_ofReal, Inter.inter, congr, MeasureTheory.Measure.restrict_apply', of_eq_true, Set.Ici, ENNReal.volume_eq_volume_preimage, eq_of_heq, HEq, DFunLike, HEq.refl, Eq.refl and 11 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma map_restrict_Ioi_eq_volume line 216 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, MeasureTheory.Measure, ENNReal, MeasureTheory.Measure.map, Real, ENNReal.ofReal, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat
Proof uses: Eq.trans, map_restrict_Ioi_eq_restrict_Ioi, MeasureTheory.Measure.restrict_eq_self_of_ae_mem, Filter.mp_mem, MeasureTheory.ae, Set.ofPred, Membership.mem, Set, Set.Ioo, Top.top, ae_in_Ioo_zero_top, Filter.univ_mem', id, And.left, LT.lt
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma NNReal.toReal_Iio_eq_Ico TODO: move somewhere else and add more lemmas for Ioo, Ico etc line 223 source
Source comment
TODO: move somewhere else and add more lemmas for Ioo, Ico etc. ?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Eq, Set, Real, Set.image, Set.Iio, Set.Ico, OfNat.ofNat
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LT.lt, LE.le, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, Eq.symm, True, true_and, Exists.intro, Real.toNNReal and 8 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma NNReal.toReal_Iio_eq_Ico {b : ℝ≥0} :
    NNReal.toReal '' Set.Iio b = Set.Ico 0 b.toReal := by
…
```
lemma NNReal.toReal_Ioi_eq_Ioi line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Eq, Set, Real, Set.image, Set.Ioi
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LT.lt, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, Eq.symm, Exists.intro, Real.toNNReal, propext, Real.lt_toNNReal_iff_coe_lt, And.intro and 5 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma NNReal.toReal_Ioo_eq_Ioo line 250 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Eq, Set, Real, Set.image, Set.Ioo
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LT.lt, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, Eq.symm, LE.le, OfNat.ofNat, LE.le.trans, NNReal.zero_le_coe, LT.lt.le and 8 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem NNReal.Ici_eq line 261 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Eq, Set, Real, Set.Ici, Inter.inter, Set.preimage, Real.toNNReal, OfNat.ofNat
Proof uses: Set.ext, Iff.intro, Membership.mem, And.intro, Eq.mpr, LE.le, id, Eq.trans, NNReal.le_toNNReal_of_coe_le, LE.le.trans, NNReal.zero_le_coe, congrArg, Eq.symm, propext, Real.le_toNNReal_iff_coe_le, Eq.mp
20 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma NNReal.volume_Iio line 274 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Eq, ENNReal, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Set.Iio
Proof uses: Eq.mpr, Real, Set.image, Subtype, LE.le, OfNat.ofNat, id, congrArg, NNReal.volume_val, Set.Ico, NNReal.image_coe_Iio, ENNReal.ofReal, HSub.hSub, Real.volume_Ico, sub_zero, ENNReal.ofReal_coe_nnreal, Eq.refl
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma NNReal.volume_Ioi line 277 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Eq, ENNReal, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Set.Ioi, Top.top
Proof uses: Eq.mpr, Real, Set.image, Subtype, LE.le, OfNat.ofNat, id, congrArg, NNReal.volume_val, NNReal.image_coe_Ioi, Real.volume_Ioi, Eq.refl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma NNReal.volume_Ioo line 280 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Eq, ENNReal, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Set.Ioo, HSub.hSub
Proof uses: Eq.mpr, Real, Set.image, Subtype, LE.le, OfNat.ofNat, id, congrArg, NNReal.volume_val, NNReal.toReal_Ioo_eq_Ioo, ENNReal.ofReal, Real.volume_Ioo, ENNReal.ofReal_sub, of_eq_true, Eq.trans, True, congrFun', congr, ENNReal.ofReal_coe_nnreal, eq_self
27 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.toReal_Iio_eq_Ico TODO: move somewhere else and add more lemmas for Ioo, Ico etc line 288 source
Source comment
TODO: move somewhere else and add more lemmas for Ioo, Ico etc. ?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Top.top, Eq, Set, Real, Set.image, ENNReal.toReal, Set.Iio, Set.Ico, OfNat.ofNat
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LT.lt, LE.le, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, Eq.symm, And.intro, of_eq_true, Iff.mpr, ENNReal.toReal_lt_toReal and 4 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma ENNReal.toReal_Iio_eq_Ico {a : ℝ≥0∞} (ha : a ≠ ∞) :
    ENNReal.toReal '' Set.Iio a = Set.Ico 0 a.toReal := by
…
```
lemma ENNReal.toReal_Iio_top_eq_Ici line 304 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Set, Real, Set.image, ENNReal, ENNReal.toReal, Set.Iio, Top.top, Set.Ici, OfNat.ofNat
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LT.lt, LE.le, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, Eq.symm, of_eq_true, Exists.intro, ENNReal.ofReal, True and 1 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.toReal_Icc_eq_Icc TODO: move somewhere else and add more lemmas for Ioo, Ico etc line 317 source
Source comment
TODO: move somewhere else and add more lemmas for Ioo, Ico etc. ?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Top.top, Eq, Set, Real, Set.image, ENNReal.toReal, Set.Icc
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LE.le, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, Eq.symm, And.intro, ENNReal.toReal_mono, ne_top_of_le_ne_top, Exists.intro, ENNReal.ofReal and 8 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma ENNReal.toReal_Icc_eq_Icc {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) :
    ENNReal.toReal '' Set.Icc a b = Set.Icc a.toReal b.toReal := by
…
```
lemma ENNReal.toReal_Ioo_eq_Ioo TODO: move somewhere else and add more lemmas for Ioo, Ico etc line 334 source
Source comment
TODO: move somewhere else and add more lemmas for Ioo, Ico etc. ?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Top.top, Eq, Set, Real, Set.image, ENNReal.toReal, Set.Ioo
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LT.lt, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, Eq.symm, And.intro, ENNReal.toReal_strict_mono, ne_top_of_lt, Exists.intro, ENNReal.ofReal and 10 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma ENNReal.toReal_Ioo_eq_Ioo {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) :
    ENNReal.toReal '' Set.Ioo a b = Set.Ioo a.toReal b.toReal := by
…
```
lemma ENNReal.toReal_Ioo_top_eq_Ioi TODO: move somewhere else and add more lemmas for Ioo, Ico etc line 351 source
Source comment
TODO: move somewhere else and add more lemmas for Ioo, Ico etc. ?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Top.top, Eq, Set, Real, Set.image, ENNReal.toReal, Set.Ioo, Set.Ioi
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LT.lt, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, Eq.symm, propext, ENNReal.toReal_lt_toReal, LT.lt.ne, Exists.intro, ENNReal.ofReal and 10 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma ENNReal.toReal_Ioo_top_eq_Ioi {a : ℝ≥0∞} (ha : a ≠ ∞) :
    ENNReal.toReal '' Set.Ioo a ⊤ = Set.Ioi a.toReal := by
…
```
lemma ENNReal.toReal_Ioi_eq_Ioi TODO: move somewhere else and add more lemmas for Ioo, Ico etc line 366 source
Source comment
TODO: move somewhere else and add more lemmas for Ioo, Ico etc. ?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Top.top, Eq, Set, Real, Set.image, ENNReal.toReal, Set.Ioi, Union.union, Singleton.singleton, OfNat.ofNat
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LT.lt, Or, id, congr, congrArg, Eq.trans, funext, congrFun', Insert.insert, Set.union_singleton, Iff.intro, dite, Or.inl, Eq.symm and 18 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma ENNReal.toReal_Ioi_eq_Ioi {a : ℝ≥0∞} (ha : a ≠ ∞) :
    ENNReal.toReal '' Set.Ioi a = Set.Ioi a.toReal ∪ {0} := by
…
```
lemma ENNReal.ofReal_Ioo_eq line 386 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, Set, Real, Set.preimage, ENNReal.ofReal, Set.Ioo, ite, Top.top, EmptyCollection.emptyCollection, And, LE.le, Set.Ioi, ENNReal.toReal
Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, of_eq_true, Eq.trans, True, congrFun', Set.Ioo_eq_empty, Not, LT.lt, False, not_false_eq_true, eq_self, ite_eq_right, And.right, Set.ext, Iff, Membership.mem and 68 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.ofReal_Iio_eq line 415 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, Set, Real, Set.preimage, ENNReal.ofReal, Set.Iio, ite, OfNat.ofNat, EmptyCollection.emptyCollection, Top.top, Set.univ, ENNReal.toReal
Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, of_eq_true, Eq.trans, True, congrFun', IsMin.Iio_eq, IsMin, Bot.bot, bot_eq_zero', eq_self, Not, ite_eq_right, LE.le, Set.range, Membership.mem, LT.lt and 13 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.toNNReal_Iio line 434 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, Set, NNReal, Set.image, ENNReal.toNNReal, Set.Iio, ite, Top.top, Set.univ
Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, Set.ext, Iff, Membership.mem, Exists, And, LT.lt, Eq.trans, True, congr, funext, congrFun', iff_true, Exists.intro, of_eq_true, eq_self and 10 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.volume_Ioi line 454 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Top.top, Eq, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Set.Ioi
Proof uses: Eq.mpr, Real, Set.image, ENNReal.toReal, id, congrArg, ENNReal.volume_val, measurableSet_Ioi, Union.union, Singleton.singleton, OfNat.ofNat, ENNReal.toReal_Ioi_eq_Ioi, Or, propext, MeasureTheory.measure_union_eq_top_iff, Or.inl, Real.volume_Ioi
32 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem ENNReal.Ioi_eq_Ioc_top TODO: move somewhere else? line 461 source
Source comment
TODO: move somewhere else?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, Set, Set.Ioi, Set.Ioc, Top.top
Proof uses: id, Set.ofPred, LT.lt, Set.ext, And, LE.le, of_eq_true, Iff, Membership.mem, Eq.trans, True, congrArg, congrFun', funext, and_true, iff_self
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem ENNReal.Ioi_eq_Ioc_top {a : ℝ≥0∞} : Ioi a = Ioc a ⊤ := by
…
```
lemma ENNReal.volume_Iio line 466 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Set.Iio
Proof uses: Eq.mpr, Real, Set.image, ENNReal.toReal, id, congrArg, ENNReal.volume_val, measurableSet_Iio, dite, Top.top, Set.Ici, OfNat.ofNat, ENNReal.toReal_Iio_top_eq_Ici, Real.volume_Ici, Eq.refl, Not, Set.Ico, ENNReal.toReal_Iio_eq_Ico, ENNReal.ofReal, HSub.hSub and 5 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.range_toReal line 475 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Set, Real, Set.range, ENNReal, ENNReal.toReal, Set.Ici, OfNat.ofNat
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, LE.le, id, congr, congrArg, Iff.intro, ENNReal.toReal_nonneg, Exists.intro, ENNReal.ofReal
14 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.volume_univ line 487 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENNReal, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Set.univ, Top.top
Proof uses: Eq.mpr, Real, Set.image, ENNReal.toReal, id, congrArg, ENNReal.volume_val, MeasurableSet.univ, Set.range, Set.image_univ, of_eq_true, Eq.trans, True, congrFun', Set.Ici, OfNat.ofNat, ENNReal.range_toReal, Real.volume_Ici, eq_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.volume_Iic line 492 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Set.Iic
Proof uses: Eq.mpr, Real, Set.image, ENNReal.toReal, id, congrArg, ENNReal.volume_val, measurableSet_Iic, dite, Top.top, of_eq_true, Eq.trans, True, congrFun', Set.Ici, OfNat.ofNat, Set.range, Set.univ, Set.Iic_top, Set.image_univ and 16 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.volume_Ioo line 501 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Set.Ioo, HSub.hSub
Proof uses: dite, Top.top, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, OfNat.ofNat, True, congr, EmptyCollection.emptyCollection, Set.Ioo_eq_empty, Not, LT.lt, False, not_false_eq_true, MeasureTheory.measure_empty, ENNReal.sub_top, eq_self, Real and 17 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
instance (instance at line 513) line 513 source
instance (instance at line 522) line 522 source
lemma ENNReal.volume_map_add_left_le_self line 533 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Top.top, Set, MeasurableSet, LE.le, MeasureTheory.Measure, MeasureTheory.Measure.map, HAdd.hAdd, MeasureTheory.MeasureSpace.volume
Proof uses: Not, Membership.mem, Or, Classical.em, Trans.trans, Eq, Real, ENNReal.toReal, Set.image, Set.preimage, rfl, Eq.mpr, id, congrArg, MeasureTheory.Measure.map_apply, Measurable.const_add, measurable_id', ENNReal.volume_val, measurableSet_preimage, MeasureTheory.measure_mono and 44 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.volume_map_add_right_le_self line 570 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Top.top, Set, MeasurableSet, LE.le, MeasureTheory.Measure, MeasureTheory.Measure.map, HAdd.hAdd, MeasureTheory.MeasureSpace.volume
Proof uses: Eq.mpr, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, DFunLike, MeasurableSpace, funext, add_comm, ENNReal.volume_map_add_left_le_self
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.volume_Ico line 575 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Set.Ico, HSub.hSub
Proof uses: Eq.mpr, Set.Ioo, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, MeasureTheory.measure_congr, Filter.EventuallyEq.symm, MeasureTheory.ae, MeasureTheory.Ioo_ae_eq_Ico, ENNReal.volume_Ioo
20 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
example (example at line 583) line 583 source
Source comment
sanity check: this measure is what you expect
```
example : volume (Set.Icc (3 : ℝ≥0∞) 42) = 39 := by
…
```
lemma lintegral_nnreal_eq_lintegral_Ici_ofReal line 590 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, ENNReal, Eq, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, Real, MeasureTheory.Measure.restrict, Set.Ici, OfNat.ofNat, Real.toNNReal
Proof uses: id, Eq.mpr, Function.comp, Membership.mem, Set, MeasureTheory.Measure.comap, congrArg, Eq.symm, MeasureTheory.lintegral_subtype_comap, measurableSet_Ici, funext, Real.toNNReal_coe, Eq.refl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma lintegral_nnreal_Ici_eq_lintegral_Ici_ofReal line 597 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, ENNReal, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ici, Real, Real.toNNReal
Proof uses: Eq.mpr, Set.indicator, id, congrArg, Eq.symm, MeasureTheory.lintegral_indicator, measurableSet_Ici, OfNat.ofNat, lintegral_nnreal_eq_lintegral_Ici_ofReal, Set.preimage, Function.comp, congrFun', funext, Inter.inter, Set, MeasureTheory.setLIntegral_indicator, MeasurableSet.preimage, measurable_real_toNNReal, MeasureTheory.setLIntegral_congr, Filter.EventuallyEq and 4 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma lintegral_nnreal_eq_lintegral_Ioi_ofReal line 606 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, MeasureTheory.lintegral, NNReal, MeasureTheory.MeasureSpace.volume, Real, MeasureTheory.Measure.restrict, Set.Ioi, OfNat.ofNat, ENNReal.ofReal
Proof uses: Eq.mpr, Set.Ici, Real.toNNReal, id, congrArg, lintegral_nnreal_eq_lintegral_Ici_ofReal, MeasureTheory.setLIntegral_congr, Filter.EventuallyEq.symm, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Ioi_ae_eq_Ici
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma lintegral_ennreal_eq_lintegral_of_nnreal line 610 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, NNReal
Proof uses: Eq.symm, MeasureTheory.Measure.map, MeasureTheory.MeasurePreserving.lintegral_comp_emb, MeasureTheory.MeasurePreserving.mk, Measurable.coe_nnreal_ennreal, measurable_id', rfl, MeasureTheory.Measure, Topology.IsEmbedding.measurableEmbedding, ENNReal.isEmbedding_coe, Eq.mpr, MeasurableSet, Set.range, Set.Iio, Top.top, id, congrArg, Set, ENNReal.range_coe', measurableSet_Iio
25 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma setLIntegral_ennreal_eq_setLintegral_of_nnreal line 616 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Set, MeasurableSet, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, NNReal, Set.preimage
Proof uses: Eq.mpr, Set.indicator, id, congrArg, Eq.symm, MeasureTheory.lintegral_indicator, lintegral_ennreal_eq_lintegral_of_nnreal, Function.comp, congrFun', funext, measurableSet_preimage, Measurable.coe_nnreal_ennreal, measurable_id', Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma lintegral_ennreal_eq_lintegral_Ioi_ofReal line 623 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, Real, MeasureTheory.Measure.restrict, Set.Ioi, OfNat.ofNat, ENNReal.ofReal
Proof uses: Eq.trans, NNReal, lintegral_ennreal_eq_lintegral_of_nnreal, lintegral_nnreal_eq_lintegral_Ioi_ofReal
14 instances, coercions and auxiliary constants left out.
lemma lintegral_nnreal_eq_lintegral_toNNReal_Ioi TODO: are there better names? line 628 source
Source comment
TODO: are there better names?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, ENNReal, Eq, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, Real, MeasureTheory.Measure.restrict, Set.Ioi, OfNat.ofNat, Real.toNNReal
Proof uses: Eq.mpr, Set.Ici, id, congrArg, lintegral_nnreal_eq_lintegral_Ici_ofReal, MeasureTheory.setLIntegral_congr, Filter.EventuallyEq.symm, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Ioi_ae_eq_Ici
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_nnreal_eq_lintegral_toNNReal_Ioi (f : ℝ≥0 → ℝ≥0∞) :
    ∫⁻ x : ℝ≥0, f x = ∫⁻ x in Ioi (0 : ℝ), f x.toNNReal := by
…
```
lemma lintegral_nnreal_toReal_eq_lintegral_Ioi TODO: do we actually use this? line 634 source
Source comment
TODO: do we actually use this?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, ENNReal, Eq, MeasureTheory.lintegral, NNReal, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.restrict, Set.Ioi, OfNat.ofNat
Proof uses: Eq.mpr, Real.toNNReal, id, congrArg, lintegral_nnreal_eq_lintegral_toNNReal_Ioi, MeasureTheory.setLIntegral_congr_fun_ae, measurableSet_Ioi, Filter.univ_mem', MeasureTheory.ae, MeasureTheory.Measure, Set.ofPred, Membership.mem, Set, Max.max, max_eq_left_of_lt, of_eq_true, Eq.trans, True, congrFun', eq_self
35 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_nnreal_toReal_eq_lintegral_Ioi (f : ℝ → ℝ≥0∞) :
    ∫⁻ x : ℝ≥0, f (x.toReal) = ∫⁻ x in Ioi (0 : ℝ), f x := by
…
```
lemma lintegral_nnreal_toReal_eq_lintegral_Ici line 642 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, ENNReal, Eq, MeasureTheory.lintegral, NNReal, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.restrict, Set.Ici, OfNat.ofNat
Proof uses: Eq.mpr, Set.Ioi, id, congrArg, lintegral_nnreal_toReal_eq_lintegral_Ioi, MeasureTheory.setLIntegral_congr, MeasureTheory.Ioi_ae_eq_Ici
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma setLIntegral_nnreal_Ici line 647 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, ENNReal, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ici, HAdd.hAdd
Proof uses: Eq.mpr, Real, OfNat.ofNat, Real.toNNReal, id, congrArg, lintegral_nnreal_eq_lintegral_Ici_ofReal, Set.preimage, Neg.neg, Eq.symm, MeasureTheory.lintegral_shift', congrFun', MeasureTheory.Measure, Set, Eq.trans, HSub.hSub, Set.preimage_add_const_Ici, sub_neg_eq_add, zero_add, lintegral_nnreal_Ici_eq_lintegral_Ici_ofReal and 13 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma lintegral_nnreal_scale_constant' line 663 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, ENNReal, Ne, OfNat.ofNat, Eq, HMul.hMul, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume
Proof uses: Eq.mpr, Real, MeasureTheory.Measure.restrict, Set.Ioi, Real.toNNReal, id, congrArg, lintegral_nnreal_eq_lintegral_toNNReal_Ioi, Eq.symm, ENNReal.ofReal, abs, MeasureTheory.lintegral_scale_constant_halfspace', LT.lt, propext, NNReal.coe_pos, pos_iff_ne_zero, HMul, Eq.rec, Eq.refl, of_eq_true and 13 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.