awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : IsOrderedAddMonoid β
f : α → β
hf : MemLp f 1 μ
⊢ MemLp.{u_1, u_8} (ε := β) (fun (a : α) ↦ |f a|) 1 μ

Tactic:
hf.abs

Premises used: abs, MeasureTheory.MemLp.abs
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : IsOrderedAddMonoid β
f : α → β
hf : MemLp f 1 μ
⊢ MemLp.{u_1, u_8} (ε := β) (fun (a : α) ↦ |f a|) 1 μ

Tactic:
exact hf.abs

Premises used: MeasureTheory.MemLp.abs
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : Integrable f μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
rw :
  ∀ (hf : MemLp f 1 μ) {g : α → R} (g_aestronglyMeasurable : AEStronglyMeasurable g μ)
    (ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞),
    MemLp.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ g x • f x) μ

Tactic:
rw [← memLp_one_iff_integrable] at *

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
⊢ MemLp.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ

Tactic:
⟨g_aestronglyMeasurable.smul hf.1, ?_⟩

Premises used: MeasureTheory.MemLp, And.left, And.intro, MeasureTheory.AEStronglyMeasurable.smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
refine : eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ < ∞
⊢ MemLp.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ

Tactic:
refine ⟨g_aestronglyMeasurable.smul hf.1, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
rwa rwa₁ rwa₂ rwa₃ : eLpNormEssSup g μ ≠ ∞
⊢ eLpNorm g ∞ μ ≠ ∞

Tactic:
rwa [eLpNorm_exponent_top]

Premises used: MeasureTheory.eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
⊢ eLpNorm g ∞ μ ≠ ∞

Tactic:
have hg' : eLpNorm g ∞ μ ≠ ∞ := by rwa [eLpNorm_exponent_top]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
hg' : eLpNorm g ∞ μ ≠ ∞
⊢ eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ ≤ eLpNorm g ∞ μ * eLpNorm f 1 μ

Tactic:
simpa using MeasureTheory.eLpNorm_smul_le_mul_eLpNorm hf.1 g_aestronglyMeasurable
        (p := ∞) (q := 1)

Premises used: MeasureTheory.eLpNorm_smul_le_mul_eLpNorm, And.left
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
hg' : eLpNorm g ∞ μ ≠ ∞
⊢ eLpNorm g ∞ μ * eLpNorm f 1 μ < ∞

Tactic:
ENNReal.mul_lt_top hg'.lt_top hf.2

Premises used: ENNReal.mul_lt_top, And.right, Ne.lt_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
R : Type u_8
inst_1 : NormedRing R
inst_2 : Module R β
inst_3 : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
hg' : MeasureTheory.eLpNorm g ∞ μ ≠ ∞
eLpNorm :
  MeasureTheory.eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ ≤
    MeasureTheory.eLpNorm g ∞ μ * MeasureTheory.eLpNorm f 1 μ
⊢ MeasureTheory.eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ g x • f x) 1 μ < ∞

Tactic:
calc
    eLpNorm (fun x : α => g x • f x) 1 μ ≤ _ := by
      simpa using MeasureTheory.eLpNorm_smul_le_mul_eLpNorm hf.1 g_aestronglyMeasurable
        (p := ∞) (q := 1)
    _ < ∞ := ENNReal.mul_lt_top hg'.lt_top hf.2

Premises used: ENNReal.mul_lt_top, And.right, Ne.lt_top, HSMul.hSMul, OfNat.ofNat, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : Integrable f μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
rw :
  ∀ (hf : MemLp f 1 μ) {g : α → β} (g_aestronglyMeasurable : AEStronglyMeasurable g μ)
    (ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞),
    MemLp.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ f x • g x) μ

Tactic:
rw [← memLp_one_iff_integrable] at *

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
⊢ MemLp.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ

Tactic:
⟨hf.1.smul g_aestronglyMeasurable, ?_⟩

Premises used: MeasureTheory.MemLp, And.left, And.intro, MeasureTheory.AEStronglyMeasurable.smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
refine : eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ < ∞
⊢ MemLp.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ

Tactic:
refine ⟨hf.1.smul g_aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
rwa rwa₁ rwa₂ rwa₃ : eLpNormEssSup g μ ≠ ∞
⊢ eLpNorm g ∞ μ ≠ ∞

Tactic:
rwa [eLpNorm_exponent_top]

Premises used: MeasureTheory.eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
⊢ eLpNorm g ∞ μ ≠ ∞

Tactic:
have hg' : eLpNorm g ∞ μ ≠ ∞ := by rwa [eLpNorm_exponent_top]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
hg' : eLpNorm g ∞ μ ≠ ∞
⊢ eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ ≤ eLpNorm f 1 μ * eLpNorm g ∞ μ

Tactic:
simpa using MeasureTheory.eLpNorm_smul_le_mul_eLpNorm g_aestronglyMeasurable hf.1
        (p := 1) (q := ∞)

Premises used: MeasureTheory.eLpNorm_smul_le_mul_eLpNorm, And.left
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
hg' : eLpNorm g ∞ μ ≠ ∞
⊢ eLpNorm f 1 μ * eLpNorm g ∞ μ < ∞

Tactic:
ENNReal.mul_lt_top hf.2 hg'.lt_top

Premises used: ENNReal.mul_lt_top, And.right, Ne.lt_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : Ne (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ) ∞
hg' : MeasureTheory.eLpNorm g ∞ μ ≠ ∞
eLpNorm :
  MeasureTheory.eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ ≤
    MeasureTheory.eLpNorm f 1 μ * MeasureTheory.eLpNorm g ∞ μ
⊢ MeasureTheory.eLpNorm.{u_1, u_2} (ε := β) (fun (x : α) ↦ f x • g x) 1 μ < ∞

Tactic:
calc
    eLpNorm (fun x : α => f x • g x) 1 μ ≤ _ := by
      simpa using MeasureTheory.eLpNorm_smul_le_mul_eLpNorm g_aestronglyMeasurable hf.1
        (p := 1) (q := ∞)
    _ < ∞ := ENNReal.mul_lt_top hf.2 hg'.lt_top

Premises used: ENNReal.mul_lt_top, And.right, Ne.lt_top, HSMul.hSMul, OfNat.ofNat, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
simp_rw :
  AEStronglyMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ∧ HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔
    AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
simp_rw₁ :
  AEStronglyMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ∧ HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔
    HasFiniteIntegral f μ
simp_rw₂ : HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔ HasFiniteIntegral f μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ ↔ Integrable f μ

Tactic:
simp_rw [Integrable, and_iff_right hf, and_iff_right hf.enorm.aestronglyMeasurable,
    hasFiniteIntegral_enorm_iff]

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.Integrable, and_iff_right, MeasureTheory.hasFiniteIntegral_enorm_iff, MeasureTheory.AEStronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
simp_rw :
  AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖) μ ∧ HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔
    AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
simp_rw₁ :
  AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖) μ ∧ HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔
    HasFiniteIntegral f μ
simp_rw₂ : HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔ HasFiniteIntegral f μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ ↔ Integrable f μ

Tactic:
simp_rw [Integrable, and_iff_right hf, and_iff_right hf.norm, hasFiniteIntegral_norm_iff]

Premises used: MeasureTheory.Integrable, and_iff_right, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.hasFiniteIntegral_norm_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
apply : ∀ (x : α), ‖f₀ x - f₁ x‖ ≤ g x → ‖f₁ x‖ ≤ ‖f₀ x‖ + g x
⊢ ∀ᵐ (a : α) ∂μ, ‖f₁ a‖ ≤ ‖f₀ a‖ + g a

Tactic:
apply h.mono

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
a : α
ha : ‖f₀ a - f₁ a‖ ≤ g a
⊢ ‖f₁ a‖ ≤ ‖f₀ a‖ + ‖f₀ a - f₁ a‖

Tactic:
norm_le_insert _ _

Premises used: norm_le_insert
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
a : α
ha : ‖f₀ a - f₁ a‖ ≤ g a
⊢ ‖f₀ a‖ + ‖f₀ a - f₁ a‖ ≤ ‖f₀ a‖ + g a

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
a : α
ha : ‖f₀ a - f₁ a‖ ≤ g a
a₁ : ‖f₀ a‖ + ‖f₀ a - f₁ a‖ ≤ ‖f₀ a‖ + g a
⊢ ‖f₁ a‖ ≤ ‖f₀ a‖ + g a

Tactic:
calc
      ‖f₁ a‖ ≤ ‖f₀ a‖ + ‖f₀ a - f₁ a‖ := norm_le_insert _ _
      _ ≤ ‖f₀ a‖ + g a := by gcongr

Premises used: norm_le_insert
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
h : ∀ (x : α) (hx1 : g₁ x ≤ f x) (hx2 : f x ≤ g₂ x), ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖

Tactic:
filter_upwards [h_le₁, h_le₂] with x hx1 hx2
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
x : α
hx1 : g₁ x ≤ f x
hx2 : f x ≤ g₂ x
⊢ |f x| ≤ max |g₁ x| |g₂ x|

Tactic:
abs_le_max_abs_abs hx1 hx2

Premises used: abs_le_max_abs_abs
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
x : α
hx1 : g₁ x ≤ f x
hx2 : f x ≤ g₂ x
⊢ |f x| ≤ max |g₁ x| |g₂ x|

Tactic:
exact abs_le_max_abs_abs hx1 hx2

Premises used: abs_le_max_abs_abs
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖

Tactic:
have : ∀ᵐ x ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖ := by
    filter_upwards [h_le₁, h_le₂] with x hx1 hx2
    simp only [Real.norm_eq_abs]
    exact abs_le_max_abs_abs hx1 hx2
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
h : ∀ (x : α) (hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖), ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
filter_upwards [this] with x hx
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
⊢ ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
hx.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
h : max ‖g₁ x‖ ‖g₂ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
⊢ ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
refine hx.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
⊢ 0 ≤ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
rw : ‖g₁ x‖ + ‖g₂ x‖
| ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
rw [Real.norm_of_nonneg (by positivity)]

Premises used: Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
h : max ‖g₁ x‖ ‖g₂ x‖ ≤ ‖g₁ x‖ + ‖g₂ x‖
⊢ max ‖g₁ x‖ ‖g₂ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
conv_rhs => rw [Real.norm_of_nonneg (by positivity)]

Premises used: Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
⊢ max ‖g₁ x‖ ‖g₂ x‖ ≤ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)

Premises used: max_le_add_of_nonneg, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
⊢ max ‖g₁ x‖ ‖g₂ x‖ ≤ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
exact max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)

Premises used: max_le_add_of_nonneg, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
have h_le_add : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖ := by
    filter_upwards [this] with x hx
    refine hx.trans ?_
    conv_rhs => rw [Real.norm_of_nonneg (by positivity)]
    exact max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
h_le_add : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ ‖g₁ a‖ + ‖g₂ a‖) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
h_le_add : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
⊢ Integrable f μ

Tactic:
exact Integrable.mono (by fun_prop) hf h_le_add

Premises used: MeasureTheory.Integrable.mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : NormedAddCommGroup γ
f : α → β
g : α → γ
hf : Integrable f μ
hg : Integrable g μ
⊢ AEStronglyMeasurable (β := β × γ) (fun (x : α) ↦ (f x, g x)) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
hq1 : 1 ≤ q
f : α → ε
inst_2 : IsFiniteMeasure μ
hfq : MemLp f q μ
⊢ Integrable f μ

Tactic:
memLp_one_iff_integrable.mp (hfq.mono_exponent hq1)

Premises used: MeasureTheory.MemLp.mono_exponent, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
⊢ ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [hε']
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
refine : ε⁻¹ ^ ENNReal.toReal 1 * eLpNorm f 1 μ ^ ENNReal.toReal 1 < ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine meas_ge_le_mul_pow_eLpNorm_enorm μ one_ne_zero one_ne_top hf.1 hε.ne' (by simp [hε'])
    |>.trans_lt ?_

Premises used: LT.lt.ne', And.left, MeasureTheory.meas_ge_le_mul_pow_eLpNorm_enorm, one_ne_zero, LE.le.trans_lt, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
a : ε⁻¹ ^ ENNReal.toReal 1 < ∞
a₁ : eLpNorm f 1 μ ^ ENNReal.toReal 1 < ∞
⊢ ε⁻¹ ^ ENNReal.toReal 1 * eLpNorm f 1 μ ^ ENNReal.toReal 1 < ∞

Tactic:
apply ENNReal.mul_lt_top

Premises used: ENNReal.mul_lt_top