awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)

Tactic:
have ae_eq₂ : (toSimpleFunc f).negPart =ᵐ[μ] (toSimpleFunc (negPart f)).map norm := by
    filter_upwards [negPart_toSimpleFunc f] with _ h
    rw [SimpleFunc.map_apply, h]
    conv_lhs => rw [← SimpleFunc.negPart_map_norm, SimpleFunc.map_apply]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
ae_eq₂ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
rw :
  MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))
hf : Integrable (ε := ℝ) (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ) μ
hg : Integrable (ε := ℝ) (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ) μ
⊢ integral f = ‖posPart f‖ - ‖negPart f‖

Tactic:
rw [integral, norm_eq_integral, norm_eq_integral, ← SimpleFunc.integral_sub]

Premises used: MeasureTheory.L1.SimpleFunc.integral, MeasureTheory.SimpleFunc.integral_sub, MeasureTheory.L1.SimpleFunc.norm_eq_integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
ae_eq₂ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
apply :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f) : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
⊢ MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))

Tactic:
apply MeasureTheory.SimpleFunc.integral_congr (SimpleFunc.integrable f)

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.integral_congr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
ae_eq₂ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
h :
  ∀ (a : α)
    (h₁ :
      Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
        ((SimpleFunc.map norm (toSimpleFunc (posPart f)) : (a : α) → ℝ) a : ℝ))
    (h₂ :
      Eq (α := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
        ((SimpleFunc.map norm (toSimpleFunc (negPart f)) : (a : α) → ℝ) a : ℝ)),
    Eq (α := ℝ) ((toSimpleFunc f : (a : α) → ℝ) a : ℝ)
      ((SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)) : (a : α) → ℝ)
          a :
        ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f) : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)

Tactic:
filter_upwards [ae_eq₁, ae_eq₂] with _ h₁ h₂
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
ae_eq₂ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
a : α
h₁ :
  Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (posPart f)) : (a : α) → ℝ) a : ℝ)
h₂ :
  Eq (α := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (negPart f)) : (a : α) → ℝ) a : ℝ)
h :
  (toSimpleFunc f : (a : α) → ℝ) a =
    HSub.hSub (α := ℝ) (β := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
      (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
⊢ Eq (α := ℝ) ((toSimpleFunc f : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)) : (a : α) → ℝ) a :
      ℝ)

Tactic:
rw [SimpleFunc.sub_apply, ← h₁, ← h₂]

Premises used: MeasureTheory.SimpleFunc.sub_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
ae_eq₂ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
a : α
h₁ :
  Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (posPart f)) : (a : α) → ℝ) a : ℝ)
h₂ :
  Eq (α := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (negPart f)) : (a : α) → ℝ) a : ℝ)
⊢ (toSimpleFunc f : (a : α) → ℝ) a =
    HSub.hSub (α := ℝ) (β := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
      (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)

Tactic:
DFunLike.congr_fun (toSimpleFunc f).posPart_sub_negPart.symm _

Premises used: MeasureTheory.SimpleFunc.posPart_sub_negPart, DFunLike.congr_fun, MeasureTheory.Lp.simpleFunc.toSimpleFunc, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
ae_eq₂ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
a : α
h₁ :
  Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (posPart f)) : (a : α) → ℝ) a : ℝ)
h₂ :
  Eq (α := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (negPart f)) : (a : α) → ℝ) a : ℝ)
⊢ (toSimpleFunc f : (a : α) → ℝ) a =
    HSub.hSub (α := ℝ) (β := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
      (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)

Tactic:
exact DFunLike.congr_fun (toSimpleFunc f).posPart_sub_negPart.symm _

Premises used: MeasureTheory.SimpleFunc.posPart_sub_negPart, DFunLike.congr_fun, MeasureTheory.Lp.simpleFunc.toSimpleFunc, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
ae_eq₂ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
⊢ Integrable (ε := ℝ) (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ) μ

Tactic:
(SimpleFunc.integrable f).pos_part.congr ae_eq₁

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.Integrable.congr, MeasureTheory.Integrable.pos_part
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
ae_eq₂ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
⊢ Integrable (ε := ℝ) (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ) μ

Tactic:
exact (SimpleFunc.integrable f).pos_part.congr ae_eq₁

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.Integrable.congr, MeasureTheory.Integrable.pos_part
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
ae_eq₂ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
⊢ Integrable (ε := ℝ) (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ) μ

Tactic:
(SimpleFunc.integrable f).neg_part.congr ae_eq₂

Premises used: MeasureTheory.Integrable.neg_part, MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.Integrable.congr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
ae_eq₂ :
  (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
⊢ Integrable (ε := ℝ) (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ) μ

Tactic:
exact (SimpleFunc.integrable f).neg_part.congr ae_eq₂

Premises used: MeasureTheory.Integrable.neg_part, MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.Integrable.congr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integral f = (integralCLM : (a : ↥(Lp E 1 μ)) → E) f

Tactic:
simp only [integral]

Premises used: MeasureTheory.L1.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ↥(Lp E 1 μ)
simp : Eq.{u_2 + 1} (α := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E) ((setToL1 ⋯ : (a : ↥(Lp E 1 μ)) → E) f : E)
⊢ integral f = (setToL1 ⋯ : (a : ↥(Lp E 1 μ)) → E) f

Tactic:
simp only [integral]

Premises used: MeasureTheory.L1.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ Eq.{u_2 + 1} (α := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E) ((setToL1 ⋯ : (a : ↥(Lp E 1 μ)) → E) f : E)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ↥(simpleFunc E 1 μ)
simp :
  (L1.integralCLM : (a : ↥(Lp E 1 μ)) → E) (↑f : ↥(Lp E 1 μ)) = MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)
⊢ L1.integral (↑f : ↥(Lp E 1 μ)) = integral f

Tactic:
simp only [integral, L1.integral]

Premises used: MeasureTheory.L1.SimpleFunc.integral, MeasureTheory.L1.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ↥(simpleFunc E 1 μ)
⊢ (L1.integralCLM : (a : ↥(Lp E 1 μ)) → E) (↑f : ↥(Lp E 1 μ)) = MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)

