-- 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 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 ε)

Tactic:
refine ⟨1, ?_⟩

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
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑1 * μ (closedBall x ε)

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

Tactic:
gcongr

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

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

Tactic:
rw [pow_succ, mul_assoc]

Result:
no goals

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

Tactic:
refine (ih.and (exists_measure_closedBall_le_mul' μ)).mono fun ε hε x => ?_

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

Proof state:
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 ≤ ε

Tactic:
exact (mem_Ioi.mp hε₀).le

Result:
no goals

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 ε)
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

Tactic:
linarith

Result:
no goals

Proof state:
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
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑1 * μ (closedBall x ε)

Tactic:
simp only [ENNReal.coe_one, one_mul]

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
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ μ (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
⊢ t ≤ 2 ^ ⌈Real.logb 2 K⌉₊

Tactic:
refine ht.trans ?_

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
⊢ K ≤ 2 ^ ⌈Real.logb 2 K⌉₊

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

Tactic:
exact hε.2 x

Result:
no goals