awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε' : Type u_5
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε'
inst_1 : TopologicalSpace ε''
inst_2 : ESeminormedAddMonoid ε''
f : α → ε'
g : α → ε''
hg : AEStronglyMeasurable g μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ + ‖g a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖g a‖ₑ ∂μ

Tactic:
lintegral_add_right' _ hg.enorm

Premises used: MeasureTheory.lintegral_add_right', MeasureTheory.AEStronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
⊢ ∫⁻ (a : α), ‖(-f) a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
inst : ENorm ε
x : MeasurableSpace α
f : α → ε
μ : Measure α
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
Iff.rfl

Premises used: Iff.rfl, MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
simp only [HasFiniteIntegral]

Premises used: MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ∞

Tactic:
simp only [hasFiniteIntegral_iff_enorm, ofReal_norm]

Premises used: ofReal_norm, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), edist (f a) 0 ∂μ < ∞

Tactic:
simp only [hasFiniteIntegral_iff_norm, edist_dist, dist_zero_right]

Premises used: edist_dist, MeasureTheory.hasFiniteIntegral_iff_norm, dist_zero_right
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : 0 ≤ᶠ[ae μ] f
rw : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞
rw₁ rw₂ : ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ < ∞ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞

Tactic:
rw [hasFiniteIntegral_iff_enorm, lintegral_enorm_of_ae_nonneg h]

Premises used: MeasureTheory.lintegral_enorm_of_ae_nonneg, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ ↔ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ < ∞

Tactic:
simp [hasFiniteIntegral_iff_norm]

Premises used: MeasureTheory.hasFiniteIntegral_iff_norm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
ε' : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
hg : HasFiniteIntegral g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ
⊢ ∫⁻ (a : α), ‖g a‖ₑ ∂μ < ∞

Tactic:
simp only [hasFiniteIntegral_iff_enorm] at *

Premises used: MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
ε' : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ
hg : ∫⁻ (a : α), ‖g a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖g a‖ₑ ∂μ

Tactic:
lintegral_mono_ae h

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
ε' : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ
hg : ∫⁻ (a : α), ‖g a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), ‖g a‖ₑ ∂μ < ∞

Tactic:
hg
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
ε' : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ
hg : ∫⁻ (a : α), ‖g a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
calc
    (∫⁻ a, ‖f a‖ₑ ∂μ) ≤ ∫⁻ a : α, ‖g a‖ₑ ∂μ := lintegral_mono_ae h
    _ < ∞ := hg

Premises used: MeasureTheory.lintegral_mono_ae, ENorm.enorm, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : NormedAddCommGroup γ
f : α → β
g : α → γ
hg : HasFiniteIntegral g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
⊢ HasFiniteIntegral f μ

Tactic:
hg.mono_enorm <| h.mono fun _x hx ↦ enorm_le_iff_norm_le.mpr hx

Premises used: Iff.mpr, enorm_le_iff_norm_le, Filter.Eventually.mono, MeasureTheory.HasFiniteIntegral.mono_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
⊢ HasFiniteIntegral f μ

Tactic:
HasFiniteIntegral.mono hg ?_

Premises used: MeasureTheory.HasFiniteIntegral.mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
refine : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
⊢ HasFiniteIntegral f μ

Tactic:
refine HasFiniteIntegral.mono hg ?_

Premises used: MeasureTheory.HasFiniteIntegral.mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
h₁ : ∀ (a : α) (hn : 0 ≤ f a) (ha : f a ≤ g a), ‖f a‖ ≤ ‖g a‖
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖

Tactic:
filter_upwards [hnonneg, h] with a hn ha
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
a : α
hn : 0 ≤ f a
ha : f a ≤ g a
h₁ : |f a| ≤ |g a|
⊢ ‖f a‖ ≤ ‖g a‖

Tactic:
apply norm_le_norm_of_abs_le_abs

Premises used: norm_le_norm_of_abs_le_abs
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
a : α
hn : 0 ≤ f a
ha : f a ≤ g a
h₁ : f a ≤ |g a|
h₂ h₃ h₄ h₅ : f a ≤ g a
⊢ |f a| ≤ |g a|

Tactic:
rwa [abs_of_nonneg hn, abs_of_nonneg (hn.trans ha)]

Premises used: abs_of_nonneg, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
g : α → ℝ≥0∞
hg : HasFiniteIntegral g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ g a
⊢ HasFiniteIntegral f μ

