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

29 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)

Imported by 3 files

def As The blow-up factor of repeatedly increasing the size of balls line 18 source
Source documentation
The blow-up factor of repeatedly increasing the size of balls.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Real
Proof uses: HPow.hPow, Nat, Nat.ceil, Real.logb, OfNat.ofNat
14 instances, coercions and auxiliary constants left out.
```
def As (A : ℝ≥0) (s : ℝ) : ℝ≥0 := A ^ ⌈Real.logb 2 s⌉₊
…
```
Mentions: A, s
lemma MeasureTheory.ball_subset_ball_of_le line 30 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, LE.le, HAdd.hAdd, Dist.dist, Set, Metric.ball
Proof uses: Metric.ball_subset_ball', Eq.mp, congrArg, add_comm, dist_comm
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.dist_lt_of_not_disjoint_ball line 35 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Not, Disjoint, Set, Metric.ball, LT.lt, Dist.dist, HAdd.hAdd
Proof uses: And, Membership.mem, Exists, Iff.mp, Set.not_disjoint_iff, Trans.trans, LE.le, dist_triangle_left, add_lt_add_of_lt_of_lt, Eq.mp, congrArg, propext, Metric.mem_ball
61 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eq_zero_of_isDoubling_zero line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, OfNat.ofNat, NNReal, Eq
Proof uses: IsEmpty, Nonempty, Or, isEmpty_or_nonempty, MeasureTheory.Measure.eq_zero_of_isEmpty, Real, ENNReal, Set, Metric.ball, LE.le, HMul.hMul, Nat, HDiv.hDiv, MeasureTheory.Measure.IsDoubling.measure_ball_two_le_same, Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm and 47 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eq_zero_of_isDoubling_lt_one line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, LT.lt, OfNat.ofNat, Eq
Proof uses: IsEmpty, Nonempty, Or, isEmpty_or_nonempty, of_eq_true, Eq.trans, True, congrFun', congrArg, MeasureTheory.Measure.eq_zero_of_isEmpty, eq_self, Real, LE.le, ENNReal, Set, Metric.ball, HMul.hMul, Trans.trans, HDiv.hDiv, Nat and 107 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.IsDoubling.mono line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, LE.le
Proof uses: MeasureTheory.Measure.IsDoubling.mk, Real, Trans.trans, ENNReal, Set, Metric.ball, HMul.hMul, OfNat.ofNat, Nat, Eq, rfl, MeasureTheory.Measure.IsDoubling.measure_ball_two_le_same, mul_le_mul', le_refl
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measure_ball_two_le_same_iterate line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, Real, Nat, LE.le, ENNReal, Set, Metric.ball, HMul.hMul, HPow.hPow, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', pow_zero, one_mul, Eq.mpr, HAdd.hAdd, id, Eq, add_comm, pow_add, pow_one, mul_assoc, le_trans, MeasureTheory.Measure.IsDoubling.measure_ball_two_le_same, mul_le_mul_right
66 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measure_ball_four_le_same line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, Real, LE.le, ENNReal, Set, Metric.ball, HMul.hMul, OfNat.ofNat, Nat, HPow.hPow
Proof uses: Eq.mpr, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, DFunLike, HMul, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit0, MeasureTheory.measure_ball_two_le_same_iterate, inferInstance
47 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measure_ball_le_same line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, Real, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, ENNReal, Set, Metric.ball, As
Proof uses: dite, Trans.trans, mul_neg_of_pos_of_neg, of_eq_true, Eq.trans, True, congr, congrArg, EmptyCollection.emptyCollection, Iff.mpr, Eq, Metric.ball_eq_empty, LT.lt.le, MeasureTheory.measure_empty, MulZeroClass.mul_zero, Not, HPow.hPow, Nat, Nat.ceil, Real.logb and 14 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measure_ball_le_of_dist_le' line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, Real, LT.lt, OfNat.ofNat, LE.le, HAdd.hAdd, Dist.dist, HMul.hMul, ENNReal, Set, Metric.ball, As
Proof uses: Trans.trans, MeasureTheory.measure_mono, MeasureTheory.ball_subset_ball_of_le, le_rfl, MeasureTheory.measure_ball_le_same
40 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.isOpenPosMeasure_of_isDoubling line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, NeZero, MeasureTheory.Measure.IsOpenPosMeasure
Proof uses: MeasureTheory.Measure.IsOpenPosMeasure.mk, Set, IsOpen, Set.Nonempty, Eq, ENNReal, OfNat.ofNat, False, Membership.mem, Real, And, GT.gt, LE.le, Metric.ball, Exists, Iff.mp, Metric.isOpen_iff, Ne, NeZero.ne, Nat and 40 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.(instance at line 144) line 144 source
lemma MeasureTheory.Nat.exists_max_image todo: move line 174 source
Source comment
todo: move

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Set.Nonempty, Nat, BddAbove, Set.image, Exists, And, Membership.mem, LE.le
Proof uses: SupSet.sSup, Eq, Nat.sSup_mem, Set.Nonempty.image, Exists.intro, And.intro, Eq.mpr, id, forall_congr, implies_congr, Eq.refl, congrArg, le_csSup, Set.mem_image_of_mem
10 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma Nat.exists_max_image {α : Type*} {s : Set α} (hs : s.Nonempty)
    {f : α → ℕ} (h : BddAbove (f '' s)) : ∃ x ∈ s, ∀ y ∈ s, f y ≤ f x := by
