awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
ε : ℝ
εpos : ε > 0
s : Set X
hs : s ∈ v.setsAt x
h's : s ⊆ closedBall x ε
⊢ ∃ s ∈ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, s ⊆ closedBall x ε

Tactic:
exact ⟨s, mem_union_left _ hs, h's⟩
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ t ∈ f x, t ⊆ closedBall x (min ε δ)

Tactic:
ffine x hx (min ε δ) (lt_min εpos δpos)

Premises used: lt_min, Min.min
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
obtain : ∀ (t : Set X) (tf : t ∈ f x) (ht : t ⊆ closedBall x (min ε δ)), ∃ t ∈ g x, t ⊆ closedBall x ε
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε

Tactic:
obtain ⟨t, tf, ht⟩ : ∃ t ∈ f x, t ⊆ closedBall x (min ε δ) :=
        ffine x hx (min ε δ) (lt_min εpos δpos)

Premises used: lt_min, Metric.closedBall, Min.min
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
inl : ∀ (h't : t ∈ v.setsAt x), ∃ t ∈ g x, t ⊆ closedBall x ε
inr :
  ∀
    (h't :
      Membership.mem (γ := Set (Set X)) {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ} t),
    ∃ t ∈ g x, t ⊆ closedBall x ε
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε

Tactic:
rcases fset x hx tf with (h't | h't)
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
h't : t ∈ v.setsAt x
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε

Tactic:
⟨t, ⟨tf, h't⟩, ht.trans (closedBall_subset_closedBall (min_le_left _ _))⟩

Premises used: HasSubset.Subset.trans, min_le_left, And.intro, Exists.intro, Metric.closedBall_subset_closedBall
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
h't : t ∈ v.setsAt x
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε

Tactic:
exact ⟨t, ⟨tf, h't⟩, ht.trans (closedBall_subset_closedBall (min_le_left _ _))⟩
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
h't : Membership.mem (γ := Set (Set X)) {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ} t
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε

Tactic:
False.elim (h't.2.2 ?_)

Premises used: False.elim, And.right
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
h't : Membership.mem (γ := Set (Set X)) {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ} t
inr : t ⊆ closedBall x δ
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε

Tactic:
refine False.elim (h't.2.2 ?_)

Premises used: False.elim, And.right
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
h't : Membership.mem (γ := Set (Set X)) {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ} t
⊢ t ⊆ closedBall x δ

Tactic:
ht.trans (closedBall_subset_closedBall (min_le_right _ _))

Premises used: HasSubset.Subset.trans, min_le_right, Metric.closedBall_subset_closedBall
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
h't : Membership.mem (γ := Set (Set X)) {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ} t
⊢ t ⊆ closedBall x δ

Tactic:
exact ht.trans (closedBall_subset_closedBall (min_le_right _ _))

Premises used: HasSubset.Subset.trans, min_le_right, Metric.closedBall_subset_closedBall
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
⊢ ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ g x, t ⊆ closedBall x ε

Tactic:
have : ∀ x ∈ s, ∀ ε : ℝ, ε > 0 → ∃ t ∈ g x, t ⊆ closedBall x ε := by
      intro x hx ε εpos
      obtain ⟨t, tf, ht⟩ : ∃ t ∈ f x, t ⊆ closedBall x (min ε δ) :=
        ffine x hx (min ε δ) (lt_min εpos δpos)
      rcases fset x hx tf with (h't | h't)
      · exact ⟨t, ⟨tf, h't⟩, ht.trans (closedBall_subset_closedBall (min_le_left _ _))⟩
      · refine False.elim (h't.2.2 ?_)
        exact ht.trans (closedBall_subset_closedBall (min_le_right _ _))
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
this : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ g x, t ⊆ closedBall x ε
rcases :
  ∀ (t : Set (X × Set X)) (ts : ∀ p ∈ t, p.1 ∈ s) (tdisj : t.PairwiseDisjoint (α := Set X) fun (p : X × Set X) ↦ p.2)
    (tg : ∀ p ∈ t, p.2 ∈ g p.1)
    (μt : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ t, p.2) : ENNReal) (0 : ENNReal)),
    ∃ (t : Set (X × Set X)),
      (∀ p ∈ t, p.1 ∈ s) ∧
        (t.PairwiseDisjoint (α := Set X) fun (p : X × Set X) ↦ p.2) ∧
          (∀ p ∈ t, p.2 ∈ f p.1) ∧
            Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ t, p.2) : ENNReal) (0 : ENNReal)
