awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
s : Set α
rw : ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (a : α) in g ⁻¹' g '' s, f (g a) ∂μ
rw₁ rw₂ : ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (a : α) in s, f (g a) ∂μ
⊢ ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (b : β) in g '' s, f b ∂ν

Tactic:
rw [← hg.setLIntegral_comp_preimage_emb hge, Set.preimage_image_eq _ hge.injective]

Premises used: MeasurableEmbedding.injective, Set.preimage_image_eq, MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
rcases :
  ∀ (φ : α → ℝ≥0∞) (hφm : Measurable φ) (hφ_le : φ ≤ f) (hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ),
    ∫⁻ (a : α), f a ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞) ≤
      ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), f a ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞) ≤
    ∫⁻ (a : α), g a ∂μ

Tactic:
rcases exists_measurable_le_lintegral_eq μ f with ⟨φ, hφm, hφ_le, hφ_eq⟩

Premises used: MeasureTheory.exists_measurable_le_lintegral_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
rw rw₁ :
  ∫⁻ (a : α), φ a ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞) =
    ∫⁻ (x : α), φ x ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞)
⊢ ∫⁻ (x : α), f x ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞) =
    ∫⁻ (x : α), φ x ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞)

Tactic:
rw [hφ_eq]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
bc : ∀ (a : α), φ a ≤ f a
⊢ ∫⁻ (x : α), φ x ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞) ≤
    ∫⁻ (x : α), φ x ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | φ x + ε ≤ g x} : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
a : α
⊢ φ a ≤ f a

Tactic:
hφ_le _
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
a : α
⊢ φ a ≤ f a

Tactic:
exact hφ_le _
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
hs : NullMeasurableSet {x : α | φ x + ε ≤ g x} μ
⊢ ∫⁻ (x : α), φ x ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | φ x + ε ≤ g x} : ℝ≥0∞) =
    ∫⁻ (x : α), φ x + indicator {x : α | φ x + ε ≤ g x} (fun (x : α) ↦ ε) x ∂μ

Tactic:
rw [lintegral_add_left hφm, lintegral_indicator₀, setLIntegral_const]

Premises used: MeasureTheory.lintegral_add_left, MeasureTheory.setLIntegral_const, MeasureTheory.lintegral_indicator₀
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ NullMeasurableSet {x : α | φ x + ε ≤ g x} μ

Tactic:
measurableSet_le (hφm.nullMeasurable.measurable'.add_const _) hg.nullMeasurable

Premises used: MeasureTheory.NullMeasurable.measurable', AEMeasurable.nullMeasurable, measurableSet_le, setOf, MeasureTheory.NullMeasurableSet, Measurable.nullMeasurable, Measurable.add_const, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ NullMeasurableSet {x : α | φ x + ε ≤ g x} μ

Tactic:
exact measurableSet_le (hφm.nullMeasurable.measurable'.add_const _) hg.nullMeasurable

Premises used: MeasureTheory.NullMeasurable.measurable', AEMeasurable.nullMeasurable, measurableSet_le, Measurable.nullMeasurable, Measurable.add_const
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (x : α), φ x + indicator {x : α | φ x + ε ≤ g x} (fun (x : α) ↦ ε) x ∂μ ≤ ∫⁻ (x : α), g x ∂μ

Tactic:
lintegral_mono_ae (hle.mono fun x hx₁ => ?_)

Premises used: MeasureTheory.lintegral_mono_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
f₁ : ∀ (x : α) (hx₁ : f x ≤ g x), φ x + indicator {x : α | φ x + ε ≤ g x} (fun (x : α) ↦ ε) x ≤ g x
⊢ ∫⁻ (a : α), f a ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞) ≤
    ∫⁻ (a : α), g a ∂μ

Tactic:
calc
    ∫⁻ x, f x ∂μ + ε * μ { x | f x + ε ≤ g x } = ∫⁻ x, φ x ∂μ + ε * μ { x | f x + ε ≤ g x } := by
      rw [hφ_eq]
    _ ≤ ∫⁻ x, φ x ∂μ + ε * μ { x | φ x + ε ≤ g x } := by
      gcongr
      exact hφ_le _
    _ = ∫⁻ x, φ x + indicator { x | φ x + ε ≤ g x } (fun _ => ε) x ∂μ := by
      rw [lintegral_add_left hφm, lintegral_indicator₀, setLIntegral_const]
      exact measurableSet_le (hφm.nullMeasurable.measurable'.add_const _) hg.nullMeasurable
    _ ≤ ∫⁻ x, g x ∂μ := lintegral_mono_ae (hle.mono fun x hx₁ => ?_)

Premises used: setOf, MeasureTheory.lintegral_mono_ae, LE.le, Filter.Eventually.mono, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
simp : (φ x + if Membership.mem (γ := Set α) {x : α | φ x + ε ≤ g x} x then ε else 0) ≤ g x
⊢ φ x + indicator {x : α | φ x + ε ≤ g x} (fun (x : α) ↦ ε) x ≤ g x

Tactic:
simp only [indicator_apply]

Premises used: Set.indicator_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
pos : ∀ (hx₂ : Membership.mem (γ := Set α) {x : α | φ x + ε ≤ g x} x), φ x + ε ≤ g x
neg : ∀ (hx₂ : x ∉ {x : α | φ x + ε ≤ g x}), φ x + 0 ≤ g x
⊢ (φ x + if Membership.mem (γ := Set α) {x : α | φ x + ε ≤ g x} x then ε else 0) ≤ g x

Tactic:
split_ifs with hx₂
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
hx₂ : Membership.mem (γ := Set α) {x : α | φ x + ε ≤ g x} x
⊢ φ x + ε ≤ g x

Tactic:
hx₂

Premises used: Set.Mem, setOf
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
hx₂ : x ∉ {x : α | φ x + ε ≤ g x}
⊢ φ x + 0 ≤ g x

Tactic:
(add_zero _).trans_le <| (hφ_le x).trans hx₁

Premises used: Eq.trans_le, LE.le.trans, add_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
hx₂ : Membership.mem (γ := Set α) {x : α | φ x + ε ≤ g x} x
⊢ φ x + ε ≤ g x

Tactic:
exacts [hx₂, (add_zero _).trans_le <| (hφ_le x).trans hx₁]

Premises used: Eq.trans_le, LE.le.trans, add_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
ε : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
simpa only [lintegral_zero, zero_add] using
    lintegral_add_mul_meas_add_le_le_lintegral (ae_of_all _ fun x => zero_le) hf ε

Premises used: zero_le, MeasureTheory.lintegral_zero, zero_add, MeasureTheory.ae_of_all, MeasureTheory.lintegral_add_mul_meas_add_le_le_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
mul_meas_ge_le_lintegral₀ hf.aemeasurable ε

Premises used: Measurable.aemeasurable, MeasureTheory.mul_meas_ge_le_lintegral₀
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : ∀ x ∈ s, 1 ≤ f x
apply :
  (μ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | 1 ≤ f x} : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
apply le_trans _ (mul_meas_ge_le_lintegral₀ hf 1)

Premises used: MeasureTheory.mul_meas_ge_le_lintegral₀, OfNat.ofNat, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : ∀ x ∈ s, 1 ≤ f x
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | 1 ≤ f x} : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | 1 ≤ f x} : ℝ≥0∞)

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : ∀ x ∈ s, 1 ≤ f x
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | 1 ≤ f x} : ℝ≥0∞)

