awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 : α) → ℝ)
⊢ integral f = ‖posPart f‖ - ‖negPart f‖
have rw : MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
  MeasureTheory.SimpleFunc.integral μ
    (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))
Tactic: rw [integral, norm_eq_integral, norm_eq_integral, ← SimpleFunc.integral_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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)))
⊢ integral f = ‖posPart f‖ - ‖negPart f‖
have hf : Integrable (ε := ℝ) (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ) μ
Tactic: rw [integral, norm_eq_integral, norm_eq_integral, ← SimpleFunc.integral_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 : α) → ℝ) μ
⊢ integral f = ‖posPart f‖ - ‖negPart f‖
have hg : Integrable (ε := ℝ) (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ) μ
Tactic: rw [integral, norm_eq_integral, norm_eq_integral, ← SimpleFunc.integral_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 : α) → ℝ)
⊢ MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))
have apply : (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f) : (a : α) → ℝ)
  (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
Tactic: apply MeasureTheory.SimpleFunc.integral_congr (SimpleFunc.integrable f)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 : α) → ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f) : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
have 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 :
      ℝ)
Tactic: filter_upwards [ae_eq₁, ae_eq₂] with _ h₁ h₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 : ℝ)
⊢ Eq (α := ℝ) ((toSimpleFunc f : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)) : (a : α) → ℝ) a :
      ℝ)
