awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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
⊢ VitaliFamily μ
have 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)
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 _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
⊢ 0 < R / 4
have linarith : R / 4 ≤ 0 → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
⊢ 0 < R / 4
have linarith₁ : R / 4 ≤ 0 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
⊢ 0 < R / 4
have linarith₂ : R / 4 ≤ 0 → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
⊢ 0 < R / 4
have linarith₃ : R / 4 ≤ 0 → 0 - R + (1 * R - HMul.hMul (α := ℝ) 4 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
⊢ closedBall y r ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
have 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)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
⊢ (∃ (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)
have 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)
Tactic: by_cases H : closedBall y r ⊆ closedBall x (R / 4)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
⊢ (∃ (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)
have 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)
Tactic: by_cases H : closedBall y r ⊆ closedBall x (R / 4)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
have 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)
Tactic: left
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
have 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)
Tactic: rcases le_or_gt r R with (hr | hr)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases le_or_gt r R with (hr | hr)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
have 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)
Tactic: refine ⟨(K + 1) * r, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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 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)
have pos : closedBall y r ⊆ closedBall x ((K + 1) * r)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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 y r ⊆ closedBall x ((K + 1) * r)
have pos : r + dist y x ≤ (K + 1) * r
Tactic: apply closedBall_subset_closedBall'
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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 + dist y x ≤ (K + 1) * r
have pos : r + dist x y ≤ (K + 1) * r
Tactic: rw [dist_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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 + dist x y ≤ (K + 1) * r
have linarith : (K + 1) * r < r + dist x y → dist x y - K * r + ((K + 1) * r - (r + dist x y)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
have h₁ : 3 * ((K + 1) * r) + dist x y ≤ (4 * K + 3) * r
Tactic: apply closedBall_subset_closedBall'
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
⊢ 3 * ((K + 1) * r) + dist x y ≤ (4 * K + 3) * r
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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
⊢ (μ : (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)
have I1 : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
have h₁ : 4 * K + 3 ≤ max (4 * K + 3) 3
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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)
⊢ (μ : (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)
have I2 : 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 ..
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * 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)
have pos : (μ : (a : Set α) → ENNReal) (closedBall y (max (4 * K + 3) 3 * r)) ≤
  HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
    ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)
Tactic: apply (measure_mono (I1.trans I2)).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
have pos : (μ : (a : Set α) → ENNReal) (closedBall x (3 * (R / 4))) ≤
  HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
    ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)
Tactic: refine ⟨_, H, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
⊢ (μ : (a : Set α) → ENNReal) (closedBall x (3 * (R / 4))) ≤
    HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)
have pos : 3 * (R / 4) + dist x y ≤ r
Tactic: grw [scalingConstantOf, ← le_max_right, ENNReal.coe_one, one_mul,
      closedBall_subset_closedBall' (y := y)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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
⊢ 3 * (R / 4) + dist x y ≤ r
have A : y ∈ closedBall y r
Tactic: have A : y ∈ closedBall y r := mem_closedBall_self rpos.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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
A : y ∈ closedBall y r
⊢ 3 * (R / 4) + dist x y ≤ r
have B : dist x y ≤ R / 4
Tactic: have B := mem_closedBall'.1 (H A)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
A : y ∈ closedBall y r
B : dist x y ≤ R / 4
⊢ 3 * (R / 4) + dist x y ≤ r
have linarith : r < 3 * (R / 4) + dist x y → 4 / 4 = 1
Tactic: linarith