awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Function.onFun Disjoint g)
simp :
  HSub.hSub (α := ENNReal) (∑' (i : ℕ), (μ : (a : Set α) → ENNReal) (g i))
      (∑' (i : ℕ), (ν : (a : Set α) → ENNReal) (g i)) =
    ∑' (i : ℕ),
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) (g i) : ENNReal)
        ((ν : (a : Set α) → ENNReal) (g i) : ENNReal)
⊢ Eq (α := ENNReal)
    ((fun (t : Set α) (x : MeasurableSet t) ↦
        HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
          ((ν : (a : Set α) → ENNReal) t : ENNReal))
      (⋃ (i : ℕ), g i) ⋯)
    (∑' (i : ℕ),
      (fun (t : Set α) (x : MeasurableSet t) ↦
          HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
            ((ν : (a : Set α) → ENNReal) t : ENNReal))
        (g i) ⋯)

Tactic:
simp only [measure_iUnion h_disj h_meas]

Premises used: MeasureTheory.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Function.onFun Disjoint g)
rw : Ne (α := ENNReal) (∑' (i : ℕ), (ν : (a : Set α) → ENNReal) (g i)) ⊤
⊢ HSub.hSub (α := ENNReal) (∑' (i : ℕ), (μ : (a : Set α) → ENNReal) (g i))
      (∑' (i : ℕ), (ν : (a : Set α) → ENNReal) (g i)) =
    ∑' (i : ℕ),
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) (g i) : ENNReal)
        ((ν : (a : Set α) → ENNReal) (g i) : ENNReal)

Tactic:
rw [ENNReal.tsum_sub _ (h₂ <| g ·)]

Premises used: ENNReal.tsum_sub
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Function.onFun Disjoint g)
rw : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) (⋃ (i : ℕ), g i) : ENNReal) (⊤ : ENNReal)
⊢ Ne (α := ENNReal) (∑' (i : ℕ), (ν : (a : Set α) → ENNReal) (g i)) ⊤

Tactic:
rw [← measure_iUnion h_disj h_meas]

Premises used: MeasureTheory.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Function.onFun Disjoint g)
⊢ Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) (⋃ (i : ℕ), g i) : ENNReal) (⊤ : ENNReal)

Tactic:
apply measure_ne_top

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
h :
  ∀ (t : Set α) (h_t_measurable_set : MeasurableSet t),
    Eq (α := ENNReal) ((ν + measure_sub : (a : Set α) → ENNReal) t : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
⊢ ν + measure_sub = μ

Tactic:
ext1 t h_t_measurable_set
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
t : Set α
h_t_measurable_set : MeasurableSet t
h :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν : (a : Set α) → ENNReal) t : ENNReal)
      ((measure_sub : (a : Set α) → ENNReal) t : ENNReal) =
    (μ : (a : Set α) → ENNReal) t
⊢ Eq (α := ENNReal) ((ν + measure_sub : (a : Set α) → ENNReal) t : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
simp only [Pi.add_apply, coe_add]

Premises used: MeasureTheory.Measure.coe_add, Pi.add_apply
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
t : Set α
h_t_measurable_set : MeasurableSet t
h :
  HAdd.hAdd (α := ENNReal) ((ν : (a : Set α) → ENNReal) t : ENNReal)
      (HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal)) =
    (μ : (a : Set α) → ENNReal) t
h₃ :
  HAdd.hAdd (β := ENNReal)
      (HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
      ((ν : (a : Set α) → ENNReal) t : ENNReal) =
    (μ : (a : Set α) → ENNReal) t
h₄ h₅ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν : (a : Set α) → ENNReal) t : ENNReal)
      ((measure_sub : (a : Set α) → ENNReal) t : ENNReal) =
    (μ : (a : Set α) → ENNReal) t

Tactic:
rw [MeasureTheory.Measure.ofMeasurable_apply _ h_t_measurable_set, add_comm,
      tsub_add_cancel_of_le (h₂ t)]

Premises used: tsub_add_cancel_of_le, add_comm, MeasureTheory.Measure.ofMeasurable_apply
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
⊢ ν + measure_sub = μ

