awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 : α →ₘ[μ] ℝ)
⊢ AEEqFun.mk (⇑s.posPart : (a : α) → ℝ) ⋯ =
    (↑(Lp.posPart
          (↑(Subtype.mk (p := fun (x : ↥(Lp ℝ 1 μ)) ↦
                Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ) x) f ⋯) :
            ↥(Lp ℝ 1 μ))) :
      α →ₘ[μ] ℝ)

Tactic:
simp only [SimpleFunc.posPart, SimpleFunc.coe_map, Function.comp_def, coe_posPart, ← hsf,
      posPart_mk]

Premises used: MeasureTheory.SimpleFunc.coe_map, MeasureTheory.L1.SimpleFunc.posPart, Function.comp_def, MeasureTheory.Lp.coe_posPart, MeasureTheory.AEEqFun.posPart_mk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ (↑(posPart f) : ↥(Lp ℝ 1 μ)) = Lp.posPart (↑f : ↥(Lp ℝ 1 μ))

Tactic:
rfl

Premises used: MeasureTheory.Lp.posPart, rfl, LipschitzWith.compLp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ (↑(negPart f) : ↥(Lp ℝ 1 μ)) = Lp.negPart (↑f : ↥(Lp ℝ 1 μ))

Tactic:
rfl

Premises used: MeasureTheory.Lp.negPart, MeasureTheory.Lp.posPart, rfl, LipschitzWith.compLp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f : ↥(simpleFunc E 1 μ)
⊢ integral f = MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)

Tactic:
rfl

Premises used: MeasureTheory.L1.SimpleFunc.integral, rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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
rw₁ rw₂ :
  (∫⁻ (a : α), ENNReal.ofReal ((toSimpleFunc f : (a : α) → ℝ) a) ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal ((toSimpleFunc f : (a : α) → ℝ) a) ∂μ).toReal
⊢ integral f = (∫⁻ (a : α), ENNReal.ofReal ((toSimpleFunc f : (a : α) → ℝ) a) ∂μ).toReal

Tactic:
rw [integral, SimpleFunc.integral_eq_lintegral (SimpleFunc.integrable f) h_pos]

Premises used: MeasureTheory.L1.SimpleFunc.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
f : ↥(simpleFunc E 1 μ)
⊢ integral f = setToL1S (weightedSMul μ) f

Tactic:
rfl

Premises used: MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.integral, 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
f g : ↥(simpleFunc E 1 μ)
h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc f) : (a : α) → E) (⇑(toSimpleFunc g) : (a : α) → E)
⊢ integral f = integral g

Tactic:
SimpleFunc.integral_congr (SimpleFunc.integrable f) h

Premises used: MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.L1.SimpleFunc.integral, MeasureTheory.SimpleFunc.integral_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
f g : ↥(simpleFunc E 1 μ)
⊢ integral (f + g) = integral f + integral g

Tactic:
setToL1S_add _ (fun _ _ => weightedSMul_null) weightedSMul_union _ _

Premises used: MeasureTheory.weightedSMul_null, MeasureTheory.weightedSMul_union, MeasureTheory.L1.SimpleFunc.integral, MeasureTheory.SimpleFunc.integral, MeasureTheory.L1.SimpleFunc.setToL1S_add
-- 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 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : SMulCommClass ℝ 𝕜 E
c : 𝕜
f : ↥(simpleFunc E 1 μ)
⊢ integral (c • f) = c • integral f

Tactic:
setToL1S_smul _ (fun _ _ => weightedSMul_null) weightedSMul_union weightedSMul_smul c f

Premises used: MeasureTheory.weightedSMul_null, MeasureTheory.weightedSMul_smul, MeasureTheory.weightedSMul_union, MeasureTheory.L1.SimpleFunc.integral, MeasureTheory.SimpleFunc.integral, MeasureTheory.L1.SimpleFunc.setToL1S_smul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f : ↥(simpleFunc E 1 μ)
rw :
  ‖MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)‖ ≤
    MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))
