awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
R : ℝ
Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R
hR :
  Ioc 0 R ⊆
    {x : ℝ |
      (fun (ε : ℝ) ↦
          ∀ (x : α),
            ∀ t ≤ K,
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                HMul.hMul (β := ℝ≥0∞)
                  (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                        ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                          ∀ (x_1 : α),
                            ∀ t ≤ K,
                              (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                        ⋯) :
                    ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
        x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rneg : r < 0
⊢ t * r < 0

Tactic:
have : t * r < 0 := mul_neg_of_pos_of_neg ht.1 rneg
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
R : ℝ
Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R
hR :
  Ioc 0 R ⊆
    {x : ℝ |
      (fun (ε : ℝ) ↦
          ∀ (x : α),
            ∀ t ≤ K,
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                HMul.hMul (β := ℝ≥0∞)
                  (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                        ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                          ∀ (x_1 : α),
                            ∀ t ≤ K,
                              (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                        ⋯) :
                    ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
        x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rneg : r < 0
this : t * r < 0
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
simp only [closedBall_eq_empty.2 this, measure_empty, zero_le]

Premises used: Iff.mpr, zero_le, MeasureTheory.measure_empty, Metric.closedBall_eq_empty
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
R : ℝ
Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R
hR :
  Ioc 0 R ⊆
    {x : ℝ |
      (fun (ε : ℝ) ↦
          ∀ (x : α),
            ∀ t ≤ K,
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                HMul.hMul (β := ℝ≥0∞)
                  (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                        ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                          ∀ (x_1 : α),
                            ∀ t ≤ K,
                              (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                        ⋯) :
                    ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
        x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
inr :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * 0)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) : ℝ≥0∞)

Tactic:
simp only [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
R : ℝ
Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R
hR :
  Ioc 0 R ⊆
    {x : ℝ |
      (fun (ε : ℝ) ↦
          ∀ (x : α),
            ∀ t ≤ K,
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                HMul.hMul (β := ℝ≥0∞)
                  (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                        ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                          ∀ (x_1 : α),
                            ∀ t ≤ K,
                              (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                        ⋯) :
                    ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
        x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) : ℝ≥0∞)

Tactic:
le_mul_of_one_le_of_le ?_ le_rfl

Premises used: le_rfl, le_mul_of_one_le_of_le
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
R : ℝ
Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R
hR :
  Ioc 0 R ⊆
    {x : ℝ |
      (fun (ε : ℝ) ↦
          ∀ (x : α),
            ∀ t ≤ K,
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                HMul.hMul (β := ℝ≥0∞)
                  (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                        ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                          ∀ (x_1 : α),
                            ∀ t ≤ K,
                              (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                        ⋯) :
                    ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
        x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
inr : 1 ≤ (↑(scalingConstantOf μ K) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) : ℝ≥0∞)

Tactic:
refine le_mul_of_one_le_of_le ?_ le_rfl

Premises used: le_rfl, le_mul_of_one_le_of_le
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
R : ℝ
Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R
hR :
  Ioc 0 R ⊆
    {x : ℝ |
      (fun (ε : ℝ) ↦
          ∀ (x : α),
            ∀ t ≤ K,
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                HMul.hMul (β := ℝ≥0∞)
                  (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                        ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                          ∀ (x_1 : α),
                            ∀ t ≤ K,
                              (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                        ⋯) :
                    ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
        x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
⊢ 1 ≤ (↑(scalingConstantOf μ K) : ℝ≥0∞)

Tactic:
apply ENNReal.one_le_coe_iff.2 (le_max_right _ _)

Premises used: le_max_right, Iff.mpr, ENNReal.one_le_coe_iff
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
R : ℝ
Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R
hR :
  Ioc 0 R ⊆
    {x : ℝ |
      (fun (ε : ℝ) ↦
          ∀ (x : α),
            ∀ t ≤ K,
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                HMul.hMul (β := ℝ≥0∞)
                  (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                        ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                          ∀ (x_1 : α),
                            ∀ t ≤ K,
                              (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                        ⋯) :
                    ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
        x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rpos : 0 < r
inr :
  HMul.hMul (β := ℝ≥0∞)
      (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
            ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
              ∀ (x_1 : α),
                ∀ t ≤ K,
                  (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                    HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
            ⋯) :
        ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
apply (hR ⟨rpos, hr⟩ x t ht.2).trans

Premises used: And.right, And.intro, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
R : ℝ
Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R
hR :
  Ioc 0 R ⊆
    {x : ℝ |
      (fun (ε : ℝ) ↦
          ∀ (x : α),
            ∀ t ≤ K,
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                HMul.hMul (β := ℝ≥0∞)
                  (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                        ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                          ∀ (x_1 : α),
                            ∀ t ≤ K,
                              (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                        ⋯) :
                    ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
        x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rpos : 0 < r
inr :
  Classical.choose (p := fun (x : ℝ≥0) ↦
      ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
        ∀ (x_1 : α),
          ∀ t ≤ K,
            (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
              HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
      ⋯ ≤
    scalingConstantOf μ K
⊢ HMul.hMul (β := ℝ≥0∞)
      (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
            ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
              ∀ (x_1 : α),
                ∀ t ≤ K,
                  (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                    HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
            ⋯) :
        ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      ∀ t ≤ K,
        (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
          HMul.hMul (β := ℝ≥0∞)
            (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                    ∀ (x_1 : α),
                      ∀ t ≤ K,
                        (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                          HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                  ⋯) :
              ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
R : ℝ
Rpos : Membership.mem (γ := Set ℝ) (Ioi 0) R
hR :
  Ioc 0 R ⊆
    {x : ℝ |
      (fun (ε : ℝ) ↦
          ∀ (x : α),
            ∀ t ≤ K,
              (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * ε)) ≤
                HMul.hMul (β := ℝ≥0∞)
                  (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                        ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                          ∀ (x_1 : α),
                            ∀ t ≤ K,
                              (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                                HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                        ⋯) :
                    ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
        x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rpos : 0 < r
⊢ Classical.choose (p := fun (x : ℝ≥0) ↦
      ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
        ∀ (x_1 : α),
          ∀ t ≤ K,
            (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
              HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
      ⋯ ≤
    scalingConstantOf μ K

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ (r : ℝ)
    (hr :
      ∀ (x : α),
        ∀ t ≤ K,
          (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
            HMul.hMul (β := ℝ≥0∞)
              (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                      ∀ (x_1 : α),
                        ∀ t ≤ K,
                          (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                            HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                    ⋯) :
                ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (x : α),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (K * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (K * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
filter_upwards [Classical.choose_spec
      (exists_eventually_forall_measure_closedBall_le_mul μ K)] with r hr x

Premises used: Classical.choose_spec, IsUnifLocDoublingMeasure.exists_eventually_forall_measure_closedBall_le_mul
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (K⁻¹ * (K * ε))) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K⁻¹) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (K * ε)) : ℝ≥0∞)

Tactic:
eventually_nhdsGT_zero_mul_left hK (eventually_measure_le_scaling_constant_mul μ K⁻¹)

Premises used: Inv.inv, IsUnifLocDoublingMeasure.eventually_measure_le_scaling_constant_mul, eventually_nhdsGT_zero_mul_left
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
h : ∀ (x : ℝ) (a : α), x = K⁻¹ * (K * x)
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x r) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K⁻¹) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (K * r)) : ℝ≥0∞)

Tactic:
convert! eventually_nhdsGT_zero_mul_left hK (eventually_measure_le_scaling_constant_mul μ K⁻¹)

Premises used: Inv.inv, IsUnifLocDoublingMeasure.eventually_measure_le_scaling_constant_mul, eventually_nhdsGT_zero_mul_left
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
x : ℝ
a : α
⊢ x = K⁻¹ * (K * x)

Tactic:
simp [inv_mul_cancel_left₀ hK.ne']

Premises used: inv_mul_cancel_left₀, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ 0 < scalingScaleOf μ K

Tactic:
(eventually_measure_mul_le_scalingConstantOf_mul μ K).choose_spec.1

Premises used: Exists.choose_spec, IsUnifLocDoublingMeasure.eventually_measure_mul_le_scalingConstantOf_mul, And.left, IsUnifLocDoublingMeasure.scalingScaleOf
-- Module: Mathlib.MeasureTheory.Measure.Doubling
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ scalingScaleOf μ K
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
(eventually_measure_mul_le_scalingConstantOf_mul μ K).choose_spec.2 x t r ht hr

Premises used: Exists.choose_spec, IsUnifLocDoublingMeasure.eventually_measure_mul_le_scalingConstantOf_mul, And.right
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ.everywherePosSubset s ⊆ s

Tactic:
fun _x hx ↦ hx.1

Premises used: Set.Subset, And.left
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h :
  ∀ (x : α),
    x ∈ μ.everywherePosSubset s ↔
      x ∈ s \ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}
⊢ μ.everywherePosSubset s = s \ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
⊢ x ∈ μ.everywherePosSubset s ↔
    x ∈ s \ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}

Tactic:
simp [everywherePosSubset, pos_iff_ne_zero]

Premises used: MeasureTheory.Measure.everywherePosSubset, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
refine : IsOpen[inst] {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ μ.everywherePosSubset s = s \ u

Tactic:
refine ⟨{x | ∃ n ∈ 𝓝[s] x, μ n = 0}, ?_, by ext x; simp [everywherePosSubset, pos_iff_ne_zero]⟩
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
rw :
  ∀ (x : α),
    Membership.mem (γ := Set α) {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}
        x →
      {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
⊢ IsOpen[inst] {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds