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

137 declarations, 0 contain sorry, 0 declared as axioms

Annulus

In this file we define an annulus in a pseudometric space X to be a set consisting of all y such that dist x y lies in an interval between r and R. An annulus is defined for each type of interval (Ioo, Ioc, etc.) with a parallel naming scheme, except that we do not define annuli for Iio and Iic, as they would be balls.

We also define EAnnulus similarly using edist instead of dist.

Upstreaming status: ready; two style questions should be answered in the process (see below).

Tags

annulus, eannulus

Imports (2)

Imported by 2 files

def Set.Annulus.oc Set.Annulus.oo has moved to Defs.lean line 42 source
Source comment
`Set.Annulus.oo` has moved to `Defs.lean`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Set
Proof uses: Set.ofPred, Membership.mem, Set.Ioc, Dist.dist
3 instances, coercions and auxiliary constants left out.
```
def oc (x : X) (r R : ℝ) := {y | dist x y ∈ Ioc r R}
```
def Set.Annulus.co line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Set
Proof uses: Set.ofPred, Membership.mem, Set.Ico, Dist.dist
3 instances, coercions and auxiliary constants left out.
def Set.Annulus.cc line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Set
Proof uses: Set.ofPred, Membership.mem, Set.Icc, Dist.dist
3 instances, coercions and auxiliary constants left out.
def Set.Annulus.oi line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Set
Proof uses: Set.ofPred, Membership.mem, Set.Ioi, Dist.dist
3 instances, coercions and auxiliary constants left out.
def Set.Annulus.ci line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Set
Proof uses: Set.ofPred, Membership.mem, Set.Ici, Dist.dist
3 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oo_eq line 48 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Eq, Set, Set.Annulus.oo, Inter.inter, Metric.ball, Compl.compl, Metric.closedBall
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, And, LT.lt, Dist.dist, True, congr, congrArg, congrFun', Set.ofPred, Set.Ioo, funext, dist_comm, Not, LE.le, iff_self
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.oc_eq line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Eq, Set, Set.Annulus.oc, Inter.inter, Metric.closedBall, Compl.compl
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, And, LE.le, Dist.dist, LT.lt, True, congr, congrArg, congrFun', Set.ofPred, Set.Ioc, funext, dist_comm, Not, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.co_eq line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Eq, Set, Set.Annulus.co, Inter.inter, Metric.ball, Compl.compl
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, And, LE.le, Dist.dist, LT.lt, True, congr, congrArg, congrFun', Set.ofPred, Set.Ico, funext, dist_comm, Not, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.cc_eq line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Eq, Set, Set.Annulus.cc, Inter.inter, Metric.closedBall, Compl.compl, Metric.ball
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, And, LE.le, Dist.dist, True, congr, congrArg, congrFun', Set.ofPred, Set.Icc, funext, dist_comm, Not, LT.lt, iff_self
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.oi_eq line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Eq, Set, Set.Annulus.oi, Compl.compl, Metric.closedBall
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, LT.lt, Dist.dist, True, congr, congrArg, congrFun', Set.ofPred, Set.Ioi, funext, Not, LE.le, dist_comm, 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 Set.Annulus.ci_eq line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Eq, Set, Set.Annulus.ci, Compl.compl, Metric.ball
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, LE.le, Dist.dist, True, congr, congrArg, congrFun', Set.ofPred, Set.Ici, funext, Not, LT.lt, dist_comm, 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 Set.Annulus.oo_eq_empty line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Eq, Set, Set.Annulus.oo, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Membership.mem, Set.Ioo, Dist.dist, False, Set.ofPred, funext, Set.Ioo_eq_empty_of_le, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.oc_eq_empty line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Eq, Set, Set.Annulus.oc, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Membership.mem, Set.Ioc, Dist.dist, False, Set.ofPred, funext, Set.Ioc_eq_empty_of_le, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.co_eq_empty line 75 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Eq, Set, Set.Annulus.co, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Membership.mem, Set.Ico, Dist.dist, False, Set.ofPred, funext, Set.Ico_eq_empty_of_le, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.cc_eq_empty line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LT.lt, Eq, Set, Set.Annulus.cc, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Membership.mem, Set.Icc, Dist.dist, False, Set.ofPred, funext, Set.Icc_eq_empty_of_lt, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.oo_subset_oo line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.oo
Proof uses: Membership.mem, LT.lt, Dist.dist, And.intro, lt_of_le_of_lt, lt_of_lt_of_le
8 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oo_subset_oc line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.oo, Set.Annulus.oc
Proof uses: Membership.mem, LT.lt, Dist.dist, And.intro, lt_of_le_of_lt, LE.le.trans, LT.lt.le
9 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oo_subset_co line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.oo, Set.Annulus.co
Proof uses: Membership.mem, LT.lt, Dist.dist, And.intro, LE.le.trans, LT.lt.le, lt_of_lt_of_le
9 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oo_subset_cc line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.oo, Set.Annulus.cc
Proof uses: Membership.mem, LT.lt, Dist.dist, And.intro, LE.le.trans, LT.lt.le
9 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oo_subset_oi line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.oo, Set.Annulus.oi
Proof uses: Membership.mem, LT.lt, Dist.dist, lt_of_le_of_lt
8 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oo_subset_ci line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.oo, Set.Annulus.ci
Proof uses: Membership.mem, LT.lt, Dist.dist, LE.le.trans, LT.lt.le
8 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oc_subset_oo line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, LT.lt, Set, Set.Annulus.oc, Set.Annulus.oo
Proof uses: Membership.mem, Dist.dist, And.intro, lt_of_le_of_lt
11 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oc_subset_oc line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.oc
Proof uses: Membership.mem, LT.lt, Dist.dist, And.intro, lt_of_le_of_lt, LE.le.trans
9 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oc_subset_co line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, LT.lt, Set, Set.Annulus.oc, Set.Annulus.co
Proof uses: Membership.mem, Dist.dist, And.intro, LE.le.trans, LT.lt.le, lt_of_le_of_lt
11 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oc_subset_cc line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.oc, Set.Annulus.cc
Proof uses: Membership.mem, LT.lt, Dist.dist, And.intro, LT.lt.le, lt_of_le_of_lt, LE.le.trans
9 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oc_subset_oi line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.oo, Set.Annulus.oi
Proof uses: Membership.mem, LT.lt, Dist.dist, lt_of_le_of_lt
8 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oc_subset_ci line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.oc, Set.Annulus.ci
Proof uses: Membership.mem, LT.lt, Dist.dist, LE.le.trans, LT.lt.le
9 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.co_subset_oo line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LT.lt, LE.le, Set, Set.Annulus.co, Set.Annulus.oo
Proof uses: Membership.mem, Dist.dist, And.intro, lt_of_lt_of_le
11 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.co_subset_oc line 132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LT.lt, LE.le, Set, Set.Annulus.co, Set.Annulus.oc
Proof uses: Membership.mem, Dist.dist, And.intro, lt_of_lt_of_le, LE.le.trans, LT.lt.le
11 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.co_subset_co line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.co
Proof uses: Membership.mem, Dist.dist, LT.lt, And.intro, LE.le.trans, lt_of_lt_of_le
9 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.co_subset_cc line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.co, Set.Annulus.cc
Proof uses: Membership.mem, Dist.dist, LT.lt, And.intro, LE.le.trans, LT.lt.le
9 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.co_subset_oi line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LT.lt, LE.le, Set, Set.Annulus.co, Set.Annulus.oi
Proof uses: Membership.mem, Dist.dist, lt_of_lt_of_le
9 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.co_subset_ci line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.co, Set.Annulus.ci
Proof uses: Membership.mem, Dist.dist, LT.lt, LE.le.trans
9 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.cc_subset_oo line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LT.lt, LE.le, Set, Set.Annulus.cc, Set.Annulus.oo
Proof uses: Membership.mem, Dist.dist, And.intro, lt_of_lt_of_le, lt_of_le_of_lt
9 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.cc_subset_oc line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LT.lt, LE.le, Set, Set.Annulus.cc, Set.Annulus.oc
Proof uses: Membership.mem, Dist.dist, And.intro, lt_of_lt_of_le, LE.le.trans
11 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.cc_subset_co line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, LT.lt, Set, Set.Annulus.cc, Set.Annulus.co
Proof uses: Membership.mem, Dist.dist, And.intro, LE.le.trans, lt_of_le_of_lt
11 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.cc_subset_cc line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.cc
Proof uses: Membership.mem, Dist.dist, And.intro, LE.le.trans
8 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.cc_subset_oi line 168 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LT.lt, LE.le, Set, Set.Annulus.cc, Set.Annulus.oi
Proof uses: Membership.mem, Dist.dist, lt_of_lt_of_le
8 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.cc_subset_ci line 171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.cc, Set.Annulus.ci
Proof uses: Membership.mem, Dist.dist, LE.le.trans
8 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oo_subset_ball line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.oo, Metric.ball
Proof uses: Membership.mem, LT.lt, Dist.dist, Iff.mpr, Metric.mem_ball'
7 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oc_subset_closedBall line 177 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.oc, Metric.closedBall
Proof uses: Membership.mem, LT.lt, Dist.dist, Iff.mpr, Metric.mem_closedBall'
8 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.co_subset_ball line 180 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.co, Metric.ball
Proof uses: Membership.mem, Dist.dist, LT.lt, Iff.mpr, Metric.mem_ball'
8 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.cc_subset_closedBall line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Set, Set.Annulus.cc, Metric.closedBall
Proof uses: Membership.mem, Dist.dist, Iff.mpr, Metric.mem_closedBall'
7 instances, coercions and auxiliary constants left out.
lemma Set.Annulus.oc_union_oo line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, LT.lt, Eq, Set, Union.union, Set.Annulus.oc, Set.Annulus.oo
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ioc, Dist.dist, Eq.mpr, Set.Ioo, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ioc_union_Ioo_eq_Ioo, iff_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.oc_union_oc line 193 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Eq, Set, Union.union, Set.Annulus.oc
Proof uses: Set.ext, id, Iff, Membership.mem, Eq.mpr, Set.ofPred, Set.Ioc, Dist.dist, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ioc_union_Ioc_eq_Ioc, iff_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.oo_union_co line 198 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LT.lt, LE.le, Eq, Set, Union.union, Set.Annulus.oo, Set.Annulus.co
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ioo, Dist.dist, Eq.mpr, Set.Ico, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ioo_union_Ico_eq_Ioo, iff_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.oo_union_cc line 203 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LT.lt, LE.le, Eq, Set, Union.union, Set.Annulus.oo, Set.Annulus.cc, Set.Annulus.oc
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ioo, Dist.dist, Set.Icc, Eq.mpr, Set.Ioc, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ioo_union_Icc_eq_Ioc, iff_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.cc_union_oo line 208 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, LT.lt, Eq, Set, Union.union, Set.Annulus.cc, Set.Annulus.oo, Set.Annulus.co
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Icc, Dist.dist, Set.Ioo, Eq.mpr, Set.Ico, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Icc_union_Ioo_eq_Ico, iff_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.cc_union_oc line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Eq, Set, Union.union, Set.Annulus.cc, Set.Annulus.oc
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Icc, Dist.dist, Eq.mpr, Set.Ioc, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Icc_union_Ioc_eq_Icc, iff_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.co_union_co line 218 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Eq, Set, Union.union, Set.Annulus.co
Proof uses: Set.ext, id, Iff, Membership.mem, Eq.mpr, Set.ofPred, Set.Ico, Dist.dist, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ico_union_Ico_eq_Ico, iff_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.co_union_cc line 223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Eq, Set, Union.union, Set.Annulus.co, Set.Annulus.cc
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ico, Dist.dist, Eq.mpr, Set.Icc, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ico_union_Icc_eq_Icc, iff_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.oc_union_oi line 228 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Eq, Set, Union.union, Set.Annulus.oc, Set.Annulus.oi
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ioc, Dist.dist, Eq.mpr, Set.Ioi, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ioc_union_Ioi_eq_Ioi, iff_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.oo_union_ci line 232 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LT.lt, Eq, Set, Union.union, Set.Annulus.oo, Set.Annulus.ci, Set.Annulus.oi
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ioo, Dist.dist, Set.Ici, Eq.mpr, Set.Ioi, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ioo_union_Ici_eq_Ioi, iff_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.cc_union_oi line 237 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Eq, Set, Union.union, Set.Annulus.cc, Set.Annulus.oi, Set.Annulus.ci
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Icc, Dist.dist, Set.Ioi, Eq.mpr, Set.Ici, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Icc_union_Ioi_eq_Ici, iff_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.co_union_ci line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, Eq, Set, Union.union, Set.Annulus.co, Set.Annulus.ci
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ico, Dist.dist, Eq.mpr, Set.Ici, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ico_union_Ici_eq_Ici, iff_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Set.Annulus.biUnion_Ici_co_map_succ Union formula for Set.Annulus.co x (f i) (f (Order.succ i)) over i ∈ Ici a line 248 source
Source documentation
Union formula for Set.Annulus.co x (f i) (f (Order.succ i)) over i ∈ Ici a. See also iUnion_co_map_succ_eq_ci for the specialization a = ⊥.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, LinearOrder, SuccOrder, IsSuccArchimedean, Real, Membership.mem, Set, Set.Ici, LE.le, Not, BddAbove, Set.image, Eq, Set.iUnion, Set.Annulus.co, Order.succ, Set.Annulus.ci
Proof uses: of_eq_true, Eq.trans, Set.ofPred, Exists, And, Dist.dist, LT.lt, True, congr, congrArg, funext, Set.Ico, Set.iUnion_ofPred, propext, exists_prop_congr, Iff.of_eq, Eq.refl, congrFun', Eq.symm, biUnion_Ici_Ico_map_succ and 2 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem biUnion_Ici_co_map_succ [SuccOrder α] [IsSuccArchimedean α] {x : X} {f : α → ℝ}
    {a : α} (hf : ∀ i ∈ Ici a, f a ≤ f i) (h2f : ¬BddAbove (f '' Ici a)) :
    ⋃ i ∈ Ici a, co x (f i) (f (succ i)) = ci x (f a) := by
