awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
x : α
apply :
  ∀ {U : Set ℝ} (hU : Membership.mem (γ := Filter ℝ) (𝓝[>] 0) U),
    ∃ x_1 ∈ U,
      (μ : (a : Set α) → ENNReal) (closedBall x (3 * x_1)) ≤
        HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
          ((μ : (a : Set α) → ENNReal) (closedBall x x_1) : ENNReal)
⊢ ∃ᶠ (r : ℝ) in 𝓝[>] 0,
    (μ : (a : Set α) → ENNReal) (closedBall x (3 * r)) ≤
      HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
        ((μ : (a : Set α) → ENNReal) (closedBall x r) : ENNReal)

Tactic:
apply frequently_iff.2 fun {U} hU => ?_

Premises used: Iff.mpr, Filter.frequently_iff
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
x : α
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (𝓝[>] 0) U
obtain :
  ∀ (ε : ℝ) (εpos : Membership.mem (γ := Set ℝ) (Ioi 0) ε) (hε : Ioc 0 ε ⊆ U),
    ∃ x_1 ∈ U,
      (μ : (a : Set α) → ENNReal) (closedBall x (3 * x_1)) ≤
        HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
          ((μ : (a : Set α) → ENNReal) (closedBall x x_1) : ENNReal)
⊢ ∃ x_1 ∈ U,
    (μ : (a : Set α) → ENNReal) (closedBall x (3 * x_1)) ≤
      HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
        ((μ : (a : Set α) → ENNReal) (closedBall x x_1) : ENNReal)

Tactic:
obtain ⟨ε, εpos, hε⟩ := mem_nhdsGT_iff_exists_Ioc_subset.1 hU

Premises used: mem_nhdsGT_iff_exists_Ioc_subset, Iff.mp
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
x : α
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (𝓝[>] 0) U
ε : ℝ
εpos : Membership.mem (γ := Set ℝ) (Ioi 0) ε
hε : Ioc 0 ε ⊆ U
⊢ ∃ x_1 ∈ U,
    (μ : (a : Set α) → ENNReal) (closedBall x (3 * x_1)) ≤
      HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
        ((μ : (a : Set α) → ENNReal) (closedBall x x_1) : ENNReal)

Tactic:
⟨min ε R, hε ⟨lt_min εpos Rpos, min_le_left _ _⟩, ?_⟩

Premises used: lt_min, min_le_left, And.intro, Exists.intro, Min.min
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
x : α
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (𝓝[>] 0) U
ε : ℝ
εpos : Membership.mem (γ := Set ℝ) (Ioi 0) ε
hε : Ioc 0 ε ⊆ U
refine :
  (μ : (a : Set α) → ENNReal) (closedBall x (3 * min ε R)) ≤
    HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (closedBall x (min ε R)) : ENNReal)
⊢ ∃ x_1 ∈ U,
    (μ : (a : Set α) → ENNReal) (closedBall x (3 * x_1)) ≤
      HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
        ((μ : (a : Set α) → ENNReal) (closedBall x x_1) : ENNReal)

Tactic:
refine ⟨min ε R, hε ⟨lt_min εpos Rpos, min_le_left _ _⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
x : α
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (𝓝[>] 0) U
ε : ℝ
εpos : Membership.mem (γ := Set ℝ) (Ioi 0) ε
hε : Ioc 0 ε ⊆ U
⊢ (μ : (a : Set α) → ENNReal) (closedBall x (3 * min ε R)) ≤
    HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (closedBall x (min ε R)) : ENNReal)

Tactic:
measure_mul_le_scalingConstantOf_mul μ
      ⟨zero_lt_three, le_max_right _ _⟩ (min_le_right _ _)

