awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this :
  ∀ (n : ℕ),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
n : ℕ
hn : K < HPow.hPow (α := ℝ) 2 n
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑(C ^ n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        ∀ t ≤ K,
          (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
            HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
use C ^ n
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this :
  ∀ (n : ℕ),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
n : ℕ
hn : K < HPow.hPow (α := ℝ) 2 n
h :
  ∀ (ε : ℝ) (hε₀ : Membership.mem (γ := Set ℝ) (Ioi 0) ε)
    (hε :
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
    (x : α) (t : ℝ) (ht : t ≤ K),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(C ^ n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑(C ^ n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
filter_upwards [eventually_mem_nhdsWithin, this n] with ε hε₀ hε x t ht

Premises used: eventually_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this :
  ∀ (n : ℕ),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
n : ℕ
hn : K < HPow.hPow (α := ℝ) 2 n
ε : ℝ
hε₀ : Membership.mem (γ := Set ℝ) (Ioi 0) ε
hε :
  ∀ (x : α),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
x : α
t : ℝ
ht : t ≤ K
h :
  ∀ (hε₀ : 0 < ε)
    (hε :
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
    (x : α) (t : ℝ) (ht : t ≤ K),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(C ^ n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(C ^ n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
rw [mem_Ioi] at hε₀

Premises used: Set.mem_Ioi
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this :
  ∀ (n : ℕ),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
n : ℕ
hn : K < HPow.hPow (α := ℝ) 2 n
ε : ℝ
hε₀ : 0 < ε
hε :
  ∀ (x : α),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
x : α
t : ℝ
ht : t ≤ K
h :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(C ^ n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
grw [ht, hn, ENNReal.coe_pow]

Premises used: ENNReal.coe_pow
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this :
  ∀ (n : ℕ),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
n : ℕ
hn : K < HPow.hPow (α := ℝ) 2 n
ε : ℝ
hε₀ : 0 < ε
hε :
  ∀ (x : α),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
x : α
t : ℝ
ht : t ≤ K
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
hε x
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this :
  ∀ (n : ℕ),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
n : ℕ
hn : K < HPow.hPow (α := ℝ) 2 n
ε : ℝ
hε₀ : 0 < ε
hε :
  ∀ (x : α),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
x : α
t : ℝ
ht : t ≤ K
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
exact hε x
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
suffices :
  ∀ (n : ℕ),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        ∀ t ≤ K,
          (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
            HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
suffices ∀ n,
      ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closedBall x ((2 : ℝ) ^ n * ε)) ≤ C ^ n * μ (closedBall x ε) by
    rcases pow_unbounded_of_one_lt K one_lt_two with ⟨n, hn⟩
    use C ^ n
    filter_upwards [eventually_mem_nhdsWithin, this n] with ε hε₀ hε x t ht
    rw [mem_Ioi] at hε₀
    grw [ht, hn, ENNReal.coe_pow]
    exact hε x
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) (β := ℕ) 2 0 * ε)) ≤
        HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑C : ℝ≥0∞) 0) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
        HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * (2 * ε))) ≤
        HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (2 * ε)) : ℝ≥0∞)

Tactic:
replace ihn := eventually_nhdsGT_zero_mul_left (two_pos : 0 < (2 : ℝ)) ihn
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * (2 * ε))) ≤
        HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (2 * ε)) : ℝ≥0∞)
h :
  ∀ (ε : ℝ)
    (hεn :
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * (2 * ε))) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (2 * ε)) : ℝ≥0∞))
    (hε :
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (2 * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
    (x : α),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 (n + 1) * ε)) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 (n + 1) * ε)) ≤
        HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
filter_upwards [ihn, eventually_measure_le_doublingConstant_mul μ] with ε hεn hε x

Premises used: IsUnifLocDoublingMeasure.eventually_measure_le_doublingConstant_mul
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * (2 * ε))) ≤
        HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (2 * ε)) : ℝ≥0∞)
ε : ℝ
hεn :
  ∀ (x : α),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * (2 * ε))) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (2 * ε)) : ℝ≥0∞)
hε :
  ∀ (x : α),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (2 * ε)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
x : α
h :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * 2 * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
h₁ :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * (2 * ε))) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
h₂ :
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (2 * ε)) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
h₃ :
  (↑C : ℝ≥0∞) ^ n *
      HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
h₄ :
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n * (↑(doublingConstant μ) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
h₅ h₆ :
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n * (↑(doublingConstant μ) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n * (↑(doublingConstant μ) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 (n + 1) * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
grw [pow_succ, mul_assoc, hεn, hε, ← mul_assoc, pow_succ]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
zero :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) (β := ℕ) 2 0 * ε)) ≤
        HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑C : ℝ≥0∞) 0) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
