awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hts : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
suffices :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))
⊢ |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)| ≤
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t))

Tactic:
suffices (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal by
    rw [this, measure_symmDiff_eq hs ht, ENNReal.toReal_add hst hts]
    convert! abs_sub (μ (s \ t)).toReal (μ (t \ s)).toReal <;> simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hts : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hts : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hts : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) -
      (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s))
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))

Tactic:
rw [measure_diff' s ht ht', measure_diff' t hs hs',
    ENNReal.toReal_sub_of_le measure_le_measure_union_right (by finiteness),
    ENNReal.toReal_sub_of_le measure_le_measure_union_right (by finiteness),
    union_comm t s]

Premises used: Set.union_comm, ENNReal.toReal_sub_of_le, MeasureTheory.measure_diff', MeasureTheory.measure_le_measure_union_right
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hts : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) -
      (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s))

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s_1 t : Set α
s : Finset ι
μ : ι → Measure α
inst : ∀ (i : ι), IsFiniteMeasure (μ i)
⊢ LT.lt (α := ℝ≥0∞) (((∑ i ∈ s, μ i : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [measure_lt_top]

Premises used: MeasureTheory.measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
inst : Finite ι
μ : ι → Measure α
inst_1 : ∀ (i : ι), IsFiniteMeasure (μ i)
intro : ∀ (val : Fintype ι), LT.lt (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
inst : Finite ι
μ : ι → Measure α
inst_1 : ∀ (i : ι), IsFiniteMeasure (μ i)
val : Fintype ι
⊢ LT.lt (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [measure_lt_top]

Premises used: MeasureTheory.measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ sᶜ
⊢ Membership.mem (γ := Set α) {a : α | (if a ∈ s then f a else g a) = g a} x

Tactic:
simp [(Set.mem_compl_iff _ _).mp hx]

Premises used: Iff.mp, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ sᶜ ⊆ {a : α | (if a ∈ s then f a else g a) = g a}

Tactic:
have h_ss : sᶜ ⊆ { a : α | ite (a ∈ s) (f a) (g a) = g a } := fun x hx => by
    simp [(Set.mem_compl_iff _ _).mp hx]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_ss : sᶜ ⊆ {a : α | (if a ∈ s then f a else g a) = g a}
⊢ (fun (x : α) ↦ if x ∈ s then f x else g x) =ᶠ[ae μ] g

Tactic:
measure_mono_null ?_ hs_zero

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_ss : sᶜ ⊆ {a : α | (if a ∈ s then f a else g a) = g a}
refine : {x : α | (fun (x : α) ↦ (fun (x : α) ↦ if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ s
⊢ (fun (x : α) ↦ if x ∈ s then f x else g x) =ᶠ[ae μ] g

Tactic:
refine measure_mono_null ?_ hs_zero

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_ss : sᶜ ⊆ {a : α | (if a ∈ s then f a else g a) = g a}
rw : sᶜᶜ
| s

Tactic:
rw [← compl_compl s]

Premises used: compl_compl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_ss : sᶜ ⊆ {a : α | (if a ∈ s then f a else g a) = g a}
conv_rhs : {x : α | (fun (x : α) ↦ (fun (x : α) ↦ if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ sᶜᶜ
⊢ {x : α | (fun (x : α) ↦ (fun (x : α) ↦ if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ s

Tactic:
conv_rhs => rw [← compl_compl s]

Premises used: compl_compl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_ss : sᶜ ⊆ {a : α | (if a ∈ s then f a else g a) = g a}
rwa rwa₁ rwa₂ rwa₃ : sᶜ ⊆ {x : α | (fun (x : α) ↦ (fun (x : α) ↦ if x ∈ s then f x else g x) x = g x) x}
⊢ {x : α | (fun (x : α) ↦ (fun (x : α) ↦ if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ sᶜᶜ

Tactic:
rwa [Set.compl_subset_compl]

Premises used: Set.compl_subset_compl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s ∈ ae μ

Tactic:
rw [← mem_ae_iff] at hs_zero

Premises used: MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hs_zero : s ∈ ae μ
h : ∀ a ∈ s, (if a ∈ s then f a else g a) = f a
⊢ (fun (x : α) ↦ if x ∈ s then f x else g x) =ᶠ[ae μ] f

Tactic:
filter_upwards [hs_zero]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hs_zero : s ∈ ae μ
a : α
h_1 : a ∈ s
h : f a = f a
⊢ (if a ∈ s then f a else g a) = f a

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hs_zero : s ∈ ae μ
a : α
h : a ∈ s
⊢ f a = f a

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
_m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : Filter α
⊢ μ.FiniteAtFilter f

Tactic:
⟨univ, univ_mem, measure_lt_top μ univ⟩

Premises used: MeasureTheory.measure_lt_top, Set.univ, MeasureTheory.Measure.FiniteAtFilter, And.intro, Exists.intro, Filter.univ_mem
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
hμ : μ.FiniteAtFilter f
p : ι → Prop
s : ι → Set α
hf : f.HasBasis p s
⊢ ∃ (i : ι), p i ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(hf.exists_iff fun {_s _t} hst ht => (measure_mono hst).trans_lt ht).1 hμ

Premises used: Filter.HasBasis.exists_iff, MeasureTheory.measure_mono, Iff.mp, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [measure_empty, zero_lt_top]

Premises used: ENNReal.zero_lt_top, MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
⊢ IsLocallyFiniteMeasure μ

Tactic:
⟨fun _ => finiteAtFilter_of_finite _ _⟩

Premises used: nhds, MeasureTheory.IsLocallyFiniteMeasure.mk, MeasureTheory.Measure.finiteAtFilter_of_finite
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
x : α
⊢ μ.FiniteAtFilter (𝓝 x)

Tactic:
IsLocallyFiniteMeasure.finiteAtNhds x

Premises used: MeasureTheory.IsLocallyFiniteMeasure.finiteAtNhds
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
c : ℝ≥0∞
hc : c ≠ ∞
⊢ c ≠ ∞

Tactic:
hc
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
c : ℝ≥0∞
hc : c ≠ ∞
lift : ∀ (c : ℝ≥0), IsFiniteMeasure ((↑c : ℝ≥0∞) • μ)
⊢ IsFiniteMeasure (c • μ)

Tactic:
lift c to ℝ≥0 using hc
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
c : ℝ≥0
⊢ IsFiniteMeasure ((↑c : ℝ≥0∞) • μ)

Tactic:
MeasureTheory.isFiniteMeasureSMulNNReal

Premises used: MeasureTheory.isFiniteMeasureSMulNNReal
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
c : ℝ≥0
⊢ IsFiniteMeasure ((↑c : ℝ≥0∞) • μ)

Tactic:
exact MeasureTheory.isFiniteMeasureSMulNNReal

Premises used: MeasureTheory.isFiniteMeasureSMulNNReal
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
x : α
⊢ ∃ (s : Set α), x ∈ s ∧ IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa only [and_assoc] using (μ.finiteAt_nhds x).exists_mem_basis (nhds_basis_opens x)

Premises used: MeasureTheory.Measure.finiteAt_nhds, and_assoc, nhds_basis_opens, MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
c : ℝ≥0
⊢ IsLocallyFiniteMeasure (c • μ)

Tactic:
⟨fun x => ?_⟩

Premises used: MeasureTheory.IsLocallyFiniteMeasure.mk
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
c : ℝ≥0
refine : ∀ (x : α), (c • μ).FiniteAtFilter (𝓝 x)
⊢ IsLocallyFiniteMeasure (c • μ)

Tactic:
refine ⟨fun x => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
c : ℝ≥0
x : α
rcases :
  ∀ (o : Set α) (xo : x ∈ o) (o_open : IsOpen[inst] o)
    (μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)), (c • μ).FiniteAtFilter (𝓝 x)
⊢ (c • μ).FiniteAtFilter (𝓝 x)

Tactic:
rcases μ.exists_isOpen_measure_lt_top x with ⟨o, xo, o_open, μo⟩

Premises used: MeasureTheory.Measure.exists_isOpen_measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
c : ℝ≥0
x : α
o : Set α
xo : x ∈ o
o_open : IsOpen[inst] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (c • μ).FiniteAtFilter (𝓝 x)

Tactic:
⟨o, o_open.mem_nhds xo, ?_⟩

Premises used: MeasureTheory.Measure.FiniteAtFilter, And.intro, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
c : ℝ≥0
x : α
o : Set α
xo : x ∈ o
o_open : IsOpen[inst] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : LT.lt (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (c • μ).FiniteAtFilter (𝓝 x)

Tactic:
refine ⟨o, o_open.mem_nhds xo, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
c : ℝ≥0
x : α
o : Set α
xo : x ∈ o
o_open : IsOpen[inst] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
apply : (↑c : ℝ≥0∞) < ∞
⊢ LT.lt (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply ENNReal.mul_lt_top _ μo

Premises used: ENNReal.mul_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
c : ℝ≥0
x : α
o : Set α
xo : x ∈ o
o_open : IsOpen[inst] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑c : ℝ≥0∞) < ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
⊢ TopologicalSpace.IsTopologicalBasis.{u_1} (α := α)
    {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}

Tactic:
TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds (fun s hs => hs.1) ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds, And.left
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
refine :
  ∀ (a : α) (u : Set α),
    a ∈ u →
      IsOpen[inst] u →
        ∃ (v : Set α),
          Membership.mem (γ := Set (Set α))
              {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)} v ∧
            a ∈ v ∧ v ⊆ u
⊢ TopologicalSpace.IsTopologicalBasis.{u_1} (α := α)
    {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}

Tactic:
refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds (fun s hs => hs.1) ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen[inst] s
rcases :
  ∀ (v : Set α) (xv : x ∈ v) (hv : IsOpen[inst] v)
    (μv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∃ (v : Set α),
      Membership.mem (γ := Set (Set α))
          {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)} v ∧
        x ∈ v ∧ v ⊆ s
⊢ ∃ (v : Set α),
    Membership.mem (γ := Set (Set α))
        {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)} v ∧
      x ∈ v ∧ v ⊆ s

Tactic:
rcases μ.exists_isOpen_measure_lt_top x with ⟨v, xv, hv, μv⟩

Premises used: MeasureTheory.Measure.exists_isOpen_measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen[inst] s
v : Set α
xv : x ∈ v
hv : IsOpen[inst] v
μv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (v : Set α),
    Membership.mem (γ := Set (Set α))
        {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)} v ∧
      x ∈ v ∧ v ⊆ s

Tactic:
⟨v ∩ s, ⟨hv.inter hs, lt_of_le_of_lt ?_ μv⟩, ⟨xv, xs⟩, inter_subset_right⟩

Premises used: lt_of_le_of_lt, Inter.inter, And.intro, IsOpen.inter, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen[inst] s
v : Set α
xv : x ∈ v
hv : IsOpen[inst] v
μv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (v ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞)
⊢ ∃ (v : Set α),
    Membership.mem (γ := Set (Set α))
        {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)} v ∧
      x ∈ v ∧ v ⊆ s

Tactic:
refine ⟨v ∩ s, ⟨hv.inter hs, lt_of_le_of_lt ?_ μv⟩, ⟨xv, xs⟩, inter_subset_right⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen[inst] s
v : Set α
xv : x ∈ v
hv : IsOpen[inst] v
μv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (v ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞)

Tactic:
measure_mono inter_subset_left

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen[inst] s
v : Set α
xv : x ∈ v
hv : IsOpen[inst] v
μv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (v ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞)

Tactic:
exact measure_mono inter_subset_left

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
inst : TopologicalSpace α
μ : Measure α
hμ : IsLocallyFiniteMeasure μ
x : α
obtain :
  ∀ (t : Set α) (ht : t ∈ 𝓝 x) (hmus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (μ.restrict s).FiniteAtFilter (𝓝 x)
⊢ (μ.restrict s).FiniteAtFilter (𝓝 x)

Tactic:
obtain ⟨t, ht, hmus⟩ := hμ.finiteAtNhds x

Premises used: MeasureTheory.IsLocallyFiniteMeasure.finiteAtNhds
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t_1 : Set α
inst : TopologicalSpace α
μ : Measure α
hμ : IsLocallyFiniteMeasure μ
x : α
t : Set α
ht : t ∈ 𝓝 x
hmus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ.restrict s).FiniteAtFilter (𝓝 x)

Tactic:
⟨t, ht, lt_of_le_of_lt (restrict_apply_le s t) hmus⟩

Premises used: lt_of_le_of_lt, MeasureTheory.Measure.restrict_apply_le, MeasureTheory.Measure.FiniteAtFilter, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t_1 : Set α
inst : TopologicalSpace α
μ : Measure α
hμ : IsLocallyFiniteMeasure μ
x : α
t : Set α
ht : t ∈ 𝓝 x
hmus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ.restrict s).FiniteAtFilter (𝓝 x)

Tactic:
exact ⟨t, ht, lt_of_le_of_lt (restrict_apply_le s t) hmus⟩