awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r0₁ : 0 < r
⊢ ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y

Tactic:
rw [← pos_iff_ne_zero] at r0

Premises used: pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
h :
  ∀ a ∈ Ioo 0 r,
    (mkMetric'.pre m a : (a : Set X) → ℝ≥0∞) (s ∪ t) =
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((mkMetric'.pre m a : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
        ((mkMetric'.pre m a : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞)
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0) (fun (r : ℝ≥0∞) ↦ (mkMetric'.pre m r : (a : Set X) → ℝ≥0∞) (s ∪ t)) fun (x : ℝ≥0∞) ↦
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((mkMetric'.pre m x : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      ((mkMetric'.pre m x : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
filter_upwards [Ioo_mem_nhdsGT r0]

Premises used: Ioo_mem_nhdsGT
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
ε : ℝ≥0∞
left : 0 < ε
εr : ε < r
⊢ (mkMetric'.pre m ε : (a : Set X) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((mkMetric'.pre m ε : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      ((mkMetric'.pre m ε : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
boundedBy_union_of_top_of_nonempty_inter ?_

Premises used: MeasureTheory.OuterMeasure.boundedBy_union_of_top_of_nonempty_inter
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
ε : ℝ≥0∞
left : 0 < ε
εr : ε < r
h :
  ∀ (u : Set X),
    (s ∩ u).Nonempty →
      (t ∩ u).Nonempty → extend (P := fun (s : Set X) ↦ ediam s ≤ ε) (fun (s : Set X) (x : ediam s ≤ ε) ↦ m s) u = ∞
⊢ (mkMetric'.pre m ε : (a : Set X) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((mkMetric'.pre m ε : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      ((mkMetric'.pre m ε : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
refine boundedBy_union_of_top_of_nonempty_inter ?_

Premises used: MeasureTheory.OuterMeasure.boundedBy_union_of_top_of_nonempty_inter
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
ε : ℝ≥0∞
left : 0 < ε
εr : ε < r
u : Set X
x : X
hxs : x ∈ s
hxu : x ∈ u
y : X
hyt : y ∈ t
hyu : y ∈ u
⊢ ε < ediam u

Tactic:
have : ε < ediam u := εr.trans_le ((hr x hxs y hyt).trans <| edist_le_ediam_of_mem hxu hyu)
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
ε : ℝ≥0∞
left : 0 < ε
εr : ε < r
u : Set X
x : X
hxs : x ∈ s
hxu : x ∈ u
y : X
hyt : y ∈ t
hyu : y ∈ u
this : ε < ediam u
⊢ extend (P := fun (s : Set X) ↦ ediam s ≤ ε) (fun (s : Set X) (x : ediam s ≤ ε) ↦ m s) u = ∞

Tactic:
iInf_eq_top.2 fun h => (this.not_ge h).elim

Premises used: Iff.mpr, iInf_eq_top, MeasureTheory.extend, False.elim, LT.lt.not_ge
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
ε : ℝ≥0∞
left : 0 < ε
εr : ε < r
u : Set X
x : X
hxs : x ∈ s
hxu : x ∈ u
y : X
hyt : y ∈ t
hyu : y ∈ u
this : ε < ediam u
⊢ extend (P := fun (s : Set X) ↦ ediam s ≤ ε) (fun (s : Set X) (x : ediam s ≤ ε) ↦ m s) u = ∞

Tactic:
exact iInf_eq_top.2 fun h => (this.not_ge h).elim

Premises used: Iff.mpr, iInf_eq_top, False.elim, LT.lt.not_ge
-- 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₂)
⊢ mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)

Tactic:
rcases (mem_nhdsGE_iff_exists_Ico_subset' zero_lt_one).1 hle with ⟨r, hr0, hr⟩

Premises used: zero_lt_one, mem_nhdsGE_iff_exists_Ico_subset', Iff.mp
-- 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₂
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₂)

Tactic:
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' => ?_)

Premises used: MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre, ENNReal.Tendsto.const_mul, Metric.ediam, le_of_tendsto_of_tendsto, Ioo_mem_nhdsGT, Or.inr, Filter.mem_of_superset
-- 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₂
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}
refine :
  ∀ (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'
⊢ mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)

Tactic:
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' => ?_)

Premises used: MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre, ENNReal.Tendsto.const_mul, le_of_tendsto_of_tendsto, Ioo_mem_nhdsGT, Or.inr, Filter.mem_of_superset
-- 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₂
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
simp :
  ((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∞)
⊢ 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'

Tactic:
simp only [mem_setOf_eq, mkMetric'.pre]

Premises used: Set.mem_setOf_eq, MeasureTheory.OuterMeasure.mkMetric'.pre
-- 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₂
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
rw :
  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∞)
⊢ ((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∞)

Tactic:
rw [← smul_eq_mul, ← smul_apply, smul_boundedBy hc]

Premises used: MeasureTheory.OuterMeasure.smul_boundedBy, smul_eq_mul, MeasureTheory.OuterMeasure.smul_apply
-- 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₂
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∞)

Tactic:
le_boundedBy.2 (fun t => (boundedBy_le _).trans ?_) _

Premises used: Iff.mpr, MeasureTheory.OuterMeasure.boundedBy_le, LE.le.trans, MeasureTheory.OuterMeasure.le_boundedBy
-- 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₂
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
refine :
  ∀ (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
⊢ 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∞)

Tactic:
refine le_boundedBy.2 (fun t => (boundedBy_le _).trans ?_) _

Premises used: Iff.mpr, MeasureTheory.OuterMeasure.boundedBy_le, LE.le.trans, MeasureTheory.OuterMeasure.le_boundedBy
-- 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₂
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
simp : (if ediam t ≤ r' then m₁ (ediam t) else ∞) ≤ c * if ediam t ≤ r' then m₂ (ediam t) else ∞
⊢ 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

Tactic:
simp only [smul_eq_mul, Pi.smul_apply, extend, iInf_eq_if]

Premises used: MeasureTheory.extend, smul_eq_mul, iInf_eq_if, Pi.smul_apply
-- 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₂
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
pos : ∀ (ht : ediam t ≤ r'), m₁ (ediam t) ≤ c * m₂ (ediam t)
neg : ∀ (ht : ¬ediam t ≤ r'), ∞ ≤ c * ∞
⊢ (if ediam t ≤ r' then m₁ (ediam t) else ∞) ≤ c * if ediam t ≤ r' then m₂ (ediam t) else ∞

Tactic:
split_ifs with ht
-- 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₂
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)

Tactic:
hr ⟨zero_le, ht.trans_lt hr'.2⟩

Premises used: zero_le, Set.Mem, setOf, And.right, And.intro, LE.le.trans_lt
-- 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₂
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)

Tactic:
exact hr ⟨zero_le, ht.trans_lt hr'.2⟩

Premises used: zero_le, And.right, And.intro, LE.le.trans_lt
-- 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₂
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 * ∞

Tactic:
simp [h0]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
simp_rw : LE.le.{u_2} (α := OuterMeasure X) ⊤ (⨆ (r : ℝ≥0∞), ⨆ (_ : r > 0), ⊤)
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) (mkMetric fun (x : ℝ≥0∞) ↦ ∞) ⊤

Tactic:
simp_rw [mkMetric, mkMetric', mkMetric'.pre, extend_top, boundedBy_top, eq_top_iff]

Premises used: eq_top_iff, MeasureTheory.OuterMeasure.mkMetric', MeasureTheory.OuterMeasure.boundedBy_top, MeasureTheory.OuterMeasure.mkMetric, MeasureTheory.OuterMeasure.mkMetric'.pre, MeasureTheory.extend_top
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
rw : ∀ (b : OuterMeasure X), (∀ (i : ℝ≥0∞), ⨆ (_ : i > 0), ⊤ ≤ b) → ⊤ ≤ b
⊢ LE.le.{u_2} (α := OuterMeasure X) ⊤ (⨆ (r : ℝ≥0∞), ⨆ (_ : r > 0), ⊤)

Tactic:
rw [le_iSup_iff]

Premises used: le_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
b : OuterMeasure X
hb : ∀ (i : ℝ≥0∞), ⨆ (_ : i > 0), ⊤ ≤ b
⊢ ⊤ ≤ b

Tactic:
simpa using hb ⊤

Premises used: Top.top
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂
⊢ mkMetric m₁ ≤ HSMul.hSMul (α := ℝ≥0∞) (β := OuterMeasure X) 1 (mkMetric m₂)

Tactic:
@mkMetric_mono_smul X _ _ m₂ _ ENNReal.one_ne_top one_ne_zero _

Premises used: one_ne_zero, ENNReal.one_ne_top, MeasureTheory.OuterMeasure.mkMetric_mono_smul
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂
h : mkMetric m₂ = HSMul.hSMul (α := ℝ≥0∞) (β := OuterMeasure X) 1 (mkMetric m₂)
convert_2 : m₁ ≤ᶠ[𝓝[≥] 0] HSMul.hSMul (α := ℝ≥0∞) 1 m₂
⊢ LE.le.{u_2} (α := OuterMeasure X) (mkMetric m₁) (mkMetric m₂)

Tactic:
convert! @mkMetric_mono_smul X _ _ m₂ _ ENNReal.one_ne_top one_ne_zero _

Premises used: one_ne_zero, ENNReal.one_ne_top, MeasureTheory.OuterMeasure.mkMetric_mono_smul
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂
⊢ mkMetric m₂ = HSMul.hSMul (α := ℝ≥0∞) (β := OuterMeasure X) 1 (mkMetric m₂)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂
⊢ m₁ ≤ᶠ[𝓝[≥] 0] HSMul.hSMul (α := ℝ≥0∞) 1 m₂

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
simp :
  Eq.{u_2 + 1} (α := OuterMeasure X)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : i > 0),
        (comap f : (a : OuterMeasure Y) → OuterMeasure X)
          (boundedBy (extend (P := fun (s : Set Y) ↦ ediam s ≤ i) fun (s : Set Y) (x : ediam s ≤ i) ↦ m (ediam s))))
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : r > 0),
        boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r) fun (s : Set X) (x : ediam s ≤ r) ↦ m (ediam s)))
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) ((comap f : (a : OuterMeasure Y) → OuterMeasure X) (mkMetric m) : OuterMeasure X)
    (mkMetric m : OuterMeasure X)

Tactic:
simp only [mkMetric, mkMetric', mkMetric'.pre, comap_iSup]

Premises used: MeasureTheory.OuterMeasure.mkMetric', MeasureTheory.OuterMeasure.mkMetric, MeasureTheory.OuterMeasure.mkMetric'.pre, MeasureTheory.OuterMeasure.comap_iSup
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
⊢ Eq.{u_2 + 1} (α := OuterMeasure X)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : i > 0),
        (comap f : (a : OuterMeasure Y) → OuterMeasure X)
          (boundedBy (extend (P := fun (s : Set Y) ↦ ediam s ≤ i) fun (s : Set Y) (x : ediam s ≤ i) ↦ m (ediam s))))
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : r > 0),
        boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r) fun (s : Set X) (x : ediam s ≤ r) ↦ m (ediam s)))

