awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n : ℝ≥0∞)⁻¹
⊢ f =ᶠ[ae μ] g

Tactic:
hfg.mp ((ae_all_iff.2 this).mono fun x hlt hle => hle.antisymm ?_)

Premises used: Iff.mpr, LE.le.antisymm, Filter.EventuallyEq, Filter.Eventually.mono, Filter.Eventually.mp, MeasureTheory.ae_all_iff
-- 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 ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n : ℝ≥0∞)⁻¹
refine : ∀ (x : α) (hlt : ∀ (i : ℕ), g x < f x + (↑i : ℝ≥0∞)⁻¹) (hle : f x ≤ g x), g x ≤ f x
⊢ f =ᶠ[ae μ] g

Tactic:
refine hfg.mp ((ae_all_iff.2 this).mono fun x hlt hle => hle.antisymm ?_)

Premises used: Iff.mpr, LE.le.antisymm, Filter.Eventually.mono, Filter.Eventually.mp, MeasureTheory.ae_all_iff
-- 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 ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n : ℝ≥0∞)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i : ℝ≥0∞)⁻¹
hle : f x ≤ g x
suffices : Tendsto (fun (n : ℕ) ↦ f x + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 (f x))
⊢ g x ≤ f x

Tactic:
suffices Tendsto (fun n : ℕ => f x + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (f x)) from
    ge_of_tendsto' this fun i => (hlt i).le
-- 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 ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n : ℝ≥0∞)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i : ℝ≥0∞)⁻¹
hle : f x ≤ g x
⊢ Tendsto (fun (n : ℕ) ↦ f x + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 (f x))

Tactic:
simpa only [inv_top, add_zero] using
    tendsto_const_nhds.add (tendsto_inv_iff.2 ENNReal.tendsto_nat_nhds_top)

Premises used: Iff.mpr, tendsto_inv_iff, tendsto_const_nhds, ENNReal.tendsto_nat_nhds_top, Filter.Tendsto.add, ENNReal.inv_top, add_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h_le : f ≤ᶠ[ae μ] g
h : ∃ᵐ (x : α) ∂μ, f x ≠ g x
contrapose! : ∀ (h : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ), ∀ᵐ (x : α) ∂μ, f x = g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

Tactic:
contrapose! h
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h_le : f ≤ᶠ[ae μ] g
h : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ ∀ᵐ (x : α) ∂μ, f x = g x

Tactic:
ae_eq_of_ae_le_of_lintegral_le h_le hfi hg h

Premises used: Filter.EventuallyEq, MeasureTheory.ae_eq_of_ae_le_of_lintegral_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h_le : f ≤ᶠ[ae μ] g
h : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ ∀ᵐ (x : α) ∂μ, f x = g x

Tactic:
exact ae_eq_of_ae_le_of_lintegral_le h_le hfi hg h

Premises used: MeasureTheory.ae_eq_of_ae_le_of_lintegral_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h_le : f ≤ᶠ[ae μ] g
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

Tactic:
lintegral_strict_mono_of_ae_le_of_frequently_ae_lt hg hfi h_le <|
    ((frequently_ae_mem_iff.2 hμs).and_eventually h).mono fun _x hx => (hx.2 hx.1).ne

Premises used: Iff.mpr, MeasureTheory.frequently_ae_mem_iff, Filter.Frequently.mono, Filter.Frequently.and_eventually, MeasureTheory.lintegral_strict_mono_of_ae_le_of_frequently_ae_lt, And.right, And.left, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : μ ≠ 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Ne, ← Measure.measure_univ_eq_zero] at hμ

Premises used: Ne, MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : μ ≠ 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
hμ₁ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ AEMeasurable g μ

Tactic:
rw [Ne, ← Measure.measure_univ_eq_zero] at hμ

Premises used: Ne, MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : μ ≠ 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
hμ₁ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
hg₁ : AEMeasurable g μ
⊢ ∫⁻ (x : α), f x ∂μ ≠ ∞

Tactic:
rw [Ne, ← Measure.measure_univ_eq_zero] at hμ

Premises used: Ne, MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : μ ≠ 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
hμ₁ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
hg₁ : AEMeasurable g μ
hfi₁ : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, f x < g x

Tactic:
rw [Ne, ← Measure.measure_univ_eq_zero] at hμ

Premises used: Ne, MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

Tactic:
lintegral_strict_mono_of_ae_le_of_ae_lt_on hg hfi (ae_le_of_ae_lt h) hμ ?_

Premises used: MeasureTheory.ae_le_of_ae_lt, MeasureTheory.lintegral_strict_mono_of_ae_le_of_ae_lt_on
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
refine : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) univ x → f x < g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

