awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
pos :
  ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) (fun (a : α) ↦ ‖g a‖ₑ) a ∂μ <
      ∞ ↔
    ∫⁻ (a : α), ‖(↑(f a) : ℝ) • g a‖ₑ ∂μ < ∞
pos₁ : AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ‖g a‖ₑ) (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
⊢ (∫⁻ (a : α), ‖g a‖ₑ ∂μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) < ∞ ↔ ∫⁻ (a : α), ‖(↑(f a) : ℝ) • g a‖ₑ ∂μ < ∞

Tactic:
rw [lintegral_withDensity_eq_lintegral_mul₀' hf.coe_nnreal_ennreal.aemeasurable]

Premises used: Measurable.aemeasurable, Measurable.coe_nnreal_ennreal, MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀'
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
⊢ ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) (fun (a : α) ↦ ‖g a‖ₑ) a ∂μ <
      ∞ ↔
    ∫⁻ (a : α), ‖(↑(f a) : ℝ) • g a‖ₑ ∂μ < ∞

Tactic:
simp [enorm_smul]

Premises used: enorm_smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ‖g a‖ₑ) (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))

Tactic:
simpa [aemeasurable_withDensity_ennreal_iff hf, enorm_smul] using H.enorm

Premises used: enorm_smul, MeasureTheory.aemeasurable_withDensity_ennreal_iff, MeasureTheory.AEStronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : ¬AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
⊢ Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ

Tactic:
simp only [Integrable, aestronglyMeasurable_withDensity_iff hf, H, false_and]

Premises used: false_and, MeasureTheory.Integrable, aestronglyMeasurable_withDensity_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ f x • g x) μ

Tactic:
integrable_withDensity_iff_integrable_coe_smul hf

Premises used: MeasureTheory.integrable_withDensity_iff_integrable_coe_smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
rw :
  Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toNNReal • g x) μ ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ
hf₁ : Measurable (β := ℝ≥0) fun (x : α) ↦ (f x).toNNReal
⊢ Integrable g (μ.withDensity f) ↔ Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ

Tactic:
rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
    integrable_withDensity_iff_integrable_smul]

Premises used: MeasureTheory.coe_toNNReal_ae_eq, MeasureTheory.integrable_withDensity_iff_integrable_smul, MeasureTheory.withDensity_congr_ae
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
simp_rw :
  Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x).toNNReal : ℝ) • g x) μ ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ
⊢ Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toNNReal • g x) μ ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ

Tactic:
simp_rw [NNReal.smul_def, ENNReal.toReal]

Premises used: NNReal.smul_def, ENNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Measurable (β := ℝ≥0) fun (x : α) ↦ (f x).toNNReal

Tactic:
hf.ennreal_toNNReal

Premises used: Measurable.ennreal_toNNReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Measurable (β := ℝ≥0) fun (x : α) ↦ (f x).toNNReal

Tactic:
exact hf.ennreal_toNNReal

Premises used: Measurable.ennreal_toNNReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
this : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞)
rw rw₁ :
  Integrable g (μ.withDensity fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞)) ↔
    Integrable g (μ.withDensity fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞))
⊢ Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable g (μ.withDensity fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞))

Tactic:
rw [withDensity_congr_ae this]

Premises used: MeasureTheory.withDensity_congr_ae
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
suffices :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞)
⊢ Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable g (μ.withDensity fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞))

Tactic:
suffices (fun x => (f x : ℝ≥0∞)) =ᵐ[μ] (fun x => (hf.mk f x : ℝ≥0)) by
        rw [withDensity_congr_ae this]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
h : ∀ (x : α) (hx : f x = AEMeasurable.mk f hf x), (↑(f x) : ℝ≥0∞) = (↑(AEMeasurable.mk f hf x) : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ≥0∞)

Tactic:
filter_upwards [hf.ae_eq_mk] with x hx

Premises used: AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ (↑(f x) : ℝ≥0∞) = (↑(AEMeasurable.mk f hf x) : ℝ≥0∞)

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
h :
  EventuallyEq.{u_1, u_8} (β := E) (ae μ) (fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ) • g x) fun (x : α) ↦
    (↑(f x) : ℝ) • g x
⊢ Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ) • g x) μ ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ

Tactic:
apply integrable_congr

Premises used: MeasureTheory.integrable_congr
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
h : ∀ (x : α) (hx : f x = AEMeasurable.mk f hf x), (↑(AEMeasurable.mk f hf x) : ℝ) • g x = (↑(f x) : ℝ) • g x
⊢ EventuallyEq.{u_1, u_8} (β := E) (ae μ) (fun (x : α) ↦ (↑(AEMeasurable.mk f hf x) : ℝ) • g x) fun (x : α) ↦
    (↑(f x) : ℝ) • g x

Tactic:
filter_upwards [hf.ae_eq_mk] with x hx

Premises used: AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ (↑(AEMeasurable.mk f hf x) : ℝ) • g x = (↑(f x) : ℝ) • g x

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
rw :
  Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x).toNNReal : ℝ) • g x) μ ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ
hf₁ : AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) μ
⊢ Integrable g (μ.withDensity f) ↔ Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ

Tactic:
rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
    integrable_withDensity_iff_integrable_coe_smul₀]

Premises used: MeasureTheory.coe_toNNReal_ae_eq, MeasureTheory.integrable_withDensity_iff_integrable_coe_smul₀, MeasureTheory.withDensity_congr_ae
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (↑(f x).toNNReal : ℝ) • g x) μ ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).toReal • g x) μ

Tactic:
congr!
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) μ

Tactic:
hf.ennreal_toNNReal

Premises used: AEMeasurable.ennreal_toNNReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) μ

Tactic:
exact hf.ennreal_toNNReal

Premises used: AEMeasurable.ennreal_toNNReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
⊢ Integrable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ f x • g x) μ

Tactic:
integrable_withDensity_iff_integrable_coe_smul₀ hf

Premises used: MeasureTheory.integrable_withDensity_iff_integrable_coe_smul₀
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ
⊢ Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ g x * (f x).toReal) fun (x : α) ↦ (f x).toReal • g x

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ
⊢ Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ g x * (f x).toReal) fun (x : α) ↦ (f x).toReal • g x

Tactic:
have : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x := by simp [mul_comm]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ
this : Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ g x * (f x).toReal) fun (x : α) ↦ (f x).toReal • g x
rw : Integrable g (μ.withDensity f) ↔ Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal • g x) μ
⊢ Integrable g (μ.withDensity f) ↔ Integrable (ε := ℝ) (fun (x : α) ↦ g x * (f x).toReal) μ

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ
this : Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ g x * (f x).toReal) fun (x : α) ↦ (f x).toReal • g x
⊢ Integrable g (μ.withDensity f) ↔ Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal • g x) μ

Tactic:
integrable_withDensity_iff_integrable_smul' hf hflt

Premises used: MeasureTheory.integrable_withDensity_iff_integrable_smul'
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ
this : Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ g x * (f x).toReal) fun (x : α) ↦ (f x).toReal • g x
⊢ Integrable g (μ.withDensity f) ↔ Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal • g x) μ

Tactic:
exact integrable_withDensity_iff_integrable_smul' hf hflt

Premises used: MeasureTheory.integrable_withDensity_iff_integrable_smul'
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
⊢ MemLp.{u_1, u_8} (ε := E)
    (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) 1 μ

Tactic:
memLp_one_iff_integrable.2 <|
    (integrable_withDensity_iff_integrable_smul f_meas).1 <| memLp_one_iff_integrable.1 (Lp.memLp u)

Premises used: Iff.mpr, MeasureTheory.Lp.memLp, MeasureTheory.integrable_withDensity_iff_integrable_smul, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
h :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
              ⋯) :
          α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ +
              MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
          α →ₘ[μ] E) :
      α → E)
⊢ MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ =
    MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ +
      MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
x : α
hu :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
hv :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
huv :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
h' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ +
                MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    ((↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
              α →ₘ[μ] E) :
          α → E) +
        (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
              α →ₘ[μ] E) :
          α → E))
      x
h'' :
  (↑(f x) : ℝ≥0∞) ≠ 0 →
    (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
      ((↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) +
          (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E))
        x
h :
  f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x +
      f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
⊢ (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ +
                MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x

Tactic:
rw [huv, h', Pi.add_apply, hu, hv]

Premises used: Pi.add_apply
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
x : α
hu :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
hv :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
huv :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
h' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ +
                MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    ((↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
              α →ₘ[μ] E) :
          α → E) +
        (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
              α →ₘ[μ] E) :
          α → E))
      x
h'' :
  (↑(f x) : ℝ≥0∞) ≠ 0 →
    (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
      ((↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) +
          (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E))
        x
hx : f x = 0
⊢ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x +
      f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x

Tactic:
simp only [hx, zero_smul, add_zero]

Premises used: zero_smul, add_zero