Misc.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

85 declarations, 0 contain sorry, 0 declared as axioms

Miscellaneous additions to mathlib, to be sorted

This file can import all ToMathlib files.
If adding more than a few results, please put them in a more appropriate file in ToMathlib.

Upstreaming status: need to split up this file (according to the lemmas' future location) Most lemmas look ready to be upstreamed; some will require small tweaks.

Imports (5)

Imported by 6 files

lemma Real.le_pow_natCeil_logb to Mathlib.Analysis.SpecialFunctions.Log.Base line 28 source
Source comment
to Mathlib.Analysis.SpecialFunctions.Log.Base

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, HPow.hPow, Nat, Nat.ceil, Real.logb
Proof uses: Trans.trans, Eq, Eq.mpr, id, congrArg, Real.rpow_logb, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 40 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma le_pow_natCeil_logb {b x : ℝ} (hb : 1 < b) (hx : 0 < x) :
    x ≤ b ^ ⌈Real.logb b x⌉₊ := by
…
```
lemma tsum_one_eq' line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Eq, ENNReal, tsum, OfNat.ofNat, SummationFilter.unconditional, Set.encard
Proof uses: dite, Set.Finite, Classical.propDecidable, Finset, Exists, CanLift.prf, of_eq_true, Eq.trans, Finset.card, True, congr, congrArg, Subtype, Membership.mem, Finset.sum, Finset.univ, tsum_fintype, Finset.attach, HSMul.hSMul, Nat and 26 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.tsum_const_eq' line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, ENNReal, Eq, tsum, SummationFilter.unconditional, HMul.hMul, Set.encard
Proof uses: Eq.mpr, OfNat.ofNat, id, congrArg, Eq.symm, one_mul, ENNReal.tsum_mul_right, tsum_one_eq', Eq.refl
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.sum_geometric_two_pow_toNNReal line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Eq, ENNReal, tsum, HPow.hPow, Int, HMul.hMul, Neg.neg, SummationFilter.unconditional, Real.toNNReal, HDiv.hDiv, Real, HSub.hSub
Proof uses: Eq.mpr, id, Eq.rec, Eq.refl, SummationFilter, funext, Eq.trans, congrArg, Eq.symm, ENNReal.rpow_intCast, of_eq_true, True, congr, neg_mul, Int.cast_neg, Int.cast_mul, Int.cast_natCast, eq_self, ENNReal.rpow_mul, ENNReal.rpow_natCast and 50 more
176 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.sum_geometric_two_pow_neg_one line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENNReal, tsum, Nat, HPow.hPow, Int, OfNat.ofNat, Neg.neg, SummationFilter.unconditional
Proof uses: Eq.mpr, HMul.hMul, id, Eq.rec, Eq.refl, SummationFilter, funext, Eq.trans, congrArg, Eq.symm, one_mul, neg_mul, Nat.cast_one, Real.toNNReal, HDiv.hDiv, Real, HSub.hSub, ENNReal.sum_geometric_two_pow_toNNReal, zero_lt_one, of_eq_true and 25 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.sum_geometric_two_pow_neg_two line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENNReal, tsum, Nat, HPow.hPow, Int, OfNat.ofNat, HMul.hMul, Neg.neg, SummationFilter.unconditional, Real.toNNReal, HDiv.hDiv, Real
Proof uses: Eq.mpr, id, Eq.rec, Eq.refl, SummationFilter, funext, Eq.trans, congrArg, Eq.symm, Nat.cast_two, HSub.hSub, ENNReal.sum_geometric_two_pow_toNNReal, zero_lt_two, of_eq_true, True, Mathlib.Meta.NormNum.instAtLeastTwo, congr, NNReal, Mathlib.Meta.NormNum.IsNNRat.to_eq, Mathlib.Meta.NormNum.isNNRat_div and 17 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma tsum_geometric_ite_eq_tsum_geometric line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, ENNReal, tsum, ite, LE.le, HPow.hPow, Int, OfNat.ofNat, HMul.hMul, Neg.neg, HSub.hSub, SummationFilter.unconditional
Proof uses: Eq.mpr, HAdd.hAdd, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, AddCommMonoid, TopologicalSpace, optParam, SummationFilter, funext, of_eq_true, Eq.trans, True, congr, congrArg, neg_mul, ite_eq_left_of_eq_true, LT.lt and 21 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.toReal_zpow line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Int, Eq, Real, HPow.hPow, ENNReal.toReal
Proof uses: Eq.mpr, id, congrArg, Eq.symm, ENNReal.rpow_intCast, ENNReal.toReal_rpow, Real.rpow_intCast, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma iSup_rpow TODO: this helper lemma may be useful in other places to, for instance in HardyLittlewood.lean line 96 source
Source comment
TODO: this helper lemma may be useful in other places to, for instance in `HardyLittlewood.lean`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, LT.lt, OfNat.ofNat, Eq, HPow.hPow, iSup
Proof uses: le_antisymm, Eq.mpr, LE.le, Inv.inv, id, congrArg, Eq.symm, propext, ENNReal.rpow_le_rpow_iff, inv_pos_of_pos, ENNReal.rpow_rpow_inv, ne_of_gt, iSup_le, ENNReal.rpow_inv_rpow, le_iSup, ENNReal.rpow_le_rpow, le_of_lt
47 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma iSup_rpow {ι : Sort*} {f : ι → ℝ≥0∞} {p : ℝ} (hp : 0 < p) :
    (⨆ n, f n) ^ p = ⨆ n, f n ^ p := by
…
```
lemma _root_.ENNReal.nnorm_toReal line 111 source
lemma Function.support_rpow_of_pos line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, LT.lt, OfNat.ofNat, Eq, Set, Function.support, HPow.hPow
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Not, True, congr, congrArg, Ne, propext, ENNReal.rpow_eq_zero_iff_of_pos, iff_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Function.support_rpow_of_neg line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, LT.lt, OfNat.ofNat, Eq, Set, Function.support, HPow.hPow, Set.ofPred, Ne, Top.top
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Not, LE.le, id, Eq.trans, And, congrFun', congrArg, Or, True, eq_true, and_true, implies_congr, Eq.refl
27 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Function.support_ofNNReal line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Set, NNReal, Function.support, ENNReal, Set.Ioi, OfNat.ofNat
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, LE.le, True, Not, LT.lt, congr, congrArg, Ne
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory._root_.AEMeasurable.piecewise line 144 source
theorem MeasureTheory._root_.AEMeasurable.ite line 154 source
lemma MeasureTheory.lintegral_Ioc_partition line 163 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, ENNReal, LE.le, OfNat.ofNat, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc, HMul.hMul, Finset.sum, Finset.Ico, HAdd.hAdd
Proof uses: LT.lt, Or, lt_or_ge, Eq.mpr, EmptyCollection.emptyCollection, Finset, id, congrArg, Finset.Ico_eq_empty, Set, Set.Ioc_eq_empty, Not, propext, not_lt, mul_le_mul_of_nonneg_right, Nat.mono_cast, le_of_lt, MeasureTheory.setLIntegral_empty, Finset.sum_empty, Eq.refl and 17 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.laverage_add_left Named for consistency with lintegral_add_left' Maybe add laverage/laverage theorems for all the other lintegral_add statements? line 184 source
Source comment
Named for consistency with `lintegral_add_left'` Maybe add laverage/laverage theorems for all the other lintegral_add statements?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, AEMeasurable, Eq, MeasureTheory.laverage, HAdd.hAdd
Proof uses: Eq.mpr, HDiv.hDiv, MeasureTheory.lintegral, Set, Set.univ, id, congr, congrArg, MeasureTheory.laverage_eq, ENNReal.div_add_div_same, of_eq_true, Eq.trans, True, congrFun', MeasureTheory.lintegral_add_left', eq_self
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma laverage_add_left {α : Type*} {m0 : MeasurableSpace α} {μ : Measure α}
    {f g : α → ENNReal} (hf : AEMeasurable f μ) :
    ⨍⁻ x, (f x + g x) ∂μ = ⨍⁻ x, f x ∂μ + ⨍⁻ x, g x ∂μ := by
…
```
Mentions: g
lemma MeasureTheory.laverage_mono Named for consistency with lintegral_mono' line 190 source
Source comment
Named for consistency with `lintegral_mono'`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, LE.le, MeasureTheory.laverage
Proof uses: Eq.mpr, HDiv.hDiv, MeasureTheory.lintegral, Set, Set.univ, id, Eq, congr, congrArg, MeasureTheory.laverage_eq, ENNReal.div_le_div_right, MeasureTheory.lintegral_mono
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma laverage_mono {α : Type*} {m0 : MeasurableSpace α} {μ : Measure α}
    {f g : α → ENNReal} (h : ∀ x, f x ≤ g x) :
    ⨍⁻ x, f x ∂μ ≤ ⨍⁻ x, g x ∂μ := by
…
```
Mentions: g
lemma MeasureTheory.laverage_const_mul line 196 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Ne, Top.top, Eq, HMul.hMul, MeasureTheory.laverage
Proof uses: Eq.mpr, HDiv.hDiv, MeasureTheory.lintegral, Set, Set.univ, id, congr, congrArg, MeasureTheory.laverage_eq, congrFun', Eq.symm, mul_div_assoc, of_eq_true, Eq.trans, True, MeasureTheory.lintegral_const_mul', eq_self
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.setLaverage_add_left' Named for consistency with lintegral_add_left' Maybe add laverage/setLaverage theorems for all the other lintegral_add statements? line 205 source
Source comment
Named for consistency with `lintegral_add_left'` Maybe add laverage/setLaverage theorems for all the other lintegral_add statements?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, ENNReal, AEMeasurable, Eq, MeasureTheory.laverage, MeasureTheory.Measure.restrict, HAdd.hAdd
Proof uses: Eq.mpr, HDiv.hDiv, MeasureTheory.lintegral, id, congr, congrArg, MeasureTheory.setLAverage_eq, ENNReal.div_add_div_same, of_eq_true, Eq.trans, True, congrFun', MeasureTheory.lintegral_add_left', AEMeasurable.restrict, eq_self
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma setLaverage_add_left' {α : Type*} {m0 : MeasurableSpace α} {μ : Measure α}
    {s : Set α} {f g : α → ENNReal} (hf : AEMeasurable f μ) :
    ⨍⁻ x in s, (f x + g x) ∂μ = ⨍⁻ x in s, f x ∂μ + ⨍⁻ x in s, g x ∂μ := by
…
```
Mentions: s, g
lemma MeasureTheory.setLaverage_mono' Named for consistency with setLintegral_mono' line 211 source
Source comment
Named for consistency with `setLintegral_mono'`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, MeasurableSet, ENNReal, Membership.mem, LE.le, MeasureTheory.laverage, MeasureTheory.Measure.restrict
Proof uses: Eq.mpr, HDiv.hDiv, MeasureTheory.lintegral, id, Eq, congr, congrArg, MeasureTheory.setLAverage_eq, ENNReal.div_le_div_right, MeasureTheory.setLIntegral_mono'
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma setLaverage_mono' {α : Type*} {m0 : MeasurableSpace α} {μ : Measure α}
    {s : Set α} (hs : MeasurableSet s) {f g : α → ENNReal} (h : ∀ x ∈ s, f x ≤ g x) :
    ⨍⁻ x in s, f x ∂μ ≤ ⨍⁻ x in s, g x ∂μ := by
…
```
Mentions: s, g
lemma MeasureTheory.AEStronglyMeasurable_continuousMap_coe line 217 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, MeasurableSpace, OpensMeasurableSpace, TopologicalSpace.PseudoMetrizableSpace, SecondCountableTopologyEither, ContinuousMap, MeasureTheory.StronglyMeasurable
Proof uses: Continuous.stronglyMeasurable, ContinuousMapClass.map_continuous
5 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.measure_mono_ae' line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Eq, ENNReal, SDiff.sdiff, OfNat.ofNat, LE.le
Proof uses: MeasureTheory.measure_mono_ae, id, Filter.EventuallyLE, MeasureTheory.ae, Eq.mpr, Set.ofPred, Not, And, congrFun', congrArg, funext
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.AEStronglyMeasurable.ennreal_toReal line 246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, MeasureTheory.AEStronglyMeasurable, Real, ENNReal.toReal
Proof uses: Iff.mpr, AEMeasurable, aestronglyMeasurable_iff_aemeasurable, Measurable.comp_aemeasurable, ENNReal.measurable_toReal, MeasureTheory.AEStronglyMeasurable.aemeasurable
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.setLaverage_const_le line 251 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, ENNReal, LE.le, MeasureTheory.laverage, MeasureTheory.Measure.restrict
Proof uses: Eq.mpr, HDiv.hDiv, MeasureTheory.lintegral, id, Eq, congrFun', congrArg, MeasureTheory.setLAverage_eq, HMul.hMul, Set.univ, MeasureTheory.lintegral_const, Inter.inter, MeasureTheory.Measure.restrict_apply, MeasurableSet.univ, Set.univ_inter, Inv.inv, div_eq_mul_inv, mul_assoc, OfNat.ofNat, Eq.rec and 7 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.eLpNormEssSup_lt_top_of_ae_ennnorm_bound line 258 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, ENNReal, Filter.Eventually, LE.le, NNNorm.nnnorm, MeasureTheory.ae, MeasureTheory.eLpNormEssSup
Proof uses: essSup_le_of_ae_le, ENorm.enorm, Filter.isCobounded_le_of_bot, Filter.map
34 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.restrict_absolutelyContinuous line 261 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, MeasureTheory.Measure.AbsolutelyContinuous, MeasureTheory.Measure.restrict
Proof uses: Eq, ENNReal, OfNat.ofNat, LE.le.antisymm, LE.le.trans, MeasureTheory.Measure.restrict_le_self, Eq.le, zero_le
13 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.eLpNormEssSup_toReal_le line 270 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, LE.le, MeasureTheory.eLpNormEssSup, Real, Function.comp, ENNReal.toReal
Proof uses: id, essSup, ENorm.enorm, essSup_mono_ae, Filter.Eventually.of_forall, MeasureTheory.ae, of_eq_true, Eq.trans, True, forall_congr, implies_true, Filter.isCobounded_le_of_bot, Filter.map, Filter.isBounded_le_of_top
40 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNormEssSup_toReal_eq line 276 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Filter.Eventually, Ne, Top.top, MeasureTheory.ae, Eq, MeasureTheory.eLpNormEssSup, Real, Function.comp, ENNReal.toReal
Proof uses: id, essSup, ENorm.enorm, essSup_congr_ae, Filter.mp_mem, Set.ofPred, Filter.univ_mem', Membership.mem, Set, of_eq_true, Eq.trans, True, congrFun', congrArg, Real.enorm_toReal, Not, False, eq_false, not_false_eq_true, eq_self
35 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNorm'_toReal_le line 283 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Real, LE.le, OfNat.ofNat, MeasureTheory.eLpNorm', Function.comp, ENNReal.toReal
Proof uses: id, HPow.hPow, MeasureTheory.lintegral, ENorm.enorm, HDiv.hDiv, ENNReal.rpow_le_rpow, MeasureTheory.lintegral_mono_fn', le_refl, of_eq_true, Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, Nat
62 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNorm'_toReal_eq line 289 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Real, Filter.Eventually, Ne, Top.top, MeasureTheory.ae, Eq, MeasureTheory.eLpNorm', Function.comp, ENNReal.toReal
Proof uses: id, HPow.hPow, MeasureTheory.lintegral, ENorm.enorm, HDiv.hDiv, OfNat.ofNat, HPow, Eq.rec, Eq.refl, MeasureTheory.lintegral_congr_ae, Filter.mp_mem, Set.ofPred, Filter.univ_mem', Membership.mem, Set, of_eq_true, Eq.trans, True, congrFun', congrArg and 6 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNorm_toReal_le line 297 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, LE.le, MeasureTheory.eLpNorm, Real, Function.comp, ENNReal.toReal
Proof uses: id, dite, ite, Eq, OfNat.ofNat, Top.top, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm', Eq.mpr, congr, congrArg, ite_eq_left, le_refl, Not, ite_eq_right, MeasureTheory.eLpNormEssSup_toReal_le, MeasureTheory.eLpNorm'_toReal_le, ENNReal.toReal_nonneg
33 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNorm_toReal_eq line 305 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Filter.Eventually, Ne, Top.top, MeasureTheory.ae, Eq, MeasureTheory.eLpNorm, Real, Function.comp, ENNReal.toReal
Proof uses: id, dite, ite, OfNat.ofNat, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm', Eq.mpr, congr, congrArg, ite_eq_left, Eq.refl, Not, ite_eq_right, MeasureTheory.eLpNormEssSup_toReal_eq, MeasureTheory.eLpNorm'_toReal_eq
34 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.sq_eLpNorm_two line 313 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, Eq, ENNReal, HPow.hPow, Nat, MeasureTheory.eLpNorm, OfNat.ofNat, MeasureTheory.lintegral, ENorm.enorm
Proof uses: Eq.mp, Real, NNReal, congr, congrArg, ENNReal.rpow_ofNat, funext, MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral, two_ne_zero
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNorm_two_eq_enorm_integral_mul_conj One of the very few cases where a norm can be moved out of an integral line 319 source
Source documentation
One of the very few cases where a norm can be moved out of an integral.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Complex, MeasureTheory.MemLp, OfNat.ofNat, ENNReal, Nat, Eq, HPow.hPow, MeasureTheory.eLpNorm, ENorm.enorm, MeasureTheory.integral, Real, HMul.hMul, RingHom, starRingEnd
Proof uses: Eq.mpr, Norm.norm, id, Eq.rec, Eq.refl, funext, Eq.trans, congrArg, RCLike.mul_conj, Eq.symm, RCLike.ofReal_pow, integral_ofReal, ENNReal.toReal, MeasureTheory.lintegral, ENNReal.ofReal, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, Filter.Eventually.of_forall, LE.le, MeasureTheory.ae, of_eq_true and 14 more
143 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma eLpNorm_two_eq_enorm_integral_mul_conj {f : α → ℂ} (lpf : MemLp f 2 μ) :
    eLpNorm f 2 μ ^ 2 = ‖∫ x, f x * conj (f x) ∂μ‖ₑ := by
…
```
theorem MeasureTheory.MemLp.toReal line 335 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, MeasureTheory.MemLp, Real, ENNReal.toReal
Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, LT.lt, MeasureTheory.eLpNorm, Top.top, AEMeasurable.aestronglyMeasurable, AEMeasurable.ennreal_toReal, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.MemLp.aestronglyMeasurable, LE.le.trans_lt, Function.comp, MeasureTheory.eLpNorm_toReal_le, MeasureTheory.MemLp.eLpNorm_lt_top
44 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.Integrable.toReal line 341 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, MeasureTheory.Integrable, Real, ENNReal.toReal
Proof uses: Eq.mpr, MeasureTheory.MemLp, OfNat.ofNat, id, Eq, congrArg, Eq.symm, propext, MeasureTheory.memLp_one_iff_integrable, MeasureTheory.MemLp.toReal, Eq.mp
33 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
structure EquivalenceOn An equivalence relation on the set s line 365 source
Source documentation
An equivalence relation on the set s.

no axioms what this means
Statement uses: Set
```
structure EquivalenceOn {α : Type*} (r : α → α → Prop) (s : Set α) : Prop where
…
```
Mentions: s
def EquivalenceOn.setoid The setoid defined from an equivalence relation on a set line 379 source
Source documentation
The setoid defined from an equivalence relation on a set.

no axioms what this means
Statement uses: Set, EquivalenceOn, Setoid
Proof uses: Setoid.mk, Membership.mem
5 instances, coercions and auxiliary constants left out.
```
protected def setoid : Setoid s where
…
```
Mentions: s
lemma EquivalenceOn.exists_rep line 388 source
no axioms what this means
Statement uses: Set, EquivalenceOn, Exists, Membership.mem, And
Proof uses: Exists.intro, And.intro, EquivalenceOn.refl
2 instances, coercions and auxiliary constants left out.
def EquivalenceOn.out An arbitrary representative of x w.r.t line 394 source
Source documentation
An arbitrary representative of x w.r.t. the equivalence relation r.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EquivalenceOn
Proof uses: dite, Membership.mem, Classical.propDecidable, Quotient.out, EquivalenceOn.setoid, Quotient.mk, Subtype.mk, Not
3 instances, coercions and auxiliary constants left out.
```
protected noncomputable def out (x : α) : α :=
…
```
lemma EquivalenceOn.out_mem line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EquivalenceOn, Membership.mem, EquivalenceOn.out
Proof uses: Eq.mpr, dite, Classical.propDecidable, Quotient.out, EquivalenceOn.setoid, Quotient.mk, Subtype.mk, Not, id, Eq, congrArg, EquivalenceOn.out.eq_1, dite_eq_left, Subtype.prop
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma EquivalenceOn.out_mem_iff line 402 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EquivalenceOn, Iff, Membership.mem, EquivalenceOn.out
Proof uses: Iff.intro, Classical.byContradiction, Not, Eq.mp, dite, Classical.propDecidable, Quotient.out, EquivalenceOn.setoid, Quotient.mk, Subtype.mk, congrArg, dite_eq_right, EquivalenceOn.out.eq_1, EquivalenceOn.out_mem
4 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma EquivalenceOn.out_rel line 408 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EquivalenceOn, Membership.mem, EquivalenceOn.out
Proof uses: Eq.mpr, dite, Classical.propDecidable, Quotient.out, EquivalenceOn.setoid, Quotient.mk, Subtype.mk, Not, id, Eq, congrArg, EquivalenceOn.out.eq_1, dite_eq_left, Quotient.mk_out
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma EquivalenceOn.rel_out line 412 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EquivalenceOn, Membership.mem, EquivalenceOn.out
Proof uses: EquivalenceOn.symm, EquivalenceOn.out_mem, EquivalenceOn.out_rel
2 instances, coercions and auxiliary constants left out.
lemma EquivalenceOn.out_inj line 414 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EquivalenceOn, Membership.mem, Eq, EquivalenceOn.out
Proof uses: id, Eq.mpr, dite, Classical.propDecidable, Quotient.out, EquivalenceOn.setoid, Quotient.mk, Subtype.mk, Not, congrFun', congrArg, Decidable, dite_eq_left, Subtype, Eq.rec, Eq.refl, Quotient
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma EquivalenceOn.out_inj' line 420 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EquivalenceOn, Membership.mem, EquivalenceOn.out, Eq
Proof uses: EquivalenceOn.out_inj, EquivalenceOn.trans, Eq.mpr, id, EquivalenceOn.rel_out, EquivalenceOn.out_rel
3 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def EquivalenceOn.reprs The set of representatives of an equivalence relation on a set line 427 source
Source documentation
The set of representatives of an equivalence relation on a set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EquivalenceOn
Proof uses: Set.image, EquivalenceOn.out
```
def reprs : Set α := hr.out '' s
```
Mentions: s
lemma EquivalenceOn.out_mem_reprs line 429 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EquivalenceOn, Membership.mem, EquivalenceOn.reprs, EquivalenceOn.out
Proof uses: Exists.intro, And, Eq, And.intro, rfl
2 instances, coercions and auxiliary constants left out.
lemma EquivalenceOn.reprs_subset line 431 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EquivalenceOn, LE.le, EquivalenceOn.reprs
Proof uses: Membership.mem, And, Eq, EquivalenceOn.out, EquivalenceOn.out_mem
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma EquivalenceOn.reprs_inj line 435 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EquivalenceOn, Membership.mem, EquivalenceOn.reprs, Eq
Proof uses: And, EquivalenceOn.out, EquivalenceOn.out_inj'
5 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Set.Finite.biSup_eq line 444 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CompleteLinearOrder, Set, Set.Finite, Set.Nonempty, Exists, And, Membership.mem, Eq, iSup
Proof uses: Eq.mpr, id, congrArg, funext, Eq.mp, Set.image, SupSet.sSup, Eq.trans, sSup_image, Set.Nonempty.csSup_mem, Set.Nonempty.image, Set.Finite.image
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Real.self_lt_two_rpow line 451 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, HPow.hPow, OfNat.ofNat, Nat
Proof uses: LE.le, Or, lt_or_ge, LT.lt.trans, Real.rpow_pos_of_pos, zero_lt_two, Trans.trans, Nat.floor, Nat.succ, Nat.lt_succ_floor, cast, Eq.symm, Eq.trans, congrArg, Real.rpow_natCast, Nat.lt_pow_self, one_lt_two, Real.rpow_le_rpow_of_exponent_le, one_le_two, Nat.floor_le
66 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Complex.measurable_starRingEnd line 460 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Measurable, Complex, RingHom, starRingEnd
Proof uses: Continuous.measurable, Complex.continuous_conj
23 instances, coercions and auxiliary constants left out.
lemma ENNReal.rpow_le_rpow_of_nonpos line 465 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, LE.le, OfNat.ofNat, HPow.hPow
Proof uses: Eq.mpr, Neg.neg, id, Eq, congrArg, Eq.symm, neg_neg, Inv.inv, ENNReal.rpow_neg, ENNReal.inv_rpow, ENNReal.rpow_le_rpow, Iff.mpr, ENNReal.inv_le_inv, neg_nonneg
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.rpow_lt_rpow_of_neg line 470 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, LT.lt, OfNat.ofNat, HPow.hPow
Proof uses: Eq.mpr, Neg.neg, id, Eq, congrArg, Eq.symm, neg_neg, Inv.inv, ENNReal.rpow_neg, ENNReal.inv_rpow, ENNReal.rpow_lt_rpow, Iff.mpr, ENNReal.inv_lt_inv, neg_pos
48 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.rpow_lt_rpow_iff_of_neg line 475 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, LT.lt, OfNat.ofNat, Iff, HPow.hPow
Proof uses: Iff.intro, lt_imp_lt_of_le_imp_le, LE.le, ENNReal.rpow_le_rpow_of_nonpos, le_of_lt, ENNReal.rpow_lt_rpow_of_neg
20 instances, coercions and auxiliary constants left out.
lemma ENNReal.rpow_le_rpow_iff_of_neg line 480 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, LT.lt, OfNat.ofNat, Iff, LE.le, HPow.hPow
Proof uses: Iff.mpr, le_iff_le_iff_lt_iff_lt, ENNReal.rpow_lt_rpow_iff_of_neg
16 instances, coercions and auxiliary constants left out.
theorem ENNReal.rpow_le_self_of_one_le line 484 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, LE.le, OfNat.ofNat, HPow.hPow
Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, ENNReal.rpow_one, ENNReal.rpow_le_rpow_of_exponent_le
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.indicator_eq_indicator' line 497 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Zero, Set, Membership.mem, Eq, Set.indicator
Proof uses: funext, dite, Classical.propDecidable, of_eq_true, Eq.trans, True, congr, congrArg, Set.indicator_of_mem, eq_self, Not, OfNat.ofNat, Set.indicator_of_notMem, False, eq_false, not_false_eq_true
3 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Set.indicator_eq_indicator_one_mul line 503 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MulZeroOneClass, Set, Eq, Set.indicator, HMul.hMul, OfNat.ofNat
Proof uses: id, dite, ite, Membership.mem, Classical.decPred, Classical.propDecidable, Eq.mpr, congr, congrArg, ite_eq_left, congrFun', of_eq_true, Eq.trans, True, one_mul, eq_self, Not, ite_eq_right, MulZeroClass.zero_mul
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Set.conj_indicator line 507 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, Set, Eq, RingHom, starRingEnd, Set.indicator
Proof uses: id, dite, ite, Membership.mem, Classical.decPred, OfNat.ofNat, Classical.propDecidable, Eq.mpr, congr, congrArg, ite_eq_left, of_eq_true, eq_self, Not, ite_eq_right, Eq.trans, True, congrFun', map_zero
44 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Set.eq_indicator_one_mul_of_norm_le line 511 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Complex, LE.le, Real, Norm.norm, Set.indicator, OfNat.ofNat, Eq, HMul.hMul
Proof uses: funext, Eq.mpr, ite, Membership.mem, Classical.decPred, id, congrArg, Eq.trans, ite_mul, ite.congr_simp, Eq.refl, one_mul, MulZeroClass.zero_mul, dite, Classical.propDecidable, ite_eq_left, Not, ite_eq_right, Eq.symm, propext and 6 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Set.indicator_one_le_one line 523 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, LE.le, Real, Set.indicator, OfNat.ofNat
Proof uses: le_trans, Max.max, ite_le_sup, Membership.mem, Classical.decPred, of_eq_true, Eq.trans, True, congrFun', congrArg, sup_of_le_left
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma norm_indicator_one_le for mathlib? line 541 source
Source comment
for mathlib?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SeminormedAddCommGroup, One, NormOneClass, Set, LE.le, Real, Norm.norm, Set.indicator, OfNat.ofNat
Proof uses: Trans.trans, Eq, norm_indicator_le_norm_self, NormOneClass.norm_one
25 instances, coercions and auxiliary constants left out.
```
lemma norm_indicator_one_le {α E}
    [SeminormedAddCommGroup E] [One E] [NormOneClass E] {s : Set α} (x : α) :
    ‖s.indicator (1 : α → E) x‖ ≤ 1 :=
…
```
Mentions: E, s
lemma norm_one_sub_exp_neg_I_mul_ofReal line 548 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Norm.norm, Complex, HSub.hSub, OfNat.ofNat, Complex.exp, Neg.neg, HMul.hMul, Complex.I
Proof uses: Eq.mpr, HAdd.hAdd, id, congrArg, Eq.trans, mul_neg, mul_sub, congr, mul_one, neg_mul, add_neg_cancel, Complex.exp_zero, sub_neg_eq_add, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Nat, Int.rawCast, inferInstance, Ring and 33 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma exp_I_mul_eq_one_iff_of_lt_of_lt line 554 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, Neg.neg, HMul.hMul, OfNat.ofNat, Nat, Real.pi, Iff, Eq, Complex, Complex.exp, Complex.I
Proof uses: Iff.intro, Real.cos, Eq.mp, Complex.re, congrFun', congrArg, Eq.trans, mul_comm, Complex.exp_ofReal_mul_I_re, id, propext, Real.cos_eq_one_iff_of_lt_of_lt, of_eq_true, True, MulZeroClass.mul_zero, Complex.exp_zero, eq_self
40 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem BddAbove.range_const line 568 source
standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, BddAbove, Set.range
Proof uses: BddAbove.mono, Singleton.singleton, Set, Set.range_const_subset, bddAbove_singleton
2 instances, coercions and auxiliary constants left out.
theorem BddAbove.range_one line 573 source
standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, One, BddAbove, Set.range, OfNat.ofNat
Proof uses: BddAbove.range_const
3 instances, coercions and auxiliary constants left out.
theorem BddAbove.range_finsetSum line 577 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Preorder, AddCommMonoid, AddLeftMono, AddRightMono, Finset, Membership.mem, BddAbove, Set.range, Finset.sum
Proof uses: Finset.induction, Classical.propDecidable, Eq, EmptyCollection.emptyCollection, of_eq_true, OfNat.ofNat, Not, Insert.insert, Eq.mpr, HAdd.hAdd, id, congrArg, Set, funext, Finset.sum_insert, BddAbove.range_add, Finset.mem_insert_self, Finset.mem_insert_of_mem
22 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma isBounded_iff_bddAbove_norm' line 593 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SeminormedCommGroup, Set, Iff, Bornology.IsBounded, BddAbove, Real, Set.image, Norm.norm
Proof uses: of_eq_true, Eq.trans, Exists, Membership.mem, LE.le, True, congr, congrArg, funext, Eq, forall_congr, And, implies_congr, Eq.refl, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma isBounded_range_iff_bddAbove_norm' line 597 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SeminormedAddCommGroup, Iff, Bornology.IsBounded, Set.range, BddAbove, Real, Norm.norm
Proof uses: Eq.mpr, Set.image, id, Eq, congrArg, propext, isBounded_iff_bddAbove_norm, Function.comp, Set, Eq.symm, Set.range_comp, Function.comp_def, Iff.rfl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma isBounded_image_iff_bddAbove_norm' line 601 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SeminormedAddCommGroup, Set, Iff, Bornology.IsBounded, Set.image, BddAbove, Real, Norm.norm
Proof uses: Eq.mpr, id, Eq, congrArg, propext, isBounded_iff_bddAbove_norm, Function.comp, Eq.symm, Set.image_comp, Function.comp_def, Iff.rfl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.HasCompactSupport.of_support_subset_closedBall line 619 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Zero, PseudoMetricSpace, ProperSpace, Real, LE.le, Set, Function.support, Metric.closedBall, HasCompactSupport
Proof uses: HasCompactSupport.of_support_subset_isCompact, ProperSpace.isCompact_closedBall
10 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.HasCompactSupport.of_support_subset_isBounded line 624 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Zero, PseudoMetricSpace, ProperSpace, Set, Bornology.IsBounded, LE.le, Function.support, HasCompactSupport
Proof uses: IsCompact.closure_of_subset, closure, Bornology.IsBounded.isCompact_closure, Trans.trans, subset_closure
19 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.Integrable.indicator_const must be in mathlib but can't find it line 636 source
Source comment
must be in mathlib but can't find it

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, Real, Set, MeasurableSet, LT.lt, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Top.top, MeasureTheory.Integrable, Set.indicator
Proof uses: Iff.mpr, MeasureTheory.IntegrableOn, MeasureTheory.integrable_indicator_iff, MeasureTheory.integrableOn_const, LT.lt.ne, enorm_ne_top
40 instances, coercions and auxiliary constants left out.
```
theorem indicator_const {c : ℝ} {s : Set X}
    (hs : MeasurableSet s) (h2s : volume s < ⊤) : Integrable (s.indicator (fun _ ↦ c)) :=
…
```
Mentions: c, s
theorem MeasureTheory.setIntegral_biUnion_le_sum_setIntegral line 647 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Real, Finset, Set, MeasureTheory.Measure, Filter.Eventually, LE.le, OfNat.ofNat, MeasureTheory.ae, MeasureTheory.Measure.restrict, Set.iUnion, Membership.mem, MeasureTheory.IntegrableOn, MeasureTheory.integral, Finset.sum
Proof uses: Eq, Eq.mpr, id, congrArg, MeasureTheory.Measure.restrict_restrict_of_subset, Set.subset_biUnion_of_mem, Eq.refl, AEMeasurable.mk, MeasureTheory.Integrable.aemeasurable, rfl, Function.comp, Iff, Filter.Eventually.congr, Filter.Eventually.mp, AEMeasurable.ae_eq_mk, Filter.Eventually.of_forall, Iff.rfl, MeasureTheory.Integrable, MeasureTheory.Integrable.restrict, MeasureTheory.Integrable.congr and 67 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
theorem ENNReal.lintegral_Lp_smul line 696 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, AEMeasurable, Real, GT.gt, OfNat.ofNat, NNReal, Eq, HPow.hPow, MeasureTheory.lintegral, HSMul.hSMul, HDiv.hDiv
Proof uses: id, Eq.mpr, HMul.hMul, congrFun', congrArg, funext, ENNReal.mul_rpow_of_nonneg, LT.lt.le, MeasureTheory.lintegral_const_mul'', AEMeasurable.pow_const, Iff.mpr, LE.le, one_div_nonneg, mul_one_div_cancel, Ne.symm, LT.lt.ne, of_eq_true, Eq.trans, True, ENNReal.rpow_one and 1 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem ENNReal.ofReal_zpow Analogous to ENNReal.ofReal_pow in Mathlib Currently unused line 706 source
Source comment
Analogous to `ENNReal.ofReal_pow` in Mathlib Currently unused

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Int, Eq, ENNReal, ENNReal.ofReal, HPow.hPow
Proof uses: Eq.mpr, NNReal.mk, LT.lt.le, id, congrArg, ENNReal.ofReal_eq_coe_nnreal, NNReal, Eq.symm, ENNReal.coe_zpow, Iff.mp, Ne, NNReal.coe_ne_zero, Ne.symm, LT.lt.ne, ENNReal.ofReal_coe_nnreal, NNReal.coe_zpow, NNReal.coe_mk, Eq.refl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem ofReal_zpow {p : ℝ} (hp : 0 < p) (n : ℤ) :
    ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n := by
…
```
theorem prod_attach_insert TODO: to mathlib line 716 source
Source comment
TODO: to mathlib

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, DecidableEq, CommMonoid, Subtype, Membership.mem, Insert.insert, Not, Eq, Finset.prod, Finset.attach, HMul.hMul, Subtype.mk, Finset.mem_insert_self, Finset.mem_insert_of_mem, Subtype.property
Proof uses: Eq.mpr, Finset.image, id, congrArg, Finset.attach_insert, Finset.prod_insert, of_eq_true, Eq.trans, False, True, Exists, And, funext, congr, Subtype.mk.injEq, true_and, propext, exists_prop_congr, Iff.of_eq, Eq.refl and 6 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem prod_attach_insert {α β : Type*} {s : Finset α} {a : α} [DecidableEq α] [CommMonoid β]
    {f : { i // i ∈ insert a s } → β} (ha : a ∉ s) :
    ∏ x ∈ (insert a s).attach, f x =
    f ⟨a, Finset.mem_insert_self a s⟩ * ∏ x ∈ s.attach, f ⟨x, Finset.mem_insert_of_mem x.2⟩ := by
…
```
Mentions: s
lemma Finset.prod_finset_product_filter_right line 727 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, DecidablePred, DecidableRel, Prod, And, Prod.fst, Prod.snd, CommMonoid, Eq, Finset.prod, Finset.filter, SProd.sprod
Proof uses: Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Finset.prod_equiv, Equiv.prodComm, Iff, Membership.mem, Equiv, id, congr, congrArg, congrFun', Prod.swap, Iff.intro, And.intro, of_eq_true, Eq.trans and 6 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Finset.sum_range_mul_conj_sum_range line 739 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Complex, Eq, HAdd.hAdd, Finset.sum, HMul.hMul, RingHom, starRingEnd, Finset.filter, Ne, Classical.propDecidable
Proof uses: Trans.trans, Eq.mpr, id, congrArg, propext, add_left_inj, Finset.sum_congr, Eq.refl, Membership.mem, ite, Singleton.singleton, EmptyCollection.emptyCollection, Finset.filter_eq, True, ite_congr, eq_true, Not, ite_true, of_eq_true, Eq.trans and 12 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Finset.pow_sum_comm line 752 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Semiring, Finset, Membership.mem, Ne, Eq, HMul.hMul, OfNat.ofNat, Nat, LE.le, HPow.hPow, Finset.sum
Proof uses: Nat.le_induction, of_eq_true, Eq.trans, True, congr, congrArg, pow_one, Finset.sum_congr, Eq.refl, eq_self, Eq.mpr, HAdd.hAdd, id, pow_succ, congrFun', Finset.sum_mul, Finset.mul_sum, Finset.sum_eq_single, HSub.hSub, Eq.symm and 6 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.sum_sq_eLpNorm_indicator_le_of_pairwiseDisjoint line 766 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, NormedAddCommGroup, MeasureTheory.Measure, Finset, Set, MeasurableSet, Set.PairwiseDisjoint, LE.le, ENNReal, Finset.sum, HPow.hPow, Nat, MeasureTheory.eLpNorm, Set.indicator, OfNat.ofNat
Proof uses: Eq.mpr, MeasureTheory.lintegral, ENorm.enorm, id, Eq, congr, congrArg, Finset.sum_congr, Eq.refl, Membership.mem, MeasureTheory.sq_eLpNorm_two, Eq.rec, funext, Eq.trans, enorm_indicator_eq_indicator_enorm, HMul.hMul, sq, Inter.inter, Eq.symm, Set.inter_indicator_mul and 6 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.measurable_measure_ball line 780 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, SecondCountableTopology, MeasurableSpace, OpensMeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, Measurable, Prod, Real, ENNReal, MeasureTheory.measurable_measure_ball.match_1, Set, Metric.ball
Proof uses: Set.ofPred, Membership.mem, measurable_measure_prodMk_right, id, MeasurableSet, LT.lt, Dist.dist, Eq.mpr, Prod.fst, Prod.snd, Eq, congrArg, funext, measurableSet_lt, Measurable.dist, Measurable.fst, measurable_id', Measurable.snd
26 instances, coercions and auxiliary constants left out.

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