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
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) (trim (mkMetric m)) (mkMetric m)
have 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∞)⁻¹)
Tactic: simp only [mkMetric, mkMetric'.eq_iSup_nat, trim_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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) (⨆ (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∞)⁻¹)
have 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∞)⁻¹)
Tactic: congr 1 with n : 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)⁻¹)
have e_s : ∀ (s : Set X), m (ediam (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) = m (ediam s)
Tactic: refine mkMetric'.trim_pre _ (fun s => ?_) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
⊢ Eq.{u_2 + 1} (α := (a : Set X) → ℝ≥0∞) (⇑(mkMetric m) : (a : Set X) → ℝ≥0∞)
    (⇑(Measure.mkMetric m) : (a : Set X) → ℝ≥0∞)
have 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∞)
Tactic: rw [← Measure.mkMetric_toOuterMeasure, Measure.coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
⊢ Eq.{u_2 + 1} (α := (a : Set X) → ℝ≥0∞) (⇑(mkMetric m) : (a : Set X) → ℝ≥0∞)
    (⇑(Measure.mkMetric m) : (a : Set X) → ℝ≥0∞)
have rw₁ : Eq.{u_2 + 1} (α := (a : Set X) → ℝ≥0∞) (⇑(Measure.mkMetric m) : (a : Set X) → ℝ≥0∞)
  (⇑(Measure.mkMetric m) : (a : Set X) → ℝ≥0∞)
Tactic: rw [← Measure.mkMetric_toOuterMeasure, Measure.coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ 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∞)
have 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
Tactic: rw [← OuterMeasure.coe_mkMetric, coe_smul, ← OuterMeasure.coe_mkMetric]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
⊢ Eq.{u_2 + 1} (α := Measure X) (mkMetric fun (x : ℝ≥0∞) ↦ ∞) ⊤
have a : Eq.{u_2 + 1} (α := OuterMeasure X) (toOuterMeasure (mkMetric fun (x : ℝ≥0∞) ↦ ∞)) (toOuterMeasure ⊤)
Tactic: apply toOuterMeasure_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) (toOuterMeasure (mkMetric fun (x : ℝ≥0∞) ↦ ∞)) (toOuterMeasure ⊤)
have a : Eq.{u_2 + 1} (α := OuterMeasure X) (OuterMeasure.mkMetric fun (x : ℝ≥0∞) ↦ ∞) (toOuterMeasure ⊤)
Tactic: rw [mkMetric_toOuterMeasure, OuterMeasure.mkMetric_top, toOuterMeasure_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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 ⊤)
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) (toOuterMeasure (mkMetric fun (x : ℝ≥0∞) ↦ ∞)) (toOuterMeasure ⊤)
have a₁ : Eq.{u_2 + 1} (α := OuterMeasure X) ⊤ (toOuterMeasure ⊤)
Tactic: rw [mkMetric_toOuterMeasure, OuterMeasure.mkMetric_top, toOuterMeasure_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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 ⊤)
⊢ Eq.{u_2 + 1} (α := OuterMeasure X) (toOuterMeasure (mkMetric fun (x : ℝ≥0∞) ↦ ∞)) (toOuterMeasure ⊤)
have a₂ : Eq.{u_2 + 1} (α := OuterMeasure X) ⊤ ⊤
Tactic: rw [mkMetric_toOuterMeasure, OuterMeasure.mkMetric_top, toOuterMeasure_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂
⊢ LE.le.{u_2} (α := Measure X) (mkMetric m₁) (mkMetric m₂)
have h : mkMetric m₂ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure 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
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₂)
⊢ LE.le.{u_2} (α := Measure 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
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
⊢ 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∞)
have 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)))
Tactic: simp only [← OuterMeasure.coe_mkMetric, OuterMeasure.mkMetric, OuterMeasure.mkMetric',
    OuterMeasure.iSup_apply, OuterMeasure.mkMetric'.pre, OuterMeasure.boundedBy_apply, extend]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)))
have id : ∀ r > 0,
  ∀ (t : ℕ → Set X) (ht : s ⊆ iUnion t),
    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: 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 => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ 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)))
have 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)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ 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)))
have 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)))
Tactic: by_cases htr : ∀ n, ediam (t n) ≤ r
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)))
⊢ 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)))
have 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)))
Tactic: by_cases htr : ∀ n, ediam (t n) ≤ r
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ 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)))
have pos : Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
  (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
Tactic: rw [iInf_eq_if, if_pos htr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
    (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)))
have pos : ∀ (n : ℕ),
  Eq (α := ℝ≥0∞) (⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)))
    (⨆ (_ : (t n).Nonempty), m (ediam (t n)))
