awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
simp :
  LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a), g.lintegral μ)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (μ.restrict s))
⊢ ∫⁻ (a : α), s.indicator f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ

Tactic:
simp only [lintegral]

Premises used: MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
apply :
  ∀ (g : α →ₛ ℝ≥0∞) (hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a),
    g.lintegral μ ≤
      ⨆ (g : α →ₛ ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (μ.restrict s)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a), g.lintegral μ)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (μ.restrict s))

Tactic:
apply iSup_le (fun g ↦ (iSup_le (fun hg ↦ ?_)))

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
⊢ (⇑g : (a : α) → ℝ≥0∞) ≤ f

Tactic:
have : g ≤ f := hg.trans (indicator_le_self s f)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
⊢ g.lintegral μ ≤
    ⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (μ.restrict s)

Tactic:
le_iSup_of_le g (le_iSup_of_le this (le_of_eq ?_))

Premises used: le_iSup_of_le, le_of_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
refine : g.lintegral μ = g.lintegral (μ.restrict s)
⊢ g.lintegral μ ≤
    ⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (μ.restrict s)

Tactic:
refine le_iSup_of_le g (le_iSup_of_le this (le_of_eq ?_))

Premises used: le_iSup_of_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
rw :
  Eq (α := ℝ≥0∞)
    (∑ x ∈ g.range,
      HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ y ∈ g.range,
      HMul.hMul (β := ℝ≥0∞) y ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {y} ∩ s) : ℝ≥0∞))
⊢ g.lintegral μ = g.lintegral (μ.restrict s)

Tactic:
rw [lintegral_restrict, SimpleFunc.lintegral]

Premises used: MeasureTheory.SimpleFunc.lintegral, MeasureTheory.SimpleFunc.lintegral_restrict
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
e_f :
  ∀ (t : ℝ≥0∞),
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
      HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ g.range,
      HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ y ∈ g.range,
      HMul.hMul (β := ℝ≥0∞) y ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {y} ∩ s) : ℝ≥0∞))

Tactic:
congr with t
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
t : ℝ≥0∞
pos :
  ∀ (H : t = 0),
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
      HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)
neg :
  ∀ (H : ¬t = 0),
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
      HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)

Tactic:
by_cases H : t = 0
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
t : ℝ≥0∞
H : t = 0
⊢ HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)

Tactic:
simp [H]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
t : ℝ≥0∞
H : ¬t = 0
neg :
  ∀ (x : α),
    Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) x ↔
      x ∈ preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s
⊢ HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
t : ℝ≥0∞
H : ¬t = 0
x : α
neg : (g : (a : α) → ℝ≥0∞) x = t → x ∈ s
⊢ Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) x ↔
    x ∈ preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s

Tactic:
simp only [mem_preimage, mem_singleton_iff, mem_inter_iff, iff_self_and]

Premises used: Set.mem_inter_iff, iff_self_and, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
x : α
H : ¬Eq (α := ℝ≥0∞) ((g : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
neg : ∀ (H : x ∉ s), Eq (α := ℝ≥0∞) ((g : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ x ∈ s

Tactic:
contrapose H
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
x : α
H : x ∉ s
⊢ Eq (α := ℝ≥0∞) ((g : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [H] using hg x
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
apply : ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α), s.indicator f a ∂μ
⊢ ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
apply le_antisymm (lintegral_indicator_le f s)

Premises used: MeasureTheory.lintegral_indicator_le, le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
simp :
  LE.le (α := ℝ≥0∞)
    (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
      ((↑x : α →ₛ ℝ≥0∞).restrict s).lintegral μ)
    (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a }),
      (↑x : α →ₛ ℝ≥0∞).lintegral μ)
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α), s.indicator f a ∂μ

Tactic:
simp only [lintegral, ← restrict_lintegral_eq_lintegral_restrict _ hs, iSup_subtype']

Premises used: iSup_subtype', MeasureTheory.SimpleFunc.restrict_lintegral_eq_lintegral_restrict, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
      ((↑x : α →ₛ ℝ≥0∞).restrict s).lintegral μ)
    (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a }),
      (↑x : α →ₛ ℝ≥0∞).lintegral μ)

Tactic:
iSup_mono' (Subtype.forall.2 fun φ hφ => ?_)

