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

27 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)

Imported by 2 files

def MeasureTheory.essProjFst For a (s : Set (α × β)) and (ν : Measure β), we define essProjFst such that x ∈ essProjFst s ν iff 0 < ν {y | ⟨x, y⟩ ∈ s} line 24 source
Source documentation
For a (s : Set (α × β)) and (ν : Measure β), we define essProjFst such that x ∈ essProjFst s ν iff 0 < ν {y | ⟨x, y⟩ ∈ s}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Set, Prod, MeasureTheory.Measure
Proof uses: Set.ofPred, LT.lt, ENNReal, OfNat.ofNat, Set.preimage, Prod.mk
7 instances, coercions and auxiliary constants left out.
```
def essProjFst (s : Set (α × β)) (ν : Measure β) : Set α := {x | 0 < ν ((x, ·) ⁻¹' s)}
```
Mentions: s
def MeasureTheory.essProjSnd For a (s : Set (α × β)) and (μ : Measure α), we define essProjSnd such that y ∈ essProjSnd s μ iff 0 < μ {x | ⟨x, y⟩ ∈ s} line 28 source
Source documentation
For a (s : Set (α × β)) and (μ : Measure α), we define essProjSnd such that y ∈ essProjSnd s μ iff 0 < μ {x | ⟨x, y⟩ ∈ s}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Set, Prod, MeasureTheory.Measure
Proof uses: Set.ofPred, LT.lt, ENNReal, OfNat.ofNat, Set.preimage, Prod.mk
7 instances, coercions and auxiliary constants left out.
```
def essProjSnd (s : Set (α × β)) (μ : Measure α) : Set β := {y | 0 < μ ((·, y) ⁻¹' s)}
…
```
Mentions: s
theorem MeasureTheory.essProjSnd_eq_essProjFst_swap line 32 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Prod, Eq, MeasureTheory.essProjSnd, MeasureTheory.essProjFst, Set.preimage, Prod.swap
Proof uses: id, Set.ofPred, LT.lt, ENNReal, OfNat.ofNat, Prod.mk, Set.ext, Iff, Membership.mem, iff_of_eq, eq_of_heq, LT, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, DFunLike
10 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.essProjFst_subset line 39 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Prod, LE.le, MeasureTheory.essProjFst, Set.image, Prod.fst
Proof uses: id, Mathlib.Tactic.Contrapose.contrapose₁, Membership.mem, Set.ofPred, LT.lt, ENNReal, OfNat.ofNat, Set.preimage, Prod.mk, Eq.mpr, Not, Eq, implies_congr, Eq.trans, Exists, congrArg, And, funext, EmptyCollection.emptyCollection, eq_of_heq and 15 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.essProjSnd_subset line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Prod, LE.le, MeasureTheory.essProjSnd, Set.image, Prod.snd
Proof uses: Eq.mpr, MeasureTheory.essProjFst, Set.preimage, Prod.swap, id, Eq, congrArg, MeasureTheory.essProjSnd_eq_essProjFst_swap, LE.le.trans_eq, Prod.fst, MeasureTheory.essProjFst_subset, Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Exists, Prod.mk, True, congr and 4 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.essProjFst_eq line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Prod, Eq, MeasureTheory.essProjFst, Set.preimage, ENNReal, Prod.mk, Set.Ioi, OfNat.ofNat
Proof uses: id, Set.ext, Set.ofPred, LT.lt, of_eq_true, Iff, Membership.mem, Eq.trans, True, congrArg, iff_self
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.essProjSnd_eq line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Prod, Eq, MeasureTheory.essProjSnd, Set.preimage, ENNReal, Prod.mk, Set.Ioi, OfNat.ofNat
Proof uses: Eq.mpr, MeasureTheory.essProjFst, Prod.swap, id, congrArg, MeasureTheory.essProjSnd_eq_essProjFst_swap, MeasureTheory.essProjFst_eq, Eq.rec, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.essProjFst_eq' line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Prod, Eq, MeasureTheory.essProjFst, Function.support, ENNReal, Set.preimage, Prod.mk
Proof uses: Eq.mpr, Set.Ioi, OfNat.ofNat, id, congrArg, MeasureTheory.essProjFst_eq, Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Not, True, congr, Ne, LT.lt, iff_self
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.essProjSnd_eq' line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Prod, Eq, MeasureTheory.essProjSnd, Function.support, ENNReal, Set.preimage, Prod.mk
Proof uses: Eq.mpr, MeasureTheory.essProjFst, Prod.swap, id, congrArg, MeasureTheory.essProjSnd_eq_essProjFst_swap, MeasureTheory.essProjFst_eq', Zero, Eq.rec, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.essProjFst_times_univ line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Ne, OfNat.ofNat, Eq, MeasureTheory.essProjFst, SProd.sprod, Prod, Set.univ
Proof uses: id, Set.ext, Set.ofPred, LT.lt, ENNReal, Set.preimage, Prod.mk, Iff, Membership.mem, Iff.intro, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, LE.le, implies_congr, Eq.refl, EmptyCollection.emptyCollection, eq_of_heq, HEq, HEq.refl and 18 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.essProjSnd_univ_times line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Ne, OfNat.ofNat, Eq, MeasureTheory.essProjSnd, SProd.sprod, Prod, Set.univ
Proof uses: Eq.mpr, MeasureTheory.essProjFst, Set.preimage, Prod.swap, id, congrArg, MeasureTheory.essProjSnd_eq_essProjFst_swap, Set.preimage_swap_prod, MeasureTheory.essProjFst_times_univ, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.essProjFst_mono line 100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Prod, LE.le, MeasureTheory.essProjFst
Proof uses: id, Membership.mem, Set.ofPred, LT.lt, ENNReal, OfNat.ofNat, Set.preimage, Prod.mk, LT.lt.trans_le, MeasureTheory.measure_mono, Set.preimage_mono
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.essProjSnd_mono line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Prod, LE.le, MeasureTheory.essProjSnd
Proof uses: Eq.mpr, MeasureTheory.essProjFst, Set.preimage, Prod.swap, id, Eq, congrArg, MeasureTheory.essProjSnd_eq_essProjFst_swap, MeasureTheory.essProjFst_mono, Set.preimage_mono
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.essProjFst_inter_times_univ line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Prod, Eq, MeasureTheory.essProjFst, Inter.inter, SProd.sprod, Set.univ
Proof uses: id, Set.ext, Set.ofPred, LT.lt, ENNReal, OfNat.ofNat, Set.preimage, Prod.mk, Eq.mpr, Iff, Membership.mem, And, congrArg, Iff.intro, And.intro, LT.lt.trans_le, MeasureTheory.measure_mono, Set.inter_subset_left, Mathlib.Tactic.Contrapose.contrapose₁, Not and 24 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.essProjSnd_inter_univ_times line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, Prod, Eq, MeasureTheory.essProjSnd, Inter.inter, SProd.sprod, Set.univ
Proof uses: Eq.mpr, MeasureTheory.essProjFst, Set.preimage, Prod.swap, id, congrArg, MeasureTheory.essProjSnd_eq_essProjFst_swap, Set.preimage_inter, Set.preimage_swap_prod, MeasureTheory.essProjFst_inter_times_univ, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.measurableSet_essProjFst line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, Set, Prod, MeasurableSet, MeasureTheory.essProjFst
Proof uses: Eq.mpr, Set.preimage, ENNReal, Prod.mk, Set.Ioi, OfNat.ofNat, id, Eq, congrArg, MeasureTheory.essProjFst_eq, measurable_measure_prodMk_left, measurableSet_Ioi
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.measurableSet_essProjSnd line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, Set, Prod, MeasurableSet, MeasureTheory.essProjSnd
Proof uses: Eq.mpr, MeasureTheory.essProjFst, Set.preimage, Prod.swap, id, Eq, congrArg, MeasureTheory.essProjSnd_eq_essProjFst_swap, MeasureTheory.measurableSet_essProjFst, Iff.mpr, measurableSet_swap_iff
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.measure_essProjFst_pos_iff line 160 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, Set, Prod, MeasurableSet, Iff, LT.lt, ENNReal, OfNat.ofNat, MeasureTheory.essProjFst, MeasureTheory.Measure.prod
Proof uses: Eq.mpr, MeasureTheory.lintegral, Set.preimage, Prod.mk, id, Eq, congrArg, MeasureTheory.Measure.prod_apply, Function.support, propext, MeasureTheory.lintegral_pos_iff_support, measurable_measure_prodMk_left, Eq.symm, MeasureTheory.essProjFst_eq', Iff.rfl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.measure_essProjSnd_pos_iff line 165 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, Set, Prod, MeasurableSet, Iff, LT.lt, ENNReal, OfNat.ofNat, MeasureTheory.essProjSnd, MeasureTheory.Measure.prod
Proof uses: Eq.mpr, MeasureTheory.lintegral, Set.preimage, Prod.mk, id, Eq, congrArg, MeasureTheory.Measure.prod_apply_symm, Function.support, propext, MeasureTheory.lintegral_pos_iff_support, measurable_measure_prodMk_right, Eq.symm, MeasureTheory.essProjSnd_eq', Iff.rfl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.exists_subset_measure_fst_image_lt_top line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SigmaFinite, MeasureTheory.SFinite, Set, Prod, MeasurableSet, LT.lt, ENNReal, OfNat.ofNat, MeasureTheory.Measure.prod, Exists, And, LE.le, Set.image, Prod.fst, Top.top
Proof uses: MeasureTheory.essProjFst, Eq.mpr, id, Eq, congrArg, propext, MeasureTheory.measure_essProjFst_pos_iff, MeasureTheory.Measure.exists_subset_measure_lt_top, MeasureTheory.measurableSet_essProjFst, Inter.inter, SProd.sprod, Set.univ, MeasurableSet.inter, MeasurableSet.prod, MeasurableSet.univ, Exists.intro, And.intro, Set.inter_subset_left, MeasureTheory.essProjFst_inter_times_univ, Set.inter_eq_right and 22 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.exists_subset_measure_snd_image_lt_top line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, MeasureTheory.SigmaFinite, Set, Prod, MeasurableSet, LT.lt, ENNReal, OfNat.ofNat, MeasureTheory.Measure.prod, Exists, And, LE.le, Set.image, Prod.snd, Top.top
Proof uses: Set.preimage, Prod.swap, Prod.fst, MeasureTheory.exists_subset_measure_fst_image_lt_top, Iff.mpr, measurableSet_swap_iff, Eq.mp, MeasureTheory.Measure.map, congrArg, MeasureTheory.Measure.map_apply, measurable_swap, Eq.symm, MeasureTheory.Measure.prod_swap, Exists.intro, And.intro, Set.image_swap_eq_preimage_swap, propext, Set.image_subset_iff, Eq.mpr, eq_of_heq and 18 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.exists_subset_measure_essProjFst_lt line 207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', MeasureTheory.SFinite, Set, Prod, MeasurableSet, LT.lt, ENNReal, OfNat.ofNat, MeasureTheory.Measure.prod, Exists, And, LE.le, MeasureTheory.essProjFst
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, propext, MeasureTheory.measure_essProjFst_pos_iff, MeasureTheory.NoAtoms'.exists_measurable_subset_lt, MeasureTheory.measurableSet_essProjFst, Inter.inter, SProd.sprod, Set.univ, MeasurableSet.inter, MeasurableSet.prod, MeasurableSet.univ, Exists.intro, And.intro, Set.inter_subset_left, MeasureTheory.essProjFst_inter_times_univ, Set.inter_eq_right and 16 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.exists_subset_measure_essProjSnd_lt line 227 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, MeasureTheory.NoAtoms', Set, Prod, MeasurableSet, LT.lt, ENNReal, OfNat.ofNat, MeasureTheory.Measure.prod, Exists, And, LE.le, MeasureTheory.essProjSnd
Proof uses: Set.preimage, Prod.swap, MeasureTheory.essProjFst, MeasureTheory.exists_subset_measure_essProjFst_lt, Iff.mpr, measurableSet_swap_iff, Eq.mp, MeasureTheory.Measure.map, congrArg, MeasureTheory.Measure.map_apply, measurable_swap, Eq.symm, MeasureTheory.Measure.prod_swap, Exists.intro, And.intro, Set.image, Set.image_swap_eq_preimage_swap, propext, Set.image_subset_iff, Eq.mpr and 5 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.setLIntegral_strict_mono_set TODO: move line 242 source
Source comment
TODO: move

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Set, Measurable, MeasurableSet, LE.le, SDiff.sdiff, Function.support, Ne, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Top.top, LT.lt
Proof uses: OfNat.ofNat, Eq.mpr, id, Eq, congrArg, propext, MeasureTheory.lintegral_pos_iff_support, Inter.inter, MeasureTheory.Measure.restrict_apply, measurableSet_support, Iff.mpr, Set.inter_eq_right, HSub.hSub, MeasureTheory.measure_sdiff, MeasurableSet.nullMeasurableSet, LT.lt.ne_top, tsub_pos_iff_lt, Trans.trans, HAdd.hAdd, rfl and 9 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem setLIntegral_strict_mono_set {α : Type*} {mα : MeasurableSpace α} {μ : Measure α}
  {f : α → ℝ≥0∞} {s t : Set α} (hf : Measurable f) (hsm : MeasurableSet s) (htm : MeasurableSet t)
  (htsf : t \ s ⊆ support f) (hfi : ∫⁻ (x : α) in s, f x ∂μ ≠ ∞) (hst : s ⊆ t) (h : μ s < μ t) :
    ∫⁻ (x : α) in s, f x ∂μ < ∫⁻ (x : α) in t, f x ∂μ := by
