awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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 : ℝ),
    0 < R ∧
      ∀ (x : α) (t r : ℝ),
        t ∈ Ioc 0 K →
          r ≤ R →
            (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
              HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have rcases : ∀ (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∞))
                          sorry) :
                      ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞))
          x}),
  ∃ (R : ℝ),
    0 < R ∧
      ∀ (x : α) (t r : ℝ),
        t ∈ Ioc 0 K →
          r ≤ R →
            (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
              HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: rcases mem_nhdsGT_iff_exists_Ioc_subset.1 h with ⟨R, Rpos, hR⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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}
⊢ ∃ (R : ℝ),
    0 < R ∧
      ∀ (x : α) (t r : ℝ),
        t ∈ Ioc 0 K →
          r ≤ R →
            (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
              HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have refine : ∀ (x : α) (t r : ℝ) (ht : t ∈ Ioc 0 K) (hr : r ≤ R),
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: refine ⟨R, Rpos, fun x t r ht hr => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have inl : ∀ (rneg : r < 0),
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: rcases lt_trichotomy r 0 with (rneg | rfl | rpos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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
inl :
  ∀ (rneg : r < 0),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
      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∞)
have inr : ∀ (hr : 0 ≤ R),
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * 0)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) : ℝ≥0∞)
Tactic: rcases lt_trichotomy r 0 with (rneg | rfl | rpos)
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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
inl :
  ∀ (rneg : r < 0),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
inr :
  ∀ (hr : 0 ≤ R),
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * 0)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have inr₁ : ∀ (rpos : 0 < r),
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: rcases lt_trichotomy r 0 with (rneg | rfl | rpos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (hypothesis)
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
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have this : t * r < 0
Tactic: have : t * r < 0 := mul_neg_of_pos_of_neg ht.1 rneg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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 (t * 0)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) : ℝ≥0∞)
have inr : (μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) ≤
  HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x 0) : ℝ≥0∞)
Tactic: simp only [mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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∞)
have inr : 1 ≤ (↑(scalingConstantOf μ K) : ℝ≥0∞)
Tactic: refine le_mul_of_one_le_of_le ?_ le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have 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∞))
          sorry) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: apply (hR ⟨rpos, hr⟩ x t ht.2).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
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
⊢ 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∞)
have 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∞))
    sorry ≤
  scalingConstantOf μ K
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (K * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have 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∞))
                  sorry) :
              ℝ≥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∞)
Tactic: filter_upwards [Classical.choose_spec
      (exists_eventually_forall_measure_closedBall_le_mul μ K)] with r hr x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K 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∞)
have h : 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∞))
          sorry) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: grw [hr x K le_rfl, scalingConstantOf, ← le_max_left]