Tactic:
refine lintegral_strict_mono_of_ae_le_of_ae_lt_on hg hfi (ae_le_of_ae_lt h) hμ ?_

Premises used: MeasureTheory.ae_le_of_ae_lt, MeasureTheory.lintegral_strict_mono_of_ae_le_of_ae_lt_on
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) univ x → f x < g x

Tactic:
simpa using h
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hg : Measurable g
hfi : ∫⁻ (x : α) in s, f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x
⊢ μ.restrict s ≠ 0

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h2f : ∫⁻ (x : α), f x ∂μ ≠ ∞
simp_rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, f x < ∞

Tactic:
simp_rw [ae_iff, ENNReal.not_lt_top]

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

Tactic:
measure_eq_top_of_lintegral_ne_top hf h2f

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

Tactic:
exact measure_eq_top_of_lintegral_ne_top hf h2f

Premises used: MeasureTheory.measure_eq_top_of_lintegral_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, f x < ∞

Tactic:
ae_lt_top' hf.aemeasurable h2f

Premises used: Measurable.aemeasurable, MeasureTheory.ae_lt_top'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
simp_rw : ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
simp_rw [← ofReal_norm]

Premises used: ofReal_norm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ

Tactic:
lintegral_mono fun x => ENNReal.ofReal_le_ofReal ?_

Premises used: ENNReal.ofReal_le_ofReal, MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
refine : ∀ (x : α), f x ≤ ‖f x‖
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ

Tactic:
refine lintegral_mono fun x => ENNReal.ofReal_le_ofReal ?_

Premises used: ENNReal.ofReal_le_ofReal, MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ f x ≤ |f x|

Tactic:
le_abs_self (f x)

Premises used: le_abs_self
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ f x ≤ |f x|

Tactic:
exact le_abs_self (f x)

Premises used: le_abs_self
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᶠ[ae μ] f
h : (ae μ).EventuallyEq (β := ENNReal) (fun (a : α) ↦ ‖f a‖ₑ) fun (a : α) ↦ ENNReal.ofReal (f a)
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᶠ[ae μ] f
h : ∀ (x : α) (hx : 0 x ≤ f x), ‖f x‖ₑ = ENNReal.ofReal (f x)
⊢ (ae μ).EventuallyEq (β := ENNReal) (fun (a : α) ↦ ‖f a‖ₑ) fun (a : α) ↦ ENNReal.ofReal (f a)

Tactic:
filter_upwards [h_nonneg] with x hx
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᶠ[ae μ] f
x : α
hx : 0 x ≤ f x
h h₁ : ENNReal.ofReal (f x) = ENNReal.ofReal (f x)
⊢ ‖f x‖ₑ = ENNReal.ofReal (f x)

Tactic:
rw [Real.enorm_eq_ofReal hx]

Premises used: Real.enorm_eq_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ f
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
lintegral_enorm_of_ae_nonneg <| .of_forall h_nonneg

Premises used: Filter.Eventually.of_forall, MeasureTheory.lintegral_enorm_of_ae_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
h_le : g ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ

Tactic:
ENNReal.eq_sub_of_add_eq hg_fin ?_

Premises used: ENNReal.eq_sub_of_add_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
h_le : g ≤ᶠ[ae μ] f
refine : ∫⁻ (a : α), f a - g a ∂μ + ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ
⊢ ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ

Tactic:
refine ENNReal.eq_sub_of_add_eq hg_fin ?_

Premises used: ENNReal.eq_sub_of_add_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
h_le : g ≤ᶠ[ae μ] f
rw : ∫⁻ (a : α), f a - g a + g a ∂μ = ∫⁻ (a : α), f a ∂μ
⊢ ∫⁻ (a : α), f a - g a ∂μ + ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ

Tactic:
rw [← lintegral_add_right' _ hg]

Premises used: MeasureTheory.lintegral_add_right'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
h_le : g ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), f a - g a + g a ∂μ = ∫⁻ (a : α), f a ∂μ

Tactic:
lintegral_congr_ae (h_le.mono fun x hx => tsub_add_cancel_of_le hx)

Premises used: tsub_add_cancel_of_le, MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
h_le : g ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), f a - g a + g a ∂μ = ∫⁻ (a : α), f a ∂μ

Tactic:
exact lintegral_congr_ae (h_le.mono fun x hx => tsub_add_cancel_of_le hx)

Premises used: tsub_add_cancel_of_le, MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : Measurable g
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
h_le : g ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ

Tactic:
lintegral_sub' hg.aemeasurable hg_fin h_le

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_sub'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
rw : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ
⊢ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ

Tactic:
rw [tsub_le_iff_right]