Tactic:
have h_measure_sub_add : ν + measure_sub = μ := by
    ext1 t h_t_measurable_set
    simp only [Pi.add_apply, coe_add]
    rw [MeasureTheory.Measure.ofMeasurable_apply _ h_t_measurable_set, add_comm,
      tsub_add_cancel_of_le (h₂ t)]
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
a : sInf {d : Measure α | μ ≤ d + ν} ≤ measure_sub
a₁ : measure_sub ≤ sInf {d : Measure α | μ ≤ d + ν}
⊢ sInf {d : Measure α | μ ≤ d + ν} = measure_sub

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
a : Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} measure_sub
⊢ sInf {d : Measure α | μ ≤ d + ν} ≤ measure_sub

Tactic:
apply sInf_le

Premises used: sInf_le
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} measure_sub

Tactic:
simp [add_comm, h_measure_sub_add]

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
a : ∀ (b : Measure α), Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} b → measure_sub ≤ b
⊢ measure_sub ≤ sInf {d : Measure α | μ ≤ d + ν}

Tactic:
apply le_sInf

Premises used: le_sInf
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
d : Measure α
h_d : Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} d
⊢ ν + measure_sub ≤ ν + d

Tactic:
rw [← h_measure_sub_add, mem_setOf_eq, add_comm d] at h_d

Premises used: Set.mem_setOf_eq, add_comm
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
d : Measure α
h_d : ν + measure_sub ≤ ν + d
⊢ measure_sub ≤ d

Tactic:
apply Measure.le_of_add_le_add_left h_d

Premises used: MeasureTheory.Measure.le_of_add_le_add_left
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ μ - ν = measure_sub

Tactic:
have h_measure_sub_eq : μ - ν = measure_sub := by
    rw [MeasureTheory.Measure.sub_def]
    apply le_antisymm
    · apply sInf_le
      simp [add_comm, h_measure_sub_add]
    apply le_sInf
    intro d h_d
    rw [← h_measure_sub_add, mem_setOf_eq, add_comm d] at h_d
    apply Measure.le_of_add_le_add_left h_d
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
h_measure_sub_eq : μ - ν = measure_sub
rw :
  (measure_sub : (a : Set α) → ENNReal) s =
    HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((ν : (a : Set α) → ENNReal) s : ENNReal)