Tactic:
measure_mono hs

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : ∀ x ∈ s, 1 ≤ f x
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | 1 ≤ f x} : ℝ≥0∞)

Tactic:
exact measure_mono hs

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
apply : ∀ (x : α), f x ≤ s.indicator 1 x
⊢ ∫⁻ (a : α), f a ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
apply (lintegral_mono (fun x ↦ ?_)).trans (lintegral_indicator_one_le s)

Premises used: MeasureTheory.lintegral_indicator_one_le, MeasureTheory.lintegral_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
pos : ∀ (hx : x ∈ s), f x ≤ s.indicator 1 x
neg : ∀ (hx : x ∉ s), f x ≤ s.indicator 1 x
⊢ f x ≤ s.indicator 1 x

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
hx : x ∈ s
⊢ f x ≤ s.indicator 1 x

Tactic:
simpa [hx] using hf x
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
hx : x ∉ s
⊢ f x ≤ s.indicator 1 x

Tactic:
simpa [hx] using h'f x hx
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
rw : ∫⁻ (a : α), s.indicator f a ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) t
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) t

Tactic:
rw [← lintegral_indicator hs]

Premises used: MeasureTheory.lintegral_indicator
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
⊢ ∀ a ∈ tᶜ, s.indicator f a = 0

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
refine : ∀ (a : α), s.indicator f a ≤ 1
⊢ ∫⁻ (a : α), s.indicator f a ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) t

Tactic:
refine lintegral_le_meas (fun a ↦ ?_) (by simp_all)

Premises used: MeasureTheory.lintegral_le_meas
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
pos : ∀ (has : a ∈ s), s.indicator f a ≤ 1
neg : ∀ (has : a ∉ s), s.indicator f a ≤ 1
⊢ s.indicator f a ≤ 1

Tactic:
by_cases has : a ∈ s
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
has : a ∈ s
pos : ∀ (hat : a ∈ t), s.indicator f a ≤ 1
neg : ∀ (hat : a ∉ t), s.indicator f a ≤ 1
⊢ s.indicator f a ≤ 1

Tactic:
by_cases hat : a ∈ t
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
pos : ∀ (has : a ∈ s) (hat : a ∈ t), s.indicator f a ≤ 1
neg : ∀ (has : a ∈ s) (hat : a ∉ t), s.indicator f a ≤ 1
neg₁ : ∀ (has : a ∉ s), s.indicator f a ≤ 1
⊢ s.indicator f a ≤ 1

