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

43 declarations, 0 contain sorry, 0 declared as axioms

Imports (4)

Imported by 2 files

theorem MeasureTheory.NoAtoms'.measure_comap_eq_subtype_coe TODO: move line 29 source
Source comment
TODO: move

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, MeasureTheory.NullMeasurableSet, Membership.mem, MeasureTheory.Measure.comap, Eq, ENNReal, Subtype, Set.image
Proof uses: MeasureTheory.Measure.comap_apply₀, Subtype.coe_injective, MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe
10 instances, coercions and auxiliary constants left out.
```
theorem measure_comap_eq_subtype_coe {α : Type*} {m0 : MeasurableSpace α} {μ : Measure α}
  {s : Set α} (hs : NullMeasurableSet s μ) {t : Set s}
  (ht : NullMeasurableSet t (μ.comap Subtype.val)) :
    μ.comap Subtype.val t = μ (((↑) : s → α) '' t) :=
…
```
Mentions: s
lemma MeasureTheory.NoAtoms'.subtype line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', Set, MeasurableSet, Membership.mem, MeasureTheory.Measure.comap
Proof uses: MeasureTheory.NoAtoms'.mk', LT.lt, ENNReal, OfNat.ofNat, And, LE.le, Set.image, Subtype, Exists, MeasureTheory.NoAtoms'.exists_measurable_subset_lt, MeasurableSet.subtype_image, Eq.mp, congrArg, comap_subtype_coe_apply, Exists.intro, Set.preimage, And.intro, Set.preimage_subset, Set.injOn_subtype_val, Eq.mpr and 4 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.exists_measurable_between line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', Set, MeasurableSet, MeasureTheory.NullMeasurableSet, LE.le, LT.lt, ENNReal, Exists, And
Proof uses: OfNat.ofNat, SDiff.sdiff, Trans.trans, HSub.hSub, Eq, rfl, Eq.mpr, id, MeasureTheory.le_measure_sdiff, MeasureTheory.NoAtoms'.exists_measurable_subset_lt₀, of_eq_true, Exists.intro, Union.union, And.intro, Set.subset_union_right, Eq.trans, True, congr, congrArg, eq_true and 15 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.exists_nullmeasurable_between line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', Set, MeasureTheory.NullMeasurableSet, LE.le, LT.lt, ENNReal, Exists, And
Proof uses: MeasurableSet, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq, Eq.mpr, id, Eq, congrArg, Eq.symm, Filter.EventuallyEq.measure_eq, MeasureTheory.NoAtoms'.exists_measurable_between, LE.le.trans, Eq.mp, Exists.intro, Union.union, And.intro, MeasureTheory.NullMeasurableSet.union, MeasurableSet.nullMeasurableSet, Set.subset_union_right, Set.union_subset and 19 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.mem_graph'_iff line 86 source
standard axioms: propext what this means
Statement uses: PFun, Iff, Membership.mem, Prod, SetRel, PFun.graph', Prod.mk, Part
Proof uses: id, of_eq_true, iff_self
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.NoAtoms'.PFun.ofGraph' Constructs a partial function `α → line 93 source
Source documentation
Constructs a partial function α →. β from its graph of type SetRel α β.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetRel, PFun
Proof uses: dite, Part, Exists, Membership.mem, Prod, Prod.mk, Classical.propDecidable, Part.some, Exists.choose, Not, Part.none
1 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
noncomputable def PFun.ofGraph' {β : Type*} (r : SetRel α β) : α →. β := fun a ↦ (by
…
```
theorem MeasureTheory.NoAtoms'.PFun.compare_of_mem_ofGraph' line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetRel, Membership.mem, Part, MeasureTheory.NoAtoms'.PFun.ofGraph', Prod, Prod.mk
Proof uses: Exists, Decidable, Classical.propDecidable, Not, False.elim, Eq.mp, Part.none, False, dite, Part.some, Exists.choose, congrFun', congrArg, dite_eq_right, Eq.mpr, id, Eq, dite_eq_left, Exists.choose_spec
7 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.mem_ofGraph'_of_compare line 111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetRel, Membership.mem, Prod, Prod.mk, Eq, Part, MeasureTheory.NoAtoms'.PFun.ofGraph'
Proof uses: id, dite, Exists, Classical.propDecidable, Part.some, Exists.choose, Not, Part.none, Eq.mpr, congrFun', congrArg, dite_eq_left, Exists.choose_spec, dite_eq_right, False, False.elim, Eq.mp, eq_false
7 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.mem_ofGraph'_iff_compare line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetRel, Membership.mem, Prod, Prod.mk, Eq, Iff, Part, MeasureTheory.NoAtoms'.PFun.ofGraph'
Proof uses: Iff.intro, MeasureTheory.NoAtoms'.PFun.compare_of_mem_ofGraph', MeasureTheory.NoAtoms'.PFun.mem_ofGraph'_of_compare
4 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.graph'_ofGraph' line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetRel, Membership.mem, Prod, Prod.mk, Eq, PFun.graph', MeasureTheory.NoAtoms'.PFun.ofGraph'
Proof uses: Set.ext, Iff, Set, Eq.mpr, Part, id, congrArg, propext, MeasureTheory.NoAtoms'.PFun.mem_graph'_iff, MeasureTheory.NoAtoms'.PFun.mem_ofGraph'_iff_compare, Iff.rfl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.graph_injective line 171 source
standard axioms: Quot.sound, propext what this means
Statement uses: Function.Injective, PFun, Set, Prod, PFun.graph
Proof uses: Eq, PFun.ext, Iff.mp, Iff, Membership.mem, Set.ext_iff, Prod.mk
1 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.graph'_injective line 176 source
standard axioms: Quot.sound, propext what this means
Statement uses: Function.Injective, PFun, SetRel, PFun.graph'
Proof uses: MeasureTheory.NoAtoms'.PFun.graph_injective
instance MeasureTheory.NoAtoms'.(instance at line 179) line 179 source
theorem MeasureTheory.NoAtoms'.PFun.le_iff line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PFun, Iff, LE.le, SetRel, Prod, PFun.graph'
Proof uses: Iff.rfl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.le_iff' line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PFun, Iff, LE.le, Membership.mem, Part
Proof uses: Eq.mpr, SetRel, Prod, PFun.graph', id, Eq, congrArg, propext, MeasureTheory.NoAtoms'.PFun.le_iff, of_eq_true, Set.ofPred, PFun.graph'.match_1, Eq.trans, True, congrFun', Set, Prod.fst, Prod.snd, Prod.mk, 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 MeasureTheory.NoAtoms'.PFun.Dom_mono line 188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PFun, LE.le, Set, PFun.Dom
Proof uses: id, Membership.mem, Set.ofPred, Part.Dom, Eq.mpr, Exists, Part, Eq, congrArg, propext, Part.dom_iff_mem, Exists.choose, Eq.mp, SetRel, Prod, PFun.graph'.match_1, Eq.trans, Prod.fst, Prod.snd, Prod.mk and 4 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.fn_mem line 199 source
no axioms what this means
Statement uses: PFun, Membership.mem, Set, PFun.Dom, Part, PFun.fn
Proof uses: Iff.mp, Eq, Part.get, Part.eq_get_iff_mem, rfl
4 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.NoAtoms'.PFun.fn_apply_eq_fn_apply_of_le line 203 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PFun, LE.le, Membership.mem, Set, PFun.Dom, Eq, PFun.fn, MeasureTheory.NoAtoms'.PFun.Dom_mono
Proof uses: Eq.mpr, Part.get, id, congrArg, PFun.fn_apply, Part, propext, Part.eq_get_iff_mem, Eq.mp, MeasureTheory.NoAtoms'.PFun.le_iff', MeasureTheory.NoAtoms'.PFun.fn_mem
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.apply_eq_of_le line 210 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PFun, LE.le, Membership.mem, Set, PFun.Dom, Eq, Part
Proof uses: Eq.mpr, Part.get, MeasureTheory.NoAtoms'.PFun.Dom_mono, id, congrArg, Eq.symm, propext, Part.eq_iff_of_dom, MeasureTheory.NoAtoms'.PFun.fn_apply_eq_fn_apply_of_le
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.NoAtoms'.(instance at line 215) line 215 source
theorem MeasureTheory.NoAtoms'.PFun.sSup_eq line 218 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, PFun, Eq, SupSet.sSup, MeasureTheory.NoAtoms'.PFun.ofGraph', Set.iUnion, Prod, Membership.mem, PFun.graph'
Proof uses: id, SupSet, of_eq_true, SupSet.mk, SetRel, Set.image, Eq.trans, True, congrFun', congrArg, funext, Set.sUnion_image, eq_self
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.exists_mem_of_mem_sSup line 223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, PFun, Membership.mem, Part, SupSet.sSup, Exists, And
Proof uses: Prod, SetRel, Set.iUnion, PFun.graph', Prod.mk, MeasureTheory.NoAtoms'.PFun.compare_of_mem_ofGraph', Eq.mp, SupSet, SupSet.mk, MeasureTheory.NoAtoms'.PFun.ofGraph', Set.image, congrFun', congrArg, funext, Set.sUnion_image, Eq.trans, propext, exists_prop_congr, Iff.of_eq, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.le_sSup line 232 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, PFun, IsChain, LE.le, Membership.mem, SupSet.sSup
Proof uses: Eq.mpr, MeasureTheory.NoAtoms'.PFun.ofGraph', Set.iUnion, Prod, PFun.graph', id, Eq, congrArg, MeasureTheory.NoAtoms'.PFun.sSup_eq, SetRel, propext, MeasureTheory.NoAtoms'.PFun.le_iff, MeasureTheory.NoAtoms'.PFun.graph'_ofGraph', Prod.mk, Eq.trans, And, Exists, implies_congr, funext, Eq.refl and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.mem_dom_of_mem line 251 source
standard axioms: Quot.sound, propext what this means
Statement uses: PFun, Membership.mem, Part, Set, PFun.Dom
Proof uses: Eq.mpr, Exists, id, Eq, Exists.intro
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.exists_fn_of_fn_sSup line 254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, PFun, IsChain, LE.le, Membership.mem, PFun.Dom, SupSet.sSup, Exists, And, Eq, PFun.fn
Proof uses: Part, MeasureTheory.NoAtoms'.PFun.exists_mem_of_mem_sSup, MeasureTheory.NoAtoms'.PFun.fn_mem, Exists.intro, And.intro, MeasureTheory.NoAtoms'.PFun.mem_dom_of_mem, Eq.symm, MeasureTheory.NoAtoms'.PFun.fn_apply_eq_fn_apply_of_le, MeasureTheory.NoAtoms'.PFun.le_sSup
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.NoAtoms'.PFun.insert Gives the partial function sending a to b and agreeing with f otherwise line 264 source
Source documentation
Gives the partial function sending a to b and agreeing with f otherwise.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PFun
Proof uses: ite, Part, Eq, Classical.propDecidable, Option.some
1 instances, coercions and auxiliary constants left out.
```
noncomputable def PFun.insert {β : Type*} (f : α →. β) (a : α) (b : β) : α →. β :=
…
```
theorem MeasureTheory.NoAtoms'.PFun.Dom_insert line 268 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PFun, Eq, Set, PFun.Dom, MeasureTheory.NoAtoms'.PFun.insert, Set.insert
Proof uses: id, ite, Part, Classical.propDecidable, Option.some, Set.ofPred, Part.Dom, Set.ext, Or, Membership.mem, Iff, dite, Part.some, Eq.mpr, congrFun', congrArg, ite_eq_left, of_eq_true, Eq.trans, True and 9 more
3 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.lt_insert line 276 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PFun, Not, Membership.mem, Set, PFun.Dom, And, LE.le, MeasureTheory.NoAtoms'.PFun.insert
Proof uses: id, And.intro, ite, Part, Eq, Classical.propDecidable, Option.some, Eq.mpr, congrArg, propext, MeasureTheory.NoAtoms'.PFun.le_iff', Decidable, Part.some, congrFun', ite_eq_right, ite_eq_left, False.elim, Eq.mp, False, eq_false and 11 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.Prop_insert line 287 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PFun, Membership.mem, Set, PFun.Dom, PFun.fn, MeasureTheory.NoAtoms'.PFun.insert
Proof uses: id, ite, Part, Eq, Classical.propDecidable, Option.some, dite, Part.get, Part.some, Eq.refl, Eq.mpr, Part.Dom, ite_eq_left, congrArg, Part.get.congr_simp, congrFun', Not, ite_eq_right
4 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.NoAtoms'.PFun.Monotone The property of a partial function f to be monotone, i.e. f a ≤ f b whenever a ≤ b and both a and b are in the domain of f line 300 source
Source documentation
The property of a partial function f to be monotone, i.e. f a ≤ f b whenever a ≤ b and both a and b are in the domain of f.

