awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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∞)
⊢ ∃ (C : ℝ≥0),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        ∀ t ≤ K,
          (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
            HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have rcases : ∀ (n : ℕ) (hn : K < HPow.hPow (α := ℝ) 2 n),
  ∃ (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: rcases pow_unbounded_of_one_lt K one_lt_two with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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
⊢ ∃ (C : ℝ≥0),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        ∀ t ≤ K,
          (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
            HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
  ∀ (x : α),
    ∀ t ≤ K,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(C ^ n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
Tactic: use C ^ n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑(C ^ n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have 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∞)
Tactic: filter_upwards [eventually_mem_nhdsWithin, this n] with ε hε₀ hε x t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(C ^ n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have 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∞)
Tactic: rw [mem_Ioi] at hε₀
Cleared hypotheses: hε₀, hε, x, t, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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 (t * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(C ^ n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have h : (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
Tactic: grw [ht, hn, ENNReal.coe_pow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
⊢ ∃ (C : ℝ≥0),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : α),
        ∀ t ≤ K,
          (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
            HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have 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∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (hypothesis)
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 + 1) * ε)) ≤
        HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have 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∞)
Tactic: replace ihn := eventually_nhdsGT_zero_mul_left (two_pos : 0 < (2 : ℝ)) ihn
Cleared hypotheses: ihn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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∞)
⊢ ∀ᶠ (ε : ℝ) 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∞)
have 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∞)
Tactic: filter_upwards [ihn, eventually_measure_le_doublingConstant_mul μ] with ε hεn hε x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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 : α
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 (n + 1) * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have h : (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * 2 * ε)) ≤
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 (n + 1) * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have h₁ : (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * (2 * ε))) ≤
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 (n + 1) * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have 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∞)
Tactic: grw [pow_succ, mul_assoc, hεn, hε, ← mul_assoc, pow_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 (n + 1) * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have 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∞)
Tactic: grw [pow_succ, mul_assoc, hεn, hε, ← mul_assoc, pow_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 (n + 1) * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have 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∞)
Tactic: grw [pow_succ, mul_assoc, hεn, hε, ← mul_assoc, pow_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 (n + 1) * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have 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∞)
Tactic: grw [pow_succ, mul_assoc, hεn, hε, ← mul_assoc, pow_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
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∞)
have 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∞)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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∞)
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (HPow.hPow (α := ℝ) 2 n * ε)) ≤
        HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ n) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have 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∞)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ ∃ (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∞)
have 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∞))
                sorry) :
            ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
Tactic: have h := Classical.choose_spec (exists_eventually_forall_measure_closedBall_le_mul μ K)