…
```
Mentions: s
instance MeasureTheory.prod.instNoAtoms_fst line 255 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', MeasureTheory.SFinite, MeasureTheory.SigmaFinite, Prod, MeasureTheory.Measure.prod
Proof uses: Eq.mpr, Set, MeasurableSet, LT.lt, ENNReal, OfNat.ofNat, Exists, And, LE.le, id, Eq, congrArg, propext, MeasureTheory.no_atoms_iff, Set.image, Prod.snd, Top.top, MeasureTheory.exists_subset_measure_snd_image_lt_top, MeasureTheory.essProjFst, MeasureTheory.exists_subset_measure_essProjFst_lt and 36 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.isAtom_swap_iff TODO: move? line 290 source
Source comment
TODO: move?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, Set, Prod, MeasurableSet, Iff, MeasureTheory.IsAtom, Set.preimage, Prod.swap, MeasureTheory.Measure.prod
Proof uses: id, Eq.mpr, And, LT.lt, ENNReal, OfNat.ofNat, LE.le, Or, Eq, MeasureTheory.Measure.map, congrArg, Eq.symm, MeasureTheory.Measure.map_apply, measurable_swap, MeasureTheory.Measure.prod_swap, Iff.intro, Eq.mp, propext, measurableSet_swap_iff, Set.preimage_subset_preimage_iff and 5 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem isAtom_swap_iff [SFinite μ] [SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) :
    IsAtom (Prod.swap ⁻¹' s) (ν.prod μ) ↔ IsAtom s (μ.prod ν) := by
…
```
Mentions: s, MeasureTheory.IsAtom
instance MeasureTheory.prod.instNoAtoms_snd line 309 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SigmaFinite, MeasureTheory.NoAtoms', MeasureTheory.SFinite, Prod, MeasureTheory.Measure.prod
Proof uses: MeasureTheory.NoAtoms'.mk, Set, MeasurableSet, Eq.mpr, Not, MeasureTheory.IsAtom, Set.preimage, Prod.swap, id, Eq, congrArg, Eq.symm, propext, MeasureTheory.isAtom_swap_iff, MeasureTheory.NoAtoms'.no_atoms, measurableSet_swap_iff
4 instances, coercions and auxiliary constants left out.

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