awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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'
⊢ mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
⊢ mkMetric m₁ ≤ HSMul.hSMul (β := OuterMeasure X) c (mkMetric m₂)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) (mkMetric fun (x : ℝ≥0∞) ↦ ∞) ⊤
have simp_rw : LE.le.{u_2} (α := OuterMeasure X) ⊤ (⨆ (r : ℝ≥0∞), ⨆ (_ : r > 0), ⊤)
Tactic: simp_rw [mkMetric, mkMetric', mkMetric'.pre, extend_top, boundedBy_top, eq_top_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
⊢ LE.le.{u_2} (α := OuterMeasure X) ⊤ (⨆ (r : ℝ≥0∞), ⨆ (_ : r > 0), ⊤)
have rw : ∀ (b : OuterMeasure X), (∀ (i : ℝ≥0∞), ⨆ (_ : i > 0), ⊤ ≤ b) → ⊤ ≤ b
Tactic: rw [le_iSup_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂
⊢ LE.le.{u_2} (α := OuterMeasure X) (mkMetric m₁) (mkMetric m₂)
have h : mkMetric m₂ = HSMul.hSMul (α := ℝ≥0∞) (β := OuterMeasure X) 1 (mkMetric m₂)
Tactic: convert! @mkMetric_mono_smul X _ _ m₂ _ ENNReal.one_ne_top one_ne_zero _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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₂)
⊢ LE.le.{u_2} (α := OuterMeasure X) (mkMetric m₁) (mkMetric m₂)
have convert_2 : m₁ ≤ᶠ[𝓝[≥] 0] HSMul.hSMul (α := ℝ≥0∞) 1 m₂
Tactic: convert! @mkMetric_mono_smul X _ _ m₂ _ ENNReal.one_ne_top one_ne_zero _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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) ((comap f : (a : OuterMeasure Y) → OuterMeasure X) (mkMetric m) : OuterMeasure X)
    (mkMetric m : OuterMeasure X)
have 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)))
Tactic: simp only [mkMetric, mkMetric', mkMetric'.pre, comap_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)))
have 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)
Tactic: refine surjective_id.iSup_congr id fun ε => surjective_id.iSup_congr id fun hε => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ 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)
have 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)))
Tactic: rw [comap_boundedBy _ (H.imp _ id)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)))
⊢ 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)
have 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)
Tactic: rw [comap_boundedBy _ (H.imp _ id)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ 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)))
have 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
Tactic: congr with s : 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ 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
have e_m : ediam (f '' s) ≤ ε ↔ ediam s ≤ id ε
Tactic: apply extend_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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 ε
⊢ 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
have e_m₁ : ∀ (ha : ediam (f '' s) ≤ ε) (hb : ediam s ≤ id ε), m (ediam (f '' s)) = m (ediam s)
Tactic: apply extend_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ 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)
have simp : ∀ (i : ediam (↑t : Set Y) ≤ ε), ⨅ (_ : ediam (↑s : Set Y) ≤ ε), m (ediam (↑s : Set Y)) ≤ m (ediam (↑t : Set Y))
Tactic: simp only [extend, le_iInf_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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 (↑t : Set Y))
have apply : ⨅ (_ : ediam (↑s : Set Y) ≤ ε), m (ediam (↑s : Set Y)) ≤ m (ediam (↑s : Set Y))
Tactic: apply le_trans _ (h_mono (ediam_mono hst))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hc' : c ≠ 0
⊢ mkMetric (c • m) = HSMul.hSMul (β := OuterMeasure X) c (mkMetric m)
have 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)))
Tactic: simp only [mkMetric, mkMetric', mkMetric'.pre]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hc' : c ≠ 0
⊢ ⨆ (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)))
have 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))))
Tactic: simp_rw [smul_iSup, smul_boundedBy hc, ennreal_smul_extend _ hc', Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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))))
⊢ ⨆ (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)))
have 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))))
Tactic: simp_rw [smul_iSup, smul_boundedBy hc, ennreal_smul_extend _ hc', Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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))))
⊢ ⨆ (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)))
have 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)))
Tactic: simp_rw [smul_iSup, smul_boundedBy hc, ennreal_smul_extend _ hc', Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0
hc : c ≠ 0
⊢ mkMetric (c • m) = HSMul.hSMul (β := OuterMeasure X) c (mkMetric m)
have rw : mkMetric ((↑c : ℝ≥0∞) • 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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)
⊢ mkMetric (c • m) = HSMul.hSMul (β := OuterMeasure X) c (mkMetric m)
have rw₁ : mkMetric ((↑c : ℝ≥0∞) • m) = HSMul.hSMul (β := OuterMeasure X) (↑c : ℝ≥0∞) (mkMetric m)
Tactic: rw [ENNReal.smul_def, ENNReal.smul_def,
    mkMetric_smul m ENNReal.coe_ne_top (ENNReal.coe_ne_zero.mpr hc)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)
⊢ mkMetric (c • m) = HSMul.hSMul (β := OuterMeasure X) c (mkMetric m)
have rw₂ : HSMul.hSMul (β := OuterMeasure X) (↑c : ℝ≥0∞) (mkMetric m) = HSMul.hSMul (β := OuterMeasure X) (↑c : ℝ≥0∞) (mkMetric m)
Tactic: rw [ENNReal.smul_def, ENNReal.smul_def,
    mkMetric_smul m ENNReal.coe_ne_top (ENNReal.coe_ne_zero.mpr hc)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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 (α := 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)
have 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)
Tactic: rw [← isometry_comap_mkMetric _ hf H, map_comap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← isometry_comap_mkMetric _ hf H, map_comap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X ≃ᵢ Y
⊢ Eq.{u_3 + 1} (α := OuterMeasure Y)
    ((map (⇑f : (a : X) → Y) : (a : OuterMeasure X) → OuterMeasure Y) (mkMetric m) : OuterMeasure Y)
    (mkMetric m : OuterMeasure Y)
have 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)
Tactic: rw [← isometryEquiv_comap_mkMetric _ f, map_comap_of_surjective f.surjective]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)
⊢ Eq.{u_3 + 1} (α := OuterMeasure Y)
    ((map (⇑f : (a : X) → Y) : (a : OuterMeasure X) → OuterMeasure Y) (mkMetric m) : OuterMeasure Y)
    (mkMetric m : OuterMeasure Y)
have rw₁ : Eq.{u_3 + 1} (α := OuterMeasure Y) (mkMetric m) (mkMetric m)
Tactic: rw [← isometryEquiv_comap_mkMetric _ f, map_comap_of_surjective f.surjective]