awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst : (j : κ) → TopologicalSpace (Y j)
inst_1 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_2 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
mZ : MeasurableSpace Z
inst_3 : TopologicalSpace Z
inst_4 : BorelSpace Z
inst_5 : HasOuterApproxClosed Z
inst_6 : Finite κ
μ : Measure Z
ν : Measure ((j : κ) → Y j)
ξ : Measure (Z × ((j : κ) → Y j))
inst_7 : IsFiniteMeasure μ
inst_8 : IsFiniteMeasure ν
inst_9 : IsFiniteMeasure ξ
h :
  ∀ (f : Z →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    ∫ (p : Z × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (z : Z), (f : (a : Z) → ℝ) z ∂μ) (∫ (y : (j : κ) → Y j), (g : (a : (j : κ) → Y j) → ℝ) y ∂ν)
f : Z →ᵇ ℝ
g : ((j : κ) → Y j) →ᵇ ℝ
rw :
  HMul.hMul (α := ℝ) (∫ (z : Z), (f : (a : Z) → ℝ) z ∂μ) (∫ (y : (j : κ) → Y j), (g : (a : (j : κ) → Y j) → ℝ) y ∂ν) =
    ∫ (p : Z × ((i : κ) → Y i)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ.prod ν
⊢ Eq (α := ℝ)
    (∫ (p : Z × ((i : κ) → Y i)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ξ)
    (∫ (p : Z × ((i : κ) → Y i)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ.prod ν)
have rw₁ : Eq (α := ℝ)
  (∫ (z : Z × ((j : κ) → Y j)),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) z.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) z.2 : ℝ) ∂μ.prod ν)
  (∫ (p : Z × ((i : κ) → Y i)),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ.prod ν)
Tactic: rw [h, ← integral_prod_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
s : ι → Set X
i : ι
I : Finset ι
hiI : i ∉ I
ihI :
  ∀ (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
hI : ∀ i_1 ∈ insert i I, ∀ j ∈ insert i I, i_1 ≠ j → AreSeparated (s i_1) (s j)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i_1 ∈ insert i I, s i_1) : ℝ≥0∞)
    (∑ i ∈ insert i I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
have hI₁ : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ I → ∀ (j : ι), j = i ∨ j ∈ I → i_1 ≠ j → AreSeparated (s i_1) (s j)
Tactic: simp only [Finset.mem_insert] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
s : ι → Set X
i : ι
I : Finset ι
hiI : i ∉ I
ihI :
  ∀ (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
hI : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ I → ∀ (j : ι), j = i ∨ j ∈ I → i_1 ≠ j → AreSeparated (s i_1) (s j)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i_1 ∈ insert i I, s i_1) : ℝ≥0∞)
    (∑ i ∈ insert i I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
have insert : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)
Tactic: rw [Finset.set_biUnion_insert, hm, ihI, Finset.sum_insert hiI]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
s : ι → Set X
i : ι
I : Finset ι
hiI : i ∉ I
ihI :
  ∀ (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
hI : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ I → ∀ (j : ι), j = i ∨ j ∈ I → i_1 ≠ j → AreSeparated (s i_1) (s j)
insert : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i_1 ∈ Insert.insert i I, s i_1) : ℝ≥0∞)
    (∑ i ∈ Insert.insert i I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
have insert₁ : AreSeparated (s i) (⋃ x ∈ I, s x)
Tactic: rw [Finset.set_biUnion_insert, hm, ihI, Finset.sum_insert hiI]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
I : Finset ι
s : ι → Set X
hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
have empty : ∀
  (hI :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → AreSeparated (s i) (s j)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : ℝ≥0∞)
    (∑ i ∈ ∅, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: induction I using Finset.induction_on with
  | empty => simp
  | insert i I hiI ihI =>
    simp only [Finset.mem_insert] at hI
    rw [Finset.set_biUnion_insert, hm, ihI, Finset.sum_insert hiI]
    exacts [fun i hi j hj hij => hI i (Or.inr hi) j (Or.inr hj) hij,
      Metric.AreSeparated.finset_iUnion_right fun j hj =>
        hI i (Or.inl rfl) j (Or.inr hj) (ne_of_mem_of_not_mem hj hiI).symm]
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
I : Finset ι
s : ι → Set X
hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)
empty :
  ∀
    (hI :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → AreSeparated (s i) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : ℝ≥0∞)
      (∑ i ∈ ∅, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
have insert : ∀ (i : ι) (I : Finset ι) (hiI : i ∉ I)
  (ihI :
    ∀ (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞))
  (hI : ∀ i_1 ∈ insert i I, ∀ j ∈ insert i I, i_1 ≠ j → AreSeparated (s i_1) (s j)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i_1 ∈ insert i I, s i_1) : ℝ≥0∞)
    (∑ i ∈ insert i I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: induction I using Finset.induction_on with
  | empty => simp
  | insert i I hiI ihI =>
    simp only [Finset.mem_insert] at hI
    rw [Finset.set_biUnion_insert, hm, ihI, Finset.sum_insert hiI]
    exacts [fun i hi j hj hij => hI i (Or.inr hi) j (Or.inr hj) hij,
      Metric.AreSeparated.finset_iUnion_right fun j hj =>
        hI i (Or.inl rfl) j (Or.inr hj) (ne_of_mem_of_not_mem hj hiI).symm]
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
I : Finset ι
s : ι → Set X
hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
have empty : ∀
  (hI :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → AreSeparated (s i) (s j)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : ℝ≥0∞)
    (∑ i ∈ ∅, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: classical
  induction I using Finset.induction_on with
  | empty => simp
  | insert i I hiI ihI =>
    simp only [Finset.mem_insert] at hI
    rw [Finset.set_biUnion_insert, hm, ihI, Finset.sum_insert hiI]
    exacts [fun i hi j hj hij => hI i (Or.inr hi) j (Or.inr hj) hij,
      Metric.AreSeparated.finset_iUnion_right fun j hj =>
        hI i (Or.inl rfl) j (Or.inr hj) (ne_of_mem_of_not_mem hj hiI).symm]
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
I : Finset ι
s : ι → Set X
hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)
empty :
  ∀
    (hI :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → AreSeparated (s i) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : ℝ≥0∞)
      (∑ i ∈ ∅, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
have insert : ∀ (i : ι) (I : Finset ι) (hiI : i ∉ I)
  (ihI :
    ∀ (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞))
  (hI : ∀ i_1 ∈ insert i I, ∀ j ∈ insert i I, i_1 ≠ j → AreSeparated (s i_1) (s j)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i_1 ∈ insert i I, s i_1) : ℝ≥0∞)
    (∑ i ∈ insert i I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: classical
  induction I using Finset.induction_on with
  | empty => simp
  | insert i I hiI ihI =>
    simp only [Finset.mem_insert] at hI
    rw [Finset.set_biUnion_insert, hm, ihI, Finset.sum_insert hiI]
    exacts [fun i hi j hj hij => hI i (Or.inr hi) j (Or.inr hj) hij,
      Metric.AreSeparated.finset_iUnion_right fun j hj =>
        hI i (Or.inl rfl) j (Or.inr hj) (ne_of_mem_of_not_mem hj hiI).symm]
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
⊢ borel X ≤ μ.caratheodory
have rw : MeasurableSpace.generateFrom {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} ≤
  μ.caratheodory
Tactic: rw [borel_eq_generateFrom_isClosed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
⊢ MeasurableSpace.generateFrom {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} ≤
    μ.caratheodory
have refine : ∀ (t : Set X)
  (ht :
    Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t)
  (s : Set X),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s
Tactic: refine MeasurableSpace.generateFrom_le fun t ht => μ.isCaratheodory_iff_le.2 fun s => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s
have Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Tactic: have Ssep (n) : Metric.AreSeparated (S n) t :=
    ⟨n⁻¹, ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _),
      fun x hx y hy ↦ hx.2.trans <| infEDist_le_edist_of_mem hy⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s
have Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
Tactic: have Ssep' : ∀ n, Metric.AreSeparated (S n) (s ∩ t) := fun n =>
    (Ssep n).mono Subset.rfl inter_subset_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s
have S_sub : ∀ (n : ℕ), S n ⊆ s \ t
Tactic: have S_sub : ∀ n, S n ⊆ s \ t := fun n =>
    subset_inter inter_subset_left (Ssep n).subset_compl_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t ∪ s \ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [inter_union_diff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s
have hSs : ∀ (n : ℕ),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s
Tactic: have hSs : ∀ n, μ (s ∩ t) + μ (S n) ≤ μ s := fun n =>
    calc
      μ (s ∩ t) + μ (S n) = μ (s ∩ t ∪ S n) := Eq.symm <| hm _ _ <| (Ssep' n).symm
      _ ≤ μ (s ∩ t ∪ s \ t) := μ.mono <| union_subset_union_right _ <| S_sub n
      _ = μ s := by rw [inter_union_diff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
⊢ ⋃ (n : ℕ), S n = s \ t
have refine : s \ t ⊆ ⋃ (n : ℕ), S n
Tactic: refine Subset.antisymm (iUnion_subset S_sub) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
x : X
hxs : x ∈ s
hxt : x ∉ t
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), S n) x
have hxt₁ : ¬infEDist x t = 0
Tactic: rw [mem_iff_infEDist_zero_of_closed ht] at hxt
Cleared hypotheses: hxt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
x : X
hxs : x ∈ s
hxt : ¬infEDist x t = 0
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), S n) x
have rcases : ∀ (n : ℕ) (hn : (↑n : ℝ≥0∞)⁻¹ < infEDist x t), Membership.mem (γ := Set X) (⋃ (n : ℕ), S n) x
Tactic: rcases ENNReal.exists_inv_nat_lt hxt with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s
have iUnion_S : ⋃ (n : ℕ), S n = s \ t
Tactic: have iUnion_S : ⋃ n, S n = s \ t := by
    refine Subset.antisymm (iUnion_subset S_sub) ?_
    rintro x ⟨hxs, hxt⟩
    rw [mem_iff_infEDist_zero_of_closed ht] at hxt
    rcases ENNReal.exists_inv_nat_lt hxt with ⟨n, hn⟩
    exact mem_iUnion.2 ⟨n, hxs, hn.le⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
iUnion_S : ⋃ (n : ℕ), S n = s \ t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s
have pos : ∀ (htop : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s
Tactic: by_cases htop : μ (s \ t) = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
iUnion_S : ⋃ (n : ℕ), S n = s \ t
pos :
  ∀ (htop : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s
have neg : ∀ (htop : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s
Tactic: by_cases htop : μ (s \ t) = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
iUnion_S : ⋃ (n : ℕ), S n = s \ t
htop : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s
have pos : LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [htop, add_top, ← htop]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} t
s : Set X
S : ℕ → Set X := fun (n : ℕ) ↦ {x : X | x ∈ s ∧ (↑n : ℝ≥0∞)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
iUnion_S : ⋃ (n : ℕ), S n = s \ t
htop : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), S n) : ℝ≥0∞)
    (⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), S n) : ℝ≥0∞)
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
Tactic: rw [iUnion_S]