…
```
Mentions: Set.Annulus.co, Set.Annulus.ci
theorem Set.Annulus.biUnion_Ici_oc_map_succ Union formula for Set.Annulus.oc x (f i) (f (Order.succ i)) over i ∈ Ici a line 255 source
Source documentation
Union formula for Set.Annulus.oc x (f i) (f (Order.succ i)) over i ∈ Ici a. See also iUnion_oc_map_succ_eq_oi for the specialization a = ⊥.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, LinearOrder, SuccOrder, IsSuccArchimedean, Real, Membership.mem, Set, Set.Ici, LE.le, Not, BddAbove, Set.image, Eq, Set.iUnion, Set.Annulus.oc, Order.succ, Set.Annulus.oi
Proof uses: of_eq_true, Eq.trans, Set.ofPred, Exists, And, LT.lt, Dist.dist, True, congr, congrArg, funext, Set.Ioc, Set.iUnion_ofPred, propext, exists_prop_congr, Iff.of_eq, Eq.refl, Set.Ioi, congrFun', Eq.symm and 3 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem biUnion_Ici_oc_map_succ [SuccOrder α] [IsSuccArchimedean α] {x : X} {f : α → ℝ}
    {a : α} (hf : ∀ i ∈ Ici a, f a ≤ f i) (h2f : ¬BddAbove (f '' Ici a)) :
    ⋃ i ∈ Ici a, oc x (f i) (f (succ i)) = oi x (f a) := by
…
```
Mentions: Set.Annulus.oc, Set.Annulus.oi
theorem Set.Annulus.iUnion_co_map_succ_eq_ci Special case a = ⊥ of biUnion_Ici_co_map_succ line 261 source
Source documentation
Special case a = ⊥ of biUnion_Ici_co_map_succ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, LinearOrder, OrderBot, SuccOrder, IsSuccArchimedean, Real, LE.le, Bot.bot, Not, BddAbove, Set.range, Eq, Set, Set.iUnion, Set.Annulus.co, Order.succ, Set.Annulus.ci
Proof uses: Eq.mp, Membership.mem, Set.Ici, congrFun', congrArg, funext, Eq.trans, True, Set.iUnion_congr_Prop, Iff.of_eq, Set.univ, Set.Ici_bot, Eq.refl, Set.iUnion_true, Set.Annulus.biUnion_Ici_co_map_succ, Eq.mpr, id, forall_congr, implies_congr, Set.image and 1 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem iUnion_co_map_succ_eq_ci [OrderBot α] [SuccOrder α] [IsSuccArchimedean α] {x : X}
    {f : α → ℝ} (hf : ∀ a, f ⊥ ≤ f a) (h2f : ¬BddAbove (range f)) :
    (⋃ a : α, co x (f a) (f (succ a))) = ci x (f ⊥) := by