Tactic:
by_cases has : a ∈ s <;> [by_cases hat : a ∈ t; skip]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
has : a ∈ s
hat : a ∈ t
⊢ s.indicator f a ≤ 1

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
has : a ∈ s
hat : a ∉ t
⊢ s.indicator f a ≤ 1

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
has : a ∉ s
⊢ s.indicator f a ≤ 1

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hμf : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∞ = HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ∞ ≤ f x} : ℝ≥0∞)

Tactic:
simp [hμf]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
hμf : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | f a = ∞} ∩ s) : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x = ∞} : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x = ∞} : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x = ∞} : ℝ≥0∞)

Tactic:
rw [← setOf_inter_eq_sep]

Premises used: Set.setOf_inter_eq_sep
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
hμf : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | f a = ∞} ∩ s) : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x = ∞} : ℝ≥0∞)

Tactic:
Measure.le_restrict_apply _ _

Premises used: MeasureTheory.Measure.le_restrict_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
hμf : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | f a = ∞} ∩ s) : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x = ∞} : ℝ≥0∞)

Tactic:
exact Measure.le_restrict_apply _ _

Premises used: MeasureTheory.Measure.le_restrict_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hμf : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
of_not_not fun h => hμf <| lintegral_eq_top_of_measure_eq_top_ne_zero hf h

Premises used: MeasureTheory.lintegral_eq_top_of_measure_eq_top_ne_zero, of_not_not
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
hμf : ∫⁻ (x : α) in s, f x ∂μ ≠ ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
of_not_not fun h => hμf <| setLIntegral_eq_top_of_measure_eq_top_ne_zero hf h

Premises used: MeasureTheory.setLIntegral_eq_top_of_measure_eq_top_ne_zero, of_not_not
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε ≠ ∞
rw : HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) ≤ ∫⁻ (a : α), f a ∂μ
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) ε ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε ≠ ∞
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
mul_meas_ge_le_lintegral₀ hf ε

Premises used: MeasureTheory.mul_meas_ge_le_lintegral₀
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε ≠ ∞
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
exact mul_meas_ge_le_lintegral₀ hf ε

Premises used: MeasureTheory.mul_meas_ge_le_lintegral₀
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a + (↑n : ℝ≥0∞)⁻¹ ≤ g a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, g x < f x + (↑n : ℝ≥0∞)⁻¹

Tactic:
simp only [ae_iff, not_lt]

Premises used: MeasureTheory.ae_iff, not_lt
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
⊢ ∫⁻ (x : α), f x ∂μ +
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞)⁻¹ : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + (↑n : ℝ≥0∞)⁻¹ ≤ g x} : ℝ≥0∞) ≤
    ∫⁻ (x : α), f x ∂μ

Tactic:
have : ∫⁻ x, f x ∂μ + (↑n)⁻¹ * μ { x : α | f x + (n : ℝ≥0∞)⁻¹ ≤ g x } ≤ ∫⁻ x, f x ∂μ :=
      (lintegral_add_mul_meas_add_le_le_lintegral hfg hg n⁻¹).trans hgf
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
this :
  ∫⁻ (x : α), f x ∂μ +
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞)⁻¹ : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + (↑n : ℝ≥0∞)⁻¹ ≤ g x} : ℝ≥0∞) ≤
    ∫⁻ (x : α), f x ∂μ
⊢ Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞)⁻¹ 0 ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + (↑n : ℝ≥0∞)⁻¹ ≤ g x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [(ENNReal.cancel_of_ne hf).add_le_iff_nonpos_right, nonpos_iff_eq_zero, mul_eq_zero] at this

Premises used: ENNReal.cancel_of_ne, mul_eq_zero, AddLECancellable.add_le_iff_nonpos_right, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
this :
  Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞)⁻¹ 0 ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + (↑n : ℝ≥0∞)⁻¹ ≤ g x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a + (↑n : ℝ≥0∞)⁻¹ ≤ g a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
this.resolve_left (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))

Premises used: Iff.mpr, ENNReal.natCast_ne_top, setOf, Or.resolve_left, ENNReal.inv_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
this :
  Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞)⁻¹ 0 ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + (↑n : ℝ≥0∞)⁻¹ ≤ g x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a + (↑n : ℝ≥0∞)⁻¹ ≤ g a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact this.resolve_left (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))

Premises used: Iff.mpr, ENNReal.natCast_ne_top, Or.resolve_left, ENNReal.inv_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n : ℝ≥0∞)⁻¹

Tactic:
have : ∀ n : ℕ, ∀ᵐ x ∂μ, g x < f x + (n : ℝ≥0∞)⁻¹ := by
    intro n
    simp only [ae_iff, not_lt]
    have : ∫⁻ x, f x ∂μ + (↑n)⁻¹ * μ { x : α | f x + (n : ℝ≥0∞)⁻¹ ≤ g x } ≤ ∫⁻ x, f x ∂μ :=
      (lintegral_add_mul_meas_add_le_le_lintegral hfg hg n⁻¹).trans hgf
    rw [(ENNReal.cancel_of_ne hf).add_le_iff_nonpos_right, nonpos_iff_eq_zero, mul_eq_zero] at this
    exact this.resolve_left (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))