⊢ ∃ (t : Set (X × Set X)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set X) fun (p : X × Set X) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧
          Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ t, p.2) : ENNReal) (0 : ENNReal)

Tactic:
rcases v.covering s g (fun x _ => inter_subset_right) this with ⟨t, ts, tdisj, tg, μt⟩

Premises used: VitaliFamily.covering, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
this : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ g x, t ⊆ closedBall x ε
t : Set (X × Set X)
ts : ∀ p ∈ t, p.1 ∈ s
tdisj : t.PairwiseDisjoint (α := Set X) fun (p : X × Set X) ↦ p.2
tg : ∀ p ∈ t, p.2 ∈ g p.1
μt : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ t, p.2) : ENNReal) (0 : ENNReal)
⊢ ∃ (t : Set (X × Set X)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set X) fun (p : X × Set X) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧
          Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ t, p.2) : ENNReal) (0 : ENNReal)

Tactic:
⟨t, ts, tdisj, fun p hp => (tg p hp).1, μt⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
this : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ g x, t ⊆ closedBall x ε
t : Set (X × Set X)
ts : ∀ p ∈ t, p.1 ∈ s
tdisj : t.PairwiseDisjoint (α := Set X) fun (p : X × Set X) ↦ p.2
tg : ∀ p ∈ t, p.2 ∈ g p.1
μt : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ t, p.2) : ENNReal) (0 : ENNReal)
⊢ ∃ (t : Set (X × Set X)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set X) fun (p : X × Set X) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧
          Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ t, p.2) : ENNReal) (0 : ENNReal)

Tactic:
exact ⟨t, ts, tdisj, fun p hp => (tg p hp).1, μt⟩
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
ι : Sort u_2
p : ι → Prop
s : ι → Set X
x : X
h : (𝓝 x).HasBasis p s
⊢ (v.filterAt x).HasBasis p fun (i : ι) ↦ {t : Set X | t ∈ v.setsAt x ∧ t ⊆ s i}

Tactic:
simpa only [← Set.setOf_inter_eq_sep] using h.smallSets.inf_principal _

Premises used: Filter.HasBasis.smallSets, Filter.HasBasis.inf_principal, Set.setOf_inter_eq_sep
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
⊢ (v.filterAt x).HasBasis (fun (x : ℝ) ↦ 0 < x) fun (x_1 : ℝ) ↦ {t : Set X | t ∈ v.setsAt x ∧ t ⊆ closedBall x x_1}

Tactic:
nhds_basis_closedBall.vitaliFamily v

Premises used: Filter.HasBasis.vitaliFamily, Metric.nhds_basis_closedBall
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
s : Set (Set X)
⊢ s ∈ v.filterAt x ↔ ∃ ε > 0, ∀ t ∈ v.setsAt x, t ⊆ closedBall x ε → t ∈ s

Tactic:
simp only [(v.filterAt_basis_closedBall x).mem_iff, ← and_imp, subset_def, mem_setOf]

Premises used: Filter.HasBasis.mem_iff, Set.subset_def, and_imp, VitaliFamily.filterAt_basis_closedBall, Set.mem_setOf
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
⊢ (v.filterAt x).NeBot

Tactic:
(v.filterAt_basis_closedBall x).neBot_iff.2 <| v.nontrivial _ _

Premises used: Iff.mpr, Filter.HasBasis.neBot_iff, VitaliFamily.filterAt_basis_closedBall, VitaliFamily.nontrivial
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
P : Set X → Prop
⊢ (∀ᶠ (t : Set X) in v.filterAt x, P t) ↔ ∃ ε > 0, ∀ t ∈ v.setsAt x, t ⊆ closedBall x ε → P t

Tactic:
v.mem_filterAt_iff

Premises used: Set.Mem, Filter.Eventually, setOf, VitaliFamily.mem_filterAt_iff
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
ι : Type u_2
l : Filter ι
f : ι → Set X
x : X
⊢ Tendsto f l (v.filterAt x) ↔ (∀ᶠ (i : ι) in l, f i ∈ v.setsAt x) ∧ ∀ ε > 0, ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε

Tactic:
simp only [filterAt, tendsto_inf, nhds_basis_closedBall.smallSets.tendsto_right_iff,
    tendsto_principal, and_comm, mem_powerset_iff]

Premises used: Filter.tendsto_inf, Set.mem_powerset_iff, Filter.tendsto_principal, and_comm, Filter.HasBasis.smallSets, Filter.HasBasis.tendsto_right_iff, Metric.nhds_basis_closedBall, VitaliFamily.filterAt
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
⊢ ∀ᶠ (t : Set X) in v.filterAt x, t ∈ v.setsAt x