Tactic:
surjective_id.iSup_congr id fun ε => surjective_id.iSup_congr id fun hε => ?_

Premises used: Function.Surjective.iSup_congr, id, Function.surjective_id
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
refine :
  ∀ (ε : ℝ≥0∞) (hε : id ε > 0),
    Eq.{u_2 + 1} (α := OuterMeasure X)
      ((comap f : (a : OuterMeasure Y) → OuterMeasure X)
          (boundedBy (extend (P := fun (s : Set Y) ↦ ediam s ≤ ε) fun (s : Set Y) (x : ediam s ≤ ε) ↦ m (ediam s))) :
        OuterMeasure X)
      (boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ id ε) fun (s : Set X) (x : ediam s ≤ id ε) ↦ m (ediam s)) :
        OuterMeasure X)
⊢ Eq.{u_2 + 1} (α := OuterMeasure X)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : i > 0),
        (comap f : (a : OuterMeasure Y) → OuterMeasure X)
          (boundedBy (extend (P := fun (s : Set Y) ↦ ediam s ≤ i) fun (s : Set Y) (x : ediam s ≤ i) ↦ m (ediam s))))
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : r > 0),
        boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r) fun (s : Set X) (x : ediam s ≤ r) ↦ m (ediam s)))

Tactic:
refine surjective_id.iSup_congr id fun ε => surjective_id.iSup_congr id fun hε => ?_

