α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
⊢ closedBall y r ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
⊢ closedBall y r ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
let R := scalingScaleOf μ (max (4 * K + 3) 3)
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
⊢ (∃ r_1,
      closedBall y r ⊆ closedBall x r_1 ∧
        ↑↑μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
⊢ closedBall y r ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
simp only [vitaliFamily, VitaliFamily.enlarge, Vitali.vitaliFamily, mem_union, mem_setOf_eq,
  isClosed_ball, true_and_iff, (nonempty_ball.2 rpos).mono ball_subset_interior_closedBall,
  measurableSet_closedBall]
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)

case neg
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
⊢ (∃ r_1,
      closedBall y r ⊆ closedBall x r_1 ∧
        ↑↑μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
by_cases H : closedBall y r ⊆ closedBall x (R / 4)
case neg
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)

case pos
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)

case neg
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
swap
case pos.h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
left
case pos.h.inl
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)

case pos.h.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
case pos.h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
rcases le_or_lt r R with (hr | hr)
no goals
case neg
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
exact Or.inr H
case pos.h.inl
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ closedBall y r ⊆ closedBall x ((K + 1) * r) ∧
    ↑↑μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
case pos.h.inl
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
refine' ⟨(K + 1) * r, _⟩
case pos.h.inl.left
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ closedBall y r ⊆ closedBall x ((K + 1) * r)

case pos.h.inl.right
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ ↑↑μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
case pos.h.inl
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ closedBall y r ⊆ closedBall x ((K + 1) * r) ∧
    ↑↑μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
constructor
case pos.h.inl.left.h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ r + dist y x ≤ (K + 1) * r
case pos.h.inl.left
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ closedBall y r ⊆ closedBall x ((K + 1) * r)
apply closedBall_subset_closedBall'
case pos.h.inl.left.h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ r + dist x y ≤ (K + 1) * r
case pos.h.inl.left.h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ r + dist y x ≤ (K + 1) * r
rw [dist_comm]
no goals
case pos.h.inl.left.h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ r + dist x y ≤ (K + 1) * r
linarith
case pos.h.inl.right
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
case pos.h.inl.right
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ ↑↑μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
have I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r) := by
  apply closedBall_subset_closedBall'
  linarith
case pos.h.inl.right
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 (max (4 * K + 3) 3 * r)
⊢ ↑↑μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
case pos.h.inl.right
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
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
case pos.h.inl.right
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 (max (4 * K + 3) 3 * r)
⊢ ↑↑μ (closedBall y (max (4 * K + 3) 3 * r)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
case pos.h.inl.right
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 (max (4 * K + 3) 3 * r)
⊢ ↑↑μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
apply (measure_mono (I1.trans I2)).trans
no goals
case pos.h.inl.right
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 (max (4 * K + 3) 3 * r)
⊢ ↑↑μ (closedBall y (max (4 * K + 3) 3 * r)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
exact measure_mul_le_scalingConstantOf_mul _
  ⟨zero_lt_three.trans_le (le_max_right _ _), le_rfl⟩ hr
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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)
apply closedBall_subset_closedBall'
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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
linarith
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 ≤ max (4 * K + 3) 3 * r
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 (max (4 * K + 3) 3 * r)
apply closedBall_subset_closedBall
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 ≤ max (4 * K + 3) 3 * r
exact mul_le_mul_of_nonneg_right (le_max_left _ _) rpos.le
case pos.h.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ ↑↑μ (closedBall x (3 * (R / 4))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
case pos.h.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
refine' ⟨R / 4, H, _⟩
case pos.h.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
case pos.h.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ ↑↑μ (closedBall x (3 * (R / 4))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
have : closedBall x (3 * (R / 4)) ⊆ closedBall y r := by
  apply closedBall_subset_closedBall'
  have A : y ∈ closedBall y r := mem_closedBall_self rpos.le
  have B := mem_closedBall'.1 (H A)
  linarith
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
case pos.h.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
apply (measure_mono this).trans _
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3))
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
refine' le_mul_of_one_le_left (zero_le _) _
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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 μ (max (4 * K + 3) 3))
exact ENNReal.one_le_coe_iff.2 (le_max_right _ _)
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ 3 * (R / 4) + dist x y ≤ r
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ closedBall x (3 * (R / 4)) ⊆ closedBall y r
apply closedBall_subset_closedBall'
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ 3 * (R / 4) + dist x y ≤ r
have A : y ∈ closedBall y r := mem_closedBall_self rpos.le
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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
have B := mem_closedBall'.1 (H A)
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (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
linarith