…
```
Mentions: s
lemma MeasureTheory.IsDoubling.measure_ball_lt_top line 184 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, MeasureTheory.IsLocallyFiniteMeasure, Real, LT.lt, ENNReal, Set, Metric.ball, Top.top
Proof uses: LE.le, OfNat.ofNat, Or, le_or_gt, of_eq_true, Eq.trans, True, congrFun', congrArg, EmptyCollection.emptyCollection, Iff.mpr, Eq, Metric.ball_eq_empty, MeasureTheory.measure_empty, And, Membership.mem, IsOpen, Exists, MeasureTheory.Measure.exists_isOpen_measure_lt_top, GT.gt and 19 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.IsDoubling.allBallsCoverBalls line 199 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, OpensMeasurableSpace, NeZero, MeasureTheory.IsLocallyFiniteMeasure, AllBallsCoverBalls, OfNat.ofNat, Real, Nat, Nat.ceil, As
Proof uses: MeasureTheory.Measure.IsOpenPosMeasure, MeasureTheory.isOpenPosMeasure_of_isDoubling, Ne, Eq, False, NeZero.ne, MeasureTheory.eq_zero_of_isDoubling_zero, Eq.symm, AllBallsCoverBalls.mk, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, GT.gt, HMul.hMul, Eq.mpr, CoveredByBalls and 181 more
256 instances, coercions and auxiliary constants left out.

Tactic trace: 110 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measureReal_ball_two_le_same line 293 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, Real, LE.le, MeasureTheory.Measure.real, Metric.ball, HMul.hMul, OfNat.ofNat, Nat
Proof uses: id, ENNReal.toReal, Set, ENNReal, Eq.mpr, Eq, congrArg, ENNReal.toReal_mono, ENNReal.mul_ne_top, ENNReal.coe_ne_top, MeasureTheory.measure_ball_ne_top, MeasureTheory.Measure.IsDoubling.measure_ball_two_le_same
30 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measureReal_ball_two_le_same_iterate line 300 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, Real, Nat, LE.le, MeasureTheory.Measure.real, Metric.ball, HMul.hMul, HPow.hPow, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, Set, congrFun', pow_zero, one_mul, Eq.mpr, HAdd.hAdd, id, Eq, add_comm, pow_add, pow_one, mul_assoc, le_trans, MeasureTheory.measureReal_ball_two_le_same and 2 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measureReal_ball_pos line 308 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasurableSpace, MeasureTheory.Measure, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, MeasureTheory.Measure.IsOpenPosMeasure, Real, LT.lt, OfNat.ofNat, MeasureTheory.Measure.real, Metric.ball
Proof uses: ENNReal.toReal_pos, Set, ENNReal, LT.lt.ne', Metric.measure_ball_pos, LT.lt.ne, Top.top, MeasureTheory.measure_ball_lt_top
16 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.one_le_A line 313 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, Nonempty, MeasureTheory.Measure.IsOpenPosMeasure, LE.le, OfNat.ofNat
Proof uses: LT.lt, Real, MeasureTheory.Measure.real, Metric.ball, MeasureTheory.measureReal_ball_pos, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.neg_congr and 53 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.A_pos line 327 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, Nonempty, MeasureTheory.Measure.IsOpenPosMeasure, LT.lt, OfNat.ofNat
Proof uses: Trans.trans, LE.le, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Nat.cast_one, Eq.refl, Bool, Bool.false, MeasureTheory.one_le_A
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.A_pos' line 333 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, Nonempty, MeasureTheory.Measure.IsOpenPosMeasure, LT.lt, ENNReal, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, congrArg, propext, ENNReal.coe_pos, MeasureTheory.A_pos
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.As_pos line 338 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, Nonempty, MeasureTheory.Measure.IsOpenPosMeasure, Real, LT.lt, OfNat.ofNat, As
Proof uses: pow_pos, MeasureTheory.A_pos, Nat.ceil, Real.logb, Nat
28 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.As_pos' line 342 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, Nonempty, MeasureTheory.Measure.IsOpenPosMeasure, Real, LT.lt, ENNReal, OfNat.ofNat, As
Proof uses: Eq.mpr, id, Eq, congrArg, propext, ENNReal.coe_pos, MeasureTheory.As_pos
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measureReal_ball_four_le_same line 345 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, Real, LE.le, MeasureTheory.Measure.real, Metric.ball, HMul.hMul, OfNat.ofNat, Nat, HPow.hPow
Proof uses: Trans.trans, Eq, of_eq_true, Eq.trans, True, congr, congrArg, Set, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, Eq.symm and 22 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measureReal_ball_le_same line 353 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, Real, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, MeasureTheory.Measure.real, Metric.ball, As
Proof uses: ENNReal, Set, MeasureTheory.measure_ball_le_same, Ne, Top.top, MeasureTheory.measure_ball_ne_top, ENNReal.coe_ne_top, Eq.mpr, ENNReal.ofReal, id, Eq, congrArg, Eq.symm, propext, ENNReal.ofReal_le_ofReal_iff, mul_nonneg, NNReal.coe_nonneg, MeasureTheory.measureReal_nonneg, Eq.mp, ENNReal.toReal and 3 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measureReal_ball_le_same' Version of measureReal_ball_le_same without ceiling function line 368 source
Source documentation
Version of measureReal_ball_le_same without ceiling function.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, Real, LT.lt, OfNat.ofNat, LE.le, MeasureTheory.Measure.real, Metric.ball, HMul.hMul, HPow.hPow, Neg.neg, Real.logb, Nat
Proof uses: Or, lt_or_ge, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', Set, MeasureTheory.eq_zero_of_isDoubling_lt_one, MulZeroClass.mul_zero, Eq, Inv.inv, Iff.mpr, eq_inv_mul_iff_mul_eq₀, LT.lt.ne', rfl, LE.le.trans, As, MeasureTheory.measureReal_ball_le_same and 71 more
133 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma measureReal_ball_le_same' (x : X) {r t : ℝ} (ht : 0 < t) (h't : t ≤ 1) :
    μ.real (ball x r) ≤ A * t ^ (- Real.logb 2 A) * μ.real (ball x (t * r)) := by
…
```
Mentions: A
lemma MeasureTheory.measureNNReal_ball_le_of_dist_le' line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, NNReal, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsDoubling, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, Real, LT.lt, OfNat.ofNat, LE.le, HAdd.hAdd, Dist.dist, HMul.hMul, ENNReal.toNNReal, Set, ENNReal, Metric.ball, As
Proof uses: Eq.mpr, id, Eq, Eq.trans, congr, congrArg, ENNReal.coe_toNNReal, MeasureTheory.measure_ball_ne_top, MeasureTheory.measure_ball_le_of_dist_le'
43 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Subsingleton.ball_eq line 409 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Subsingleton, Real, Eq, Set, Metric.ball, ite, GT.gt, OfNat.ofNat, Singleton.singleton, EmptyCollection.emptyCollection
Proof uses: Set.ext, HEq, Subsingleton.elim, Iff, Membership.mem, Eq.refl, of_eq_true, Eq.trans, LT.lt, True, congr, congrArg, Dist.dist, congrFun', dist_self, And, ite_congr, Not, eq_self, and_true and 3 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.InnerProductSpace.IsDoubling line 413 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MeasurableSpace, BorelSpace, FiniteDimensional, MeasureTheory.Measure.IsDoubling, MeasureTheory.MeasureSpace.volume, HPow.hPow, NNReal, Nat, OfNat.ofNat, Module.finrank
Proof uses: MeasureTheory.Measure.IsDoubling.mk, Subsingleton, Nontrivial, Or, LE.le, ENNReal, MeasureTheory.Measure, Set, Metric.ball, HMul.hMul, subsingleton_or_nontrivial, Eq.mpr, ite, GT.gt, Singleton.singleton, EmptyCollection.emptyCollection, id, Eq, congr, congrArg and 26 more
122 instances, coercions and auxiliary constants left out.

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