Premises used: le_max_right, zero_lt_three, IsUnifLocDoublingMeasure.measure_mul_le_scalingConstantOf_mul, And.intro, min_le_right
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
x : α
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (𝓝[>] 0) U
ε : ℝ
εpos : Membership.mem (γ := Set ℝ) (Ioi 0) ε
hε : Ioc 0 ε ⊆ U
⊢ (μ : (a : Set α) → ENNReal) (closedBall x (3 * min ε R)) ≤
    HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (closedBall x (min ε R)) : ENNReal)

Tactic:
exact measure_mul_le_scalingConstantOf_mul μ
      ⟨zero_lt_three, le_max_right _ _⟩ (min_le_right _ _)

Premises used: le_max_right, zero_lt_three, IsUnifLocDoublingMeasure.measure_mul_le_scalingConstantOf_mul, And.intro, min_le_right
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
⊢ ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ENNReal) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
          ((μ : (a : Set α) → ENNReal) (closedBall x r) : ENNReal)

Tactic:
have A : ∀ x : α, ∃ᶠ r in 𝓝[>] (0 : ℝ),
      μ (closedBall x (3 * r)) ≤ scalingConstantOf μ (max (4 * K + 3) 3) * μ (closedBall x r) := by
    intro x
    apply frequently_iff.2 fun {U} hU => ?_
    obtain ⟨ε, εpos, hε⟩ := mem_nhdsGT_iff_exists_Ioc_subset.1 hU
    refine ⟨min ε R, hε ⟨lt_min εpos Rpos, min_le_left _ _⟩, ?_⟩
    exact measure_mul_le_scalingConstantOf_mul μ
      ⟨zero_lt_three, le_max_right _ _⟩ (min_le_right _ _)
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
A :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ENNReal) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
          ((μ : (a : Set α) → ENNReal) (closedBall x r) : ENNReal)
linarith : R / 4 ≤ 0 → 4 / 4 = 1
linarith₁ : R / 4 ≤ 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : R / 4 ≤ 0 → GT.gt (α := ℝ) 4 0
linarith₃ : R / 4 ≤ 0 → 0 - R + (1 * R - HMul.hMul (α := ℝ) 4 0) = 0
⊢ 0 < R / 4

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
A :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ENNReal) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
          ((μ : (a : Set α) → ENNReal) (closedBall x r) : ENNReal)
⊢ VitaliFamily μ

Tactic:
exact (Vitali.vitaliFamily μ (scalingConstantOf μ (max (4 * K + 3) 3)) A).enlarge (R / 4)
    (by linarith)