Tactic:
hg.mono_enorm <| h.mono fun _x hx ↦ le_trans hx le_rfl

Premises used: le_rfl, Filter.Eventually.mono, MeasureTheory.HasFiniteIntegral.mono_enorm, le_trans
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
g : α → ℝ
hg : HasFiniteIntegral g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a
⊢ HasFiniteIntegral f μ

Tactic:
hg.mono <| h.mono fun _x hx => le_trans hx (le_abs_self _)

Premises used: le_abs_self, MeasureTheory.HasFiniteIntegral.mono, Filter.Eventually.mono, le_trans
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
ε' : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
hf : HasFiniteIntegral f μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ
⊢ HasFiniteIntegral g μ

Tactic:
hf.mono_enorm <| EventuallyEq.le <| EventuallyEq.symm h

Premises used: Filter.EventuallyEq.le, MeasureTheory.HasFiniteIntegral.mono_enorm, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : NormedAddCommGroup γ
f : α → β
g : α → γ
hf : HasFiniteIntegral f μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖
⊢ HasFiniteIntegral g μ

Tactic:
hf.mono <| EventuallyEq.le <| EventuallyEq.symm h

Premises used: MeasureTheory.HasFiniteIntegral.mono, Filter.EventuallyEq.le, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
ε' : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ
⊢ HasFiniteIntegral f μ ↔ HasFiniteIntegral g μ

Tactic:
⟨fun hf => hf.congr'_enorm h, fun hg => hg.congr'_enorm <| EventuallyEq.symm h⟩

Premises used: MeasureTheory.HasFiniteIntegral.congr'_enorm, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : NormedAddCommGroup γ
f : α → β
g : α → γ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖
⊢ HasFiniteIntegral f μ ↔ HasFiniteIntegral g μ

Tactic:
⟨fun hf => hf.congr' h, fun hg => hg.congr' <| EventuallyEq.symm h⟩

Premises used: MeasureTheory.HasFiniteIntegral.congr', Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f g : α → ε
hf : HasFiniteIntegral f μ
h : f =ᶠ[ae μ] g
⊢ HasFiniteIntegral g μ

Tactic:
hf.congr'_enorm <| h.fun_comp enorm

Premises used: MeasureTheory.HasFiniteIntegral.congr'_enorm, ENorm.enorm, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f g : α → ε
h : f =ᶠ[ae μ] g
⊢ HasFiniteIntegral f μ ↔ HasFiniteIntegral g μ

Tactic:
hasFiniteIntegral_congr'_enorm <| h.fun_comp enorm

Premises used: MeasureTheory.hasFiniteIntegral_congr'_enorm, ENorm.enorm, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
c : ε
hc : ‖c‖ₑ ≠ ∞
⊢ HasFiniteIntegral.{u_1, u_4} (ε := ε) (fun (x : α) ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ

Tactic:
simpa [hasFiniteIntegral_iff_enorm, lt_top_iff_ne_top, ENNReal.mul_eq_top,
    or_iff_not_imp_left, isFiniteMeasure_iff] using fun h h' ↦ (hc h').elim

Premises used: MeasureTheory.isFiniteMeasure_iff, False.elim, lt_top_iff_ne_top, ENNReal.mul_eq_top, Classical.or_iff_not_imp_left, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
c : β
⊢ HasFiniteIntegral.{u_1, u_2} (ε := β) (fun (x : α) ↦ c) μ ↔ c = 0 ∨ IsFiniteMeasure μ

Tactic:
simp [hasFiniteIntegral_const_iff_enorm enorm_ne_top]

Premises used: MeasureTheory.hasFiniteIntegral_const_iff_enorm, enorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
c : ε
hc : ‖c‖ₑ ≠ 0
hc' : ‖c‖ₑ ≠ ∞
⊢ HasFiniteIntegral.{u_1, u_4} (ε := ε) (fun (x : α) ↦ c) μ ↔ IsFiniteMeasure μ

