-- Mathlib/MeasureTheory/Covering/DensityTheorem.lean
theorem closedBall_mem_vitaliFamily_of_dist_le_mul {K : ℝ} {x y : α} {r : ℝ} (h : dist x y ≤ K * r)
    (rpos : 0 < r) : closedBall y r ∈ (vitaliFamily μ K).setsAt x

Proof state:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
this : closedBall x (3 * (R / 4)) ⊆ closedBall y r
⊢ μ (closedBall y r) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y r)

Tactic:
refine le_mul_of_one_le_left (zero_le _) ?_

Result:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
this : closedBall x (3 * (R / 4)) ⊆ closedBall y r
⊢ 1 ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3))

Proof state:
case pos.h.inr
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
this : closedBall x (3 * (R / 4)) ⊆ closedBall y r
⊢ μ (closedBall x (3 * (R / 4))) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y r)

Tactic:
apply (measure_mono this).trans _

Result:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
this : closedBall x (3 * (R / 4)) ⊆ closedBall y r
⊢ μ (closedBall y r) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y r)

Proof state:
case pos.h.inl.left.h
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ r + dist y x ≤ (K + 1) * r

Tactic:
rw [dist_comm]

Result:
case pos.h.inl.left.h
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ r + dist x y ≤ (K + 1) * r

Proof state:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)
⊢ closedBall y ((4 * K + 3) * r) ⊆ closedBall y (((4 * K + 3) ⊔ 3) * r)

Tactic:
apply closedBall_subset_closedBall

Result:
case h
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)
⊢ (4 * K + 3) * r ≤ ((4 * K + 3) ⊔ 3) * r

Proof state:
case pos.h.inl.right
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)
I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (((4 * K + 3) ⊔ 3) * r)
⊢ μ (closedBall y (((4 * K + 3) ⊔ 3) * r)) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y r)

Tactic:
exact measure_mul_le_scalingConstantOf_mul _
  ⟨zero_lt_three.trans_le (le_max_right _ _), le_rfl⟩ hr

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
⊢ closedBall y r ∈ (vitaliFamily μ K).setsAt x

Tactic:
simp only [vitaliFamily, VitaliFamily.enlarge, Vitali.vitaliFamily, mem_union, mem_setOf_eq,
  isClosed_closedBall, true_and, (nonempty_ball.2 rpos).mono ball_subset_interior_closedBall,
  measurableSet_closedBall]

Result:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
⊢ (∃ r_1,
      closedBall y r ⊆ closedBall x r_1 ∧
        μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ ((4 * K + 3) ⊔ 3) / 4)

Proof state:
case pos.h.inl.left
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ closedBall y r ⊆ closedBall x ((K + 1) * r)

Tactic:
apply closedBall_subset_closedBall'

Result:
case pos.h.inl.left.h
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ r + dist y x ≤ (K + 1) * r