awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
have neg : Eq (α := ℝ≥0∞)
  ((ν : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: suffices ν (f ⁻¹' {f x}) = 0 by
      have A : μ (f ⁻¹' {f x}) = 0 := by simpa using (hμν _ |>.trans_eq this)
      simp [measureReal_def, A, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
⊢ Eq (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have neg : LE.le (α := ℝ≥0∞)
  ((ν : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
    ℝ≥0∞)
  ((ν : (a : Set α) → ℝ≥0∞) {a : α | ¬LE.le.{u_3} (α := F) (0 a : F) ((f : (a : α) → F) a : F)} : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero, ← ae_iff.mp hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
⊢ LE.le (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) {a : α | ¬LE.le.{u_3} (α := F) (0 a : F) ((f : (a : α) → F) a : F)} : ℝ≥0∞)
have neg : ∀ (y : α)
  (hy :
    Membership.mem (γ := Set α)
      (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) y),
  Membership.mem (γ := Set α) {a : α | ¬LE.le.{u_3} (α := F) (0 a : F) ((f : (a : α) → F) a : F)} y
Tactic: refine measure_mono fun y hy ↦ ?_
-- 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 α
f : ↥(simpleFunc E 1 μ)
⊢ ‖f‖ = SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))
have rw : Eq (α := ℝ) (∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := E) (⇑(toSimpleFunc f) : (a : α) → E) {x}) * ‖x‖)
  (∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := E) (⇑(toSimpleFunc f) : (a : α) → E) {x}) • ‖x‖)
Tactic: rw [norm_eq_sum_mul f, (toSimpleFunc f).map_integral norm (SimpleFunc.integrable f) norm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ) (Lp.posPart (↑f : ↥(Lp ℝ 1 μ)))
have rcases : ∀ (f : ↥(Lp ℝ 1 μ)) (s : α →ₛ ℝ) (hsf : AEEqFun.mk (⇑s : (a : α) → ℝ) sorry = (↑f : α →ₘ[μ] ℝ)),
  Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ)
    (Lp.posPart
      (↑(Subtype.mk (p := fun (x : ↥(Lp ℝ 1 μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ) x) f
            sorry) :
        ↥(Lp ℝ 1 μ)))
Tactic: rcases f with ⟨f, s, hsf⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : α →ₛ ℝ
hsf : AEEqFun.mk (⇑s : (a : α) → ℝ) ⋯ = (↑f : α →ₘ[μ] ℝ)
⊢ Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ)
    (Lp.posPart
      (↑(Subtype.mk (p := fun (x : ↥(Lp ℝ 1 μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ) x) f
            ⋯) :
        ↥(Lp ℝ 1 μ)))
have h : AEEqFun.mk (⇑s.posPart : (a : α) → ℝ) sorry =
  (↑(Lp.posPart
        (↑(Subtype.mk (p := fun (x : ↥(Lp ℝ 1 μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ) x)
              f sorry) :
          ↥(Lp ℝ 1 μ))) :
    α →ₘ[μ] ℝ)
Tactic: use s.posPart
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
h_pos : (ae μ).EventuallyLE (β := ℝ) 0 (⇑(toSimpleFunc f) : (a : α) → ℝ)
⊢ integral f = (∫⁻ (a : α), ENNReal.ofReal ((toSimpleFunc f : (a : α) → ℝ) a) ∂μ).toReal
have rw : MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
  (∫⁻ (a : α), ENNReal.ofReal ((toSimpleFunc f : (a : α) → ℝ) a) ∂μ).toReal
Tactic: rw [integral, SimpleFunc.integral_eq_lintegral (SimpleFunc.integrable f) h_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
h_pos : (ae μ).EventuallyLE (β := ℝ) 0 (⇑(toSimpleFunc f) : (a : α) → ℝ)
rw :
  MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    (∫⁻ (a : α), ENNReal.ofReal ((toSimpleFunc f : (a : α) → ℝ) a) ∂μ).toReal
⊢ integral f = (∫⁻ (a : α), ENNReal.ofReal ((toSimpleFunc f : (a : α) → ℝ) a) ∂μ).toReal
have rw₁ : (∫⁻ (a : α), ENNReal.ofReal ((toSimpleFunc f : (a : α) → ℝ) a) ∂μ).toReal =
  (∫⁻ (a : α), ENNReal.ofReal ((toSimpleFunc f : (a : α) → ℝ) a) ∂μ).toReal
Tactic: rw [integral, SimpleFunc.integral_eq_lintegral (SimpleFunc.integrable f) h_pos]
-- 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
f : ↥(simpleFunc E 1 μ)
⊢ ‖integral f‖ ≤ ‖f‖
have rw : ‖MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)‖ ≤
  MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))
