-- 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:
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

Tactic:
linarith

Result:
no goals

Proof state:
case pos.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)
⊢ ∃ r_1,
    closedBall y r ⊆ closedBall x r_1 ∧
      μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y r)

Tactic:
rcases le_or_lt r R with (hr | hr)

Result:
case pos.h.inl
α : 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_1,
    closedBall y r ⊆ closedBall x r_1 ∧
      μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y r)

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
⊢ ∃ r_1,
    closedBall y r ⊆ closedBall x r_1 ∧
      μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y r)

Proof state:
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
A : y ∈ closedBall y r
⊢ 3 * (R / 4) + dist x y ≤ r

Tactic:
have B := mem_closedBall'.1 (H A)

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
A : y ∈ closedBall y r
B : dist x y ≤ R / 4
⊢ 3 * (R / 4) + dist x y ≤ 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)
⊢ μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y r)

Tactic:
have I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r) := by
  apply closedBall_subset_closedBall
  exact mul_le_mul_of_nonneg_right (le_max_left _ _) rpos.le

Result:
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 x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y 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 x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y r)

Tactic:
apply (measure_mono (I1.trans I2)).trans

Result:
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)

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
⊢ closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 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
⊢ 3 * ((K + 1) * r) + dist x y ≤ (4 * K + 3) * r

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

Tactic:
exact mul_le_mul_of_nonneg_right (le_max_left _ _) rpos.le

Result:
no goals