awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ ∫ (x : X), f x * c ∂μ = (∫ (x : X), f x ∂μ) * c
have pos : ∀ (hA : CompleteSpace A), ∫ (x : X), f x * c ∂μ = (∫ (x : X), f x ∂μ) * c
Tactic: by_cases hA : CompleteSpace A
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ ∫ (x : X), f x * c ∂μ = (∫ (x : X), f x ∂μ) * c
have neg : ∀ (hA : ¬CompleteSpace A), ∫ (x : X), f x * c ∂μ = (∫ (x : X), f x ∂μ) * c
Tactic: by_cases hA : CompleteSpace A
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
have 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)
Tactic: change ∫ x, (ContinuousLinearMap.mul ℝ _).flip c (f x) ∂μ
      = (ContinuousLinearMap.mul ℝ _).flip c (∫ x, f x ∂μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ 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)
have 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)
Tactic: rw [ContinuousLinearMap.integral_comp_comm _ hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)
have 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 ∂μ)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)
have 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 ∂μ)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
have 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 ∂μ)
Tactic: by_cases hg : Integrable g (μ.withDensity fun x => f x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)
have 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 ∂μ)
Tactic: by_cases hg : Integrable g (μ.withDensity fun x => f x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
have neg : ¬Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • g x) μ
Tactic: rw [integral_undef hg, integral_undef]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
have 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)
Tactic: refine Integrable.induction
    (P := fun g => ∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, f x • g x ∂μ) ?_ ?_ ?_ ?_ hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)
have 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)
Tactic: refine Integrable.induction
    (P := fun g => ∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, f x • g x ∂μ) ?_ ?_ ?_ ?_ hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)
have 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)}
Tactic: refine Integrable.induction
    (P := fun g => ∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, f x • g x ∂μ) ?_ ?_ ?_ ?_ hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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)}
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)
have 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
Tactic: refine Integrable.induction
    (P := fun g => ∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, f x • g x ∂μ) ?_ ?_ ?_ ?_ hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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), 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) ∂μ)
have 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) ∂μ)
Tactic: rw [integral_indicator s_meas]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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, c ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), HSMul.hSMul (β := E) (f x) (s.indicator (fun (x : X) ↦ c) x) ∂μ)
have 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 ∂μ)
Tactic: simp_rw [← Set.indicator_smul_apply, integral_indicator s_meas]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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, c ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (a : X) in s, f a • c ∂μ)
have pos : (∫⁻ (x : X) in s, (↑(f x) : ℝ≥0∞) ∂μ).toReal • c = ∫ (a : X) in s, f a • c ∂μ
Tactic: simp only [s_meas, integral_const, Measure.restrict_apply', Set.univ_inter, withDensity_apply,
      measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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∞)
⊢ (∫⁻ (x : X) in s, (↑(f x) : ℝ≥0∞) ∂μ).toReal • c = ∫ (a : X) in s, f a • c ∂μ
have pos : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(f x) : ℝ) • c ∂μ) (∫ (a : X) in s, f a • c ∂μ)
Tactic: rw [lintegral_coe_eq_integral, ENNReal.toReal_ofReal, ← integral_smul_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
⊢ (∫⁻ (x : X) in s, (↑(f x) : ℝ≥0∞) ∂μ).toReal • c = ∫ (a : X) in s, f a • c ∂μ
have pos₁ : LE.le (α := ℝ) 0 (∫ (a : X) in s, (↑(f a) : ℝ) ∂μ)
Tactic: rw [lintegral_coe_eq_integral, ENNReal.toReal_ofReal, ← integral_smul_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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) : ℝ) ∂μ)
⊢ (∫⁻ (x : X) in s, (↑(f x) : ℝ≥0∞) ∂μ).toReal • c = ∫ (a : X) in s, f a • c ∂μ
have pos₂ : Integrable (ε := ℝ) (fun (x : X) ↦ (↑(f x) : ℝ)) (μ.restrict s)
Tactic: rw [lintegral_coe_eq_integral, ENNReal.toReal_ofReal, ← integral_smul_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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)
have pos : HasFiniteIntegral (ε := ℝ) (fun (x : X) ↦ (↑(f x) : ℝ)) (μ.restrict s)
Tactic: refine ⟨f_meas.coe_nnreal_real.aemeasurable.aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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∞))
u u' : X → E
h_1 : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u'_int : Integrable u' (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
h : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
h' : Eq.{u_3 + 1} (α := E) (∫ (x : X), u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u' x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), (u + u') x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), f x • (u + u') x ∂μ)
have pos : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x + u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
  (∫ (x : X), f x • (u x + u' x) ∂μ)
Tactic: change
      (∫ x : X, u x + u' x ∂μ.withDensity fun x : X => ↑(f x)) = ∫ x : X, f x • (u x + u' x) ∂μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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∞))
u u' : X → E
h_1 : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u'_int : Integrable u' (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
h : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
h' : Eq.{u_3 + 1} (α := E) (∫ (x : X), u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u' x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), u x + u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), f x • (u x + u' x) ∂μ)
have pos : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x + u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
  (∫ (x : X), f x • u x + f x • u' x ∂μ)
Tactic: simp_rw [smul_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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∞))
u u' : X → E
h_1 : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u'_int : Integrable u' (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
h : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
h' : Eq.{u_3 + 1} (α := E) (∫ (x : X), u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u' x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), u x + u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), f x • u x + f x • u' x ∂μ)
have pos : Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • u x) μ
Tactic: rw [integral_add u_int u'_int, h, h', integral_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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∞))
u u' : X → E
h_1 : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u'_int : Integrable u' (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
h : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
h' : Eq.{u_3 + 1} (α := E) (∫ (x : X), u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u' x ∂μ)
pos : Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • u x) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), u x + u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), f x • u x + f x • u' x ∂μ)
have pos₁ : Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • u' x) μ
Tactic: rw [integral_add u_int u'_int, h, h', integral_add]