Tactic:
setToL1_eq_setToL1SCLM (dominatedFinMeasAdditive_weightedSMul μ) f

Premises used: Multiset.sum, Multiset.foldr, Set.Mem, MeasureTheory.L1.setToL1_eq_setToL1SCLM, MeasureTheory.L1.SimpleFunc.integral, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, MeasureTheory.SimpleFunc.integral, MeasureTheory.L1.SimpleFunc.integralCLM', MeasureTheory.dominatedFinMeasAdditive_weightedSMul, Finset.sum
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ↥(simpleFunc E 1 μ)
⊢ (L1.integralCLM : (a : ↥(Lp E 1 μ)) → E) (↑f : ↥(Lp E 1 μ)) = MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)

Tactic:
exact setToL1_eq_setToL1SCLM (dominatedFinMeasAdditive_weightedSMul μ) f

Premises used: MeasureTheory.L1.setToL1_eq_setToL1SCLM, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
inst_6 : CompleteSpace E
f : ↥(simpleFunc E 1 μ)
apply :
  DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E 𝕜) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))
⊢ (L1.integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) (↑f : ↥(Lp E 1 μ)) = integral f

Tactic:
apply ContinuousLinearMap.extend_eq _ _ simpleFunc.isUniformInducing

Premises used: ContinuousLinearMap.extend_eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
inst_6 : CompleteSpace E
f : ↥(simpleFunc E 1 μ)
⊢ DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E 𝕜) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))

Tactic:
simpleFunc.denseRange one_ne_top

Premises used: Set.Mem, MeasureTheory.Lp.simpleFunc.denseRange, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
inst_6 : CompleteSpace E
f : ↥(simpleFunc E 1 μ)
⊢ DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E 𝕜) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))

Tactic:
exact simpleFunc.denseRange one_ne_top

Premises used: MeasureTheory.Lp.simpleFunc.denseRange, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
inst_6 : CompleteSpace E
f : ↥(Lp E 1 μ)
apply : Continuous (X := ↥(Lp E 1 μ)) integral
apply₁ :
  ∀ (a : ↥(simpleFunc E 1 μ)), integral (↑a : ↥(Lp E 1 μ)) = (integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) (↑a : ↥(Lp E 1 μ))
⊢ integral f = (integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) f

Tactic:
apply isClosed_property (simpleFunc.denseRange one_ne_top)
    (isClosed_eq _ (integralCLM' 𝕜).continuous) _ f

Premises used: MeasureTheory.L1.integralCLM', MeasureTheory.Lp.simpleFunc.denseRange, ContinuousLinearMap.continuous, isClosed_eq, isClosed_property, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
inst_6 : CompleteSpace E
f : ↥(Lp E 1 μ)
simp_rw : Continuous (X := ↥(Lp E 1 μ)) (Y := E) (⇑integralCLM : (a : ↥(Lp E 1 μ)) → E)
⊢ Continuous (X := ↥(Lp E 1 μ)) integral

Tactic:
simp_rw [integral_def]

Premises used: MeasureTheory.L1.integral_def
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
inst_6 : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ Continuous (X := ↥(Lp E 1 μ)) (Y := E) (⇑integralCLM : (a : ↥(Lp E 1 μ)) → E)

Tactic:
(integralCLM (E := E)).continuous

Premises used: MeasureTheory.L1.integralCLM, ContinuousLinearMap.continuous
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
inst_6 : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ Continuous (X := ↥(Lp E 1 μ)) (Y := E) (⇑integralCLM : (a : ↥(Lp E 1 μ)) → E)

Tactic:
exact (integralCLM (E := E)).continuous

Premises used: MeasureTheory.L1.integralCLM, ContinuousLinearMap.continuous
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
inst_6 : CompleteSpace E
f_1 : ↥(Lp E 1 μ)
f : ↥(simpleFunc E 1 μ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : SimpleFunc.integral f = SimpleFunc.integral f
⊢ integral (↑f : ↥(Lp E 1 μ)) = (integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) (↑f : ↥(Lp E 1 μ))

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
simp : Eq.{u_2 + 1} (α := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) 0 : E) (0 : E)
⊢ Eq.{u_2 + 1} (α := E) (integral.{u_1, u_2} (α := α) (m := m) (μ := μ) 0) 0

Tactic:
simp only [integral]

Premises used: MeasureTheory.L1.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
⊢ Eq.{u_2 + 1} (α := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) 0 : E) (0 : E)

Tactic:
map_zero integralCLM

Premises used: map_zero, MeasureTheory.L1.integralCLM
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
⊢ Eq.{u_2 + 1} (α := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) 0 : E) (0 : E)