have h : (toSimpleFunc f : (a : α) → ℝ) a =
  HSub.hSub (α := ℝ) (β := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
    (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
Tactic: rw [SimpleFunc.sub_apply, ← h₁, ← h₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 = (setToL1 ⋯ : (a : ↥(Lp E 1 μ)) → E) f
have simp : Eq.{u_2 + 1} (α := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E) ((setToL1 sorry : (a : ↥(Lp E 1 μ)) → E) f : E)
Tactic: simp only [integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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.integral (↑f : ↥(Lp E 1 μ)) = integral f
have simp : (L1.integralCLM : (a : ↥(Lp E 1 μ)) → E) (↑f : ↥(Lp E 1 μ)) = MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)
Tactic: simp only [integral, L1.integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 μ)
⊢ (L1.integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) (↑f : ↥(Lp E 1 μ)) = integral f
have apply : DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E 𝕜) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))
Tactic: apply ContinuousLinearMap.extend_eq _ _ simpleFunc.isUniformInducing
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 μ)
⊢ integral f = (integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) f
have apply : Continuous (X := ↥(Lp E 1 μ)) integral
Tactic: apply isClosed_property (simpleFunc.denseRange one_ne_top)
    (isClosed_eq _ (integralCLM' 𝕜).continuous) _ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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
⊢ integral f = (integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) f
have apply₁ : ∀ (a : ↥(simpleFunc E 1 μ)), integral (↑a : ↥(Lp E 1 μ)) = (integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) (↑a : ↥(Lp E 1 μ))
Tactic: apply isClosed_property (simpleFunc.denseRange one_ne_top)
    (isClosed_eq _ (integralCLM' 𝕜).continuous) _ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 μ)) integral
have simp_rw : Continuous (X := ↥(Lp E 1 μ)) (Y := E) (⇑integralCLM : (a : ↥(Lp E 1 μ)) → E)
Tactic: simp_rw [integral_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 μ)
⊢ integral (↑f : ↥(Lp E 1 μ)) = (integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) (↑f : ↥(Lp E 1 μ))
have norm_cast : SimpleFunc.integral f = SimpleFunc.integral f
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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) (integral.{u_1, u_2} (α := α) (m := m) (μ := μ) 0) 0
have simp : Eq.{u_2 + 1} (α := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) 0 : E) (0 : E)
Tactic: simp only [integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 μ)
⊢ integral (f + g) = integral f + integral g
have 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)
Tactic: simp only [integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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) = -integral f
have simp : Eq.{u_2 + 1} (α := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) (-f) : E) (-(integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E)
Tactic: simp only [integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 μ)
⊢ integral (f - g) = integral f - integral g
have 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)
Tactic: simp only [integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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 μ)
⊢ integral (c • f) = c • integral f
have rw : integral (c • f) = HSMul.hSMul (β := E) c ((integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) f : E)
Tactic: rw [integral_eq' 𝕜 f, integral_eq' 𝕜 (c • f), map_smul (integralCLM' 𝕜) c f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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)
⊢ integral (c • f) = c • integral f
have rw₁ : (integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) (c • f) =
  HSMul.hSMul (β := E) c ((integralCLM' 𝕜 : (a : ↥(Lp E 1 μ)) → E) f : E)
Tactic: rw [integral_eq' 𝕜 f, integral_eq' 𝕜 (c • f), map_smul (integralCLM' 𝕜) c f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
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)
⊢ integral (c • f) = c • integral f
have 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)
Tactic: rw [integral_eq' 𝕜 f, integral_eq' 𝕜 (c • f), map_smul (integralCLM' 𝕜) c f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
⊢ Continuous (Y := E) fun (f : ↥(Lp E 1 μ)) ↦ integral f
have simp : Continuous (Y := E) fun (f : ↥(Lp E 1 μ)) ↦ (integralCLM : (a : ↥(Lp E 1 μ)) → E) f
Tactic: simp only [integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖
have refine_1 : Continuous.{u_1, 0} (X := ↥(Lp ℝ 1 μ)) integral
Tactic: refine @isClosed_property _ _ _ ((↑) : (α →₁ₛ[μ] ℝ) → α →₁[μ] ℝ)
      (fun f : α →₁[μ] ℝ => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖)
      (simpleFunc.denseRange one_ne_top) (isClosed_eq ?_ ?_) ?_ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
refine_1 : Continuous.{u_1, 0} (X := ↥(Lp ℝ 1 μ)) integral
⊢ integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖
have refine_2 : Continuous (Y := ℝ) fun (x : ↥(Lp ℝ 1 μ)) ↦ ‖Lp.posPart x‖ - ‖Lp.negPart x‖
Tactic: refine @isClosed_property _ _ _ ((↑) : (α →₁ₛ[μ] ℝ) → α →₁[μ] ℝ)
      (fun f : α →₁[μ] ℝ => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖)
      (simpleFunc.denseRange one_ne_top) (isClosed_eq ?_ ?_) ?_ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
refine_1 : Continuous.{u_1, 0} (X := ↥(Lp ℝ 1 μ)) integral
refine_2 : Continuous (Y := ℝ) fun (x : ↥(Lp ℝ 1 μ)) ↦ ‖Lp.posPart x‖ - ‖Lp.negPart x‖
⊢ integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖
have refine_3 : ∀ (a : ↥(simpleFunc ℝ 1 μ)), (fun (f : ↥(Lp ℝ 1 μ)) ↦ integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖) (↑a : ↥(Lp ℝ 1 μ))
Tactic: refine @isClosed_property _ _ _ ((↑) : (α →₁ₛ[μ] ℝ) → α →₁[μ] ℝ)
      (fun f : α →₁[μ] ℝ => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖)
      (simpleFunc.denseRange one_ne_top) (isClosed_eq ?_ ?_) ?_ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous.{u_1, 0} (X := ↥(Lp ℝ 1 μ)) integral
have refine_1 : Continuous.{u_1, 0} (X := ↥(Lp ℝ 1 μ)) (Y := ℝ) (⇑integralCLM : (a : ↥(Lp ℝ 1 μ)) → ℝ)
Tactic: simp only [integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : ↥(simpleFunc ℝ 1 μ)
⊢ integral (↑s : ↥(Lp ℝ 1 μ)) = ‖Lp.posPart (↑s : ↥(Lp ℝ 1 μ))‖ - ‖Lp.negPart (↑s : ↥(Lp ℝ 1 μ))‖
have refine_3 : SimpleFunc.integral s = ‖SimpleFunc.posPart s‖ - ‖SimpleFunc.negPart s‖
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
hst : s =ᶠ[ae μ] t
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in t, f x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in t, f x ∂μ)
Tactic: rw [Measure.restrict_congr_set hst]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ ∫ (x : X) in s \ t, f x ∂μ = HSub.hSub (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in t, f x ∂μ)
have hst : AEDisjoint μ (s \ t) t
Tactic: rw [eq_sub_iff_add_eq, ← setIntegral_union₀, diff_union_of_subset hts]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
hst : AEDisjoint μ (s \ t) t
ht₁ : NullMeasurableSet t μ
⊢ ∫ (x : X) in s \ t, f x ∂μ = HSub.hSub (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in t, f x ∂μ)
have hfs₁ : IntegrableOn f (s \ t) μ
Tactic: rw [eq_sub_iff_add_eq, ← setIntegral_union₀, diff_union_of_subset hts]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
hst : AEDisjoint μ (s \ t) t
ht₁ : NullMeasurableSet t μ
hfs₁ : IntegrableOn f (s \ t) μ
⊢ ∫ (x : X) in s \ t, f x ∂μ = HSub.hSub (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in t, f x ∂μ)
have hft : IntegrableOn f t μ
Tactic: rw [eq_sub_iff_add_eq, ← setIntegral_union₀, diff_union_of_subset hts]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s ∩ t, f x ∂μ) (∫ (x : X) in s \ t, f x ∂μ) = ∫ (x : X) in s, f x ∂μ
have hμ : Integrable f (μ.restrict (s ∩ t))
Tactic: rw [← Measure.restrict_inter_add_diff₀ s ht, integral_add_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hμ : Integrable f (μ.restrict (s ∩ t))
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s ∩ t, f x ∂μ) (∫ (x : X) in s \ t, f x ∂μ) = ∫ (x : X) in s, f x ∂μ
have hν : Integrable f (μ.restrict (s \ t))
Tactic: rw [← Measure.restrict_inter_add_diff₀ s ht, integral_add_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
s_1 : Finset ι
hat : a ∉ s_1
IH :
  ∀ (hs : ∀ i ∈ s_1, MeasurableSet (s i)) (h's : (↑s_1 : Set ι).Pairwise (Disjoint on s))
    (hf : ∀ i ∈ s_1, IntegrableOn f (s i) μ),
    Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) (∑ i ∈ s_1, ∫ (x : X) in s i, f x ∂μ)
hs : ∀ i ∈ insert a s_1, MeasurableSet (s i)
h's : (↑(insert a s_1) : Set ι).Pairwise (Disjoint on s)
hf : ∀ i ∈ insert a s_1, IntegrableOn f (s i) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ insert a s_1, s i, f x ∂μ) (∑ i ∈ insert a s_1, ∫ (x : X) in s i, f x ∂μ)
have insert : ∀ (hs : MeasurableSet (s a) ∧ ∀ x ∈ s_1, MeasurableSet (s x))
  (hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ s_1, IntegrableOn f (s x) μ)
  (h's :
    (↑s_1 : Set ι).Pairwise (Disjoint on s) ∧ ∀ b ∈ (↑s_1 : Set ι), a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a),
  Eq.{u_3 + 1} (α := E) (∫ (x : X) in s a ∪ ⋃ x ∈ s_1, s x, f x ∂μ) (∑ i ∈ insert a s_1, ∫ (x : X) in s i, f x ∂μ)
Tactic: simp only [Finset.coe_insert, Finset.forall_mem_insert, Set.pairwise_insert,
      Finset.set_biUnion_insert] at hs hf h's ⊢
Cleared hypotheses: hs, h's, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
s_1 : Finset ι
hat : a ∉ s_1
IH :
  ∀ (hs : ∀ i ∈ s_1, MeasurableSet (s i)) (h's : (↑s_1 : Set ι).Pairwise (Disjoint on s))
    (hf : ∀ i ∈ s_1, IntegrableOn f (s i) μ),
    Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) (∑ i ∈ s_1, ∫ (x : X) in s i, f x ∂μ)
hs : MeasurableSet (s a) ∧ ∀ x ∈ s_1, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ s_1, IntegrableOn f (s x) μ
h's : (↑s_1 : Set ι).Pairwise (Disjoint on s) ∧ ∀ b ∈ (↑s_1 : Set ι), a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s a ∪ ⋃ x ∈ s_1, s x, f x ∂μ) (∑ i ∈ insert a s_1, ∫ (x : X) in s i, f x ∂μ)
have insert : HAdd.hAdd (α := E) (∫ (x : X) in s a, f x ∂μ) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) =
  ∑ i ∈ insert a s_1, ∫ (x : X) in s i, f x ∂μ
Tactic: rw [setIntegral_union _ _ hf.1 (integrableOn_finset_iUnion.2 hf.2)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
s_1 : Finset ι
hat : a ∉ s_1
IH :
  ∀ (hs : ∀ i ∈ s_1, MeasurableSet (s i)) (h's : (↑s_1 : Set ι).Pairwise (Disjoint on s))
    (hf : ∀ i ∈ s_1, IntegrableOn f (s i) μ),
    Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) (∑ i ∈ s_1, ∫ (x : X) in s i, f x ∂μ)
hs : MeasurableSet (s a) ∧ ∀ x ∈ s_1, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ s_1, IntegrableOn f (s x) μ
h's : (↑s_1 : Set ι).Pairwise (Disjoint on s) ∧ ∀ b ∈ (↑s_1 : Set ι), a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
insert :
  HAdd.hAdd (α := E) (∫ (x : X) in s a, f x ∂μ) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) =
    ∑ i ∈ Insert.insert a s_1, ∫ (x : X) in s i, f x ∂μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s a ∪ ⋃ x ∈ s_1, s x, f x ∂μ)
    (∑ i ∈ Insert.insert a s_1, ∫ (x : X) in s i, f x ∂μ)
have rw : Disjoint (s a) (⋃ i ∈ s_1, s i)
Tactic: rw [setIntegral_union _ _ hf.1 (integrableOn_finset_iUnion.2 hf.2)]