Tactic:
simp [hasFiniteIntegral_const_iff_enorm hc', hc, isFiniteMeasure_iff]

Premises used: MeasureTheory.isFiniteMeasure_iff, MeasureTheory.hasFiniteIntegral_const_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
c : β
hc : c ≠ 0
⊢ HasFiniteIntegral.{u_1, u_2} (ε := β) (fun (x : α) ↦ c) μ ↔ IsFiniteMeasure μ

Tactic:
hasFiniteIntegral_const_iff_isFiniteMeasure_enorm (enorm_ne_zero.mpr hc) enorm_ne_top

Premises used: Iff.mpr, enorm_ne_zero, MeasureTheory.hasFiniteIntegral_const_iff_isFiniteMeasure_enorm, enorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
inst_1 : IsFiniteMeasure μ
c : ε
hc : ‖c‖ₑ ≠ ∞
⊢ HasFiniteIntegral.{u_1, u_4} (ε := ε) (fun (x : α) ↦ c) μ

Tactic:
(hasFiniteIntegral_const_iff_enorm hc).2 <| .inr ‹_›

Premises used: Iff.mpr, MeasureTheory.hasFiniteIntegral_const_iff_enorm, Or.inr
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
c : β
⊢ HasFiniteIntegral.{u_1, u_2} (ε := β) (fun (x : α) ↦ c) μ

Tactic:
hasFiniteIntegral_const_iff.2 <| .inr ‹_›

Premises used: Iff.mpr, MeasureTheory.hasFiniteIntegral_const_iff, Or.inr
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
⊢ ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ∞

Tactic:
simp [ha, hb]
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
⊢ ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ∞

Tactic:
have : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ⊤ := by simp [ha, hb]
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
this : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ∞
apply : ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ
⊢ HasFiniteIntegral X μ

Tactic:
apply (hasFiniteIntegral_const_enorm this (μ := μ)).mono'_enorm

Premises used: MeasureTheory.HasFiniteIntegral.mono'_enorm, MeasureTheory.hasFiniteIntegral_const_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
this : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ∞
ω : α
h₁ : a ≤ X ω
h₂ : X ω ≤ b
⊢ ‖X ω‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ

Tactic:
simp [h₂]
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
this : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ∞
h₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ a ≤ X x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ X x ≤ b) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a_4 : α) ↦ ‖X a_4‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ) x} x}
            x}
      a_1
h₂ h₃ : ∀ (ω : α) (h₁ : a ≤ X ω) (h₂ : X ω ≤ b), ‖X ω‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ

Tactic:
filter_upwards [h.mono fun ω h ↦ h.1, h.mono fun ω h ↦ h.2] with ω h₁ h₂ using by simp [h₂]

Premises used: Filter.Eventually.mono, And.right, And.left
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ
X : α → ℝ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
apply : ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ ≤ max ‖a‖ ‖b‖
⊢ HasFiniteIntegral X μ

Tactic:
apply (hasFiniteIntegral_const (max ‖a‖ ‖b‖)).mono'

Premises used: Norm.norm, MeasureTheory.HasFiniteIntegral.mono', MeasureTheory.hasFiniteIntegral_const, Max.max
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ
X : α → ℝ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
ω : α
⊢ a ≤ X ω → X ω ≤ b → ‖X ω‖ ≤ max ‖a‖ ‖b‖

Tactic:
abs_le_max_abs_abs

Premises used: abs_le_max_abs_abs
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ
X : α → ℝ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
h₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ a ≤ X x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ X x ≤ b) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a_4 : α) ↦ ‖X a_4‖ ≤ max ‖a‖ ‖b‖) x} x}
            x}
      a_1
h₂ h₃ : ∀ (ω : α), a ≤ X ω → X ω ≤ b → ‖X ω‖ ≤ max ‖a‖ ‖b‖
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ ≤ max ‖a‖ ‖b‖

Tactic:
filter_upwards [h.mono fun ω h ↦ h.1, h.mono fun ω h ↦ h.2] with ω using abs_le_max_abs_abs

Premises used: abs_le_max_abs_abs, Filter.Eventually.mono, And.right, And.left
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
inst_1 : IsFiniteMeasure μ
f : α → ε
C : ℝ≥0∞
hC' : ‖C‖ₑ ≠ ∞
hC : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ C
⊢ HasFiniteIntegral f μ

