awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ≤ ε
⊢ ⨅ (_ : ediam (↑s : Set Y) ≤ ε), m (ediam (↑s : Set Y)) ≤ m (ediam (↑s : Set Y))

Tactic:
simp only [(ediam_mono hst).trans ht, le_refl, ciInf_pos]

Premises used: le_refl, Metric.ediam_mono, LE.le.trans, ciInf_pos
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hc' : c ≠ 0
simp :
  ⨆ (r : ℝ≥0∞),
      ⨆ (_ : r > 0),
        boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r) fun (s : Set X) (x : ediam s ≤ r) ↦ (c • m) (ediam s)) =
    HSMul.hSMul (β := OuterMeasure X) c
      (⨆ (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)))
⊢ mkMetric (c • m) = HSMul.hSMul (β := OuterMeasure X) c (mkMetric m)

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

Premises used: MeasureTheory.OuterMeasure.mkMetric', MeasureTheory.OuterMeasure.mkMetric, MeasureTheory.OuterMeasure.mkMetric'.pre
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hc' : c ≠ 0
simp_rw :
  Eq.{u_2 + 1} (α := OuterMeasure X)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : r > 0),
        boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r) fun (s : Set X) (x : ediam s ≤ r) ↦ (c • m) (ediam s)))
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : i > 0),
        HSMul.hSMul (β := OuterMeasure X) c
          (boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ i) fun (s : Set X) (x : ediam s ≤ i) ↦ m (ediam s))))
simp_rw₁ :
  Eq.{u_2 + 1} (α := OuterMeasure X)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : r > 0),
        boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r) fun (s : Set X) (x : ediam s ≤ r) ↦ (c • m) (ediam s)))
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : i > 0),
        boundedBy
          (HSMul.hSMul (β := Set X → ℝ≥0∞) c
            (extend (P := fun (s : Set X) ↦ ediam s ≤ i) fun (s : Set X) (x : ediam s ≤ i) ↦ m (ediam s))))