Premises used: HMul.hMul, IsUnifLocDoublingMeasure.scalingConstantOf, HDiv.hDiv, HAdd.hAdd, Max.max, VitaliFamily.enlarge, OfNat.ofNat, Vitali.vitaliFamily
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
simp :
  (∃ (r_1 : ℝ),
      closedBall y r ⊆ closedBall x r_1 ∧
        (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
          HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
            ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
⊢ closedBall y r ∈ VitaliFamily.setsAt (vitaliFamily μ K) 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]

Premises used: Set.mem_union, Iff.mpr, Metric.ball_subset_interior_closedBall, Metric.isClosed_closedBall, IsUnifLocDoublingMeasure.vitaliFamily, Metric.nonempty_ball, Set.mem_setOf_eq, Set.Nonempty.mono, VitaliFamily.enlarge, measurableSet_closedBall, Vitali.vitaliFamily, true_and
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
pos :
  ∀ (H : closedBall y r ⊆ closedBall x (R / 4)),
    (∃ (r_1 : ℝ),
        closedBall y r ⊆ closedBall x r_1 ∧
          (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
            HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
              ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)) ∨
      ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
neg :
  ∀ (H : ¬closedBall y r ⊆ closedBall x (R / 4)),
    (∃ (r_1 : ℝ),
        closedBall y r ⊆ closedBall x r_1 ∧
          (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
            HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
              ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)) ∨
      ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
⊢ (∃ (r_1 : ℝ),
      closedBall y r ⊆ closedBall x r_1 ∧
        (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
          HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
            ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)

Tactic:
by_cases H : closedBall y r ⊆ closedBall x (R / 4)

Premises used: HDiv.hDiv, Metric.closedBall, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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 ∧
        (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
          HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
            ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)

Tactic:
Or.inr H

Premises used: Or.inr
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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 ∧
        (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
          HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
            ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)

Tactic:
exact Or.inr H

Premises used: Or.inr
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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)
pos :
  ∃ (r_1 : ℝ),
    closedBall y r ⊆ closedBall x r_1 ∧
      (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
        HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
          ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)
⊢ (∃ (r_1 : ℝ),
      closedBall y r ⊆ closedBall x r_1 ∧
        (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
          HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
            ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)

Tactic:
left
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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)
pos :
  ∀ (hr : r ≤ R),
    ∃ (r_1 : ℝ),
      closedBall y r ⊆ closedBall x r_1 ∧
        (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
          HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
            ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)
pos₁ :
  ∀ (hr : R < r),
    ∃ (r_1 : ℝ),
      closedBall y r ⊆ closedBall x r_1 ∧
        (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
          HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
            ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)
⊢ ∃ (r_1 : ℝ),
    closedBall y r ⊆ closedBall x r_1 ∧
      (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
        HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
          ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)

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

Premises used: le_or_gt
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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 ∧
      (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
        HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
          ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)

Tactic:
⟨(K + 1) * r, ?_⟩

Premises used: HMul.hMul, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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
pos :
  closedBall y r ⊆ closedBall x ((K + 1) * r) ∧
    (μ : (a : Set α) → ENNReal) (closedBall x (3 * ((K + 1) * r))) ≤
      HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
        ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)
⊢ ∃ (r_1 : ℝ),
    closedBall y r ⊆ closedBall x r_1 ∧
      (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
        HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
          ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)

Tactic:
refine ⟨(K + 1) * r, ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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
pos : closedBall y r ⊆ closedBall x ((K + 1) * r)
pos₁ :
  (μ : (a : Set α) → ENNReal) (closedBall x (3 * ((K + 1) * r))) ≤
    HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)
⊢ closedBall y r ⊆ closedBall x ((K + 1) * r) ∧
    (μ : (a : Set α) → ENNReal) (closedBall x (3 * ((K + 1) * r))) ≤
      HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
        ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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
pos : r + dist y x ≤ (K + 1) * r
⊢ closedBall y r ⊆ closedBall x ((K + 1) * r)

Tactic:
apply closedBall_subset_closedBall'

Premises used: Metric.closedBall_subset_closedBall'
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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
pos : r + dist x y ≤ (K + 1) * r
⊢ r + dist y x ≤ (K + 1) * r

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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
linarith : (K + 1) * r < r + dist x y → dist x y - K * r + ((K + 1) * r - (r + dist x y)) = 0
⊢ r + dist x y ≤ (K + 1) * r

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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
h₁ : 3 * ((K + 1) * r) + dist x y ≤ (4 * K + 3) * r
⊢ closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)

Tactic:
apply closedBall_subset_closedBall'

Premises used: Metric.closedBall_subset_closedBall'
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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
linarith :
  (4 * K + 3) * r < 3 * ((K + 1) * r) + dist x y →
    dist x y - K * r + ((4 * K + 3) * r - (3 * ((K + 1) * r) + dist x y)) = 0
⊢ 3 * ((K + 1) * r) + dist x y ≤ (4 * K + 3) * r

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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)

Tactic:
have I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r) := by
        apply closedBall_subset_closedBall'
        linarith
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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)
h₁ : 4 * K + 3 ≤ max (4 * K + 3) 3
⊢ closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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 ≤ max (4 * K + 3) 3

Tactic:
le_max_left ..

Premises used: le_max_left
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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 ≤ max (4 * K + 3) 3

Tactic:
exact le_max_left ..

Premises used: le_max_left
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : 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)

Tactic:
have I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r) := by
        gcongr
        exact le_max_left ..