Tactic:
(hasFiniteIntegral_const_enorm hC').mono'_enorm hC

Premises used: MeasureTheory.HasFiniteIntegral.mono'_enorm, MeasureTheory.hasFiniteIntegral_const_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
C : ℝ
hC : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ C
⊢ HasFiniteIntegral f μ

Tactic:
(hasFiniteIntegral_const C).mono' hC

Premises used: MeasureTheory.HasFiniteIntegral.mono', MeasureTheory.hasFiniteIntegral_const
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
f : α → β
⊢ HasFiniteIntegral f μ

Tactic:
let ⟨_⟩ := nonempty_fintype α
  .of_bounded <| ae_of_all μ <| norm_le_pi_norm f

Premises used: _private.0.MeasureTheory.HasFiniteIntegral.of_finite.match_1, norm_le_pi_norm, MeasureTheory.HasFiniteIntegral.of_bounded, nonempty_fintype, MeasureTheory.ae_of_all, MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst : ENorm ε
f : α → ε
h : HasFiniteIntegral f ν
hμ : μ ≤ ν
⊢ HasFiniteIntegral f μ

Tactic:
lt_of_le_of_lt (lintegral_mono' hμ le_rfl) h

Premises used: lt_of_le_of_lt, le_rfl, MeasureTheory.lintegral_mono', MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst : ENorm ε
f : α → ε
hμ : HasFiniteIntegral f μ
hν : HasFiniteIntegral f ν
simp : ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ∞
⊢ HasFiniteIntegral f (μ + ν)

Tactic:
simp only [HasFiniteIntegral, lintegral_add_measure] at *

Premises used: MeasureTheory.lintegral_add_measure, MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst : ENorm ε
f : α → ε
hμ : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
hν : ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ∞

Tactic:
add_lt_top.2 ⟨hμ, hν⟩

Premises used: Iff.mpr, And.intro, ENNReal.add_lt_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst : ENorm ε
f : α → ε
hμ : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
hν : ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ∞

Tactic:
exact add_lt_top.2 ⟨hμ, hν⟩

Premises used: Iff.mpr, And.intro, ENNReal.add_lt_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst : ENorm ε
f : α → ε
h : HasFiniteIntegral f (μ + ν)
⊢ HasFiniteIntegral f μ

Tactic:
h.mono_measure <| Measure.le_add_right <| le_rfl

Premises used: le_rfl, MeasureTheory.HasFiniteIntegral.mono_measure, MeasureTheory.Measure.le_add_right
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst : ENorm ε
f : α → ε
h : HasFiniteIntegral f (μ + ν)
⊢ HasFiniteIntegral f ν

Tactic:
h.mono_measure <| Measure.le_add_left <| le_rfl

Premises used: le_rfl, MeasureTheory.HasFiniteIntegral.mono_measure, MeasureTheory.Measure.le_add_left
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst : ENorm ε
f : α → ε
⊢ HasFiniteIntegral f (μ + ν) ↔ HasFiniteIntegral f μ ∧ HasFiniteIntegral f ν

Tactic:
⟨fun h => ⟨h.left_of_add_measure, h.right_of_add_measure⟩, fun h => h.1.add_measure h.2⟩

Premises used: MeasureTheory.HasFiniteIntegral.right_of_add_measure, MeasureTheory.HasFiniteIntegral.left_of_add_measure, And.right, And.left, And.intro, Iff.intro, MeasureTheory.HasFiniteIntegral.add_measure
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
h : HasFiniteIntegral f μ
c : ℝ≥0∞
hc : c ≠ ∞
simp : c • ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
⊢ HasFiniteIntegral f (c • μ)

Tactic:
simp only [HasFiniteIntegral, lintegral_smul_measure] at *

Premises used: MeasureTheory.lintegral_smul_measure, MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
h : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
c : ℝ≥0∞
hc : c ≠ ∞
⊢ c • ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
mul_lt_top hc.lt_top h

Premises used: ENNReal.mul_lt_top, Ne.lt_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
h : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
c : ℝ≥0∞
hc : c ≠ ∞
⊢ c • ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
exact mul_lt_top hc.lt_top h

Premises used: ENNReal.mul_lt_top, Ne.lt_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε : Type u_4
inst : ENorm ε
m : MeasurableSpace α
f : α → ε
⊢ @HasFiniteIntegral _ _ _ m f 0

Tactic:
simp only [HasFiniteIntegral, lintegral_zero_measure, zero_lt_top]

Premises used: ENNReal.zero_lt_top, MeasureTheory.lintegral_zero_measure, MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
⊢ HasFiniteIntegral.{u_1, u_7} (ε := ε) (fun (x : α) ↦ 0) μ

Tactic:
simp [hasFiniteIntegral_iff_enorm]

Premises used: MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hfi : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (-f) μ

Tactic:
simpa [hasFiniteIntegral_iff_enorm] using hfi

Premises used: MeasureTheory.hasFiniteIntegral_iff_enorm