Premises used: Iff.mpr, iSup_mono', Subtype.forall
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
refine :
  ∀ (φ : α →ₛ ℝ≥0∞) (hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
    ∃ (i' : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a }),
      ((↑(Subtype.mk (p := fun (a : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑a : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) φ
                      hφ) :
                  α →ₛ ℝ≥0∞).restrict
              s).lintegral
          μ ≤
        (↑i' : α →ₛ ℝ≥0∞).lintegral μ
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
      ((↑x : α →ₛ ℝ≥0∞).restrict s).lintegral μ)
    (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a }),
      (↑x : α →ₛ ℝ≥0∞).lintegral μ)

Tactic:
refine iSup_mono' (Subtype.forall.2 fun φ hφ => ?_)

Premises used: Iff.mpr, iSup_mono', Subtype.forall
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
⊢ ∃ (i' : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a }),
    ((↑(Subtype.mk (p := fun (a : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑a : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) φ
                    hφ) :
                α →ₛ ℝ≥0∞).restrict
            s).lintegral
        μ ≤
      (↑i' : α →ₛ ℝ≥0∞).lintegral μ

Tactic:
⟨⟨φ.restrict s, fun x => ?_⟩, le_rfl⟩

Premises used: le_rfl, Subtype.mk, MeasureTheory.SimpleFunc.restrict, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
refine :
  ∀ (x : α),
    LE.le (α := (fun (a : α) ↦ ℝ≥0∞) x) ((φ.restrict s : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
      ((fun (a : α) ↦ s.indicator f a) x : ℝ≥0∞)
⊢ ∃ (i' : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a }),
    ((↑(Subtype.mk (p := fun (a : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑a : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) φ
                    hφ) :
                α →ₛ ℝ≥0∞).restrict
            s).lintegral
        μ ≤
      (↑i' : α →ₛ ℝ≥0∞).lintegral μ

Tactic:
refine ⟨⟨φ.restrict s, fun x => ?_⟩, le_rfl⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
x : α
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) x) ((φ.restrict s : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
    ((fun (a : α) ↦ s.indicator f a) x : ℝ≥0∞)

Tactic:
simp [hφ x, hs, indicator_le_indicator]

Premises used: Set.indicator_le_indicator
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
rw : ∫⁻ (a : α) in s, f a ∂μ.restrict t = ∫⁻ (a : α) in s ∩ t, f a ∂μ
rw₁ rw₂ : ∫⁻ (a : α) in s ∩ t, f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ
⊢ ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ

Tactic:
rw [lintegral_indicator hs, Measure.restrict_restrict hs]

Premises used: MeasureTheory.Measure.restrict_restrict, MeasureTheory.lintegral_indicator
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
f : α → ℝ≥0∞
rw : ∫⁻ (a : α), (toMeasurable μ s).indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
rw₁ : ∫⁻ (a : α) in toMeasurable μ s, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
rw₂ rw₃ : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
⊢ ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
rw [← lintegral_congr_ae (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
    lintegral_indicator (measurableSet_toMeasurable _ _),
    Measure.restrict_congr_set hs.toMeasurable_ae_eq]

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.lintegral_congr_ae, MeasureTheory.lintegral_indicator, indicator_ae_eq_of_ae_eq_set, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
hs : NullMeasurableSet s (μ.restrict t)
rw : ∫⁻ (a : α) in s, f a ∂μ.restrict t = ∫⁻ (a : α) in s ∩ t, f a ∂μ
rw₁ rw₂ : ∫⁻ (a : α) in s ∩ t, f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ
⊢ ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ

Tactic:
rw [lintegral_indicator₀ hs, Measure.restrict_restrict₀ hs]

Premises used: MeasureTheory.Measure.restrict_restrict₀, MeasureTheory.lintegral_indicator₀
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0∞
⊢ ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ ≤ HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
(lintegral_indicator_le _ _).trans (setLIntegral_const s c).le

Premises used: Eq.le, MeasureTheory.lintegral_indicator_le, MeasureTheory.setLIntegral_const, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
c : ℝ≥0∞
rw : ∫⁻ (a : α) in s, c ∂μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [lintegral_indicator₀ hs, setLIntegral_const]

Premises used: MeasureTheory.setLIntegral_const, MeasureTheory.lintegral_indicator₀
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
c : ℝ≥0∞
⊢ ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
lintegral_indicator_const₀ hs.nullMeasurableSet c

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.lintegral_indicator_const₀
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
apply : ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α) in s, f x ∂μ
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
apply le_antisymm (setLIntegral_le_lintegral s fun x ↦ f x)

Premises used: le_antisymm, MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
apply : ∫⁻ (x : α), f x ∂μ = ∫⁻ (a : α), s.indicator f a ∂μ
⊢ ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α) in s, f x ∂μ

Tactic:
apply le_trans (le_of_eq _) (lintegral_indicator_le _ _)

Premises used: MeasureTheory.lintegral_indicator_le, le_of_eq, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
e_f : ∀ (x : α), f x = s.indicator f x
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (a : α), s.indicator f a ∂μ

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
pos : ∀ (h : x ∈ s), f x = f x
neg : ∀ (h : x ∉ s), f x = 0
⊢ f x = if x ∈ s then f x else 0

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
h : x ∈ s
⊢ f x = f x

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
h : x ∉ s
⊢ f x = 0

Tactic:
Function.support_subset_iff'.1 hsf x h

Premises used: Iff.mp, Function.support_subset_iff'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
h : x ∉ s
⊢ f x = 0

Tactic:
exact Function.support_subset_iff'.1 hsf x h

Premises used: Iff.mp, Function.support_subset_iff'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
⊢ ∀ (x : α), Membership.mem (γ := Set α) {x : α | f x = r} x → f x = r

Tactic:
have : ∀ x ∈ { x | f x = r }, f x = r := fun _ hx => hx
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ (x : α), Membership.mem (γ := Set α) {x : α | f x = r} x → f x = r
rw : ∫⁻ (x : α) in {x : α | f x = r}, r ∂μ = HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
rw₁ : MeasurableSet.{u_1} (α := α) {x : α | f x = r}
⊢ ∫⁻ (x : α) in {x : α | f x = r}, f x ∂μ = HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)

Tactic:
rw [setLIntegral_congr_fun _ this]

Premises used: MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ (x : α), Membership.mem (γ := Set α) {x : α | f x = r} x → f x = r
rw :
  HMul.hMul (β := ℝ≥0∞) r ((μ.restrict {x : α | f x = r} : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
rw₁ :
  HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ {x : α | f x = r}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
rw₂ rw₃ :
  HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
⊢ ∫⁻ (x : α) in {x : α | f x = r}, r ∂μ = HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)

Tactic:
rw [lintegral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ (x : α), Membership.mem (γ := Set α) {x : α | f x = r} x → f x = r
⊢ MeasurableSet.{u_1} (α := α) {x : α | f x = r}

Tactic:
hf (measurableSet_singleton r)

Premises used: MeasurableSingletonClass.measurableSet_singleton, Set.Mem, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ (x : α), Membership.mem (γ := Set α) {x : α | f x = r} x → f x = r
⊢ MeasurableSet.{u_1} (α := α) {x : α | f x = r}

Tactic:
exact hf (measurableSet_singleton r)

Premises used: MeasurableSingletonClass.measurableSet_singleton
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ∫⁻ (a : α), s.indicator 1 a ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
(lintegral_indicator_const_le _ _).trans <| (one_mul _).le

Premises used: ENNReal.ofNNReal, Eq.le, MeasureTheory.lintegral_indicator_const_le, WithTop.some, LE.le.trans, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
⊢ ∫⁻ (a : α), s.indicator 1 a ∂μ = (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
(lintegral_indicator_const₀ hs _).trans <| one_mul _

Premises used: ENNReal.ofNNReal, WithTop.some, MeasureTheory.lintegral_indicator_const₀, one_mul, Eq.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α), s.indicator 1 a ∂μ = (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ = ν
x : α → ℝ≥0∞
h_1 : Measurable x
rw rw₁ : ∫⁻ (a : α), x a ∂ν = ∫⁻ (a : α), x a ∂ν
⊢ ∫⁻ (a : α), x a ∂μ = ∫⁻ (a : α), x a ∂ν

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
refine : (∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν) → μ = ν
⊢ μ = ν ↔ ∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν

Tactic:
refine ⟨fun h _ _ ↦ by rw [h], ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν
h₁ :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν
s : Set α
hs : MeasurableSet s
h₁ : ∫⁻ (a : α), s.indicator 1 a ∂μ = ∫⁻ (a : α), s.indicator 1 a ∂ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [← lintegral_indicator_one hs]

Premises used: MeasureTheory.lintegral_indicator_one
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α), s.indicator 1 a ∂μ = ∫⁻ (a : α), s.indicator 1 a ∂ν

Tactic:
h (s.indicator 1) ((measurable_indicator_const_iff 1).mpr hs)

Premises used: Iff.mpr, Set.indicator, measurable_indicator_const_iff, OfNat.ofNat