succ :
  ∀ (n : ℕ)
    (ihn :
      ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
        ∀ (x : α),
          (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
            HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 (n + 1) * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
        HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
induction n with
  | zero => simp
  | succ n ihn =>
    replace ihn := eventually_nhdsGT_zero_mul_left (two_pos : 0 < (2 : ℝ)) ihn
    filter_upwards [ihn, eventually_measure_le_doublingConstant_mul μ] with ε hεn hε x
    grw [pow_succ, mul_assoc, hεn, hε, ← mul_assoc, pow_succ]

Premises used: pow_succ, mul_assoc, IsUnifLocDoublingMeasure.eventually_measure_le_doublingConstant_mul
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ 1 ≤ scalingConstantOf μ K

Tactic:
le_max_of_le_right <| le_refl 1

Premises used: le_refl, IsUnifLocDoublingMeasure.scalingConstantOf, le_max_of_le_right, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)

Tactic:
have h := Classical.choose_spec (exists_eventually_forall_measure_closedBall_le_mul μ K)
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
rcases :
  ∀ (R : ℝ) (Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R)
    (hR :
      Ioc 0 R ⊆
        {x : ℝ |
          (fun (ε : ℝ) ↦
              ∀ (x : α),
                ∀ t ≤ K,
                  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                    HMul.hMul (β := ℝ≥0∞)
                      (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                            ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                              ∀ (x_1 : α),
                                ∀ t ≤ K,
                                  (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                    HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞)
                                      ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                            ⋯) :
                        ℝ≥0∞)
                      ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
            x}),
    ∃ (R : ℝ),
      0 < R ∧
        ∀ (x : α) (t r : ℝ),
          t ∈ Ioc 0 K →
            r ≤ R →
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
                HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ ∃ (R : ℝ),
    0 < R ∧
      ∀ (x : α) (t r : ℝ),
        t ∈ Ioc 0 K →
          r ≤ R →
            (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
              HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
rcases mem_nhdsGT_iff_exists_Ioc_subset.1 h with ⟨R, Rpos, hR⟩

Premises used: mem_nhdsGT_iff_exists_Ioc_subset, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
R : ℝ
Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R
hR :
  Ioc 0 R ⊆
    {x : ℝ |
      (fun (ε : ℝ) ↦
          ∀ (x : α),
            ∀ t ≤ K,
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                HMul.hMul (β := ℝ≥0∞)
                  (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                        ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                          ∀ (x_1 : α),
                            ∀ t ≤ K,
                              (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                        ⋯) :
                    ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
        x}
⊢ ∃ (R : ℝ),
    0 < R ∧
      ∀ (x : α) (t r : ℝ),
        t ∈ Ioc 0 K →
          r ≤ R →
            (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
              HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
⟨R, Rpos, fun x t r ht hr => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
R : ℝ
Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R
hR :
  Ioc 0 R ⊆
    {x : ℝ |
      (fun (ε : ℝ) ↦
          ∀ (x : α),
            ∀ t ≤ K,
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                HMul.hMul (β := ℝ≥0∞)
                  (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                        ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                          ∀ (x_1 : α),
                            ∀ t ≤ K,
                              (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                        ⋯) :
                    ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
        x}
refine :
  ∀ (x : α) (t r : ℝ) (ht : t ∈ Ioc 0 K) (hr : r ≤ R),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ ∃ (R : ℝ),
    0 < R ∧
      ∀ (x : α) (t r : ℝ),
        t ∈ Ioc 0 K →
          r ≤ R →
            (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
              HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
refine ⟨R, Rpos, fun x t r ht hr => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
R : ℝ
Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R
hR :
  Ioc 0 R ⊆
    {x : ℝ |
      (fun (ε : ℝ) ↦
          ∀ (x : α),
            ∀ t ≤ K,
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                HMul.hMul (β := ℝ≥0∞)
                  (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                        ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                          ∀ (x_1 : α),
                            ∀ t ≤ K,
                              (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                        ⋯) :
                    ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
        x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
inl :
  ∀ (rneg : r < 0),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
inr :
  ∀ (hr : 0 ≤ R),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * 0)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) : ℝ≥0∞)
inr₁ :
  ∀ (rpos : 0 < r),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
rcases lt_trichotomy r 0 with (rneg | rfl | rpos)

Premises used: OfNat.ofNat, rfl, lt_trichotomy