Tactic:
(v.tendsto_filterAt_iff.mp tendsto_id).1

Premises used: Set.Mem, Filter.tendsto_id, And.left, VitaliFamily.tendsto_filterAt_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (t : Set X) in v.filterAt x, t ⊆ closedBall x ε

Tactic:
(v.tendsto_filterAt_iff.mp tendsto_id).2 ε hε

Premises used: Filter.tendsto_id, And.right, VitaliFamily.tendsto_filterAt_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
a : Set X
ha : a ∈ v.setsAt x
⊢ MeasurableSet a

Tactic:
v.measurableSet _ _ ha

Premises used: VitaliFamily.measurableSet
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
h :
  ∀ (a : Set X),
    Membership.mem (γ := Set (Set X))
      {x_1 : Set X |
        Membership.mem (γ := Set (Set X)) {x_2 : Set X | (fun (t : Set X) ↦ t ∈ v.setsAt x) x_2} x_1 →
          Membership.mem (γ := Set (Set X)) {x : Set X | (fun (t : Set X) ↦ MeasurableSet t) x} x_1}
      a
h₁ h₂ : ∀ (a : Set X) (ha : a ∈ v.setsAt x), MeasurableSet a
⊢ ∀ᶠ (t : Set X) in v.filterAt x, MeasurableSet t

Tactic:
filter_upwards [v.eventually_filterAt_mem_setsAt x] with _ ha using v.measurableSet _ _ ha

Premises used: VitaliFamily.eventually_filterAt_mem_setsAt
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
P : Set X → Prop
⊢ (∃ᶠ (t : Set X) in v.filterAt x, P t) ↔ ∀ ε > 0, ∃ t ∈ v.setsAt x, t ⊆ closedBall x ε ∧ P t

Tactic:
simp only [(v.filterAt_basis_closedBall x).frequently_iff, ← and_assoc, subset_def, mem_setOf]

Premises used: Set.subset_def, VitaliFamily.filterAt_basis_closedBall, Set.mem_setOf, Filter.HasBasis.frequently_iff, and_assoc
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
o : Set X
hx : o ∈ 𝓝 x
⊢ ∀ᶠ (t : Set X) in v.filterAt x, t ⊆ o

Tactic:
(eventually_smallSets_subset.2 hx).filter_mono inf_le_left

Premises used: Iff.mpr, Filter.Eventually.filter_mono, inf_le_left, Filter.eventually_smallSets_subset, VitaliFamily.filterAt
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
h : ∀ (x : X), (v.enlarge δ δpos).filterAt x = v.filterAt x
⊢ (v.enlarge δ δpos).filterAt = v.filterAt

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
this : {t : Set X | MeasurableSet t → (interior t).Nonempty → ¬t ⊆ closedBall x δ → t ∈ v.setsAt x} ∈ (𝓝 x).smallSets
⊢ (v.enlarge δ δpos).filterAt x = v.filterAt x

Tactic:
simpa [VitaliFamily.filterAt, VitaliFamily.enlarge, ← sup_principal, inf_sup_left,
      mem_inf_principal]

Premises used: Filter.sup_principal, inf_sup_left, Filter.mem_inf_principal, VitaliFamily.enlarge, VitaliFamily.filterAt
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
h : {t : Set X | MeasurableSet t → (interior t).Nonempty → ¬t ⊆ closedBall x δ → t ∈ v.setsAt x} ∈ (𝓝 x).smallSets
⊢ (v.enlarge δ δpos).filterAt x = v.filterAt x

Tactic:
suffices {t | MeasurableSet t → (interior t).Nonempty → ¬t ⊆ closedBall x δ →
      t ∈ v.setsAt x} ∈ (𝓝 x).smallSets by
    simpa [VitaliFamily.filterAt, VitaliFamily.enlarge, ← sup_principal, inf_sup_left,
      mem_inf_principal]
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
h : ∀ a ⊆ closedBall x δ, MeasurableSet a → (interior a).Nonempty → ¬a ⊆ closedBall x δ → a ∈ v.setsAt x
⊢ {t : Set X | MeasurableSet t → (interior t).Nonempty → ¬t ⊆ closedBall x δ → t ∈ v.setsAt x} ∈ (𝓝 x).smallSets

Tactic:
filter_upwards [eventually_smallSets_subset.mpr (closedBall_mem_nhds _ δpos)]