Tactic: congr 1 with n : 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ 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)))
have neg : Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞
Tactic: rw [iInf_eq_if, if_neg htr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
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
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞
have htr₁ : ∃ (n : ℕ), r < ediam (t n)
Tactic: push Not at htr
Cleared hypotheses: htr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞
have neg : ∀ (n : ℕ) (hn : r < ediam (t n)),
  Eq (α := ℝ≥0∞) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞
Tactic: rcases htr with ⟨n, hn⟩
Cleared hypotheses: htr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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))) ∞
have neg : Eq (α := ℝ≥0∞) (⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞
Tactic: refine ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞) (⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞
have neg : ¬ediam (t n) ≤ r
Tactic: rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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 : ¬ediam (t n) ≤ r
⊢ Eq (α := ℝ≥0∞) (⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n))) ∞
have neg₁ : (t n).Nonempty
Tactic: rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)
⊢ (t n).Nonempty
have neg : ∀ (x : X) (hx : x ∈ t n), (t n).Nonempty
Tactic: rcases ediam_pos_iff.1 hn.pos with ⟨x, hx, -⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
⊢ 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∞)
have We : 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: classical
  -- We mostly unfold the definitions but we need to switch the order of `∑'` and `⨅`
  simp only [← OuterMeasure.coe_mkMetric, OuterMeasure.mkMetric, OuterMeasure.mkMetric',
    OuterMeasure.iSup_apply, OuterMeasure.mkMetric'.pre, OuterMeasure.boundedBy_apply, extend]
  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 => ?_
  dsimp
  by_cases htr : ∀ n, ediam (t n) ≤ r
  · rw [iInf_eq_if, if_pos htr]
    congr 1 with n : 1
    simp only [iInf_eq_if, htr n, if_true]
  · rw [iInf_eq_if, if_neg htr]
    push Not at htr; rcases htr with ⟨n, hn⟩
    refine ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩
    rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg]
    · exact hn.not_ge
    rcases ediam_pos_iff.1 hn.pos with ⟨x, hx, -⟩
    exact ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
We :
  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∞)
have We₁ : ∀ r > 0,
  ∀ (t : ℕ → Set X) (ht : s ⊆ iUnion t),
    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: classical
  -- We mostly unfold the definitions but we need to switch the order of `∑'` and `⨅`
  simp only [← OuterMeasure.coe_mkMetric, OuterMeasure.mkMetric, OuterMeasure.mkMetric',
    OuterMeasure.iSup_apply, OuterMeasure.mkMetric'.pre, OuterMeasure.boundedBy_apply, extend]
  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 => ?_
  dsimp
  by_cases htr : ∀ n, ediam (t n) ≤ r
  · rw [iInf_eq_if, if_pos htr]
    congr 1 with n : 1
    simp only [iInf_eq_if, htr n, if_true]
  · rw [iInf_eq_if, if_neg htr]
    push Not at htr; rcases htr with ⟨n, hn⟩
    refine ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩
    rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg]
    · exact hn.not_ge
    rcases ediam_pos_iff.1 hn.pos with ⟨x, hx, -⟩
    exact ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
We :
  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)))
We₁ :
  ∀ r > 0,
    ∀ (t : ℕ → Set X) (ht : s ⊆ iUnion t),
      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)))
⊢ 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∞)
have We₂ : ∀ r > 0,
  ∀ (t : ℕ → Set X) (ht : s ⊆ iUnion t),
    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: classical
  -- We mostly unfold the definitions but we need to switch the order of `∑'` and `⨅`
  simp only [← OuterMeasure.coe_mkMetric, OuterMeasure.mkMetric, OuterMeasure.mkMetric',
    OuterMeasure.iSup_apply, OuterMeasure.mkMetric'.pre, OuterMeasure.boundedBy_apply, extend]
  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 => ?_
  dsimp
  by_cases htr : ∀ n, ediam (t n) ≤ r
  · rw [iInf_eq_if, if_pos htr]
    congr 1 with n : 1
    simp only [iInf_eq_if, htr n, if_true]
  · rw [iInf_eq_if, if_neg htr]
    push Not at htr; rcases htr with ⟨n, hn⟩
    refine ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩
    rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg]
    · exact hn.not_ge
    rcases ediam_pos_iff.1 hn.pos with ⟨x, hx, -⟩
    exact ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
We :
  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)))
We₁ :
  ∀ r > 0,
    ∀ (t : ℕ → Set X) (ht : s ⊆ iUnion t),
      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)))
We₂ :
  ∀ r > 0,
    ∀ (t : ℕ → Set X) (ht : s ⊆ iUnion t),
      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∞) (((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∞)
have pos : ∀ r > 0,
  ∀ (t : ℕ → Set X) (ht : s ⊆ iUnion t) (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)))
Tactic: classical
  -- We mostly unfold the definitions but we need to switch the order of `∑'` and `⨅`
  simp only [← OuterMeasure.coe_mkMetric, OuterMeasure.mkMetric, OuterMeasure.mkMetric',
    OuterMeasure.iSup_apply, OuterMeasure.mkMetric'.pre, OuterMeasure.boundedBy_apply, extend]
  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 => ?_
  dsimp
  by_cases htr : ∀ n, ediam (t n) ≤ r
  · rw [iInf_eq_if, if_pos htr]
    congr 1 with n : 1
    simp only [iInf_eq_if, htr n, if_true]
  · rw [iInf_eq_if, if_neg htr]
    push Not at htr; rcases htr with ⟨n, hn⟩
    refine ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩
    rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg]
    · exact hn.not_ge
    rcases ediam_pos_iff.1 hn.pos with ⟨x, hx, -⟩
    exact ⟨x, hx⟩