awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
pos : ∀ (hf : Integrable f μ), ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
neg : ∀ (hf : ¬Integrable f μ), ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
⊢ ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
hf : Integrable f μ
⊢ ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c

Tactic:
((1 : 𝕜 →L[𝕜] 𝕜).smulRight c).integral_comp_comm hf

Premises used: ContinuousLinearMap.smulRight, OfNat.ofNat, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
hf : Integrable f μ
⊢ ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c

Tactic:
exact ((1 : 𝕜 →L[𝕜] 𝕜).smulRight c).integral_comp_comm hf

Premises used: ContinuousLinearMap.smulRight, OfNat.ofNat, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
pos : ∀ (hc : c = 0), ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
neg : ∀ (hc : ¬c = 0), ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c
⊢ ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : c = 0
⊢ ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c

Tactic:
simp [hc, integral_zero, smul_zero]

Premises used: smul_zero, MeasureTheory.integral_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : ¬c = 0
neg : ¬Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • c) μ
⊢ ∫ (x : X), f x • c ∂μ = HSMul.hSMul.{u_8, u_3, u_3} (α := 𝕜) (∫ (x : X), f x ∂μ) c

Tactic:
rw [integral_undef hf, integral_undef, zero_smul]

Premises used: MeasureTheory.integral_undef, zero_smul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : ¬c = 0
neg : ¬Integrable f μ
⊢ ¬Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • c) μ

Tactic:
rw [integrable_smul_const hc]

Premises used: MeasureTheory.integrable_smul_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : ¬c = 0
neg : ¬False
⊢ ¬Integrable f μ

Tactic:
simp_rw [hf, not_false_eq_true]

Premises used: not_false_eq_true
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
A : Type u_8
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
pos : ∀ (hA : CompleteSpace A), ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ
neg : ∀ (hA : ¬CompleteSpace A), ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ
⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ

Tactic:
by_cases hA : CompleteSpace A

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
A : Type u_8
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
hA : CompleteSpace A
pos :
  Eq (α := A)
    (∫ (x : X), (((ContinuousLinearMap.mul ℝ A : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A) (f x) ∂μ : A)
    ((((ContinuousLinearMap.mul ℝ A : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A) (∫ (x : X), f x ∂μ) : A)
⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ

Tactic:
change ∫ x, ContinuousLinearMap.mul ℝ _ c (f x) ∂μ = ContinuousLinearMap.mul ℝ _ c (∫ x, f x ∂μ)

Premises used: Real, ContinuousLinearMap.mul, MeasureTheory.integral, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
A : Type u_8
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
hA : CompleteSpace A
pos pos₁ :
  Eq (α := A)
    ((((ContinuousLinearMap.mul ℝ A : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A) (∫ (x : X), f x ∂μ) : A)
    ((((ContinuousLinearMap.mul ℝ A : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A) (∫ (x : X), f x ∂μ) : A)
⊢ Eq (α := A)
    (∫ (x : X), (((ContinuousLinearMap.mul ℝ A : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A) (f x) ∂μ : A)
    ((((ContinuousLinearMap.mul ℝ A : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A) (∫ (x : X), f x ∂μ) : A)

Tactic:
rw [ContinuousLinearMap.integral_comp_comm _ hf]

Premises used: ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
A : Type u_8
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
hA : ¬CompleteSpace A
⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ

Tactic:
simp [integral, hA]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
A : Type u_8
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
pos : ∀ (hA : CompleteSpace A), ∫ (x : X), f x * c ∂μ = (∫ (x : X), f x ∂μ) * c
neg : ∀ (hA : ¬CompleteSpace A), ∫ (x : X), f x * c ∂μ = (∫ (x : X), f x ∂μ) * c
⊢ ∫ (x : X), f x * c ∂μ = (∫ (x : X), f x ∂μ) * c

Tactic:
by_cases hA : CompleteSpace A

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
A : Type u_8
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
hA : CompleteSpace A
pos :
  Eq (α := A)
    (∫ (x : X),
        (((ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ A) : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A)
          (f x) ∂μ :
      A)
    ((((ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ A) : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A)
        (∫ (x : X), f x ∂μ) :
      A)
⊢ ∫ (x : X), f x * c ∂μ = (∫ (x : X), f x ∂μ) * c

Tactic:
change ∫ x, (ContinuousLinearMap.mul ℝ _).flip c (f x) ∂μ
      = (ContinuousLinearMap.mul ℝ _).flip c (∫ x, f x ∂μ)

Premises used: MeasureTheory.integral, ContinuousLinearMap.flip, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
A : Type u_8
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
hA : CompleteSpace A
pos pos₁ :
  Eq (α := A)
    ((((ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ A) : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A)
        (∫ (x : X), f x ∂μ) :
      A)
    ((((ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ A) : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A)
        (∫ (x : X), f x ∂μ) :
      A)
⊢ Eq (α := A)
    (∫ (x : X),
        (((ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ A) : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A)
          (f x) ∂μ :
      A)
    ((((ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ A) : (a : A) → A →L[ℝ] A) c : A →L[ℝ] A) : (a : A) → A)
        (∫ (x : X), f x ∂μ) :
      A)

Tactic:
rw [ContinuousLinearMap.integral_comp_comm _ hf]

Premises used: ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
inst : MeasurableSpace X
μ : Measure X
A : Type u_8
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
hA : ¬CompleteSpace A
⊢ ∫ (x : X), f x * c ∂μ = (∫ (x : X), f x ∂μ) * c

Tactic:
simp [integral, hA]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
pos :
  ∀ (hE : CompleteSpace E),
    Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)
neg :
  ∀ (hE : ¬CompleteSpace E),
    Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : ¬CompleteSpace E
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)

Tactic:
simp [integral, hE]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
pos :
  ∀ (hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))),
    Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)
neg :
  ∀ (hg : ¬Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))),
    Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)

Tactic:
by_cases hg : Integrable g (μ.withDensity fun x => f x)

Premises used: MeasureTheory.Measure.withDensity, ENNReal.ofNNReal, MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : ¬Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
neg : ¬Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • g x) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)

Tactic:
rw [integral_undef hg, integral_undef]

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg neg neg₁ neg₂ neg₃ : ¬Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
⊢ ¬Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • g x) μ

Tactic:
rwa [← integrable_withDensity_iff_integrable_smul f_meas]

Premises used: MeasureTheory.integrable_withDensity_iff_integrable_smul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)

Tactic:
Integrable.induction
    (P := fun g => ∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, f x • g x ∂μ) ?_ ?_ ?_ ?_ hg

Premises used: MeasureTheory.Measure.withDensity, ENNReal.ofNNReal, MeasureTheory.integral, HSMul.hSMul, Eq, MeasureTheory.Integrable.induction
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
pos :
  ∀ (c : E) ⦃s : Set X⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        (fun (g : X → E) ↦
            Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
              (∫ (x : X), f x • g x ∂μ))
          (s.indicator fun (x : X) ↦ c)
pos₁ :
  ∀ ⦃f_1 g : X → E⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Integrable f_1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) →
        Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) →
          (fun (g : X → E) ↦
                Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
                  (∫ (x : X), f x • g x ∂μ))
              f_1 →
            (fun (g : X → E) ↦
                  Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
                    (∫ (x : X), f x • g x ∂μ))
                g →
              (fun (g : X → E) ↦
                  Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
                    (∫ (x : X), f x • g x ∂μ))
                (f_1 + g)
pos₂ :
  IsClosed (X := ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))))
    {f_1 : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))) |
      (fun (g : X → E) ↦
          Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ))
        (↑(↑f_1 : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E)}
pos₃ :
  ∀ ⦃f_1 g : X → E⦄,
    f_1 =ᶠ[ae (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))] g →
      Integrable f_1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) →
        (fun (g : X → E) ↦
              Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
                (∫ (x : X), f x • g x ∂μ))
            f_1 →
          (fun (g : X → E) ↦
              Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
                (∫ (x : X), f x • g x ∂μ))
            g
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)

Tactic:
refine Integrable.induction
    (P := fun g => ∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, f x • g x ∂μ) ?_ ?_ ?_ ?_ hg

Premises used: MeasureTheory.Measure.withDensity, ENNReal.ofNNReal, MeasureTheory.integral, HSMul.hSMul, Eq, MeasureTheory.Integrable.induction
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
c : E
s : Set X
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, c ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), HSMul.hSMul (β := E) (f x) (s.indicator (fun (x : X) ↦ c) x) ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator (fun (x : X) ↦ c) x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), HSMul.hSMul (β := E) (f x) (s.indicator (fun (x : X) ↦ c) x) ∂μ)

Tactic:
rw [integral_indicator s_meas]

Premises used: MeasureTheory.integral_indicator
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
c : E
s : Set X
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, c ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (a : X) in s, f a • c ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, c ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), HSMul.hSMul (β := E) (f x) (s.indicator (fun (x : X) ↦ c) x) ∂μ)

Tactic:
simp_rw [← Set.indicator_smul_apply, integral_indicator s_meas]

Premises used: MeasureTheory.integral_indicator, Set.indicator_smul_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
c : E
s : Set X
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : (∫⁻ (x : X) in s, (↑(f x) : ℝ≥0∞) ∂μ).toReal • c = ∫ (a : X) in s, f a • c ∂μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, c ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (a : X) in s, f a • c ∂μ)

Tactic:
simp only [s_meas, integral_const, Measure.restrict_apply', Set.univ_inter, withDensity_apply,
      measureReal_def]

Premises used: Set.univ_inter, MeasureTheory.integral_const, MeasureTheory.measureReal_def, MeasureTheory.Measure.restrict_apply', MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
c : E
s : Set X
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(f x) : ℝ) • c ∂μ) (∫ (a : X) in s, f a • c ∂μ)
pos₁ : LE.le (α := ℝ) 0 (∫ (a : X) in s, (↑(f a) : ℝ) ∂μ)
pos₂ : Integrable (ε := ℝ) (fun (x : X) ↦ (↑(f x) : ℝ)) (μ.restrict s)
⊢ (∫⁻ (x : X) in s, (↑(f x) : ℝ≥0∞) ∂μ).toReal • c = ∫ (a : X) in s, f a • c ∂μ

Tactic:
rw [lintegral_coe_eq_integral, ENNReal.toReal_ofReal, ← integral_smul_const]

Premises used: integral_smul_const, ENNReal.toReal_ofReal, MeasureTheory.lintegral_coe_eq_integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
c : E
s : Set X
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(f x) : ℝ) • c ∂μ) (∫ (a : X) in s, f a • c ∂μ)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
c : E
s : Set X
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (a : X) in s, (↑(f a) : ℝ) ∂μ)

Tactic:
integral_nonneg fun x => NNReal.coe_nonneg _

Premises used: MeasureTheory.integral_nonneg, NNReal.coe_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
c : E
s : Set X
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (a : X) in s, (↑(f a) : ℝ) ∂μ)

Tactic:
exact integral_nonneg fun x => NNReal.coe_nonneg _

Premises used: MeasureTheory.integral_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
c : E
s : Set X
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable (ε := ℝ) (fun (x : X) ↦ (↑(f x) : ℝ)) (μ.restrict s)

Tactic:
⟨f_meas.coe_nnreal_real.aemeasurable.aestronglyMeasurable, ?_⟩

Premises used: AEMeasurable.aestronglyMeasurable, Measurable.aemeasurable, MeasureTheory.Integrable, Measurable.coe_nnreal_real, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
c : E
s : Set X
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : HasFiniteIntegral (ε := ℝ) (fun (x : X) ↦ (↑(f x) : ℝ)) (μ.restrict s)
⊢ Integrable (ε := ℝ) (fun (x : X) ↦ (↑(f x) : ℝ)) (μ.restrict s)

Tactic:
refine ⟨f_meas.coe_nnreal_real.aemeasurable.aestronglyMeasurable, ?_⟩