-- 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 : α
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∞))
            ⋯) :
        ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
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∞))
            ⋯) :
        ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞)
      (↑(max
            (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∞))
              ⋯)
            1) :
        ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ (μ : (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∞)
    (↑(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∞)
Tactic: grw [hr x K le_rfl, scalingConstantOf, ← le_max_left]