simp_rw₂ :
  Eq.{u_2 + 1} (α := OuterMeasure X)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : r > 0),
        boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ r) fun (s : Set X) (x : ediam s ≤ r) ↦ (c • m) (ediam s)))
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : i > 0),
        boundedBy (extend (P := fun (s : Set X) ↦ ediam s ≤ i) fun (s : Set X) (h : ediam s ≤ i) ↦ c • 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) ↦ (c • m) (ediam s)) =
    HSMul.hSMul (β := OuterMeasure X) c
      (⨆ (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:
simp_rw [smul_iSup, smul_boundedBy hc, ennreal_smul_extend _ hc', Pi.smul_apply]

Premises used: MeasureTheory.ennreal_smul_extend, MeasureTheory.OuterMeasure.smul_boundedBy, MeasureTheory.OuterMeasure.smul_iSup, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0
hc : c ≠ 0
rw : mkMetric ((↑c : ℝ≥0∞) • m) = HSMul.hSMul (β := OuterMeasure X) c (mkMetric m)
rw₁ : mkMetric ((↑c : ℝ≥0∞) • m) = HSMul.hSMul (β := OuterMeasure X) (↑c : ℝ≥0∞) (mkMetric m)
rw₂ rw₃ :
  HSMul.hSMul (β := OuterMeasure X) (↑c : ℝ≥0∞) (mkMetric m) =
    HSMul.hSMul (β := OuterMeasure X) (↑c : ℝ≥0∞) (mkMetric m)
⊢ mkMetric (c • m) = HSMul.hSMul (β := OuterMeasure X) c (mkMetric m)

Tactic:
rw [ENNReal.smul_def, ENNReal.smul_def,
    mkMetric_smul m ENNReal.coe_ne_top (ENNReal.coe_ne_zero.mpr hc)]

Premises used: Iff.mpr, ENNReal.smul_def, ENNReal.coe_ne_zero, MeasureTheory.OuterMeasure.mkMetric_smul, ENNReal.coe_ne_top
-- 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
rw :
  Eq.{u_3 + 1} (α := OuterMeasure Y)
    ((map f : (a : OuterMeasure X) → OuterMeasure Y) ((comap f : (a : OuterMeasure Y) → OuterMeasure X) (mkMetric m)) :
      OuterMeasure Y)
    ((restrict (range f) : (a : OuterMeasure Y) → OuterMeasure Y) (mkMetric m) : OuterMeasure Y)
rw₁ rw₂ :
  Eq (α := OuterMeasure Y) ((restrict (range f) : (a : OuterMeasure Y) → OuterMeasure Y) (mkMetric m) : OuterMeasure Y)
    ((restrict (range f) : (a : OuterMeasure Y) → OuterMeasure Y) (mkMetric m) : OuterMeasure Y)
⊢ Eq (α := OuterMeasure Y) ((map f : (a : OuterMeasure X) → OuterMeasure Y) (mkMetric m) : OuterMeasure Y)
    ((restrict (range f) : (a : OuterMeasure Y) → OuterMeasure Y) (mkMetric m) : OuterMeasure Y)

Tactic:
rw [← isometry_comap_mkMetric _ hf H, map_comap]

Premises used: MeasureTheory.OuterMeasure.isometry_comap_mkMetric, MeasureTheory.OuterMeasure.map_comap
-- 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
⊢ Eq.{u_2 + 1} (α := OuterMeasure X)
    ((comap (⇑f : (a : X) → Y) : (a : OuterMeasure Y) → OuterMeasure X) (mkMetric m) : OuterMeasure X)
    (mkMetric m : OuterMeasure X)

Tactic:
isometry_comap_mkMetric _ f.isometry (Or.inr f.surjective)

Premises used: MeasureTheory.OuterMeasure.isometry_comap_mkMetric, Or.inr, IsometryEquiv.isometry, IsometryEquiv.surjective
-- 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
rw :
  Eq.{u_3 + 1} (α := OuterMeasure Y)
    ((map (⇑f : (a : X) → Y) : (a : OuterMeasure X) → OuterMeasure Y)
        ((comap (⇑f : (a : X) → Y) : (a : OuterMeasure Y) → OuterMeasure X) (mkMetric m)) :
      OuterMeasure Y)
    (mkMetric m : OuterMeasure Y)
rw₁ rw₂ : Eq.{u_3 + 1} (α := OuterMeasure Y) (mkMetric m) (mkMetric m)
⊢ Eq.{u_3 + 1} (α := OuterMeasure Y)
    ((map (⇑f : (a : X) → Y) : (a : OuterMeasure X) → OuterMeasure Y) (mkMetric m) : OuterMeasure Y)
    (mkMetric m : OuterMeasure Y)

Tactic:
rw [← isometryEquiv_comap_mkMetric _ f, map_comap_of_surjective f.surjective]

Premises used: MeasureTheory.OuterMeasure.map_comap_of_surjective, IsometryEquiv.surjective, MeasureTheory.OuterMeasure.isometryEquiv_comap_mkMetric
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
simp :
  Eq.{u_2 + 1} (α := OuterMeasure X) (⨆ (i : ℕ), trim (mkMetric'.pre (fun (s : Set X) ↦ m (ediam s)) (↑i : ℝ≥0∞)⁻¹))
    (⨆ (n : ℕ), mkMetric'.pre (fun (s : Set X) ↦ m (ediam s)) (↑n : ℝ≥0∞)⁻¹)
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) (trim (mkMetric m)) (mkMetric m)

Tactic:
simp only [mkMetric, mkMetric'.eq_iSup_nat, trim_iSup]

Premises used: MeasureTheory.OuterMeasure.mkMetric, MeasureTheory.OuterMeasure.mkMetric'.eq_iSup_nat, MeasureTheory.OuterMeasure.trim_iSup
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
e_s :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := OuterMeasure X) (trim (mkMetric'.pre (fun (s : Set X) ↦ m (ediam s)) (↑n : ℝ≥0∞)⁻¹))
      (mkMetric'.pre (fun (s : Set X) ↦ m (ediam s)) (↑n : ℝ≥0∞)⁻¹)
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) (⨆ (i : ℕ), trim (mkMetric'.pre (fun (s : Set X) ↦ m (ediam s)) (↑i : ℝ≥0∞)⁻¹))
    (⨆ (n : ℕ), mkMetric'.pre (fun (s : Set X) ↦ m (ediam s)) (↑n : ℝ≥0∞)⁻¹)

Tactic:
congr 1 with n : 1
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
n : ℕ
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) (trim (mkMetric'.pre (fun (s : Set X) ↦ m (ediam s)) (↑n : ℝ≥0∞)⁻¹))
    (mkMetric'.pre (fun (s : Set X) ↦ m (ediam s)) (↑n : ℝ≥0∞)⁻¹)

Tactic:
mkMetric'.trim_pre _ (fun s => ?_) _

Premises used: MeasureTheory.OuterMeasure.mkMetric'.trim_pre
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
n : ℕ
e_s : ∀ (s : Set X), m (ediam (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) = m (ediam s)
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) (trim (mkMetric'.pre (fun (s : Set X) ↦ m (ediam s)) (↑n : ℝ≥0∞)⁻¹))
    (mkMetric'.pre (fun (s : Set X) ↦ m (ediam s)) (↑n : ℝ≥0∞)⁻¹)

Tactic:
refine mkMetric'.trim_pre _ (fun s => ?_) _

Premises used: MeasureTheory.OuterMeasure.mkMetric'.trim_pre
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
n : ℕ
s : Set X
⊢ m (ediam (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) = m (ediam s)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
μ : OuterMeasure X
r : ℝ≥0∞
h0 : 0 < r
hr : ∀ (s : Set X), ediam s ≤ r → (μ : (a : Set X) → ℝ≥0∞) s ≤ m (ediam s)
⊢ μ ≤ mkMetric m

Tactic:
le_iSup₂_of_le r h0 <| mkMetric'.le_pre.2 fun _ hs => hr _ hs

Premises used: Iff.mpr, Set.Mem, le_iSup₂_of_le, MeasureTheory.OuterMeasure.mkMetric'.le_pre
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : Set X → ℝ≥0∞
⊢ toOuterMeasure (mkMetric' m) = (OuterMeasure.mkMetric' m).trim

Tactic:
rfl

Premises used: MeasureTheory.inducedOuterMeasure, MeasureTheory.OuterMeasure.trim, rfl, MeasureTheory.OuterMeasure.ofFunction
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) (toOuterMeasure (mkMetric m)) (OuterMeasure.mkMetric m)

Tactic:
OuterMeasure.trim_mkMetric m

Premises used: MeasureTheory.inducedOuterMeasure, MeasureTheory.OuterMeasure.trim, MeasureTheory.OuterMeasure.trim_mkMetric, MeasureTheory.OuterMeasure.ofFunction
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
rw :
  Eq.{u_2 + 1} (α := (a : Set X) → ℝ≥0∞) (⇑(Measure.toOuterMeasure (Measure.mkMetric m)) : (a : Set X) → ℝ≥0∞)
    (⇑(Measure.mkMetric m) : (a : Set X) → ℝ≥0∞)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := (a : Set X) → ℝ≥0∞) (⇑(Measure.mkMetric m) : (a : Set X) → ℝ≥0∞)
    (⇑(Measure.mkMetric m) : (a : Set X) → ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := (a : Set X) → ℝ≥0∞) (⇑(mkMetric m) : (a : Set X) → ℝ≥0∞)
    (⇑(Measure.mkMetric m) : (a : Set X) → ℝ≥0∞)

Tactic:
rw [← Measure.mkMetric_toOuterMeasure, Measure.coe_toOuterMeasure]

Premises used: MeasureTheory.Measure.coe_toOuterMeasure, MeasureTheory.Measure.mkMetric_toOuterMeasure
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
s : Set X
rw :
  ((OuterMeasure.mkMetric m₁ : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s ≤
    HSMul.hSMul (β := (a : Set X) → ℝ≥0∞) c (⇑(OuterMeasure.mkMetric m₂) : (a : Set X) → ℝ≥0∞) s
⊢ LE.le (α := ℝ≥0∞) (((mkMetric m₁ : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (β := Measure X) c (mkMetric m₂) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← OuterMeasure.coe_mkMetric, coe_smul, ← OuterMeasure.coe_mkMetric]

Premises used: MeasureTheory.Measure.coe_smul, MeasureTheory.OuterMeasure.coe_mkMetric
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
s : Set X
⊢ ((OuterMeasure.mkMetric m₁ : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s ≤
    HSMul.hSMul (β := (a : Set X) → ℝ≥0∞) c (⇑(OuterMeasure.mkMetric m₂) : (a : Set X) → ℝ≥0∞) s

Tactic:
OuterMeasure.mkMetric_mono_smul hc h0 hle s

Premises used: MeasureTheory.OuterMeasure.mkMetric_mono_smul
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
s : Set X
⊢ ((OuterMeasure.mkMetric m₁ : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s ≤
    HSMul.hSMul (β := (a : Set X) → ℝ≥0∞) c (⇑(OuterMeasure.mkMetric m₂) : (a : Set X) → ℝ≥0∞) s

Tactic:
exact OuterMeasure.mkMetric_mono_smul hc h0 hle s

Premises used: MeasureTheory.OuterMeasure.mkMetric_mono_smul
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
a : Eq.{u_2 + 1} (α := OuterMeasure X) (toOuterMeasure (mkMetric fun (x : ℝ≥0∞) ↦ ∞)) (toOuterMeasure ⊤)
⊢ Eq.{u_2 + 1} (α := Measure X) (mkMetric fun (x : ℝ≥0∞) ↦ ∞) ⊤

Tactic:
apply toOuterMeasure_injective

Premises used: MeasureTheory.Measure.toOuterMeasure_injective
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
a : Eq.{u_2 + 1} (α := OuterMeasure X) (OuterMeasure.mkMetric fun (x : ℝ≥0∞) ↦ ∞) (toOuterMeasure ⊤)
a₁ : Eq.{u_2 + 1} (α := OuterMeasure X) ⊤ (toOuterMeasure ⊤)
a₂ a₃ : Eq.{u_2 + 1} (α := OuterMeasure X) ⊤ ⊤
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) (toOuterMeasure (mkMetric fun (x : ℝ≥0∞) ↦ ∞)) (toOuterMeasure ⊤)

Tactic:
rw [mkMetric_toOuterMeasure, OuterMeasure.mkMetric_top, toOuterMeasure_top]

Premises used: MeasureTheory.OuterMeasure.mkMetric_top, MeasureTheory.Measure.toOuterMeasure_top, MeasureTheory.Measure.mkMetric_toOuterMeasure
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂
⊢ mkMetric m₁ ≤ HSMul.hSMul (α := ℝ≥0∞) (β := Measure 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.Measure.mkMetric_mono_smul
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂
h : mkMetric m₂ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) 1 (mkMetric m₂)
convert_2 : m₁ ≤ᶠ[𝓝[≥] 0] HSMul.hSMul (α := ℝ≥0∞) 1 m₂
⊢ LE.le.{u_2} (α := Measure 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.Measure.mkMetric_mono_smul
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂
⊢ mkMetric m₂ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) 1 (mkMetric m₂)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace 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
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
simp :
  Eq (α := ℝ≥0∞)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : i > 0),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ i), m (ediam (t n)))
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
⊢ Eq (α := ℝ≥0∞) (((mkMetric m : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (⨆ (r : ℝ≥0∞),
        ⨆ (_ : 0 < r),
          ⨅ (t : ℕ → Set X),
            ⨅ (_ : s ⊆ iUnion t),
              ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)) :
      ℝ≥0∞)

Tactic:
simp only [← OuterMeasure.coe_mkMetric, OuterMeasure.mkMetric, OuterMeasure.mkMetric',
    OuterMeasure.iSup_apply, OuterMeasure.mkMetric'.pre, OuterMeasure.boundedBy_apply, extend]

Premises used: MeasureTheory.extend, MeasureTheory.OuterMeasure.mkMetric', MeasureTheory.OuterMeasure.boundedBy_apply, MeasureTheory.OuterMeasure.mkMetric, MeasureTheory.OuterMeasure.mkMetric'.pre, MeasureTheory.OuterMeasure.coe_mkMetric, MeasureTheory.OuterMeasure.iSup_apply
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
⊢ Eq (α := ℝ≥0∞)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : i > 0),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ i), m (ediam (t n)))
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))

Tactic:
surjective_id.iSup_congr id fun r =>
      iSup_congr_Prop Iff.rfl fun _ =>
        surjective_id.iInf_congr _ fun t => iInf_congr_Prop Iff.rfl fun ht => ?_

Premises used: Function.Surjective.iSup_congr, Iff.rfl, id, iSup_congr_Prop, Function.surjective_id, iInf_congr_Prop, Function.Surjective.iInf_congr
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
id :
  ∀ r > 0,
    ∀ (t : ℕ → Set X) (ht : s ⊆ iUnion t),
      Eq (α := ℝ≥0∞)
        (∑' (n : ℕ), ⨆ (_ : (_root_.id t n).Nonempty), ⨅ (_ : ediam (_root_.id t n) ≤ r), m (ediam (_root_.id t n)))
        (⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ _root_.id r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
⊢ Eq (α := ℝ≥0∞)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : i > 0),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ i), m (ediam (t n)))
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))

Tactic:
refine
    surjective_id.iSup_congr id fun r =>
      iSup_congr_Prop Iff.rfl fun _ =>
        surjective_id.iInf_congr _ fun t => iInf_congr_Prop Iff.rfl fun ht => ?_
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
h : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
dsimp :
  Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
    (⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (id t n).Nonempty), ⨅ (_ : ediam (id t n) ≤ r), m (ediam (id t n)))
    (⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ id r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))

Tactic:
dsimp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
h : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
pos :
  ∀ (htr : ∀ (n : ℕ), ediam (t n) ≤ r),
    Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
      (⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
neg :
  ∀ (htr : ¬∀ (n : ℕ), ediam (t n) ≤ r),
    Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
      (⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
    (⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))

Tactic:
by_cases htr : ∀ n, ediam (t n) ≤ r
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
h : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∀ (n : ℕ), ediam (t n) ≤ r
pos :
  Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
    (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
    (⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))

Tactic:
rw [iInf_eq_if, if_pos htr]

Premises used: if_pos, iInf_eq_if
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
h : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∀ (n : ℕ), ediam (t n) ≤ r
pos :
  ∀ (n : ℕ),
    Eq (α := ℝ≥0∞) (⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
      (⨆ (_ : (t n).Nonempty), m (ediam (t n)))
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
    (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))

Tactic:
congr 1 with n : 1
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
h : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∀ (n : ℕ), ediam (t n) ≤ r
n : ℕ
⊢ Eq (α := ℝ≥0∞) (⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
    (⨆ (_ : (t n).Nonempty), m (ediam (t n)))

Tactic:
simp only [iInf_eq_if, htr n, if_true]

Premises used: if_true, iInf_eq_if
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
h : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ¬∀ (n : ℕ), ediam (t n) ≤ r
neg : Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
    (⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))

Tactic:
rw [iInf_eq_if, if_neg htr]

Premises used: iInf_eq_if, if_neg
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
h : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ¬∀ (n : ℕ), ediam (t n) ≤ r
⊢ ∃ (n : ℕ), r < ediam (t n)

Tactic:
push Not at htr

Premises used: Not
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
h : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∃ (n : ℕ), r < ediam (t n)
neg :
  ∀ (n : ℕ) (hn : r < ediam (t n)),
    Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞

Tactic:
rcases htr with ⟨n, hn⟩
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
h : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < ediam (t n)
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞

Tactic:
ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩

Premises used: ENNReal.tsum_eq_top_of_eq_top, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
h : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < ediam (t n)
neg : Eq (α := ℝ≥0∞) (⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞

Tactic:
refine ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩

Premises used: ENNReal.tsum_eq_top_of_eq_top, Exists.intro