Tactic:
exact map_zero integralCLM

Premises used: map_zero, MeasureTheory.L1.integralCLM
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : ↥(Lp E 1 μ)
simp :
  (integralCLM : (a : ↥(Lp E 1 μ)) → E) (f + g) =
    HAdd.hAdd (α := E) (β := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E)
      ((integralCLM : (a : ↥(Lp E 1 μ)) → E) g : E)
⊢ integral (f + g) = integral f + integral g

Tactic:
simp only [integral]

Premises used: MeasureTheory.L1.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ (integralCLM : (a : ↥(Lp E 1 μ)) → E) (f + g) =
    HAdd.hAdd (α := E) (β := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E)
      ((integralCLM : (a : ↥(Lp E 1 μ)) → E) g : E)

Tactic:
map_add integralCLM f g

Premises used: map_add, MeasureTheory.L1.integralCLM
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ (integralCLM : (a : ↥(Lp E 1 μ)) → E) (f + g) =
    HAdd.hAdd (α := E) (β := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E)
      ((integralCLM : (a : ↥(Lp E 1 μ)) → E) g : E)

Tactic:
exact map_add integralCLM f g

Premises used: map_add, MeasureTheory.L1.integralCLM
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ↥(Lp E 1 μ)
simp :
  Eq.{u_2 + 1} (α := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) (-f) : E) (-(integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E)
⊢ integral (-f) = -integral f

Tactic:
simp only [integral]

Premises used: MeasureTheory.L1.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ Eq.{u_2 + 1} (α := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) (-f) : E) (-(integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E)

Tactic:
map_neg integralCLM f

Premises used: MeasureTheory.L1.integralCLM, map_neg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ Eq.{u_2 + 1} (α := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) (-f) : E) (-(integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E)

Tactic:
exact map_neg integralCLM f

Premises used: MeasureTheory.L1.integralCLM, map_neg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : ↥(Lp E 1 μ)
simp :
  (integralCLM : (a : ↥(Lp E 1 μ)) → E) (f - g) =
    HSub.hSub (α := E) (β := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E)
      ((integralCLM : (a : ↥(Lp E 1 μ)) → E) g : E)
⊢ integral (f - g) = integral f - integral g

Tactic:
simp only [integral]

Premises used: MeasureTheory.L1.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ (integralCLM : (a : ↥(Lp E 1 μ)) → E) (f - g) =
    HSub.hSub (α := E) (β := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E)
      ((integralCLM : (a : ↥(Lp E 1 μ)) → E) g : E)

Tactic:
map_sub integralCLM f g

Premises used: map_sub, MeasureTheory.L1.integralCLM
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ (integralCLM : (a : ↥(Lp E 1 μ)) → E) (f - g) =
    HSub.hSub (α := E) (β := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E)
      ((integralCLM : (a : ↥(Lp E 1 μ)) → E) g : E)

Tactic:
exact map_sub integralCLM f g

Premises used: map_sub, MeasureTheory.L1.integralCLM
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
inst_6 : CompleteSpace E
c : 𝕜
f : ↥(Lp E 1 μ)
rw : integral (c • f) = HSMul.hSMul (β := E) c ((integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) f : E)
rw₁ :
  (integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) (c • f) =
    HSMul.hSMul (β := E) c ((integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) f : E)
rw₂ rw₃ :
  HSMul.hSMul (β := E) c ((integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) f : E) =
    HSMul.hSMul (β := E) c ((integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) f : E)
⊢ integral (c • f) = c • integral f

Tactic:
rw [integral_eq' 𝕜 f, integral_eq' 𝕜 (c • f), map_smul (integralCLM' 𝕜) c f]

Premises used: MeasureTheory.L1.integralCLM', HSMul.hSMul, MeasureTheory.L1.integral_eq', map_smul