awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
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∞)
⊢ |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)| ≤
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t))
have hst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hst : μ (s \ t) ≠ ∞ := (measure_lt_top_of_subset diff_subset hs').ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
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∞)
⊢ |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)| ≤
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t))
have hts : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hts : μ (t \ s) ≠ ∞ := (measure_lt_top_of_subset diff_subset ht').ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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∞)
this :
  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))
have rw : |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))| ≤
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))
Tactic: rw [this, measure_symmDiff_eq hs ht, ENNReal.toReal_add hst hts]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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∞)
this :
  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 \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))| ≤
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))
have h : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) = |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t))|
Tactic: convert! abs_sub (μ (s \ t)).toReal (μ (t \ s)).toReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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∞)
this :
  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))
h : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) = |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t))|
⊢ |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) - ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))| ≤
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))
have h₁ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s)) = |ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))|
Tactic: convert! abs_sub (μ (s \ t)).toReal (μ (t \ s)).toReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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))
have 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))
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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 \ s))
have 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))
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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)
⊢ LT.lt (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have intro : ∀ (val : Fintype ι), LT.lt (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
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∞)
⊢ (fun (x : α) ↦ if x ∈ s then f x else g x) =ᶠ[ae μ] g
have h_ss : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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
have refine : {x : α | (fun (x : α) ↦ (fun (x : α) ↦ if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ s
Tactic: refine measure_mono_null ?_ hs_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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}
| s
have rw : sᶜᶜ
Tactic: rw [← compl_compl s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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}
⊢ {x : α | (fun (x : α) ↦ (fun (x : α) ↦ if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ s
have conv_rhs : {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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
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∞)
⊢ (fun (x : α) ↦ if x ∈ s then f x else g x) =ᶠ[ae μ] f
have hs_zero₁ : s ∈ ae μ
Tactic: rw [← mem_ae_iff] at hs_zero
Cleared hypotheses: hs_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hs_zero : s ∈ ae μ
⊢ (fun (x : α) ↦ if x ∈ s then f x else g x) =ᶠ[ae μ] f
have h : ∀ a ∈ s, (if a ∈ s then f a else g a) = f a
Tactic: filter_upwards [hs_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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
⊢ (if a ∈ s then f a else g a) = f a
have h : f a = f a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
c : ℝ≥0∞
hc : c ≠ ∞
⊢ IsFiniteMeasure (c • μ)
have lift : ∀ (c : ℝ≥0), IsFiniteMeasure ((↑c : ℝ≥0∞) • μ)
Tactic: lift c to ℝ≥0 using hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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 • μ)
have refine : ∀ (x : α), (c • μ).FiniteAtFilter (𝓝 x)
Tactic: refine ⟨fun x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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 : α
⊢ (c • μ).FiniteAtFilter (𝓝 x)
have rcases : ∀ (o : Set α) (xo : x ∈ o) (o_open : IsOpen[inst] o)
  (μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)), (c • μ).FiniteAtFilter (𝓝 x)
Tactic: rcases μ.exists_isOpen_measure_lt_top x with ⟨o, xo, o_open, μo⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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)
have refine : LT.lt (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨o, o_open.mem_nhds xo, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
have apply : (↑c : ℝ≥0∞) < ∞
Tactic: apply ENNReal.mul_lt_top _ μo
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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∞)}
have 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
Tactic: refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds (fun s hs => hs.1) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen[inst] 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
have 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
Tactic: rcases μ.exists_isOpen_measure_lt_top x with ⟨v, xv, hv, μv⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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
have refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (v ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞)
Tactic: refine ⟨v ∩ s, ⟨hv.inter hs, lt_of_le_of_lt ?_ μv⟩, ⟨xv, xs⟩, inter_subset_right⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
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 : α
⊢ (μ.restrict s).FiniteAtFilter (𝓝 x)
have obtain : ∀ (t : Set α) (ht : t ∈ 𝓝 x) (hmus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  (μ.restrict s).FiniteAtFilter (𝓝 x)
Tactic: obtain ⟨t, ht, hmus⟩ := hμ.finiteAtNhds x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
μ : Measure β
inst_2 : IsFiniteMeasureOnCompacts μ
f : α → β
f_cont : Continuous[inst, inst_1] f
f_me : MeasurableEmbedding f
K : Set α
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' K) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [f_me.comap_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
U : ι → Set α
hU : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), U i) univ
hμ : μ ≠ 0
⊢ ∃ (i : ι), LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U i) : ℝ≥0∞)
have contrapose! : ∀ (H : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U i) : ℝ≥0∞) (0 : ℝ≥0∞)), μ = 0
Tactic: contrapose! hμ with H
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
U : ι → Set α
hU : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), U i) univ
H : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ = 0
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), U i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← measure_univ_eq_zero, ← hU]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
δ : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace δ
f : α → δ
x : δ
hμ : μ ≠ 0
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f ⁻¹' Metric.ball x (↑i : ℝ)) univ
have rw : f ⁻¹' ⋃ (i : ℕ), Metric.ball x (↑i : ℝ) = univ
Tactic: rw [← preimage_iUnion, Metric.iUnion_ball_nat, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
δ : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace δ
f : α → δ
x : δ
hμ : μ ≠ 0
rw : f ⁻¹' ⋃ (i : ℕ), Metric.ball x (↑i : ℝ) = univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f ⁻¹' Metric.ball x (↑i : ℝ)) univ
have rw₁ : f ⁻¹' univ = univ
Tactic: rw [← preimage_iUnion, Metric.iUnion_ball_nat, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
δ : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace δ
f : α → δ
x : δ
hμ : μ ≠ 0
rw : f ⁻¹' ⋃ (i : ℕ), Metric.ball x (↑i : ℝ) = univ
rw₁ : f ⁻¹' univ = univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f ⁻¹' Metric.ball x (↑i : ℝ)) univ
have rw₂ : Eq.{u_1 + 1} (α := Set α) univ univ
Tactic: rw [← preimage_iUnion, Metric.iUnion_ball_nat, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
h : ∀ (b : β), ∃ᵐ (x : α) ∂μ, f x ≠ b
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
⊢ ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
have h₁ : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: replace h : ∀ b : β, m {b}ᶜ ≠ 0 := fun b => not_eventually.mpr (h b)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
have inhabit : ∀ (inhabited_h : Inhabited β),
  ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
Tactic: inhabit β
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabited_h : Inhabited β
⊢ ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
have this : Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have : m univ ≠ 0 := ne_bot_of_le_ne_bot (h default) (measure_mono <| subset_univ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabited_h : Inhabited β
this : Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
have rcases : ∀ (b : β) (hb : ∀ t ∈ 𝓝[univ] b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)),
  ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
Tactic: rcases exists_mem_forall_mem_nhdsWithin_pos_measure this with ⟨b, -, hb⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabited_h : Inhabited β
this : Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
b : β
hb : ∀ t ∈ 𝓝[univ] b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
have hb₁ : ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp only [nhdsWithin_univ] at hb
Cleared hypotheses: hb