…
```
Mentions: Set.Annulus.co, Set.Annulus.ci
theorem Set.Annulus.iUnion_oc_map_succ_eq_oi Special case a = ⊥ of biUnion_Ici_oc_map_succ line 267 source
Source documentation
Special case a = ⊥ of biUnion_Ici_oc_map_succ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, LinearOrder, OrderBot, SuccOrder, IsSuccArchimedean, Real, LE.le, Bot.bot, Not, BddAbove, Set.range, Eq, Set, Set.iUnion, Set.Annulus.oc, Order.succ, Set.Annulus.oi
Proof uses: Eq.mp, Membership.mem, Set.Ici, congrFun', congrArg, funext, Eq.trans, True, Set.iUnion_congr_Prop, Iff.of_eq, Set.univ, Set.Ici_bot, Eq.refl, Set.iUnion_true, Set.Annulus.biUnion_Ici_oc_map_succ, Eq.mpr, id, forall_congr, implies_congr, Set.image and 1 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem iUnion_oc_map_succ_eq_oi [OrderBot α] [SuccOrder α] [IsSuccArchimedean α] {x : X}
    {f : α → ℝ} (hf : ∀ a, f ⊥ ≤ f a) (h2f : ¬BddAbove (range f)) :
    (⋃ a : α, oc x (f a) (f (succ a))) = oi x (f ⊥) := by
…
```
Mentions: Set.Annulus.oc, Set.Annulus.oi
theorem Set.Annulus.pairwise_disjoint_on_co_succ line 284 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, LinearOrder, SuccOrder, Real, Monotone, Pairwise, Function.onFun, Set, Disjoint, Set.Annulus.co, Order.succ
Proof uses: Ne, Disjoint.preimage, Dist.dist, Set.Ico, Monotone.pairwise_disjoint_on_Ico_succ
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Set.Annulus.pairwise_disjoint_on_oc_succ line 290 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, LinearOrder, SuccOrder, Real, Monotone, Pairwise, Function.onFun, Set, Disjoint, Set.Annulus.oc, Order.succ
Proof uses: Ne, Disjoint.preimage, Dist.dist, Set.Ioc, Monotone.pairwise_disjoint_on_Ioc_succ
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.measurableSet_oo line 299 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, OpensMeasurableSpace, Real, MeasurableSet, Set.Annulus.oo
Proof uses: Eq.mpr, Inter.inter, Set, Metric.ball, Compl.compl, Metric.closedBall, id, Eq, congrArg, Set.Annulus.oo_eq, MeasurableSet.inter, measurableSet_ball, measurableSet_closedBall
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.measurableSet_oc line 303 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, OpensMeasurableSpace, Real, MeasurableSet, Set.Annulus.oc
Proof uses: Eq.mpr, Inter.inter, Set, Metric.closedBall, Compl.compl, id, Eq, congrArg, Set.Annulus.oc_eq, MeasurableSet.inter, measurableSet_closedBall
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.measurableSet_co line 307 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, OpensMeasurableSpace, Real, MeasurableSet, Set.Annulus.co
Proof uses: Eq.mpr, Inter.inter, Set, Metric.ball, Compl.compl, id, Eq, congrArg, Set.Annulus.co_eq, MeasurableSet.inter, measurableSet_ball
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.measurableSet_cc line 311 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, OpensMeasurableSpace, Real, MeasurableSet, Set.Annulus.cc
Proof uses: Eq.mpr, Inter.inter, Set, Metric.closedBall, Compl.compl, Metric.ball, id, Eq, congrArg, Set.Annulus.cc_eq, MeasurableSet.inter, measurableSet_closedBall, measurableSet_ball
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.measurableSet_oi line 315 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, OpensMeasurableSpace, Real, MeasurableSet, Set.Annulus.oi
Proof uses: Eq.mpr, Compl.compl, Set, Metric.closedBall, id, Eq, congrArg, Set.Annulus.oi_eq, measurableSet_closedBall
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.Annulus.measurableSet_ci line 319 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, OpensMeasurableSpace, Real, MeasurableSet, Set.Annulus.ci
Proof uses: Eq.mpr, Compl.compl, Set, Metric.ball, id, Eq, congrArg, Set.Annulus.ci_eq, measurableSet_ball
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Set.EAnnulus.oc Set.EAnnulus.oo has moved to Defs.lean line 329 source
Source comment
`Set.EAnnulus.oo` has moved to `Defs.lean`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, Set
Proof uses: Set.ofPred, Membership.mem, Set.Ioc, EDist.edist
8 instances, coercions and auxiliary constants left out.
```
def oc (x : X) (r R : ℝ≥0∞) := {y | edist x y ∈ Ioc r R}
```
def Set.EAnnulus.co line 330 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, Set
Proof uses: Set.ofPred, Membership.mem, Set.Ico, EDist.edist
8 instances, coercions and auxiliary constants left out.
def Set.EAnnulus.cc line 331 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, Set
Proof uses: Set.ofPred, Membership.mem, Set.Icc, EDist.edist
8 instances, coercions and auxiliary constants left out.
def Set.EAnnulus.oi line 332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, Set
Proof uses: Set.ofPred, Membership.mem, Set.Ioi, EDist.edist
8 instances, coercions and auxiliary constants left out.
def Set.EAnnulus.ci line 333 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, Set
Proof uses: Set.ofPred, Membership.mem, Set.Ici, EDist.edist
8 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oo_eq_annulus line 335 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, OfNat.ofNat, Eq, Set, Set.EAnnulus.oo, ENNReal.ofReal, Set.Annulus.oo
Proof uses: id, Set.ofPred, Membership.mem, ENNReal, Set.Ioo, EDist.edist, Eq.mpr, Dist.dist, congrFun', congrArg, funext, edist_dist, And, LT.lt, congr, propext, ENNReal.ofReal_lt_ofReal_iff_of_nonneg, of_eq_true, Eq.trans, True and 2 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oc_eq_annulus line 340 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, OfNat.ofNat, Eq, Set, Set.EAnnulus.oc, ENNReal.ofReal, Set.Annulus.oc
Proof uses: dite, id, Set.ofPred, Membership.mem, ENNReal, Set.Ioc, EDist.edist, Eq.mpr, Dist.dist, congrFun', congrArg, funext, edist_dist, And, LT.lt, congr, propext, ENNReal.ofReal_lt_ofReal_iff_of_nonneg, of_eq_true, Eq.trans and 15 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.co_eq_annulus line 351 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Eq, Set, Set.EAnnulus.co, ENNReal.ofReal, Set.Annulus.co
Proof uses: id, Set.ofPred, Membership.mem, ENNReal, Set.Ico, EDist.edist, Eq.mpr, Dist.dist, congrFun', congrArg, funext, edist_dist, And, LE.le, LT.lt, congr, propext, ENNReal.ofReal_le_ofReal_iff, dist_nonneg, of_eq_true and 4 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.cc_eq_annulus line 356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Or, LT.lt, OfNat.ofNat, LE.le, Eq, Set, Set.EAnnulus.cc, ENNReal.ofReal, Set.Annulus.cc
Proof uses: dite, id, Set.ofPred, Membership.mem, ENNReal, Set.Icc, EDist.edist, Eq.mpr, Dist.dist, congrFun', congrArg, funext, edist_dist, And, congr, propext, ENNReal.ofReal_le_ofReal_iff, dist_nonneg, of_eq_true, Eq.trans and 15 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oi_eq_annulus line 367 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, OfNat.ofNat, Eq, Set, Set.EAnnulus.oi, ENNReal.ofReal, Set.Annulus.oi
Proof uses: id, Set.ofPred, Membership.mem, ENNReal, Set.Ioi, EDist.edist, Eq.mpr, Dist.dist, congrFun', congrArg, funext, edist_dist, LT.lt, congr, of_eq_true, Eq.trans, True, propext, ENNReal.ofReal_lt_ofReal_iff_of_nonneg, eq_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.ci_eq_annulus line 370 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Eq, Set, Set.EAnnulus.ci, ENNReal.ofReal, Set.Annulus.ci
Proof uses: id, Set.ofPred, Membership.mem, ENNReal, Set.Ici, EDist.edist, Eq.mpr, Dist.dist, congrFun', congrArg, funext, edist_dist, LE.le, congr, of_eq_true, Eq.trans, True, propext, ENNReal.ofReal_le_ofReal_iff, dist_nonneg and 1 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oo_eq_of_lt_top line 373 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, Top.top, Eq, Set, Set.EAnnulus.oo, Inter.inter, Metric.ball, ENNReal.toReal, Compl.compl, Metric.closedBall
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, And, Real, Dist.dist, True, congr, congrArg, congrFun', Set.ofPred, Set.Ioo, EDist.edist, funext, ENNReal.ofReal, edist_dist, propext, ENNReal.lt_ofReal_iff_toReal_lt and 7 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oc_eq_of_lt_top line 379 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, Top.top, Eq, Set, Set.EAnnulus.oc, Inter.inter, Metric.closedBall, ENNReal.toReal, Compl.compl
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, And, LE.le, Real, Dist.dist, True, congr, congrArg, congrFun', Set.ofPred, Set.Ioc, EDist.edist, funext, ENNReal.ofReal, edist_dist, propext and 6 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.co_eq_of_lt_top line 385 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, Top.top, Eq, Set, Set.EAnnulus.co, Inter.inter, Metric.ball, ENNReal.toReal, Compl.compl
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, And, LE.le, Real, Dist.dist, True, congr, congrArg, congrFun', Set.ofPred, Set.Ico, EDist.edist, funext, ENNReal.ofReal, edist_dist, propext and 7 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.cc_eq_of_lt_top line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, Top.top, Eq, Set, Set.EAnnulus.cc, Inter.inter, Metric.closedBall, ENNReal.toReal, Compl.compl, Metric.ball
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, And, LE.le, Real, Dist.dist, True, congr, congrArg, congrFun', Set.ofPred, Set.Icc, EDist.edist, funext, ENNReal.ofReal, edist_dist, propext and 7 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oi_eq_of_lt_top line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, Top.top, Eq, Set, Set.EAnnulus.oi, Compl.compl, Metric.closedBall, ENNReal.toReal
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Real, Dist.dist, True, congr, congrArg, congrFun', Set.ofPred, Set.Ioi, EDist.edist, funext, ENNReal.ofReal, edist_dist, propext, ENNReal.lt_ofReal_iff_toReal_lt, LT.lt.ne and 4 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.ci_eq_of_lt_top line 400 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, Top.top, Eq, Set, Set.EAnnulus.ci, Compl.compl, Metric.ball, ENNReal.toReal
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, LE.le, Real, Dist.dist, True, congr, congrArg, congrFun', Set.ofPred, Set.Ici, EDist.edist, funext, ENNReal.ofReal, edist_dist, propext, ENNReal.le_ofReal_iff_toReal_le and 5 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oo_eq_empty line 404 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Eq, Set, Set.EAnnulus.oo, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Membership.mem, Set.Ioo, EDist.edist, False, Set.ofPred, funext, Set.Ioo_eq_empty_of_le, eq_self
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oc_eq_empty line 408 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Eq, Set, Set.EAnnulus.oc, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Membership.mem, Set.Ioc, EDist.edist, False, Set.ofPred, funext, Set.Ioc_eq_empty_of_le, eq_self
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.co_eq_empty line 412 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Eq, Set, Set.EAnnulus.co, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Membership.mem, Set.Ico, EDist.edist, False, Set.ofPred, funext, Set.Ico_eq_empty_of_le, eq_self
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.cc_eq_empty line 416 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, Eq, Set, Set.EAnnulus.cc, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Membership.mem, Set.Icc, EDist.edist, False, Set.ofPred, funext, Set.Icc_eq_empty_of_lt, eq_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.cc_top_eq_empty line 420 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, Eq, Set, Set.EAnnulus.cc, Top.top, EmptyCollection.emptyCollection
Proof uses: Set.eq_empty_of_forall_notMem, Membership.mem, edist_ne_top, Iff.mp, LE.le, EDist.edist, top_le_iff, And.left
15 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oi_eq_empty line 424 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Eq, Set, Set.EAnnulus.oi, Top.top, ENNReal, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Membership.mem, Set.Ioi, EDist.edist, False, Set.ofPred, funext, ENNReal.ofReal, Dist.dist, congr, IsMax.Ioi_eq, IsMax, eq_self, edist_dist
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.ci_eq_empty line 427 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Eq, Set, Set.EAnnulus.ci, Top.top, ENNReal, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Membership.mem, Set.Ici, EDist.edist, False, Set.ofPred, funext, ENNReal.ofReal, Dist.dist, Singleton.singleton, congr, Set.Ici_top, edist_dist, eq_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oo_eq_of_top line 429 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, Top.top, Eq, Set, Set.EAnnulus.oo, Compl.compl, Metric.closedBall, ENNReal.toReal
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, ENNReal.ofReal, Dist.dist, Real, id, congr, congrArg, congrFun', Set.ofPred, Set.Ioo, EDist.edist, funext, Eq.trans, And, edist_dist, True, and_true and 5 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oc_eq_of_top line 433 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, Top.top, Eq, Set, Set.EAnnulus.oc, Compl.compl, Metric.closedBall, ENNReal.toReal
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, ENNReal.ofReal, Dist.dist, Real, id, congr, congrArg, congrFun', Set.ofPred, Set.Ioc, EDist.edist, funext, Eq.trans, Set.Ioi, Set.Ioc_top, edist_dist, Not and 4 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.co_eq_of_top line 437 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, Top.top, Eq, Set, Set.EAnnulus.co, Compl.compl, Metric.ball, ENNReal.toReal
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, LE.le, ENNReal.ofReal, Dist.dist, Real, id, congr, congrArg, congrFun', Set.ofPred, Set.Ico, EDist.edist, funext, Eq.trans, And, edist_dist, True and 6 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.cc_eq_of_top line 440 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, Top.top, Eq, Set, Set.EAnnulus.cc, Compl.compl, Metric.ball, ENNReal.toReal
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, LE.le, ENNReal.ofReal, Dist.dist, Real, id, congr, congrArg, congrFun', Set.ofPred, Set.Icc, EDist.edist, funext, Eq.trans, Set.Ici, Set.Icc_top, edist_dist and 5 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oo_subset_oo line 444 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.oo
Proof uses: Membership.mem, LT.lt, EDist.edist, And.intro, lt_of_le_of_lt, lt_of_lt_of_le
13 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oo_subset_oc line 448 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.oo, Set.EAnnulus.oc
Proof uses: Membership.mem, LT.lt, EDist.edist, And.intro, lt_of_le_of_lt, LE.le.trans, LT.lt.le
14 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oo_subset_co line 452 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.oo, Set.EAnnulus.co
Proof uses: Membership.mem, LT.lt, EDist.edist, And.intro, LE.le.trans, LT.lt.le, lt_of_lt_of_le
14 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oo_subset_cc line 456 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.oo, Set.EAnnulus.cc
Proof uses: Membership.mem, LT.lt, EDist.edist, And.intro, LE.le.trans, LT.lt.le
14 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oo_subset_oi line 460 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.oo, Set.EAnnulus.oi
Proof uses: Membership.mem, LT.lt, EDist.edist, lt_of_le_of_lt
13 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oo_subset_ci line 463 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.oo, Set.EAnnulus.ci
Proof uses: Membership.mem, LT.lt, EDist.edist, LE.le.trans, LT.lt.le
13 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oc_subset_oo line 466 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, LT.lt, Set, Set.EAnnulus.oc, Set.EAnnulus.oo
Proof uses: Membership.mem, EDist.edist, And.intro, lt_of_le_of_lt
17 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oc_subset_oc line 471 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.oc
Proof uses: Membership.mem, LT.lt, EDist.edist, And.intro, lt_of_le_of_lt, LE.le.trans
14 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oc_subset_co line 475 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, LT.lt, Set, Set.EAnnulus.oc, Set.EAnnulus.co
Proof uses: Membership.mem, EDist.edist, And.intro, LE.le.trans, LT.lt.le, lt_of_le_of_lt
17 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oc_subset_cc line 479 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.oc, Set.EAnnulus.cc
Proof uses: Membership.mem, LT.lt, EDist.edist, And.intro, LT.lt.le, lt_of_le_of_lt, LE.le.trans
14 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oc_subset_oi line 483 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.oo, Set.EAnnulus.oi
Proof uses: Membership.mem, LT.lt, EDist.edist, lt_of_le_of_lt
13 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oc_subset_ci line 486 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.oc, Set.EAnnulus.ci
Proof uses: Membership.mem, LT.lt, EDist.edist, LE.le.trans, LT.lt.le
14 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.co_subset_oo line 489 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, LE.le, Set, Set.EAnnulus.co, Set.EAnnulus.oo
Proof uses: Membership.mem, EDist.edist, And.intro, lt_of_lt_of_le
17 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.co_subset_oc line 493 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, LE.le, Set, Set.EAnnulus.co, Set.EAnnulus.oc
Proof uses: Membership.mem, EDist.edist, And.intro, lt_of_lt_of_le, LE.le.trans, LT.lt.le
17 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.co_subset_co line 498 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.co
Proof uses: Membership.mem, EDist.edist, LT.lt, And.intro, LE.le.trans, lt_of_lt_of_le
14 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.co_subset_cc line 502 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.co, Set.EAnnulus.cc
Proof uses: Membership.mem, EDist.edist, LT.lt, And.intro, LE.le.trans, LT.lt.le
14 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.co_subset_oi line 506 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, LE.le, Set, Set.EAnnulus.co, Set.EAnnulus.oi
Proof uses: Membership.mem, EDist.edist, lt_of_lt_of_le
15 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.co_subset_ci line 509 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.co, Set.EAnnulus.ci
Proof uses: Membership.mem, EDist.edist, LT.lt, LE.le.trans
14 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.cc_subset_oo line 512 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, LE.le, Set, Set.EAnnulus.cc, Set.EAnnulus.oo
Proof uses: Membership.mem, EDist.edist, And.intro, lt_of_lt_of_le, lt_of_le_of_lt
15 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.cc_subset_oc line 516 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, LE.le, Set, Set.EAnnulus.cc, Set.EAnnulus.oc
Proof uses: Membership.mem, EDist.edist, And.intro, lt_of_lt_of_le, LE.le.trans
17 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.cc_subset_co line 520 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, LT.lt, Set, Set.EAnnulus.cc, Set.EAnnulus.co
Proof uses: Membership.mem, EDist.edist, And.intro, LE.le.trans, lt_of_le_of_lt
17 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.cc_subset_cc line 525 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.cc
Proof uses: Membership.mem, EDist.edist, And.intro, LE.le.trans
13 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.cc_subset_oi line 529 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, LE.le, Set, Set.EAnnulus.cc, Set.EAnnulus.oi
Proof uses: Membership.mem, EDist.edist, lt_of_lt_of_le
15 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.cc_subset_ci line 532 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Set, Set.EAnnulus.cc, Set.EAnnulus.ci
Proof uses: Membership.mem, EDist.edist, LE.le.trans
13 instances, coercions and auxiliary constants left out.
lemma Set.EAnnulus.oc_union_oo line 536 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, LT.lt, Eq, Set, Union.union, Set.EAnnulus.oc, Set.EAnnulus.oo
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ioc, EDist.edist, Eq.mpr, Set.Ioo, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ioc_union_Ioo_eq_Ioo, iff_self
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oc_union_oc line 541 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Eq, Set, Union.union, Set.EAnnulus.oc
Proof uses: Set.ext, id, Iff, Membership.mem, Eq.mpr, Set.ofPred, Set.Ioc, EDist.edist, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ioc_union_Ioc_eq_Ioc, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oo_union_co line 546 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, LE.le, Eq, Set, Union.union, Set.EAnnulus.oo, Set.EAnnulus.co
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ioo, EDist.edist, Eq.mpr, Set.Ico, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ioo_union_Ico_eq_Ioo, iff_self
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oo_union_cc line 551 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, LE.le, Eq, Set, Union.union, Set.EAnnulus.oo, Set.EAnnulus.cc, Set.EAnnulus.oc
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ioo, EDist.edist, Set.Icc, Eq.mpr, Set.Ioc, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ioo_union_Icc_eq_Ioc, iff_self
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.cc_union_oo line 556 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, LT.lt, Eq, Set, Union.union, Set.EAnnulus.cc, Set.EAnnulus.oo, Set.EAnnulus.co
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Icc, EDist.edist, Set.Ioo, Eq.mpr, Set.Ico, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Icc_union_Ioo_eq_Ico, iff_self
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.cc_union_oc line 561 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Eq, Set, Union.union, Set.EAnnulus.cc, Set.EAnnulus.oc
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Icc, EDist.edist, Eq.mpr, Set.Ioc, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Icc_union_Ioc_eq_Icc, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.co_union_co line 566 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Eq, Set, Union.union, Set.EAnnulus.co
Proof uses: Set.ext, id, Iff, Membership.mem, Eq.mpr, Set.ofPred, Set.Ico, EDist.edist, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ico_union_Ico_eq_Ico, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.co_union_cc line 571 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Eq, Set, Union.union, Set.EAnnulus.co, Set.EAnnulus.cc
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ico, EDist.edist, Eq.mpr, Set.Icc, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ico_union_Icc_eq_Icc, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oc_union_oi line 576 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Eq, Set, Union.union, Set.EAnnulus.oc, Set.EAnnulus.oi
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ioc, EDist.edist, Eq.mpr, Set.Ioi, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ioc_union_Ioi_eq_Ioi, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.oo_union_ci line 580 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LT.lt, Eq, Set, Union.union, Set.EAnnulus.oo, Set.EAnnulus.ci, Set.EAnnulus.oi
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ioo, EDist.edist, Set.Ici, Eq.mpr, Set.Ioi, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ioo_union_Ici_eq_Ioi, iff_self
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.cc_union_oi line 585 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Eq, Set, Union.union, Set.EAnnulus.cc, Set.EAnnulus.oi, Set.EAnnulus.ci
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Icc, EDist.edist, Set.Ioi, Eq.mpr, Set.Ici, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Icc_union_Ioi_eq_Ici, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.co_union_ci line 589 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, LE.le, Eq, Set, Union.union, Set.EAnnulus.co, Set.EAnnulus.ci
Proof uses: Set.ext, id, Iff, Membership.mem, Set.ofPred, Set.Ico, EDist.edist, Eq.mpr, Set.Ici, Or, congrFun', congrArg, of_eq_true, Eq.trans, True, Set.Ico_union_Ici_eq_Ici, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.measurableSet_oo line 596 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, OpensMeasurableSpace, ENNReal, MeasurableSet, Set.EAnnulus.oo
Proof uses: dite, Eq, Top.top, of_eq_true, Eq.trans, EmptyCollection.emptyCollection, Set, True, congrArg, congrFun', Set.EAnnulus.oo_eq_empty, LE.le, Not, LT.lt, Ne.lt_top, Metric.closedBall, ENNReal.toReal, Compl.compl, Set.EAnnulus.oo_eq_of_top, Eq.mpr and 7 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.measurableSet_oc line 606 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, OpensMeasurableSpace, ENNReal, MeasurableSet, Set.EAnnulus.oc
Proof uses: dite, Eq, Top.top, of_eq_true, Eq.trans, EmptyCollection.emptyCollection, Set, True, congrArg, congrFun', Set.EAnnulus.oc_eq_empty, LE.le, Not, LT.lt, Ne.lt_top, Metric.closedBall, ENNReal.toReal, Compl.compl, Set.EAnnulus.oc_eq_of_top, Eq.mpr and 5 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.measurableSet_co line 616 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, OpensMeasurableSpace, ENNReal, MeasurableSet, Set.EAnnulus.co
Proof uses: dite, Eq, Top.top, of_eq_true, Eq.trans, EmptyCollection.emptyCollection, Set, True, congrArg, congrFun', Set.EAnnulus.co_eq_empty, LE.le, Not, LT.lt, Ne.lt_top, Metric.ball, ENNReal.toReal, Compl.compl, Set.EAnnulus.co_eq_of_top, Eq.mpr and 5 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.measurableSet_cc line 626 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, OpensMeasurableSpace, ENNReal, MeasurableSet, Set.EAnnulus.cc
Proof uses: dite, Eq, Top.top, of_eq_true, Eq.trans, EmptyCollection.emptyCollection, Set, True, congrArg, congrFun', Set.EAnnulus.cc_top_eq_empty, Not, LT.lt, Ne.lt_top, Metric.ball, ENNReal.toReal, Compl.compl, Set.EAnnulus.cc_eq_of_top, Eq.mpr, Inter.inter and 6 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.measurableSet_oi line 636 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, OpensMeasurableSpace, ENNReal, MeasurableSet, Set.EAnnulus.oi
Proof uses: dite, Eq, Top.top, of_eq_true, Eq.trans, EmptyCollection.emptyCollection, Set, True, congrArg, Set.EAnnulus.oi_eq_empty, Not, Eq.mpr, Compl.compl, Metric.closedBall, ENNReal.toReal, id, Set.EAnnulus.oi_eq_of_lt_top, Ne.lt_top, measurableSet_closedBall
13 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Set.EAnnulus.measurableSet_ci line 642 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, OpensMeasurableSpace, ENNReal, MeasurableSet, Set.EAnnulus.ci
Proof uses: dite, Eq, Top.top, of_eq_true, Eq.trans, EmptyCollection.emptyCollection, Set, True, congrArg, Set.EAnnulus.ci_eq_empty, Not, Eq.mpr, Compl.compl, Metric.ball, ENNReal.toReal, id, Set.EAnnulus.ci_eq_of_lt_top, Ne.lt_top, measurableSet_ball
13 instances, coercions and auxiliary constants left out.

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