Premises used: Iff.mpr, Metric.closedBall_mem_nhds, Filter.eventually_smallSets_subset
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
⊢ ∀ a ⊆ closedBall x δ, MeasurableSet a → (interior a).Nonempty → ¬a ⊆ closedBall x δ → a ∈ v.setsAt x

Tactic:
simp +contextual
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
⊢ v.FineSubfamilyOn f s ↔ ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x

Tactic:
forall₂_congr fun x hx ↦ ?_

Premises used: forall₂_congr, VitaliFamily.FineSubfamilyOn
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
refine :
  ∀ (x : X) (hx : x ∈ s),
    (∀ ε > 0, ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε) ↔ ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x
⊢ v.FineSubfamilyOn f s ↔ ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x

Tactic:
refine forall₂_congr fun x hx ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
x : X
hx : x ∈ s
⊢ (∀ ε > 0, ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε) ↔ ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x

Tactic:
simp [frequently_filterAt_iff, ← and_assoc, and_right_comm]

Premises used: VitaliFamily.frequently_filterAt_iff, and_assoc, and_right_comm
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h rwa rwa₁ rwa₂ rwa₃ : ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x
⊢ v.FineSubfamilyOn f s

Tactic:
rwa [fineSubfamilyOn_iff_frequently]

Premises used: VitaliFamily.fineSubfamilyOn_iff_frequently
-- Module: Mathlib.MeasureTheory.Function.AEEqFun.DomAct
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SMul M α
inst_3 : MeasurableConstSMul M α
inst_4 : SMulInvariantMeasure M α μ
c : Mᵈᵐᵃ
f : α →ₘ[μ] β
⊢ (↑(c • f) : α → β) =ᶠ[ae μ] fun (x : α) ↦
    (↑f : α → β) (HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c : M) x)

Tactic:
f.coeFn_compMeasurePreserving _

Premises used: MeasureTheory.AEEqFun.cast, dite, MeasureTheory.AEEqFun.coeFn_compMeasurePreserving
-- Module: Mathlib.MeasureTheory.Function.AEEqFun.DomAct
Goal:
M : Type u_3
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SMul M α
inst_3 : MeasurableConstSMul M α
inst_4 : SMulInvariantMeasure M α μ
c : M
f : α → β
hf : AEStronglyMeasurable f μ
⊢ HSMul.hSMul (α := Mᵈᵐᵃ) ((mk : (a : M) → Mᵈᵐᵃ) c : Mᵈᵐᵃ) (AEEqFun.mk f hf) = AEEqFun.mk (fun (x : α) ↦ f (c • x)) ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.AEEqFun.compQuasiMeasurePreserving, MulOpposite.unop, rfl, MeasureTheory.AEEqFun.mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun.DomAct
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SMul M α
inst_3 : MeasurableConstSMul M α
inst_4 : SMulInvariantMeasure M α μ
c : Mᵈᵐᵃ
b : β
⊢ HSMul.hSMul (β := α →ₘ[μ] β) c (AEEqFun.const α b) = AEEqFun.const α b

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.AEEqFun.compQuasiMeasurePreserving, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.const
-- Module: Mathlib.MeasureTheory.Function.AEEqFun.DomAct
Goal:
M : Type u_3
N : Type u_1
α : Type u_4
β : Type u_2
inst : MeasurableSpace N
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : TopologicalSpace β
inst_3 : SMul M α
inst_4 : MeasurableConstSMul M α
inst_5 : SMulInvariantMeasure M α μ
inst_6 : SMul N β
inst_7 : ContinuousConstSMul N β
m : Mᵈᵐᵃ
n : N
a : α →ₘ[μ] β
a_1 : { f : α → β // AEStronglyMeasurable f μ }
⊢ m •
      HSMul.hSMul (β := α →ₘ[μ] β) n
        (Quot.mk
          (⇑(Measure.aeEqSetoid β μ) :
            { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
          a_1) =
    n •
      HSMul.hSMul (β := α →ₘ[μ] β) m
        (Quot.mk
          (⇑(Measure.aeEqSetoid β μ) :
            { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
          a_1)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.AEEqFun.DomAct
Goal:
M : Type u_3
N : Type u_1
α : Type u_4
β : Type u_2
inst : MeasurableSpace N
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : TopologicalSpace β
inst_3 : SMul M α
inst_4 : MeasurableConstSMul M α
inst_5 : SMulInvariantMeasure M α μ
inst_6 : SMul N β
inst_7 : ContinuousConstSMul N β
⊢ SMulCommClass N Mᵈᵐᵃ (α →ₘ[μ] β)

Tactic:
.symm _ _ _

Premises used: SMulCommClass.symm