awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (t \ s) : ENNReal) ≤
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
      ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) (t \ s) : ENNReal)

Tactic:
add_le_add ?_ ?_

Premises used: add_le_add
-- Module: Mathlib.MeasureTheory.Measure.Sub
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 :
  LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
    ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
a₁ :
  LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t \ s) : ENNReal)
    ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) (t \ s) : ENNReal)
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (t \ s) : ENNReal) ≤
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
      ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) (t \ s) : ENNReal)

Tactic:
refine add_le_add ?_ ?_

Premises used: add_le_add
-- Module: Mathlib.MeasureTheory.Measure.Sub
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 :
  (μ : (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)
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
    ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)

Tactic:
rw [add_apply, add_apply]

Premises used: MeasureTheory.Measure.add_apply
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
apply :
  (μ : (a : Set α) → ENNReal) (t ∩ s) ≤
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν' : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
      ((ν : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
⊢ (μ : (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)

Tactic:
apply le_add_right _

Premises used: le_add_right
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
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)
⊢ (μ : (a : Set α) → ENNReal) (t ∩ s) ≤
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν' : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
      ((ν : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)

Tactic:
rw [← restrict_eq_self μ inter_subset_right,
          ← restrict_eq_self ν inter_subset_right]

Premises used: MeasureTheory.Measure.restrict_eq_self, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
⊢ (μ.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:
apply h_ν'_in
-- Module: Mathlib.MeasureTheory.Measure.Sub
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 :
  LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ sᶜ) : ENNReal)
    ((ν' + ν + ⊤ : (a : Set α) → ENNReal) (t ∩ sᶜ) : ENNReal)
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t \ s) : ENNReal)
    ((ν' + ν + restrict ⊤ sᶜ : (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]

Premises used: MeasurableSet.diff, Set.inter_self, MeasureTheory.Measure.restrict_apply, Set.diff_eq, MeasureTheory.Measure.add_apply, Set.inter_assoc
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
⊢ μ ≤ ν' + ν + ⊤

Tactic:
simp only [add_top, le_top]

Premises used: MeasureTheory.Measure.add_top, le_top
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
⊢ μ ≤ ν' + ν + ⊤

Tactic:
have h_mu_le_add_top : μ ≤ ν' + ν + ⊤ := by simp only [add_top, le_top]
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
h_mu_le_add_top : μ ≤ ν' + ν + ⊤
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ sᶜ) : ENNReal)
    ((ν' + ν + ⊤ : (a : Set α) → ENNReal) (t ∩ sᶜ) : ENNReal)

Tactic:
Measure.le_iff'.1 h_mu_le_add_top _

Premises used: MeasureTheory.Measure.le_iff', Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
h_mu_le_add_top : μ ≤ ν' + ν + ⊤
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ sᶜ) : ENNReal)
    ((ν' + ν + ⊤ : (a : Set α) → ENNReal) (t ∩ sᶜ) : ENNReal)

Tactic:
exact Measure.le_iff'.1 h_mu_le_add_top _

Premises used: MeasureTheory.Measure.le_iff', Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
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)
⊢ (fun (μ : Measure α) ↦ μ.restrict s) (ν' + restrict ⊤ sᶜ) = ν'.restrict s

Tactic:
ext1 t h_meas_t
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
⊢ Eq (α := ENNReal)
    ((((fun (μ : Measure α) ↦ μ.restrict s) (ν' + restrict ⊤ sᶜ) : Measure α) : (a : Set α) → ENNReal) t : ENNReal)
    ((ν'.restrict s : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
simp [restrict_apply h_meas_t, restrict_apply (h_meas_t.inter h_meas_s), inter_assoc]

Premises used: MeasureTheory.Measure.restrict_apply, Set.inter_assoc, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Sub
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 + ν}))

Tactic:
sInf_le_sInf_of_isCoinitialFor ?_

Premises used: sInf_le_sInf_of_isCoinitialFor
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty.{u_1} (α := Measure α) {d : Measure α | μ ≤ d + ν}
a :
  IsCoinitialFor.{u_1} (α := Measure α) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν})
    {d : Measure α | μ.restrict s ≤ d + ν.restrict s}
⊢ LE.le.{u_1} (α := Measure α) (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
    (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))

Tactic:
refine sInf_le_sInf_of_isCoinitialFor ?_

Premises used: sInf_le_sInf_of_isCoinitialFor
-- Module: Mathlib.MeasureTheory.Measure.Sub
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}

Tactic:
forall_mem_image.2 fun t h_t_in => ⟨t.restrict s, ?_, le_rfl⟩

Premises used: Iff.mpr, IsCoinitialFor, le_rfl, MeasureTheory.Measure.restrict, And.intro, Exists.intro, Set.forall_mem_image
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty.{u_1} (α := Measure α) {d : Measure α | μ ≤ d + ν}
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)
⊢ IsCoinitialFor.{u_1} (α := Measure α) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν})
    {d : Measure α | μ.restrict s ≤ d + ν.restrict s}

Tactic:
refine forall_mem_image.2 fun t h_t_in => ⟨t.restrict s, ?_, le_rfl⟩

Premises used: Iff.mpr, Set.forall_mem_image
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
a : μ.restrict s ≤ (t + ν).restrict s
⊢ Membership.mem (γ := Set (Measure α)) {d : Measure α | μ.restrict s ≤ d + ν.restrict s} (t.restrict s)

Tactic:
rw [Set.mem_setOf_eq, ← restrict_add]

Premises used: MeasureTheory.Measure.restrict_add, Set.mem_setOf_eq
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
⊢ μ.restrict s ≤ (t + ν).restrict s

Tactic:
restrict_mono Subset.rfl h_t_in

Premises used: MeasureTheory.Measure.restrict_mono, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Measure.Sub
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
⊢ μ.restrict s ≤ (t + ν).restrict s

Tactic:
exact restrict_mono Subset.rfl h_t_in

Premises used: MeasureTheory.Measure.restrict_mono, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_le : μ.restrict s ≤ ν.restrict s
h_meas_s : MeasurableSet s
rw : Eq (α := ENNReal) (((0 : Measure α) : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
rw₁ : μ.restrict s ≤ ν.restrict s
rw₂ : MeasurableSet s
⊢ Eq (α := ENNReal) ((μ - ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
rw [← restrict_apply_self, restrict_sub_eq_restrict_sub_restrict, sub_eq_zero_of_le]

Premises used: MeasureTheory.Measure.restrict_apply_self, MeasureTheory.Measure.sub_eq_zero_of_le, MeasureTheory.Measure.restrict_sub_eq_restrict_sub_restrict
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_le : μ.restrict s ≤ ν.restrict s
h_meas_s : MeasurableSet s
⊢ Eq (α := ENNReal) (((0 : Measure α) : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_le : μ.restrict s ≤ ν.restrict s
h_meas_s : MeasurableSet s
⊢ μ.restrict s ≤ ν.restrict s

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_le : μ.restrict s ≤ ν.restrict s
h_meas_s : MeasurableSet s
⊢ MeasurableSet s

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
s : Set α
inst : IsFiniteMeasure μ
⊢ IsFiniteMeasure (μ - ν)

Tactic:
isFiniteMeasure_of_le μ sub_le

Premises used: MeasureTheory.isFiniteMeasure_of_le, MeasureTheory.Measure.sub_le
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure ν
h_le : ν ≤ μ
⊢ μ - ν ≤ ξ ↔ μ ≤ ξ + ν

Tactic:
⟨fun h ↦ ?_, Measure.sub_le_of_le_add⟩

Premises used: MeasureTheory.Measure.sub_le_of_le_add, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure ν
h_le : ν ≤ μ
refine : ∀ (h : μ - ν ≤ ξ), μ ≤ ξ + ν
⊢ μ - ν ≤ ξ ↔ μ ≤ ξ + ν

Tactic:
refine ⟨fun h ↦ ?_, Measure.sub_le_of_le_add⟩
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure ν
h_le : ν ≤ μ
h : μ - ν ≤ ξ
⊢ μ ≤ ξ + ν

Tactic:
simpa [sub_add_cancel_of_le h_le] using add_le_add_left h ν

Premises used: MeasureTheory.Measure.sub_add_cancel_of_le, add_le_add_left
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ μ - ν ≤ ξ ↔ μ ≤ ξ + ν

Tactic:
⟨fun h ↦ ?_, sub_le_of_le_add⟩

Premises used: MeasureTheory.Measure.sub_le_of_le_add, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
refine : ∀ (h : μ - ν ≤ ξ), μ ≤ ξ + ν
⊢ μ - ν ≤ ξ ↔ μ ≤ ξ + ν

Tactic:
refine ⟨fun h ↦ ?_, sub_le_of_le_add⟩
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ - ν ≤ ξ
obtain : ∀ (s : Set α) (hs : IsHahnDecomposition μ ν s), μ ≤ ξ + ν
⊢ μ ≤ ξ + ν

Tactic:
obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν

Premises used: MeasureTheory.exists_isHahnDecomposition
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ - ν ≤ ξ
s : Set α
hs : IsHahnDecomposition μ ν 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)
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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ᶜ

Tactic:
(sub_le_iff_le_add_of_le hs.ge_on_compl).mp ?_

Premises used: MeasureTheory.Measure.sub_le_iff_le_add_of_le, MeasureTheory.IsHahnDecomposition.ge_on_compl, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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
refine : μ.restrict sᶜ - ν.restrict sᶜ ≤ ξ.restrict sᶜ
⊢ μ.restrict sᶜ ≤ ξ.restrict sᶜ + ν.restrict sᶜ

Tactic:
refine (sub_le_iff_le_add_of_le hs.ge_on_compl).mp ?_

Premises used: MeasureTheory.Measure.sub_le_iff_le_add_of_le, MeasureTheory.IsHahnDecomposition.ge_on_compl, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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
rw : (μ - ν).restrict sᶜ ≤ ξ.restrict sᶜ
⊢ μ.restrict sᶜ - ν.restrict sᶜ ≤ ξ.restrict sᶜ

Tactic:
rw [← restrict_sub_eq_restrict_sub_restrict hs.measurableSet.compl]

Premises used: MeasurableSet.compl, MeasureTheory.Measure.restrict_sub_eq_restrict_sub_restrict, MeasureTheory.IsHahnDecomposition.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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ᶜ

Tactic:
restrict_mono subset_rfl h

Premises used: MeasureTheory.Measure.restrict_mono, subset_rfl
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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ᶜ

Tactic:
exact restrict_mono subset_rfl h

Premises used: MeasureTheory.Measure.restrict_mono, subset_rfl
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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ᶜ

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
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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ᶜ
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]

Premises used: MeasureTheory.Measure.restrict_add_restrict_compl, MeasureTheory.IsHahnDecomposition.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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ᶜ
this : μ.restrict s + μ.restrict sᶜ ≤ ξ.restrict s + ν.restrict s + (ξ.restrict sᶜ + ν.restrict sᶜ)
⊢ ξ.restrict s + ν.restrict s + (ξ.restrict sᶜ + ν.restrict sᶜ) =
    ξ.restrict s + ξ.restrict sᶜ + (ν.restrict s + ν.restrict sᶜ)

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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ᶜ
suffices : μ.restrict s + μ.restrict sᶜ ≤ ξ.restrict s + ν.restrict s + (ξ.restrict sᶜ + ν.restrict sᶜ)
⊢ μ.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)
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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ᶜ)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst : IsFiniteMeasure (μ.withDensity g)
hg : Measurable g
hgf : g ≤ᶠ[ae μ] f
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∞)
⊢ μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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 ∂μ
rw : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (f - g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity f - μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

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)]

Premises used: MeasureTheory.ae_restrict_of_ae, MeasureTheory.Measure.sub_apply, MeasureTheory.lintegral_sub, MeasureTheory.withDensity_mono, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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
⊢ ∫⁻ (a : α) in s, (f - g) a ∂μ = ∫⁻ (a : α) in s, f a - g a ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.SubFinite
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

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm