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 α
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
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν : (a : Set α) → ENNReal) t : ENNReal)
      ((measure_sub : (a : Set α) → ENNReal) t : ENNReal) =
    (μ : (a : Set α) → ENNReal) t
have h₄ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: rw [MeasureTheory.Measure.ofMeasurable_apply _ h_t_measurable_set, add_comm,
      tsub_add_cancel_of_le (h₂ t)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (hypothesis)
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))
    ⋯ ⋯
⊢ (μ - ν : (a : Set α) → ENNReal) s =
    HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((ν : (a : Set α) → ENNReal) s : ENNReal)
have h_measure_sub_add : ν + 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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
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 = μ
⊢ sInf {d : Measure α | μ ≤ d + ν} = measure_sub
have a : sInf {d : Measure α | μ ≤ d + ν} ≤ measure_sub
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
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
⊢ sInf {d : Measure α | μ ≤ d + ν} = measure_sub
have a₁ : measure_sub ≤ sInf {d : Measure α | μ ≤ d + ν}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
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 = μ
⊢ sInf {d : Measure α | μ ≤ d + ν} ≤ measure_sub
have a : Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} measure_sub
Tactic: apply sInf_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
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 ≤ sInf {d : Measure α | μ ≤ d + ν}
have a : ∀ (b : Measure α), Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} b → measure_sub ≤ b
Tactic: apply le_sInf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (hypothesis)
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
have h_d₁ : ν + measure_sub ≤ ν + d
Tactic: rw [← h_measure_sub_add, mem_setOf_eq, add_comm d] at h_d
Cleared hypotheses: h_d
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (hypothesis)
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 : Set α) → ENNReal) s =
    HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((ν : (a : Set α) → ENNReal) s : ENNReal)
have h_measure_sub_eq : μ - ν = 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
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
⊢ (μ - ν : (a : Set α) → ENNReal) s =
    HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((ν : (a : Set α) → ENNReal) s : ENNReal)
have rw : (measure_sub : (a : Set α) → ENNReal) s =
  HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
    ((ν : (a : Set α) → ENNReal) s : ENNReal)
