awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty.{u_1} (α := Measure α) {d : Measure α | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ (μ : (a : Set α) → ENNReal) (t ∩ s) ≤
    HAdd.hAdd (β := ENNReal)
      (HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν' : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
        ((ν : (a : Set α) → ENNReal) (t ∩ s) : ENNReal))
      (((restrict ⊤ sᶜ : Measure α) : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
have apply : (μ : (a : Set α) → ENNReal) (t ∩ s) ≤
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν' : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
    ((ν : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
Tactic: apply le_add_right _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty.{u_1} (α := Measure α) {d : Measure α | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ (μ : (a : Set α) → ENNReal) (t ∩ s) ≤
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν' : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
      ((ν : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
have rw : (μ.restrict s : (a : Set α) → ENNReal) (t ∩ s) ≤
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν' : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
    ((ν.restrict s : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
Tactic: rw [← restrict_eq_self μ inter_subset_right,
          ← restrict_eq_self ν inter_subset_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty.{u_1} (α := Measure α) {d : Measure α | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t \ s) : ENNReal)
    ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) (t \ s) : ENNReal)
have a : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ sᶜ) : ENNReal)
  ((ν' + ν + ⊤ : (a : Set α) → ENNReal) (t ∩ sᶜ) : ENNReal)
Tactic: rw [add_apply, restrict_apply (h_meas_t.diff h_meas_s), diff_eq, inter_assoc, inter_self,
          ← add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty.{u_1} (α := Measure α) {d : Measure α | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ sᶜ) : ENNReal)
    ((ν' + ν + ⊤ : (a : Set α) → ENNReal) (t ∩ sᶜ) : ENNReal)
have h_mu_le_add_top : μ ≤ ν' + ν + ⊤
Tactic: have h_mu_le_add_top : μ ≤ ν' + ν + ⊤ := by simp only [add_top, le_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty.{u_1} (α := Measure α) {d : Measure α | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
⊢ (fun (μ : Measure α) ↦ μ.restrict s) (ν' + restrict ⊤ sᶜ) = ν'.restrict s
have a : ∀ (t : Set α) (h_meas_t : MeasurableSet t),
  Eq (α := ENNReal)
    ((((fun (μ : Measure α) ↦ μ.restrict s) (ν' + restrict ⊤ sᶜ) : Measure α) : (a : Set α) → ENNReal) t : ENNReal)
    ((ν'.restrict s : (a : Set α) → ENNReal) t : ENNReal)
Tactic: ext1 t h_meas_t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty.{u_1} (α := Measure α) {d : Measure α | μ ≤ d + ν}
⊢ LE.le.{u_1} (α := Measure α) (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
    (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
have a : IsCoinitialFor.{u_1} (α := Measure α) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν})
  {d : Measure α | μ.restrict s ≤ d + ν.restrict s}
Tactic: refine sInf_le_sInf_of_isCoinitialFor ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty.{u_1} (α := Measure α) {d : Measure α | μ ≤ d + ν}
⊢ IsCoinitialFor.{u_1} (α := Measure α) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν})
    {d : Measure α | μ.restrict s ≤ d + ν.restrict s}
have a : ∀ (t : Measure α) (h_t_in : Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} t),
  Membership.mem (γ := Set (Measure α)) {d : Measure α | μ.restrict s ≤ d + ν.restrict s} (t.restrict s)
Tactic: refine forall_mem_image.2 fun t h_t_in => ⟨t.restrict s, ?_, le_rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty.{u_1} (α := Measure α) {d : Measure α | μ ≤ d + ν}
t : Measure α
h_t_in : Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} t
⊢ Membership.mem (γ := Set (Measure α)) {d : Measure α | μ.restrict s ≤ d + ν.restrict s} (t.restrict s)
have a : μ.restrict s ≤ (t + ν).restrict s
Tactic: rw [Set.mem_setOf_eq, ← restrict_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_le : μ.restrict s ≤ ν.restrict s
h_meas_s : MeasurableSet s
⊢ Eq (α := ENNReal) ((μ - ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
have rw : Eq (α := ENNReal) (((0 : Measure α) : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
Tactic: rw [← restrict_apply_self, restrict_sub_eq_restrict_sub_restrict, sub_eq_zero_of_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure ν
h_le : ν ≤ μ
⊢ μ - ν ≤ ξ ↔ μ ≤ ξ + ν
have refine : ∀ (h : μ - ν ≤ ξ), μ ≤ ξ + ν
Tactic: refine ⟨fun h ↦ ?_, Measure.sub_le_of_le_add⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ μ - ν ≤ ξ ↔ μ ≤ ξ + ν
have refine : ∀ (h : μ - ν ≤ ξ), μ ≤ ξ + ν
Tactic: refine ⟨fun h ↦ ?_, sub_le_of_le_add⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ - ν ≤ ξ
⊢ μ ≤ ξ + ν
have obtain : ∀ (s : Set α) (hs : IsHahnDecomposition μ ν s), μ ≤ ξ + ν
Tactic: obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ - ν ≤ ξ
s : Set α
hs : IsHahnDecomposition μ ν s
⊢ μ ≤ ξ + ν
have h_le_s : μ.restrict s ≤ ξ.restrict s + ν.restrict s
Tactic: have h_le_s : μ.restrict s ≤ ξ.restrict s + ν.restrict s :=
    hs.le_on.trans (Measure.le_add_left le_rfl)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ - ν ≤ ξ
s : Set α
hs : IsHahnDecomposition μ ν s
h_le_s : μ.restrict s ≤ ξ.restrict s + ν.restrict s
⊢ μ.restrict sᶜ ≤ ξ.restrict sᶜ + ν.restrict sᶜ
have refine : μ.restrict sᶜ - ν.restrict sᶜ ≤ ξ.restrict sᶜ
Tactic: refine (sub_le_iff_le_add_of_le hs.ge_on_compl).mp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ - ν ≤ ξ
s : Set α
hs : IsHahnDecomposition μ ν s
h_le_s : μ.restrict s ≤ ξ.restrict s + ν.restrict s
⊢ μ.restrict sᶜ - ν.restrict sᶜ ≤ ξ.restrict sᶜ
have rw : (μ - ν).restrict sᶜ ≤ ξ.restrict sᶜ
Tactic: rw [← restrict_sub_eq_restrict_sub_restrict hs.measurableSet.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ - ν ≤ ξ
s : Set α
hs : IsHahnDecomposition μ ν s
h_le_s : μ.restrict s ≤ ξ.restrict s + ν.restrict s
⊢ μ ≤ ξ + ν
have h_le_s_compl : μ.restrict sᶜ ≤ ξ.restrict sᶜ + ν.restrict sᶜ
Tactic: have h_le_s_compl : μ.restrict sᶜ ≤ ξ.restrict sᶜ + ν.restrict sᶜ := by
    refine (sub_le_iff_le_add_of_le hs.ge_on_compl).mp ?_
    rw [← restrict_sub_eq_restrict_sub_restrict hs.measurableSet.compl]
    exact restrict_mono subset_rfl h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ - ν ≤ ξ
s : Set α
hs : IsHahnDecomposition μ ν s
h_le_s : μ.restrict s ≤ ξ.restrict s + ν.restrict s
h_le_s_compl : μ.restrict sᶜ ≤ ξ.restrict sᶜ + ν.restrict sᶜ
⊢ μ ≤ ξ + ν
have rw : μ.restrict s + μ.restrict sᶜ ≤ ξ.restrict s + ξ.restrict sᶜ + (ν.restrict s + ν.restrict sᶜ)
Tactic: rw [← restrict_add_restrict_compl (μ := μ) hs.measurableSet,
    ← restrict_add_restrict_compl (μ := ξ) hs.measurableSet,
    ← restrict_add_restrict_compl (μ := ν) hs.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ - ν ≤ ξ
s : Set α
hs : IsHahnDecomposition μ ν s
h_le_s : μ.restrict s ≤ ξ.restrict s + ν.restrict s
h_le_s_compl : μ.restrict sᶜ ≤ ξ.restrict sᶜ + ν.restrict sᶜ
⊢ μ.restrict s + μ.restrict sᶜ ≤ ξ.restrict s + ξ.restrict sᶜ + (ν.restrict s + ν.restrict sᶜ)
have suffices : μ.restrict s + μ.restrict sᶜ ≤ ξ.restrict s + ν.restrict s + (ξ.restrict sᶜ + ν.restrict sᶜ)
Tactic: suffices μ.restrict s + μ.restrict sᶜ ≤
    ξ.restrict s + ν.restrict s + (ξ.restrict sᶜ + ν.restrict sᶜ) from this.trans_eq (by abel)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hg : Measurable g
hgf : g ≤ᶠ[ae μ] f
⊢ μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity (f - g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity f - μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hg : Measurable g
hgf : g ≤ᶠ[ae μ] f
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (f - g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity f - μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (a : α) in s, (f - g) a ∂μ = ∫⁻ (a : α) in s, f a - g a ∂μ
Tactic: rw [sub_apply hs (withDensity_mono hgf), withDensity_apply _ hs, withDensity_apply _ hs,
    withDensity_apply _ hs, ← lintegral_sub hg _ (ae_restrict_of_ae hgf)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hg : Measurable g
hgf : g ≤ᶠ[ae μ] f
s : Set α
hs : MeasurableSet s
h : ∫⁻ (a : α) in s, (f - g) a ∂μ = ∫⁻ (a : α) in s, f a - g a ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (f - g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity f - μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
Tactic: rw [sub_apply hs (withDensity_mono hgf), withDensity_apply _ hs, withDensity_apply _ hs,
    withDensity_apply _ hs, ← lintegral_sub hg _ (ae_restrict_of_ae hgf)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g
have refine_1 : μ.withDensity (f - g) ≤ μ.withDensity f - μ.withDensity g
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
refine_1 : μ.withDensity (f - g) ≤ μ.withDensity f - μ.withDensity g
⊢ μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g
have refine_2 : μ.withDensity f - μ.withDensity g ≤ μ.withDensity (f - g)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
⊢ μ.withDensity (f - g) ≤ μ.withDensity f - μ.withDensity g
have ht : MeasurableSet t
Tactic: have ht : MeasurableSet t := measurableSet_le hf hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
⊢ μ.withDensity (f - g) ≤ μ.withDensity f - μ.withDensity g
have refine_1 : (μ.withDensity (f - g)).restrict t + (μ.withDensity (f - g)).restrict tᶜ ≤
  (μ.withDensity f - μ.withDensity g).restrict t + (μ.withDensity f - μ.withDensity g).restrict tᶜ
Tactic: rw [← restrict_add_restrict_compl (μ := μ.withDensity (f - g)) ht,
      ← restrict_add_restrict_compl (μ := μ.withDensity f - μ.withDensity g) ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
⊢ (μ.withDensity (f - g)).restrict t = 0
have simp : Eq (α := ℝ≥0∞) ((μ.withDensity (f - g) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [restrict_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (f - g) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : f - g =ᶠ[ae (μ.restrict t)] 0
Tactic: rw [withDensity_apply _ ht, lintegral_eq_zero_iff (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
⊢ f - g =ᶠ[ae (μ.restrict t)] 0
have refine : ∀ (x : α) (hx : x ∈ t), (f - g) x = 0 x
Tactic: refine ae_restrict_of_forall_mem ht fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
⊢ (μ.withDensity (f - g)).restrict t + (μ.withDensity (f - g)).restrict tᶜ ≤
    (μ.withDensity f - μ.withDensity g).restrict t + (μ.withDensity f - μ.withDensity g).restrict tᶜ
have h_zero : (μ.withDensity (f - g)).restrict t = 0
Tactic: have h_zero : (μ.withDensity (f - g)).restrict t = 0 := by
      simp only [restrict_eq_zero]
      rw [withDensity_apply _ ht, lintegral_eq_zero_iff (by fun_prop)]
      refine ae_restrict_of_forall_mem ht fun x hx ↦ ?_
      simpa [tsub_eq_zero_iff_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ (μ.withDensity (f - g)).restrict t + (μ.withDensity (f - g)).restrict tᶜ ≤
    (μ.withDensity f - μ.withDensity g).restrict t + (μ.withDensity f - μ.withDensity g).restrict tᶜ
have refine_1 : (μ.withDensity (f - g)).restrict tᶜ ≤
  (μ.withDensity f - μ.withDensity g).restrict t + (μ.withDensity f - μ.withDensity g).restrict tᶜ
Tactic: rw [h_zero, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ (μ.withDensity (f - g)).restrict tᶜ ≤
    (μ.withDensity f - μ.withDensity g).restrict t + (μ.withDensity f - μ.withDensity g).restrict tᶜ
have refine_1 : (μ.withDensity (f - g)).restrict tᶜ ≤ (μ.withDensity f - μ.withDensity g).restrict tᶜ
Tactic: suffices (μ.withDensity (f - g)).restrict tᶜ ≤
      (μ.withDensity f - μ.withDensity g).restrict tᶜ from this.trans (Measure.le_add_left le_rfl)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ (μ.withDensity (f - g)).restrict tᶜ ≤ (μ.withDensity f - μ.withDensity g).restrict tᶜ
have refine_1 : (μ.withDensity (f - g)).restrict tᶜ ≤ (μ.withDensity f).restrict tᶜ - (μ.withDensity g).restrict tᶜ
Tactic: rw [restrict_sub_eq_restrict_sub_restrict ht.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ (μ.withDensity (f - g)).restrict tᶜ ≤ (μ.withDensity f).restrict tᶜ - (μ.withDensity g).restrict tᶜ
have refine_1 : (μ.restrict tᶜ).withDensity (f - g) ≤ (μ.restrict tᶜ).withDensity f - (μ.restrict tᶜ).withDensity g
Tactic: simp_rw [restrict_withDensity ht.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
have rw : IsFiniteMeasure ((μ.withDensity g).restrict tᶜ)
Tactic: rw [← restrict_withDensity ht.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
⊢ (μ.restrict tᶜ).withDensity (f - g) ≤ (μ.restrict tᶜ).withDensity f - (μ.restrict tᶜ).withDensity g
have this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
Tactic: have : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g) := by
      rw [← restrict_withDensity ht.compl]
      infer_instance
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
⊢ (μ.restrict tᶜ).withDensity (f - g) ≤ (μ.restrict tᶜ).withDensity f - (μ.restrict tᶜ).withDensity g
have refine_1 : g ≤ᶠ[ae (μ.restrict tᶜ)] f
Tactic: rw [withDensity_sub_of_le hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
⊢ g ≤ᶠ[ae (μ.restrict tᶜ)] f
have refine_1 : ∀ (x : α) (hx : x ∈ tᶜ), g x ≤ f x
Tactic: refine ae_restrict_of_forall_mem ht.compl fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x : α | f x ≤ g x}
ht : MeasurableSet t
h_zero : (μ.withDensity (f - g)).restrict t = 0
this : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g)
x : α
hx : x ∈ tᶜ
⊢ g x ≤ f x
have hx₁ : g x < f x
Tactic: simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le, t] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity f - μ.withDensity g ≤ μ.withDensity (f - g)
have refine_2 : μ.withDensity f ≤ μ.withDensity (f - g) + μ.withDensity g
Tactic: refine sub_le_of_le_add ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SubFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity f ≤ μ.withDensity (f - g) + μ.withDensity g
have refine_2 : μ.withDensity f ≤ μ.withDensity (f - g + g)
Tactic: rw [← withDensity_add_right _ hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ ν : Measure X
⊢ (μ + ν).support = μ.support ∪ ν.support
have h : ∀ (x : X), x ∈ (μ + ν).support ↔ x ∈ μ.support ∪ ν.support
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
⊢ IsClosed[inst] μ.support
have simp_rw : ∀ (x : X),
  (∀ (i : Set X),
      x ∈ i ∧ IsOpen[inst] i →
        ∃ x ∈ i,
          ∀ (i : Set X),
            x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) i : ENNReal)) →
    ∀ (i : Set X), x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) i : ENNReal)
Tactic: simp_rw [isClosed_iff_frequently, nhds_basis_opens _ |>.mem_measureSupport,
    nhds_basis_opens _ |>.frequently_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
⊢ μ.supportᶜ =
    ⋃₀ {t : Set X | IsOpen[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) t : ENNReal) (0 : ENNReal)}
have h : ∀ (x : X),
  x ∈ μ.supportᶜ ↔
    Membership.mem (γ := Set X)
      (⋃₀ {t : Set X | IsOpen[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) t : ENNReal) (0 : ENNReal)}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
⊢ μ.support =
    ⋂₀ {t : Set X | IsClosed[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) tᶜ : ENNReal) (0 : ENNReal)}
have h : μ.support = μ.supportᶜᶜ
Tactic: convert! congr($(compl_support_eq_sUnion (μ := μ))ᶜ)