-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
rcases :
  ∀ (r : ℝ≥0∞) (hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r)
    (hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}),
    mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)
rcases₁ :
  ∀ (r : ℝ≥0∞) (hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r)
    (hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}) (s : Set X) (r' : ℝ≥0∞) (hr' : r' ∈ Ioo 0 r),
    Membership.mem (γ := Set ℝ≥0∞)
      {x : ℝ≥0∞ |
        (fun (x : ℝ≥0∞) ↦
            LE.le (α := ℝ≥0∞)
              ((fun (r : ℝ≥0∞) ↦
                  (((mkMetric'.pre (fun (s : Set X) ↦ m₁ (ediam s)) r : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞))
                x)
              ((fun (b : ℝ≥0∞) ↦
                  HMul.hMul (β := ℝ≥0∞) c
                    (((mkMetric'.pre (fun (s : Set X) ↦ m₂ (ediam s)) b : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s :
                      ℝ≥0∞))
                x))
          x}
      r'
rcases₂ :
  ∀ (r : ℝ≥0∞) (hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r)
    (hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}) (s : Set X) (r' : ℝ≥0∞) (hr' : r' ∈ Ioo 0 r),
    ((boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₁ (ediam s)) :
            OuterMeasure X) :
          (a : Set X) → ℝ≥0∞)
        s ≤
      HMul.hMul (β := ℝ≥0∞) c
        (((boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₂ (ediam s)) :
                OuterMeasure X) :
              (a : Set X) → ℝ≥0∞)
            s :
          ℝ≥0∞)
rcases₃ :
  ∀ (r : ℝ≥0∞) (hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r)
    (hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}) (s : Set X) (r' : ℝ≥0∞) (hr' : r' ∈ Ioo 0 r),
    LE.le (α := ℝ≥0∞)
      (((boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₁ (ediam s)) :
              OuterMeasure X) :
            (a : Set X) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((boundedBy
              (HSMul.hSMul (β := Set X → ℝ≥0∞) c
                (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₂ (ediam s))) :
            (a : Set X) → ℝ≥0∞)
          s :
        ℝ≥0∞)
rcases₄ :
  ∀ (r : ℝ≥0∞) (hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r)
    (hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}) (s : Set X) (r' : ℝ≥0∞) (hr' : r' ∈ Ioo 0 r)
    (t : Set X),
    extend (P := fun (s : Set X) ↦ ediam s ≤ r') (fun (s : Set X) (x : ediam s ≤ r') ↦ m₁ (ediam s)) t ≤
      HSMul.hSMul (β := Set X → ℝ≥0∞) c
        (extend (P := fun (s : Set X) ↦ ediam s ≤ r') fun (s : Set X) (x : ediam s ≤ r') ↦ m₂ (ediam s)) t
rcases₅ :
  ∀ (r : ℝ≥0∞) (hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r)
    (hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}) (s : Set X) (r' : ℝ≥0∞) (hr' : r' ∈ Ioo 0 r)
    (t : Set X), (if ediam t ≤ r' then m₁ (ediam t) else ∞) ≤ c * if ediam t ≤ r' then m₂ (ediam t) else ∞
pos :
  ∀ (r : ℝ≥0∞) (hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r)
    (hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}) (s : Set X) (r' : ℝ≥0∞) (hr' : r' ∈ Ioo 0 r)
    (t : Set X) (ht : ediam t ≤ r'), m₁ (ediam t) ≤ c * m₂ (ediam t)
neg neg₁ :
  ∀ (r : ℝ≥0∞) (hr0 : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) r)
    (hr : Ico 0 r ⊆ {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ m₁ x ≤ (c • m₂) x) x}) (s : Set X) (r' : ℝ≥0∞) (hr' : r' ∈ Ioo 0 r)
    (t : Set X) (ht : ¬ediam t ≤ r'), ∞ ≤ c * ∞
⊢ mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)

Tactic:
classical
  rcases (mem_nhdsGE_iff_exists_Ico_subset' zero_lt_one).1 hle with ⟨r, hr0, hr⟩
  refine fun s =>
    le_of_tendsto_of_tendsto (mkMetric'.tendsto_pre _ s)
      (ENNReal.Tendsto.const_mul (mkMetric'.tendsto_pre _ s) (Or.inr hc))
      (mem_of_superset (Ioo_mem_nhdsGT hr0) fun r' hr' => ?_)
  simp only [mem_setOf_eq, mkMetric'.pre]
  rw [← smul_eq_mul, ← smul_apply, smul_boundedBy hc]
  refine le_boundedBy.2 (fun t => (boundedBy_le _).trans ?_) _
  simp only [smul_eq_mul, Pi.smul_apply, extend, iInf_eq_if]
  split_ifs with ht
  · exact hr ⟨zero_le, ht.trans_lt hr'.2⟩
  · simp [h0]

Premises used: Iff.mpr, MeasureTheory.extend, MeasureTheory.OuterMeasure.boundedBy_le, Set.mem_setOf_eq, zero_lt_one, mem_nhdsGE_iff_exists_Ico_subset', MeasureTheory.OuterMeasure.smul_boundedBy, MeasureTheory.OuterMeasure.mkMetric'.pre, Iff.mp, LE.le.trans, smul_eq_mul, iInf_eq_if, MeasureTheory.OuterMeasure.le_boundedBy, MeasureTheory.OuterMeasure.smul_apply, Pi.smul_apply