⊢ ‖integral f‖ ≤ ‖f‖

Tactic:
rw [integral, norm_eq_integral]

Premises used: MeasureTheory.L1.SimpleFunc.integral, MeasureTheory.L1.SimpleFunc.norm_eq_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
f : ↥(simpleFunc E 1 μ)
⊢ ‖MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)‖ ≤
    MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))

Tactic:
(toSimpleFunc f).norm_integral_le_integral_norm (SimpleFunc.integrable f)

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc, MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.norm_integral_le_integral_norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f : ↥(simpleFunc E 1 μ)
⊢ ‖MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)‖ ≤
    MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))

Tactic:
exact (toSimpleFunc f).norm_integral_le_integral_norm (SimpleFunc.integrable f)

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc, MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.norm_integral_le_integral_norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 μ)
rw rw₁ : ‖f‖ ≤ ‖f‖
⊢ ‖f‖ ≤ 1 * ‖f‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f : ↥(simpleFunc E 1 μ)
⊢ norm.{u_2} (E := E)
      (({ toFun := integral, map_add' := ⋯, map_smul' := ⋯ : ↥(simpleFunc E 1 μ) →ₗ[ℝ] E } :
            (a : ↥(simpleFunc E 1 μ)) → E)
          f :
        E) ≤
    1 * ‖f‖

Tactic:
simpa [one_mul] using norm_integral_le_norm f

Premises used: MeasureTheory.L1.SimpleFunc.norm_integral_le_norm, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ ∀ (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
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 →
    (↑(↑(Lp.posPart (↑f : ↥(Lp ℝ 1 μ))) : α →ₘ[μ] ℝ) : α → ℝ) a =
        max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0 →
      (toSimpleFunc f : (a : α) → ℝ) a = (↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a →
        Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
⊢ (toSimpleFunc (posPart f) : (a : α) → ℝ) a = (↑(↑(↑(posPart f) : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a →
    (↑(↑(Lp.posPart (↑f : ↥(Lp ℝ 1 μ))) : α →ₘ[μ] ℝ) : α → ℝ) a =
        max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0 →
      (toSimpleFunc f : (a : α) → ℝ) a = (↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a →
        Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq :
  ∀ (a : α), Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
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 : ℝ)
⊢ ∀ᵐ (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₃

Premises used: MeasureTheory.L1.SimpleFunc.posPart, MeasureTheory.Lp.coeFn_posPart, Subtype.val, MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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
⊢ (↑(↑(Lp.posPart (↑f : ↥(Lp ℝ 1 μ))) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0

Tactic:
h₂
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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_1 : (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
h : max ((toSimpleFunc f : (a : α) → ℝ) a) 0 = max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0
⊢ Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)

Tactic:
convert! h₂ using 1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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_1 : (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
h h₁ : max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0
⊢ max ((toSimpleFunc f : (a : α) → ℝ) a) 0 = max ((↑(↑(↑f : ↥(Lp ℝ 1 μ)) : α →ₘ[μ] ℝ) : α → ℝ) a) 0

Tactic:
rw [h₃]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 : ℝ)

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₃]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 : α) → ℝ)

Tactic:
ae_eq.mono fun a h => ?_

Premises used: Filter.EventuallyEq, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 : ℝ)
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 : ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc (posPart f)) : (a : α) → ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)

Tactic:
refine ae_eq.mono fun a h => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 : ℝ)
rw₁ rw₂ : Eq (α := ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ) (max ((toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
⊢ Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)

Tactic:
rw [h, eq]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
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 : ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc (posPart (-f))) : (a : α) → ℝ) (⇑(-toSimpleFunc f).posPart : (a : α) → ℝ)

Tactic:
filter_upwards [posPart_toSimpleFunc (-f), neg_toSimpleFunc f]

Premises used: MeasureTheory.Lp.simpleFunc.neg_toSimpleFunc, MeasureTheory.L1.SimpleFunc.posPart_toSimpleFunc, Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 : ℝ)
h : Eq (α := ℝ) (((toSimpleFunc (-f)).posPart : (a : α) → ℝ) a : ℝ) (((-toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
⊢ Eq (α := ℝ) ((toSimpleFunc (posPart (-f)) : (a : α) → ℝ) a : ℝ) (((-toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)

Tactic:
rw [h₁]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 : ℝ)
h : Eq (α := ℝ) (max ((-(⇑(toSimpleFunc f) : (a : α) → ℝ)) a) 0 : ℝ) (max ((-toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)
⊢ Eq (α := ℝ) (max ((toSimpleFunc (-f) : (a : α) → ℝ) a) 0 : ℝ) (max ((-toSimpleFunc f : (a : α) → ℝ) a) 0 : ℝ)

Tactic:
rw [h₂]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 : ℝ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
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 : ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).posPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f))) : (a : α) → ℝ)

Tactic:
filter_upwards [posPart_toSimpleFunc f] with _ h

Premises used: MeasureTheory.L1.SimpleFunc.posPart_toSimpleFunc
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
h₁ : ((toSimpleFunc f).posPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
⊢ Eq (α := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (posPart f)) : (a : α) → ℝ) a : ℝ)

