awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i)
P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i
mem_C : ∀ {i : ι} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i), i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂), C₁ ⊆ C₂
C : Finset ι
hC : C ∈ Cs
hPC : ¬P C = ∅
hCM : (↑C : Set ι).encard ≤ (↑M : ℕ∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) (#({a ∈ F | a ∈ C})) ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
nsmul_le_nsmul_left zero_le <| calc {a ∈ F | a ∈ C}.card
        _ ≤ C.card := card_mono <| fun i hi ↦ (F.mem_filter.mp hi).2
        _ = (C : Set ι).ncard := (ncard_coe_finset C).symm
        _ ≤ M := ENat.toNat_le_of_le_coe hCM

Premises used: zero_le, Trans.trans, nsmul_le_nsmul_left, ENat.toNat_le_of_le_coe, And.right, Iff.mp, Finset.mem_filter, Eq.symm, rfl, Set.ncard_coe_finset, Finset.card_mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i)
P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i
mem_C : ∀ {i : ι} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i), i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂), C₁ ⊆ C₂
C : Finset ι
hC : C ∈ Cs
hPC : ¬P C = ∅
hCM : (↑C : Set ι).encard ≤ (↑M : ℕ∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) (#({a ∈ F | a ∈ C})) ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact nsmul_le_nsmul_left zero_le <| calc {a ∈ F | a ∈ C}.card
        _ ≤ C.card := card_mono <| fun i hi ↦ (F.mem_filter.mp hi).2
        _ = (C : Set ι).ncard := (ncard_coe_finset C).symm
        _ ≤ M := ENat.toNat_le_of_le_coe hCM

Premises used: zero_le, Membership.mem, nsmul_le_nsmul_left, ENat.toNat_le_of_le_coe, SetLike.coe, And.right, Iff.mp, Finset.card, Finset.mem_filter, Set.ncard, Eq.symm, Finset.filter, Set.ncard_coe_finset, Finset.card_mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i)
P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i
mem_C : ∀ {i : ι} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i), i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂), C₁ ⊆ C₂
rw : (↑Cs : Set (Finset ι)).Pairwise (Disjoint on P)
⊢ ∑ C ∈ Cs, HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (⋃ C ∈ Cs, P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [← smul_sum, ← Cs.tsum_subtype, μ.restrict_biUnion_finset _ P_meas, Measure.sum_apply _ ht]

Premises used: MeasureTheory.Measure.sum_apply, MeasureTheory.Measure.restrict_biUnion_finset, Finset.smul_sum, Finset.tsum_subtype
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i)
P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i
mem_C : ∀ {i : ι} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i), i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂), C₁ ⊆ C₂
⊢ (↑Cs : Set (Finset ι)).Pairwise (Disjoint on P)

Tactic:
fun C₁ hC₁ C₂ hC₂ hC ↦ Set.disjoint_iff.mpr fun x hx ↦ hC <| ?_

Premises used: Iff.mpr, Set.Pairwise, Set.disjoint_iff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i)
P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i
mem_C : ∀ {i : ι} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i), i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂), C₁ ⊆ C₂
refine :
  ∀ (C₁ : Finset ι) (hC₁ : C₁ ∈ (↑Cs : Set (Finset ι))) (C₂ : Finset ι) (hC₂ : C₂ ∈ (↑Cs : Set (Finset ι)))
    (hC : C₁ ≠ C₂) (x : α) (hx : x ∈ P C₁ ∩ P C₂), C₁ = C₂
⊢ (↑Cs : Set (Finset ι)).Pairwise (Disjoint on P)

Tactic:
refine fun C₁ hC₁ C₂ hC₂ hC ↦ Set.disjoint_iff.mpr fun x hx ↦ hC <| ?_

Premises used: Iff.mpr, Set.disjoint_iff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
x_1 : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i)
P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i
mem_C : ∀ {i : ι} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i), i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂), C₁ ⊆ C₂
C₁ : Finset ι
hC₁ : C₁ ∈ (↑Cs : Set (Finset ι))
C₂ : Finset ι
hC₂ : C₂ ∈ (↑Cs : Set (Finset ι))
hC : C₁ ≠ C₂
x : α
hx : x ∈ P C₁ ∩ P C₂
⊢ C₁ = C₂

Tactic:
subset_antisymm (C_subset_C hC₁ hx) (C_subset_C hC₂ (Set.inter_comm _ _ ▸ hx))

Premises used: subset_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
x_1 : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i)
P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i
mem_C : ∀ {i : ι} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i), i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂), C₁ ⊆ C₂
C₁ : Finset ι
hC₁ : C₁ ∈ (↑Cs : Set (Finset ι))
C₂ : Finset ι
hC₂ : C₂ ∈ (↑Cs : Set (Finset ι))
hC : C₁ ≠ C₂
x : α
hx : x ∈ P C₁ ∩ P C₂
⊢ C₁ = C₂

Tactic:
exact subset_antisymm (C_subset_C hC₁ hx) (C_subset_C hC₂ (Set.inter_comm _ _ ▸ hx))