Tactic: rw [integral, norm_eq_integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : SMulCommClass ℝ 𝕜 E
f : ↥(simpleFunc E 1 μ)
⊢ ‖f‖ ≤ 1 * ‖f‖
have rw : ‖f‖ ≤ ‖f‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc (posPart f)) : (a : α) → ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
have eq : ∀ (a : α), Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
Tactic: have eq : ∀ a, (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0 := fun a => rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq :
  ∀ (a : α), Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
have h : ∀ (a : α),
  (toSimpleFunc (posPart f) : (a : α) → ℝ) a = (↑(↑(↑(posPart f) : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a →
    ∀
      (h₂ :
        (↑(↑(Lp.posPart (↑f : ↥(Lp ℝ 1 μ))) : α →ₘ[μ] ℝ) : α → ℝ) a =
          max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0)
      (h₃ : (toSimpleFunc f : (a : α) → ℝ) a = (↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a),
      Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
Tactic: filter_upwards [toSimpleFunc_eq_toFun (posPart f), Lp.coeFn_posPart (f : α →₁[μ] ℝ),
      toSimpleFunc_eq_toFun f] with _ _ h₂ h₃
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq :
  ∀ (a : α), Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
a : α
h : (toSimpleFunc (posPart f) : (a : α) → ℝ) a = (↑(↑(↑(posPart f) : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a
h₂ :
  (↑(↑(Lp.posPart (↑f : ↥(Lp ℝ 1 μ))) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₃ : (toSimpleFunc f : (a : α) → ℝ) a = (↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a
⊢ Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
have h : max ((toSimpleFunc f : (a : α) → ℝ) a) 0 = max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0
Tactic: convert! h₂ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq :
  ∀ (a : α), Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
a : α
h : (toSimpleFunc (posPart f) : (a : α) → ℝ) a = (↑(↑(↑(posPart f) : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a
h₂ :
  (↑(↑(Lp.posPart (↑f : ↥(Lp ℝ 1 μ))) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₃ : (toSimpleFunc f : (a : α) → ℝ) a = (↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a
⊢ max ((toSimpleFunc f : (a : α) → ℝ) a) 0 = max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0
have h : max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0
Tactic: rw [h₃]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq :
  ∀ (a : α), Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc (posPart f)) : (a : α) → ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
have ae_eq : ∀ᵐ (a : α) ∂μ,
  Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
Tactic: have ae_eq : ∀ᵐ a ∂μ, toSimpleFunc (posPart f) a = max ((toSimpleFunc f) a) 0 := by
    filter_upwards [toSimpleFunc_eq_toFun (posPart f), Lp.coeFn_posPart (f : α →₁[μ] ℝ),
      toSimpleFunc_eq_toFun f] with _ _ h₂ h₃
    convert! h₂ using 1
    rw [h₃]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq :
  ∀ (a : α), Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
ae_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc (posPart f)) : (a : α) → ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
have refine : ∀ (a : α)
  (h : Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)),
  Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
Tactic: refine ae_eq.mono fun a h => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq :
  ∀ (a : α), Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
ae_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
⊢ Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
have rw : Eq (α := ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
Tactic: rw [h, eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq :
  ∀ (a : α), Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
ae_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
rw : Eq (α := ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
⊢ Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
have rw₁ : Eq (α := ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
Tactic: rw [h, eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc (posPart (-f))) : (a : α) → ℝ) (⇑(-toSimpleFunc f).posPart : (a : α) → ℝ)
have h : ∀ (a : α),
  Eq (α := ℝ) ((toSimpleFunc (posPart (-f)) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc (-f)).posPart : (a : α) → ℝ) a : ℝ) →
    Eq (α := ℝ) ((toSimpleFunc (-f) : (a : α) → ℝ) a : ℝ) ((-(⇑(toSimpleFunc f) : (a : α) → ℝ)) a : ℝ) →
      Eq (α := ℝ) ((toSimpleFunc (posPart (-f)) : (a : α) → ℝ) a : ℝ) (((-toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
Tactic: filter_upwards [posPart_toSimpleFunc (-f), neg_toSimpleFunc f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h₁ : Eq (α := ℝ) ((toSimpleFunc (posPart (-f)) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc (-f)).posPart : (a : α) → ℝ) a : ℝ)
h₂ : Eq (α := ℝ) ((toSimpleFunc (-f) : (a : α) → ℝ) a : ℝ) ((-(⇑(toSimpleFunc f) : (a : α) → ℝ)) a : ℝ)
⊢ Eq (α := ℝ) ((toSimpleFunc (posPart (-f)) : (a : α) → ℝ) a : ℝ) (((-toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
have h : Eq (α := ℝ) (((toSimpleFunc (-f)).posPart : (a : α) → ℝ) a : ℝ) (((-toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h₁ : Eq (α := ℝ) ((toSimpleFunc (posPart (-f)) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc (-f)).posPart : (a : α) → ℝ) a : ℝ)
h₂ : Eq (α := ℝ) ((toSimpleFunc (-f) : (a : α) → ℝ) a : ℝ) ((-(⇑(toSimpleFunc f) : (a : α) → ℝ)) a : ℝ)
⊢ Eq (α := ℝ) (max ((toSimpleFunc (-f) : (a : α) → ℝ) a) 0 : ℝ) (max ((-toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
have h : Eq (α := ℝ) (max ((-(⇑(toSimpleFunc f) : (a : α) → ℝ)) a) 0 : ℝ) (max ((-toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
have h : ∀ (a : α)
  (h : Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)),
  Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (posPart f)) : (a : α) → ℝ) a : ℝ)
Tactic: filter_upwards [posPart_toSimpleFunc f] with _ h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
⊢ Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (posPart f)) : (a : α) → ℝ) a : ℝ)
have h₁ : ((toSimpleFunc f).posPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
Tactic: rw [SimpleFunc.map_apply, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
| ((toSimpleFunc f).posPart : (a : α) → ℝ) a
have rw : norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
Tactic: rw [← SimpleFunc.posPart_map_norm, SimpleFunc.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
⊢ ((toSimpleFunc f).posPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
have conv_lhs : ((toSimpleFunc f).posPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
Tactic: conv_lhs => rw [← SimpleFunc.posPart_map_norm, SimpleFunc.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
conv_lhs : ((toSimpleFunc f).posPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
⊢ ((toSimpleFunc f).posPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
have h₁ : norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ) =
  norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
Tactic: conv_lhs => rw [← SimpleFunc.posPart_map_norm, SimpleFunc.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ integral f = ‖posPart f‖ - ‖negPart f‖
have ae_eq₁ : (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
  (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)
Tactic: have ae_eq₁ : (toSimpleFunc f).posPart =ᵐ[μ] (toSimpleFunc (posPart f)).map norm := by
    filter_upwards [posPart_toSimpleFunc f] with _ h
    rw [SimpleFunc.map_apply, h]
    conv_lhs => rw [← SimpleFunc.posPart_map_norm, SimpleFunc.map_apply]
-- 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 μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)
have h : ∀ (a : α)
  (h : Eq (α := ℝ) ((toSimpleFunc (negPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)),
  Eq (α := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (negPart f)) : (a : α) → ℝ) a : ℝ)
Tactic: filter_upwards [negPart_toSimpleFunc f] with _ 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 : α) → ℝ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (negPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
⊢ Eq (α := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (negPart f)) : (a : α) → ℝ) a : ℝ)
have h₁ : ((toSimpleFunc f).negPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
Tactic: rw [SimpleFunc.map_apply, 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 : α) → ℝ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (negPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
| ((toSimpleFunc f).negPart : (a : α) → ℝ) a
have rw : norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
Tactic: rw [← SimpleFunc.negPart_map_norm, SimpleFunc.map_apply]
-- 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 : α) → ℝ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (negPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
⊢ ((toSimpleFunc f).negPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
have conv_lhs : ((toSimpleFunc f).negPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
Tactic: conv_lhs => rw [← SimpleFunc.negPart_map_norm, SimpleFunc.map_apply]
-- 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 : α) → ℝ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (negPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
conv_lhs : ((toSimpleFunc f).negPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
⊢ ((toSimpleFunc f).negPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
have h₁ : norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ) =
  norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
Tactic: conv_lhs => rw [← SimpleFunc.negPart_map_norm, SimpleFunc.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (hypothesis)
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 : α) → ℝ)
⊢ integral f = ‖posPart f‖ - ‖negPart f‖
have ae_eq₂ : (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]