Tactic: rw [h_measure_sub_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
h₁ : ν ≤ μ
⊢ μ - ν + ν = μ
have 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
h₁ : ν ≤ μ
s : Set α
h_s_meas : MeasurableSet s
⊢ Eq (α := ENNReal) ((μ - ν + ν : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
have h : HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ - ν : (a : Set α) → ENNReal) s : ENNReal)
    ((ν : (a : Set α) → ENNReal) s : ENNReal) =
  (μ : (a : Set α) → ENNReal) s
Tactic: rw [add_apply, sub_apply h_s_meas h₁, tsub_add_cancel_of_le (h₁ s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
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
⊢ Eq (α := ENNReal) ((μ - ν + ν : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
have 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
Tactic: rw [add_apply, sub_apply h_s_meas h₁, tsub_add_cancel_of_le (h₁ s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
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
⊢ Eq (α := ENNReal) ((μ - ν + ν : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
have h₃ : 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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
⊢ μ + ν - ν = μ
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ENNReal) ((μ + ν - ν : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ENNReal) ((μ + ν - ν : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
have h : HSub.hSub (α := ENNReal) (β := ENNReal) ((μ + ν : (a : Set α) → ENNReal) s : ENNReal)
    ((ν : (a : Set α) → ENNReal) s : ENNReal) =
  (μ : (a : Set α) → ENNReal) s
Tactic: rw [sub_apply hs (Measure.le_add_left (le_refl _)), add_apply,
    ENNReal.add_sub_cancel_right (measure_ne_top ν s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
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
⊢ Eq (α := ENNReal) ((μ + ν - ν : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
have 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
Tactic: rw [sub_apply hs (Measure.le_add_left (le_refl _)), add_apply,
    ENNReal.add_sub_cancel_right (measure_ne_top ν s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
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
⊢ Eq (α := ENNReal) ((μ + ν - ν : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
have h₂ : 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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ Eq (α := Measure α) (restrict (sInf {d : Measure α | μ ≤ d + ν}) s)
    (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
have h_nonempty : Set.Nonempty.{u_1} (α := Measure α) {d : Measure α | μ ≤ d + ν}
Tactic: have h_nonempty : { d | μ ≤ d + ν }.Nonempty := ⟨μ, Measure.le_add_right 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 + ν}
⊢ Eq (α := Measure α) (restrict (sInf {d : Measure α | μ ≤ d + ν}) s)
    (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
have rw : Eq.{u_1 + 1} (α := Measure α) (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
  (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
Tactic: rw [restrict_sInf_eq_sInf_restrict h_nonempty h_meas_s]
-- 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 + ν}
⊢ Eq.{u_1 + 1} (α := Measure α) (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
    (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
have a : LE.le.{u_1} (α := Measure α) (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
  (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
Tactic: apply le_antisymm
-- 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 + ν}
a :
  LE.le.{u_1} (α := Measure α) (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
    (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
⊢ Eq.{u_1 + 1} (α := Measure α) (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
    (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
have a₁ : LE.le.{u_1} (α := Measure α) (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
  (sInf ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
Tactic: apply le_antisymm
-- 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 ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}))
    (sInf {d : Measure α | μ.restrict s ≤ d + ν.restrict s})
have a : IsCoinitialFor.{u_1} (α := Measure α) {d : Measure α | μ.restrict s ≤ d + ν.restrict s}
  ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν})
Tactic: refine sInf_le_sInf_of_isCoinitialFor ?_
-- 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 : Membership.mem (γ := Set (Measure α)) {d : Measure α | μ.restrict s ≤ d + ν.restrict s} ν'
⊢ ∃ (b : Measure α),
    Membership.mem (γ := Set (Measure α)) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}) b ∧
      b ≤ ν'
have h_ν'_in₁ : μ.restrict s ≤ ν' + ν.restrict s
Tactic: rw [mem_setOf_eq] at h_ν'_in
Cleared hypotheses: h_ν'_in
-- 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
⊢ ∃ (b : Measure α),
    Membership.mem (γ := Set (Measure α)) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν}) b ∧
      b ≤ ν'
have a : Membership.mem (γ := Set (Measure α)) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν})
  (ν'.restrict s)
Tactic: refine ⟨ν'.restrict s, ?_, restrict_le_self⟩
-- 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
⊢ Membership.mem (γ := Set (Measure α)) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν})
    (ν'.restrict s)
have a : Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} (ν' + restrict ⊤ sᶜ)
Tactic: refine ⟨ν' + (⊤ : Measure α).restrict sᶜ, ?_, ?_⟩
-- 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
a : Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} (ν' + restrict ⊤ sᶜ)
⊢ Membership.mem (γ := Set (Measure α)) ((fun (μ : Measure α) ↦ μ.restrict s) '' {d : Measure α | μ ≤ d + ν})
    (ν'.restrict s)
have a₁ : (fun (μ : Measure α) ↦ μ.restrict s) (ν' + restrict ⊤ sᶜ) = ν'.restrict s
Tactic: refine ⟨ν' + (⊤ : Measure α).restrict sᶜ, ?_, ?_⟩
-- 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
⊢ Membership.mem (γ := Set (Measure α)) {d : Measure α | μ ≤ d + ν} (ν' + restrict ⊤ sᶜ)
have a : ∀ (s_1 : Set α),
  MeasurableSet s_1 →
    LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) s_1 : ENNReal)
      ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) s_1 : ENNReal)
Tactic: rw [mem_setOf_eq, add_right_comm, Measure.le_iff]
-- 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 : ENNReal)
    ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) t : ENNReal)
have a : 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]
-- 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
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (t \ s) : ENNReal) ≤
    (ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) t
have 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)
Tactic: rw [← measure_inter_add_diff t h_meas_s]
-- 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 : ENNReal)
    ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) t : ENNReal)
have 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)
Tactic: repeat rw [← measure_inter_add_diff t h_meas_s]
-- 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
⊢ 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)
have a : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
  ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal)
Tactic: refine add_le_add ?_ ?_
-- 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 :
  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)
have a₁ : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t \ s) : ENNReal)
  ((ν' + ν + restrict ⊤ sᶜ : (a : Set α) → ENNReal) (t \ s) : ENNReal)
Tactic: refine add_le_add ?_ ?_
-- 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 : (μ : (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: rw [add_apply, add_apply]