Premises used: Function.Surjective.iSup_congr, id, Function.surjective_id
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
rw :
  Eq.{u_2 + 1} (α := OuterMeasure X)
    (boundedBy fun (s : Set X) ↦
      extend (P := fun (s : Set Y) ↦ ediam s ≤ ε) (fun (s : Set Y) (x : ediam s ≤ ε) ↦ m (ediam s)) (f '' s))
    (boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ id ε) fun (s : Set X) (x : ediam s ≤ id ε) ↦ m (ediam s)))
rw₁ :
  Monotone m →
    Monotone (β := ℝ≥0∞) fun (s : { s : Set Y // s.Nonempty }) ↦
      extend (P := fun (s : Set Y) ↦ ediam s ≤ ε) (fun (s : Set Y) (x : ediam s ≤ ε) ↦ m (ediam s)) (↑s : Set Y)
⊢ Eq.{u_2 + 1} (α := OuterMeasure X)
    ((comap f : (a : OuterMeasure Y) → OuterMeasure X)
        (boundedBy (extend (P := fun (s : Set Y) ↦ ediam s ≤ ε) fun (s : Set Y) (x : ediam s ≤ ε) ↦ m (ediam s))) :
      OuterMeasure X)
    (boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ id ε) fun (s : Set X) (x : ediam s ≤ id ε) ↦ m (ediam s)) :
      OuterMeasure X)