Tactic:
rw [SimpleFunc.map_apply, h]

Premises used: MeasureTheory.SimpleFunc.map_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (posPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
rw : norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
| ((toSimpleFunc f).posPart : (a : α) → ℝ) a

Tactic:
rw [← SimpleFunc.posPart_map_norm, SimpleFunc.map_apply]

Premises used: MeasureTheory.SimpleFunc.posPart_map_norm, MeasureTheory.SimpleFunc.map_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 : ℝ)
h₁ :
  norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ) =
    norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)
⊢ ((toSimpleFunc f).posPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).posPart : (a : α) → ℝ) a : ℝ)

Tactic:
conv_lhs => rw [← SimpleFunc.posPart_map_norm, SimpleFunc.map_apply]

Premises used: MeasureTheory.SimpleFunc.posPart_map_norm, MeasureTheory.SimpleFunc.map_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ (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]
-- 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 : α) → ℝ)
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 : ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑(toSimpleFunc f).negPart : (a : α) → ℝ)
    (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f))) : (a : α) → ℝ)

Tactic:
filter_upwards [negPart_toSimpleFunc f] with _ h

Premises used: MeasureTheory.L1.SimpleFunc.negPart_toSimpleFunc
-- 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 : α) → ℝ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (negPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
h₁ : ((toSimpleFunc f).negPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
⊢ Eq (α := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
    ((SimpleFunc.map norm (toSimpleFunc (negPart f)) : (a : α) → ℝ) a : ℝ)

Tactic:
rw [SimpleFunc.map_apply, h]

Premises used: MeasureTheory.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 : α) → ℝ)
a : α
h : Eq (α := ℝ) ((toSimpleFunc (negPart f) : (a : α) → ℝ) a : ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
rw : norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
| ((toSimpleFunc f).negPart : (a : α) → ℝ) a

Tactic:
rw [← SimpleFunc.negPart_map_norm, SimpleFunc.map_apply]

Premises used: MeasureTheory.SimpleFunc.negPart_map_norm, MeasureTheory.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 : α) → ℝ)
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 : ℝ)
h₁ :
  norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ) =
    norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)
⊢ ((toSimpleFunc f).negPart : (a : α) → ℝ) a = norm (E := ℝ) (((toSimpleFunc f).negPart : (a : α) → ℝ) a : ℝ)

Tactic:
conv_lhs => rw [← SimpleFunc.negPart_map_norm, SimpleFunc.map_apply]

Premises used: MeasureTheory.SimpleFunc.negPart_map_norm, MeasureTheory.SimpleFunc.map_apply