no axioms what this means
Statement uses: Preorder, PFun
Proof uses: Membership.mem, Set, PFun.Dom, LE.le, PFun.fn
2 instances, coercions and auxiliary constants left out.
```
def PFun.Monotone [Preorder α] {β : Type*} [Preorder β] (f : α →. β) : Prop :=
…
```
theorem MeasureTheory.NoAtoms'.PFun.Monotone.Monotone line 304 source
standard axioms: propext what this means
Statement uses: Preorder, PFun, MeasureTheory.NoAtoms'.PFun.Monotone, Monotone, PFun.Dom, Membership.mem, Set, PFun.fn, Subtype.property
Proof uses: LE.le, Eq.mpr, Subtype, id, Eq
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.PFun.Monotone.insert line 312 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Preorder, PFun, MeasureTheory.NoAtoms'.PFun.Monotone, LE.le, Membership.mem, Set, PFun.Dom, PFun.fn, GE.ge, MeasureTheory.NoAtoms'.PFun.insert
Proof uses: id, ite, Part, Eq, Classical.propDecidable, Option.some, dite, Part.get, Part.some, Eq.refl, Eq.mpr, Part.Dom, ite_eq_left, congrFun', congrArg, Part.get.congr_simp, of_eq_true, Not, ite_eq_right, Eq.symm and 6 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.NoAtoms'.TopologicalSpace.SeparableSpace.subtype TODO: move line 336 source
Source comment
TODO: move

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, TopologicalSpace.SeparableSpace, TopologicalSpace.PseudoMetrizableSpace, Set, Membership.mem
Proof uses: TopologicalSpace.IsSeparable.separableSpace, TopologicalSpace.IsSeparable.of_separableSpace
3 instances, coercions and auxiliary constants left out.
```
instance TopologicalSpace.SeparableSpace.subtype {X : Type*} [TopologicalSpace X] [SeparableSpace X]
    [PseudoMetrizableSpace X] {s : Set X} : SeparableSpace ↑s :=
…
```
Mentions: s
instance MeasureTheory.NoAtoms'.ClosedIicTopology.subtype TODO: move line 341 source
Source comment
TODO: move

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Preorder, ClosedIicTopology, Subtype
Proof uses: ClosedIicTopology.mk, Eq.mpr, IsClosed, Set.Iic, Set.preimage, id, Eq, congrArg, Set, Eq.symm, Set.preimage_subtype_val_Iic, isClosed_induced, isClosed_Iic
5 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
instance ClosedIicTopology.subtype [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {p : α → Prop} :
    ClosedIicTopology (Subtype p) where
…
```
instance MeasureTheory.NoAtoms'.instIsCountablyGenerated_atTop TODO: move line 349 source
Source comment
TODO: move

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, LinearOrder, ClosedIicTopology, TopologicalSpace.SeparableSpace, Filter.IsCountablyGenerated, Filter.atTop
Proof uses: Eq, Set, Set.ofPred, IsTop, EmptyCollection.emptyCollection, Set.Nonempty, Or, Set.eq_empty_or_nonempty, And, Set.Countable, Dense, Exists, TopologicalSpace.exists_countable_dense, Filter, Filter.generate, Set.image, Set.Ici, Filter.atTop_eq_generate_of_not_bddAbove, BddAbove, False and 23 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
instance instIsCountablyGenerated_atTop [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [SeparableSpace α] :
    IsCountablyGenerated (atTop : Filter α) := by
…
```
instance MeasureTheory.NoAtoms'.instIsCountablyGenerated_atBot TODO: move line 364 source
Source comment
TODO: move

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, LinearOrder, ClosedIciTopology, TopologicalSpace.SeparableSpace, Filter.IsCountablyGenerated, Filter.atBot
Proof uses: OrderDual
16 instances, coercions and auxiliary constants left out.
```
instance instIsCountablyGenerated_atBot [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [SeparableSpace α] :
    IsCountablyGenerated (atBot : Filter α) :=
…
```
theorem MeasureTheory.NoAtoms'.iInter_of_monotone_of_frequently line 368 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Preorder, Filter.IsCountablyGenerated, Filter.atBot, Set, Monotone, Filter.Frequently, MeasurableSet, Set.iInter
Proof uses: Nat, And, Filter.Tendsto, Filter.atTop, Exists, Filter.exists_seq_forall_of_frequently, Eq.mpr, id, Eq, congrArg, Eq.symm, Monotone.iInter_comp_tendsto_atBot, MeasurableSet.iInter
25 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.iInter_of_monotone line 375 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Preorder, IsCodirectedOrder, Filter.IsCountablyGenerated, Filter.atBot, Set, Monotone, MeasurableSet, Set.iInter
Proof uses: IsEmpty, Nonempty, Or, Eq, isEmpty_or_nonempty, Or.inl, of_eq_true, Eq.trans, Set.univ, True, congrArg, Set.iInter_of_empty, Or.inr, MeasureTheory.NoAtoms'.iInter_of_monotone_of_frequently, Filter.Frequently.of_forall, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.exists_measurable_sets_measure_eq line 383 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', Exists, ENNReal, Set.Iic, Set, Set.univ, And, Monotone, Membership.mem, MeasurableSet, Eq
Proof uses: PFun, Set.ofPred, MeasureTheory.NoAtoms'.PFun.Monotone, PFun.Dom, PFun.fn, LE.le, zorn_le₀, IsChain, Exists.intro, SupSet.sSup, And.intro, id, Eq.mpr, Part, Eq.substr, congrFun', congrArg, funext, forall_congr, Eq.trans and 95 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 272 steps (first 200 of 272)
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.exists_measurable_set_measure_eq line 622 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', ENNReal, LE.le, Set, Set.univ, Exists, And, MeasurableSet, Eq
Proof uses: Set.Iic, Monotone, Membership.mem, MeasureTheory.NoAtoms'.exists_measurable_sets_measure_eq, Exists.intro, Subtype.mk
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.exists_measurable_subset_measure_eq line 628 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', Set, MeasureTheory.NullMeasurableSet, ENNReal, LE.le, Exists, And, MeasurableSet, Eq
Proof uses: Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq, Membership.mem, MeasureTheory.Measure.comap, Set.univ, id, LE.le.trans', Subtype, Set.image, MeasureTheory.Measure.measure_subtype_coe_le_comap, MeasurableSet.nullMeasurableSet, Eq.mpr, congrArg, Eq.trans, Set.range, Set.ofPred, Set.image_univ, Subtype.range_coe_subtype, Filter.EventuallyEq.measure_eq and 11 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.exists_measurable_between_measure_eq line 642 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', Set, MeasurableSet, MeasureTheory.NullMeasurableSet, LE.le, ENNReal, Exists, And, Eq
Proof uses: HSub.hSub, SDiff.sdiff, Trans.trans, rfl, tsub_le_tsub, le_refl, MeasureTheory.le_measure_sdiff, MeasureTheory.NoAtoms'.exists_measurable_subset_measure_eq, of_eq_true, Exists.intro, Union.union, And.intro, Set.subset_union_right, Eq.trans, True, congr, congrArg, eq_true, Iff.mp, Disjoint and 10 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.exists_nullmeasurable_between_measure_eq line 656 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', Set, MeasureTheory.NullMeasurableSet, LE.le, ENNReal, Exists, And, Eq
Proof uses: MeasurableSet, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq, MeasureTheory.NoAtoms'.exists_measurable_between_measure_eq, LE.le.trans, Eq.mp, congrArg, Eq.symm, Filter.EventuallyEq.measure_eq, Exists.intro, Union.union, And.intro, MeasureTheory.NullMeasurableSet.union, MeasurableSet.nullMeasurableSet, Set.subset_union_right, Set.union_subset, Trans.trans, rfl, MeasureTheory.measure_congr and 13 more
22 instances, coercions and auxiliary constants left out.

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