Tactic:
rw [comap_boundedBy _ (H.imp _ id)]

Premises used: id, MeasureTheory.OuterMeasure.comap_boundedBy, Or.imp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
e_m :
  ∀ (s : Set X),
    extend (P := fun (s : Set Y) ↦ ediam s ≤ ε) (fun (s : Set Y) (x : ediam s ≤ ε) ↦ m (ediam s)) (f '' s) =
      extend (P := fun (s : Set X) ↦ ediam s ≤ id ε) (fun (s : Set X) (x : ediam s ≤ id ε) ↦ m (ediam s)) s
⊢ Eq.{u_2 + 1} (α := OuterMeasure X)
    (boundedBy fun (s : Set X) ↦
      extend (P := fun (s : Set Y) ↦ ediam s ≤ ε) (fun (s : Set Y) (x : ediam s ≤ ε) ↦ m (ediam s)) (f '' s))
    (boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ id ε) fun (s : Set X) (x : ediam s ≤ id ε) ↦ m (ediam s)))

Tactic:
congr with s : 1
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
s : Set X
e_m : ediam (f '' s) ≤ ε ↔ ediam s ≤ id ε
e_m₁ : ∀ (ha : ediam (f '' s) ≤ ε) (hb : ediam s ≤ id ε), m (ediam (f '' s)) = m (ediam s)
⊢ extend (P := fun (s : Set Y) ↦ ediam s ≤ ε) (fun (s : Set Y) (x : ediam s ≤ ε) ↦ m (ediam s)) (f '' s) =
    extend (P := fun (s : Set X) ↦ ediam s ≤ id ε) (fun (s : Set X) (x : ediam s ≤ id ε) ↦ m (ediam s)) s

Tactic:
apply extend_congr

Premises used: MeasureTheory.extend_congr
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
s : Set X
⊢ ediam (f '' s) ≤ ε ↔ ediam s ≤ id ε

Tactic:
simp [hf.ediam_image]

Premises used: Isometry.ediam_image
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
s : Set X
⊢ ∀ (ha : ediam (f '' s) ≤ ε) (hb : ediam s ≤ id ε), m (ediam (f '' s)) = m (ediam s)

Tactic:
simp [hf.ediam_image]

Premises used: Isometry.ediam_image
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
h_mono : Monotone m
s t : { s : Set Y // s.Nonempty }
hst : s ≤ t
simp : ∀ (i : ediam (↑t : Set Y) ≤ ε), ⨅ (_ : ediam (↑s : Set Y) ≤ ε), m (ediam (↑s : Set Y)) ≤ m (ediam (↑t : Set Y))
⊢ LE.le (α := ℝ≥0∞)
    ((fun (s : { s : Set Y // s.Nonempty }) ↦
        extend (P := fun (s : Set Y) ↦ ediam s ≤ ε) (fun (s : Set Y) (x : ediam s ≤ ε) ↦ m (ediam s)) (↑s : Set Y))
      s)
    ((fun (s : { s : Set Y // s.Nonempty }) ↦
        extend (P := fun (s : Set Y) ↦ ediam s ≤ ε) (fun (s : Set Y) (x : ediam s ≤ ε) ↦ m (ediam s)) (↑s : Set Y))
      t)

Tactic:
simp only [extend, le_iInf_iff]

Premises used: MeasureTheory.extend, le_iInf_iff
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
h_mono : Monotone m
s t : { s : Set Y // s.Nonempty }
hst : s ≤ t
ht : ediam (↑t : Set Y) ≤ ε
apply : ⨅ (_ : ediam (↑s : Set Y) ≤ ε), m (ediam (↑s : Set Y)) ≤ m (ediam (↑s : Set Y))
⊢ ⨅ (_ : ediam (↑s : Set Y) ≤ ε), m (ediam (↑s : Set Y)) ≤ m (ediam (↑t : Set Y))

Tactic:
apply le_trans _ (h_mono (ediam_mono hst))

Premises used: Metric.ediam_mono, le_trans