⊢ (μ - ν : (a : Set α) → ENNReal) s =
    HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((ν : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
rw [h_measure_sub_eq]
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
h_measure_sub_eq : μ - ν = measure_sub
⊢ (measure_sub : (a : Set α) → ENNReal) s =
    HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((ν : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
apply Measure.ofMeasurable_apply _ h₁

Premises used: MeasureTheory.Measure.ofMeasurable_apply
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
h₁ : ν ≤ μ
h :
  ∀ (s : Set α) (h_s_meas : MeasurableSet s),
    Eq (α := ENNReal) ((μ - ν + ν : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
⊢ μ - ν + ν = μ

Tactic:
ext1 s h_s_meas
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
h₁ : ν ≤ μ
s : Set α
h_s_meas : MeasurableSet s
h :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ - ν : (a : Set α) → ENNReal) s : ENNReal)
      ((ν : (a : Set α) → ENNReal) s : ENNReal) =
    (μ : (a : Set α) → ENNReal) s
h₂ :
  HAdd.hAdd (β := ENNReal)
      (HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
        ((ν : (a : Set α) → ENNReal) s : ENNReal))
      ((ν : (a : Set α) → ENNReal) s : ENNReal) =
    (μ : (a : Set α) → ENNReal) s
h₃ h₄ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((μ - ν + ν : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
rw [add_apply, sub_apply h_s_meas h₁, tsub_add_cancel_of_le (h₁ s)]

Premises used: tsub_add_cancel_of_le, MeasureTheory.Measure.add_apply, MeasureTheory.Measure.sub_apply
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ENNReal) ((μ + ν - ν : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
⊢ μ + ν - ν = μ

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
h :
  HSub.hSub (α := ENNReal) (β := ENNReal) ((μ + ν : (a : Set α) → ENNReal) s : ENNReal)
      ((ν : (a : Set α) → ENNReal) s : ENNReal) =
    (μ : (a : Set α) → ENNReal) s
h₁ :
  HSub.hSub (β := ENNReal)
      (HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
        ((ν : (a : Set α) → ENNReal) s : ENNReal))
      ((ν : (a : Set α) → ENNReal) s : ENNReal) =
    (μ : (a : Set α) → ENNReal) s
h₂ h₃ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((μ + ν - ν : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
rw [sub_apply hs (Measure.le_add_left (le_refl _)), add_apply,
    ENNReal.add_sub_cancel_right (measure_ne_top ν s)]

Premises used: le_refl, ENNReal.add_sub_cancel_right, MeasureTheory.measure_ne_top, MeasureTheory.Measure.add_apply, MeasureTheory.Measure.sub_apply, MeasureTheory.Measure.le_add_left
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ Set.Nonempty.{u_1} (α := Measure α) {d : Measure α | μ ≤ d + ν}

Tactic:
have h_nonempty : { d | μ ≤ d + ν }.Nonempty := ⟨μ, Measure.le_add_right le_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 + ν}
rw :
  Eq.{u_1 + 1} (α := Measure α) (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
    (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
⊢ Eq (α := Measure α) (restrict (sInf {d : Measure α | μ ≤ d + ν}) s)
    (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})

Tactic:
rw [restrict_sInf_eq_sInf_restrict h_nonempty h_meas_s]

Premises used: MeasureTheory.Measure.restrict_sInf_eq_sInf_restrict
-- 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 :
  LE.le.{u_1} (α := Measure α) (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
    (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
a₁ :
  LE.le.{u_1} (α := Measure α) (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
    (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
⊢ Eq.{u_1 + 1} (α := Measure α) (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
    (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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 ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
    (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})

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 α) {d : Measure α | μ.restrict s ≤ d + ν.restrict s}
    ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν})
⊢ LE.le.{u_1} (α := Measure α) (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
    (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})

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 + ν}
ν' : Measure α
h_ν'_in : Membership.mem (γ := Set (Measure α)) {d : Measure α | μ.restrict s ≤ d + ν.restrict s} ν'
⊢ μ.restrict s ≤ ν' + ν.restrict s

Tactic:
rw [mem_setOf_eq] at h_ν'_in

Premises used: 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 + ν}
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
⊢ ∃ (b : Measure α),
    Membership.mem (γ := Set (Measure α)) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}) b ∧
      b ≤ ν'

Tactic:
⟨ν'.restrict s, ?_, restrict_le_self⟩

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.Measure.restrict_le_self, And.intro, Exists.intro
-- 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 :
  Membership.mem (γ := Set (Measure α)) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν})
    (ν'.restrict s)
⊢ ∃ (b : Measure α),
    Membership.mem (γ := Set (Measure α)) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}) b ∧
      b ≤ ν'

Tactic:
refine ⟨ν'.restrict s, ?_, restrict_le_self⟩
-- 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
⊢ Membership.mem (γ := Set (Measure α)) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν})
    (ν'.restrict s)

Tactic:
⟨ν' + (⊤ : Measure α).restrict sᶜ, ?_, ?_⟩

Premises used: Set.Mem, Compl.compl, setOf, MeasureTheory.Measure.restrict, HAdd.hAdd, And.intro, Exists.intro, Set.image, Top.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
a : Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} (ν' + restrict ⊤ sᶜ)
a₁ : (fun (μ : Measure α) ↦ μ.restrict s) (ν' + restrict ⊤ sᶜ) = ν'.restrict s
⊢ Membership.mem (γ := Set (Measure α)) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν})
    (ν'.restrict s)

Tactic:
refine ⟨ν' + (⊤ : Measure α).restrict sᶜ, ?_, ?_⟩
-- 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 :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) s_1 : ENNReal)
        ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) s_1 : ENNReal)
⊢ Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} (ν' + restrict ⊤ sᶜ)

Tactic:
rw [mem_setOf_eq, add_right_comm, Measure.le_iff]

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

Tactic:
rw [← measure_inter_add_diff t h_meas_s]

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

Tactic:
rw [← measure_inter_add_diff t h_meas_s]

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

Tactic:
repeat rw [← measure_inter_add_diff t h_meas_s]

Premises used: MeasureTheory.measure_inter_add_diff