Premises used: subset_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i)
P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i
mem_C : ∀ {i : ι} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i), i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂), C₁ ⊆ C₂
⊢ HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (⋃ C ∈ Cs, P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
nsmul_le_nsmul_right (μ.restrict_mono_set iUnion_P t) M

Premises used: MeasureTheory.Measure.restrict_mono_set, nsmul_le_nsmul_right
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i)
P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i
mem_C : ∀ {i : ι} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i), i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂), C₁ ⊆ C₂
⊢ HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (⋃ C ∈ Cs, P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact nsmul_le_nsmul_right (μ.restrict_mono_set iUnion_P t) M

Premises used: MeasureTheory.Measure.restrict_mono_set, nsmul_le_nsmul_right
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
rcases : ∀ (t : Set X) (ht : t ∈ 𝒜), 𝒜.Nonempty
⊢ 𝒜.Nonempty

Tactic:
rcases h𝒜.approx ∅ MeasurableSet.empty (by simp) 1 (by simp) with ⟨t, ht, -⟩

Premises used: MeasureTheory.Measure.MeasureDense.approx, MeasurableSet.empty, EmptyCollection.emptyCollection, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
⊢ 𝒜.Nonempty

Tactic:
⟨t, ht⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
⊢ 𝒜.Nonempty

Tactic:
exact ⟨t, ht⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
rcases :
  ∀ (t : Set X) (ht : t ∈ 𝒜) (hμt : (μ : (a : Set X) → ℝ≥0∞) (∅ ∆ t) < ENNReal.ofReal 1),
    Set.Nonempty.{u_1} (α := Set X) {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
⊢ Set.Nonempty.{u_1} (α := Set X) {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}

Tactic:
rcases h𝒜.approx ∅ MeasurableSet.empty (by simp) 1 (by simp) with ⟨t, ht, hμt⟩

Premises used: MeasureTheory.Measure.MeasureDense.approx, MeasurableSet.empty, EmptyCollection.emptyCollection, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : (μ : (a : Set X) → ℝ≥0∞) (∅ ∆ t) < ENNReal.ofReal 1
⊢ Set.Nonempty.{u_1} (α := Set X) {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}

Tactic:
⟨t, ht, ?_⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : (μ : (a : Set X) → ℝ≥0∞) (∅ ∆ t) < ENNReal.ofReal 1
refine : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Set.Nonempty.{u_1} (α := Set X) {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}

Tactic:
refine ⟨t, ht, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : (μ : (a : Set X) → ℝ≥0∞) (∅ ∆ t) < ENNReal.ofReal 1
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (∅ ∆ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ne_top_of_lt hμt

Premises used: ne_top_of_lt
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : (μ : (a : Set X) → ℝ≥0∞) (∅ ∆ t) < ENNReal.ofReal 1
h : t = ∅ ∆ t
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
convert! ne_top_of_lt hμt

Premises used: ne_top_of_lt
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : (μ : (a : Set X) → ℝ≥0∞) (∅ ∆ t) < ENNReal.ofReal 1
h : t = ⊥ ∆ t
h₁ h₂ : t = t
⊢ t = ∅ ∆ t

Tactic:
rw [← bot_eq_empty, bot_symmDiff]

Premises used: bot_symmDiff, Set.bot_eq_empty
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
s : Set X
hs : MeasurableSet s
h : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ s) < ENNReal.ofReal ε

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
obtain :
  ∀ (t : Set X) (ht : t ∈ 𝒜) (hμst : (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε),
    ∃ t ∈ 𝒜, (μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜, (μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
obtain ⟨t, ht, hμst⟩ :=
      h𝒜.approx (toMeasurable μ s) (measurableSet_toMeasurable μ s) (by simpa) ε ε_pos

Premises used: MeasureTheory.Measure.MeasureDense.approx, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
ht : t ∈ 𝒜
hμst : (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜, (μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
⟨t, ht, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
ht : t ∈ 𝒜
hμst : (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε
refine : (μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜, (μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
refine ⟨t, ht, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
ht : t ∈ 𝒜
hμst : (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε
⊢ (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε

Tactic:
hμst
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
ht : t ∈ 𝒜
hμst : (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε
h :
  Eq (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) : ℝ≥0∞)
⊢ (μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
convert! hμst using 1
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
ht : t ∈ 𝒜
hμst : (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) : ℝ≥0∞)

Tactic:
rw [completion_apply]

Premises used: MeasureTheory.Measure.completion_apply
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
ht : t ∈ 𝒜
hμst : (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) : ℝ≥0∞)

Tactic:
measure_congr <| ae_eq_set_symmDiff (NullMeasurableSet.toMeasurable_ae_eq hs).symm
      Filter.EventuallyEq.rfl

Premises used: MeasureTheory.measure_congr, MeasureTheory.ae_eq_set_symmDiff, Filter.EventuallyEq.rfl, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
ht : t ∈ 𝒜
hμst : (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) : ℝ≥0∞)

Tactic:
exact measure_congr <| ae_eq_set_symmDiff (NullMeasurableSet.toMeasurable_ae_eq hs).symm
      Filter.EventuallyEq.rfl

Premises used: MeasureTheory.measure_congr, MeasureTheory.ae_eq_set_symmDiff, Filter.EventuallyEq.rfl, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
rcases :
  ∀ (t : Set X) (t_mem : t ∈ 𝒜) (ht : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε),
    ∃ t ∈ 𝒜,
      Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜,
    Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
rcases h𝒜.approx s ms hμs ε ε_pos with ⟨t, t_mem, ht⟩

Premises used: MeasureTheory.Measure.MeasureDense.approx
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
t_mem : t ∈ 𝒜
ht : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜,
    Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
⟨t, t_mem, (measure_ne_top_iff_of_symmDiff <| ne_top_of_lt ht).1 hμs, ht⟩

Premises used: MeasureTheory.measure_ne_top_iff_of_symmDiff, And.intro, Exists.intro, Iff.mp, ne_top_of_lt
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
t_mem : t ∈ 𝒜
ht : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜,
    Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
exact ⟨t, t_mem, (measure_ne_top_iff_of_symmDiff <| ne_top_of_lt ht).1 hμs, ht⟩