-- Mathlib/MeasureTheory/Measure/Doubling.lean
theorem exists_eventually_forall_measure_closedBall_le_mul (K : ℝ) :
    ∃ C : ℝ≥0, ∀ᶠ ε in 𝓝[>] 0, ∀ x, ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ C * μ (closedBall x ε)

Proof state:
case h.h.h.h
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε : ∀ (x : α), μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * μ (closedBall x ε)
hε₀ : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ K ≤ 2 ^ ⌈Real.logb 2 K⌉₊

Tactic:
rw [← Real.rpow_natCast, ← Real.logb_le_iff_le_rpow]

Result:
case h.h.h.h
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε : ∀ (x : α), μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * μ (closedBall x ε)
hε₀ : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ Real.logb 2 K ≤ ↑⌈Real.logb 2 K⌉₊

case h.h.h.h.hb
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε : ∀ (x : α), μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * μ (closedBall x ε)
hε₀ : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ 1 < 2

case h.h.h.h.hx
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε : ∀ (x : α), μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * μ (closedBall x ε)
hε₀ : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ 0 < K

Proof state:
case h
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε : ∀ (x : α), μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * μ (closedBall x ε)
hε₀ : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ μ (closedBall x (t * ε)) ≤ μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε))

Tactic:
gcongr

Result:
case h.h.h.a0
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε : ∀ (x : α), μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * μ (closedBall x ε)
hε₀ : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ 0 ≤ ε

case h.h.h.h
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε : ∀ (x : α), μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * μ (closedBall x ε)
hε₀ : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ t ≤ 2 ^ ⌈Real.logb 2 K⌉₊

Proof state:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
⊢ ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)

Tactic:
intro n

Result:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)

Proof state:
case h
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε : ∀ (x : α), μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * μ (closedBall x ε)
hε₀ : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ μ (closedBall x (t * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * μ (closedBall x ε)

Tactic:
refine le_trans ?_ (hε x)

Result:
case h
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε : ∀ (x : α), μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * μ (closedBall x ε)
hε₀ : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ μ (closedBall x (t * ε)) ≤ μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε))

Proof state:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑C * μ (closedBall x ε)

Tactic:
rcases lt_or_le K 1 with (hK | hK)

Result:
case inl
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : K < 1
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑C * μ (closedBall x ε)

case inr
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑C * μ (closedBall x ε)

Proof state:
case zero
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ 0 * ε)) ≤ ↑(C ^ 0) * μ (closedBall x ε)

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑C * μ (closedBall x ε)

Tactic:
use C ^ ⌈Real.logb 2 K⌉₊

Result:
case h
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * μ (closedBall x ε)