awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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}
⊢ ∀ (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⟩
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ ∀ (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
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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)
⊢ ∀ (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
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : ℕ
rw rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t ∪ s \ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [inter_union_diff]

Premises used: Set.inter_union_diff
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : ℕ),
    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]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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

Tactic:
Subset.antisymm (iUnion_subset S_sub) ?_

Premises used: Set.Subset.antisymm, Set.iUnion_subset
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
refine : s \ t ⊆ ⋃ (n : ℕ), S n
⊢ ⋃ (n : ℕ), S n = s \ t

Tactic:
refine Subset.antisymm (iUnion_subset S_sub) ?_

Premises used: Set.Subset.antisymm, Set.iUnion_subset
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ ¬infEDist x t = 0

Tactic:
rw [mem_iff_infEDist_zero_of_closed ht] at hxt

Premises used: Metric.mem_iff_infEDist_zero_of_closed
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
rcases : ∀ (n : ℕ) (hn : (↑n : ℝ≥0∞)⁻¹ < infEDist x t), Membership.mem (γ := Set X) (⋃ (n : ℕ), S n) x
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), S n) x

Tactic:
rcases ENNReal.exists_inv_nat_lt hxt with ⟨n, hn⟩

Premises used: ENNReal.exists_inv_nat_lt
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
n : ℕ
hn : (↑n : ℝ≥0∞)⁻¹ < infEDist x t
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), S n) x

Tactic:
mem_iUnion.2 ⟨n, hxs, hn.le⟩

Premises used: Iff.mpr, Set.mem_iUnion, LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
n : ℕ
hn : (↑n : ℝ≥0∞)⁻¹ < infEDist x t
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), S n) x

Tactic:
exact mem_iUnion.2 ⟨n, hxs, hn.le⟩
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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

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⟩
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
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
⊢ 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) = ∞

Premises used: SDiff.sdiff, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
pos : LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥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:
rw [htop, add_top, ← htop]

Premises used: add_top
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
μ.mono diff_subset

Premises used: Set.diff_subset, MeasureTheory.OuterMeasure.mono
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact μ.mono diff_subset

Premises used: Set.diff_subset, MeasureTheory.OuterMeasure.mono
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
rw 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∞)
⊢ 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∞)

Tactic:
rw [iUnion_S]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞) (⋃ (n : ℕ), S n) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      (⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
      (⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) =
    ⨆ (n : ℕ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞)

Tactic:
ENNReal.add_iSup ..

Premises used: ENNReal.add_iSup
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (n : ℕ),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
          ((μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞) :
      ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
iSup_le hSs

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
μ₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), S n) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥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∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s

Tactic:
calc
    μ (s ∩ t) + μ (s \ t) = μ (s ∩ t) + μ (⋃ n, S n) := by rw [iUnion_S]
    _ ≤ μ (s ∩ t) + ⨆ n, μ (S n) := by gcongr
    _ = ⨆ n, μ (s ∩ t) + μ (S n) := ENNReal.add_iSup ..
    _ ≤ μ s := iSup_le hSs

Premises used: Inter.inter, ENNReal.add_iSup, SDiff.sdiff, iSup_le, DFunLike.coe, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
neg :
  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∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) s

Tactic:
suffices μ (⋃ n, S n) ≤ ⨆ n, μ (S n) by calc
    μ (s ∩ t) + μ (s \ t) = μ (s ∩ t) + μ (⋃ n, S n) := by rw [iUnion_S]
    _ ≤ μ (s ∩ t) + ⨆ n, μ (S n) := by gcongr
    _ = ⨆ n, μ (s ∩ t) + μ (S n) := ENNReal.add_iSup ..
    _ ≤ μ s := iSup_le hSs
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
⊢ ∀ (n : ℕ), S n ⊆ S (n + 1)

Tactic:
have : ∀ n, S n ⊆ S (n + 1) := fun n x hx =>
    ⟨hx.1, le_trans (ENNReal.inv_le_inv.2 <| Nat.cast_le.2 n.le_succ) hx.2⟩
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : ∀ (n : ℕ), S n ⊆ S (n + 1)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), S n) : ℝ≥0∞)
    (⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (S n) : ℝ≥0∞)

Tactic:
(μ.iUnion_nat_of_monotone_of_tsum_ne_top this ?_).le

Premises used: MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top, Eq.le