Premises used: tsub_le_iff_right
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
pos : ∀ (hfi : ∫⁻ (x : α), f x ∂μ = ∞), ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ
neg : ∀ (hfi : ¬∫⁻ (x : α), f x ∂μ = ∞), ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ

Tactic:
by_cases hfi : ∫⁻ x, f x ∂μ = ∞
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ = ∞
pos : ∫⁻ (x : α), g x ∂μ ≤ ∞
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ

Tactic:
rw [hfi, add_top]

Premises used: add_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ = ∞
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∞

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ = ∞
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∞

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ¬∫⁻ (x : α), f x ∂μ = ∞
neg : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (a : α), g a - f a + f a ∂μ
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ

Tactic:
rw [← lintegral_add_right' _ hf]

Premises used: MeasureTheory.lintegral_add_right'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ¬∫⁻ (x : α), f x ∂μ = ∞
neg : ∀ (x : α), g x ≤ g x - f x + f x
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (a : α), g a - f a + f a ∂μ

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ¬∫⁻ (x : α), f x ∂μ = ∞
x : α
⊢ g x ≤ g x - f x + f x

Tactic:
le_tsub_add

Premises used: le_tsub_add
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ¬∫⁻ (x : α), f x ∂μ = ∞
x : α
⊢ g x ≤ g x - f x + f x

Tactic:
exact le_tsub_add

Premises used: le_tsub_add
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ

Tactic:
lintegral_sub_le' f g hf.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_sub_le'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono_1 : ∀ (n : ℕ), f n.succ ≤ᶠ[ae μ] f n
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
fn_le_f0 : ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f n.succ a ≤ f n a
a : α
h : ∀ (n : ℕ), f n.succ a ≤ f n a
⊢ f 0 a ≤ f 0 a

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono_1 : ∀ (n : ℕ), f n.succ ≤ᶠ[ae μ] f n
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
fn_le_f0 : ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f n.succ a ≤ f n a
a : α
h : ∀ (n : ℕ), f n.succ a ≤ f n a
n : ℕ
ih : f n a ≤ f 0 a
⊢ f (n + 1) a ≤ f 0 a

Tactic:
(h n).trans ih

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono_1 : ∀ (n : ℕ), f n.succ ≤ᶠ[ae μ] f n
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
fn_le_f0 : ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f n.succ a ≤ f n a
a : α
h : ∀ (n : ℕ), f n.succ a ≤ f n a
n : ℕ
ih : f n a ≤ f 0 a
⊢ f (n + 1) a ≤ f 0 a

Tactic:
exact (h n).trans ih

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono_1 : ∀ (n : ℕ), f n.succ ≤ᶠ[ae μ] f n
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
fn_le_f0 : ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f n.succ a ≤ f n a
n : ℕ
a : α
h : ∀ (n : ℕ), f n.succ a ≤ f n a
zero : f 0 a ≤ f 0 a
succ : ∀ (n : ℕ) (ih : f n a ≤ f 0 a), f (n + 1) a ≤ f 0 a
⊢ f n a ≤ f 0 a

Tactic:
induction n with
              | zero => rfl
              | succ n ih => exact (h n).trans ih
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_anti : Antitone f
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
lintegral_iInf_ae h_meas (fun n => ae_of_all _ <| h_anti n.le_succ) h_fin

Premises used: MeasureTheory.lintegral_iInf_ae, Nat.le_succ, MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
simp_rw : ∫⁻ (a : α), (⨅ (i : ℕ), f i) a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
simp_rw [← iInf_apply]

Premises used: iInf_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
⊢ ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x

Tactic:
have hp : ∀ᵐ x ∂μ, p x fun i => f i x := h_anti
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
pos : ∀ (hx : x ∈ aeSeqSet h_meas p), aeSeq h_meas p m x ≤ aeSeq h_meas p n x
neg : ∀ (hx : x ∉ aeSeqSet h_meas p), aeSeq h_meas p m x ≤ aeSeq h_meas p n x
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x

Tactic:
by_cases hx : x ∈ aeSeqSet h_meas p

Premises used: aeSeqSet
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∈ aeSeqSet h_meas p
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x

Tactic:
aeSeq.prop_of_mem_aeSeqSet h_meas hx hnm

Premises used: aeSeq.prop_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∈ aeSeqSet h_meas p
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x

Tactic:
exact aeSeq.prop_of_mem_aeSeqSet h_meas hx hnm

Premises used: aeSeq.prop_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∉ aeSeqSet h_meas p
neg : LE.le (α := ℝ≥0∞) (Nonempty.some ⋯) (Nonempty.some ⋯)
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x

Tactic:
simp only [aeSeq, hx, if_false]

Premises used: if_false, aeSeq