-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem posPart_toSimpleFunc (f : α →₁ₛ[μ] ℝ) :
    toSimpleFunc (posPart f) =ᵐ[μ] (toSimpleFunc f).posPart

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = (toSimpleFunc f) a ⊔ 0
⊢ ⇑(toSimpleFunc (posPart f)) =ᶠ[ae μ] ⇑(toSimpleFunc f).posPart

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₃]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = (toSimpleFunc f) a ⊔ 0
ae_eq : ∀ᵐ (a : α) ∂μ, (toSimpleFunc (posPart f)) a = (toSimpleFunc f) a ⊔ 0
⊢ ⇑(toSimpleFunc (posPart f)) =ᶠ[ae μ] ⇑(toSimpleFunc f).posPart

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = (toSimpleFunc f) a ⊔ 0
⊢ ∀ᵐ (a : α) ∂μ, (toSimpleFunc (posPart f)) a = (toSimpleFunc f) a ⊔ 0

Tactic:
filter_upwards [toSimpleFunc_eq_toFun (posPart f), Lp.coeFn_posPart (f : α →₁[μ] ℝ),
  toSimpleFunc_eq_toFun f] with _ _ h₂ h₃

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = (toSimpleFunc f) a ⊔ 0
a✝¹ : α
a✝ : (toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = ↑↑↑f a✝¹ ⊔ 0
h₃ : (toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
⊢ (toSimpleFunc (posPart f)) a✝¹ = (toSimpleFunc f) a✝¹ ⊔ 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ ⇑(toSimpleFunc (posPart f)) =ᶠ[ae μ] ⇑(toSimpleFunc f).posPart

Tactic:
have eq : ∀ a, (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0 := fun a => rfl

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = (toSimpleFunc f) a ⊔ 0
⊢ ⇑(toSimpleFunc (posPart f)) =ᶠ[ae μ] ⇑(toSimpleFunc f).posPart

Proof state:
case h.e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = (toSimpleFunc f) a ⊔ 0
a✝¹ : α
a✝ : (toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = ↑↑↑f a✝¹ ⊔ 0
h₃ : (toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
⊢ (toSimpleFunc f) a✝¹ ⊔ 0 = ↑↑↑f a✝¹ ⊔ 0

Tactic:
rw [h₃]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = (toSimpleFunc f) a ⊔ 0
ae_eq : ∀ᵐ (a : α) ∂μ, (toSimpleFunc (posPart f)) a = (toSimpleFunc f) a ⊔ 0
⊢ ⇑(toSimpleFunc (posPart f)) =ᶠ[ae μ] ⇑(toSimpleFunc f).posPart

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

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = (toSimpleFunc f) a ⊔ 0
ae_eq : ∀ᵐ (a : α) ∂μ, (toSimpleFunc (posPart f)) a = (toSimpleFunc f) a ⊔ 0
a : α
h : (toSimpleFunc (posPart f)) a = (toSimpleFunc f) a ⊔ 0
⊢ (toSimpleFunc (posPart f)) a = (toSimpleFunc f).posPart a

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = (toSimpleFunc f) a ⊔ 0
ae_eq : ∀ᵐ (a : α) ∂μ, (toSimpleFunc (posPart f)) a = (toSimpleFunc f) a ⊔ 0
a : α
h : (toSimpleFunc (posPart f)) a = (toSimpleFunc f) a ⊔ 0
⊢ (toSimpleFunc (posPart f)) a = (toSimpleFunc f).posPart a

Tactic:
rw [h, eq]

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = (toSimpleFunc f) a ⊔ 0
a✝¹ : α
a✝ : (toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = ↑↑↑f a✝¹ ⊔ 0
h₃ : (toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
⊢ (toSimpleFunc (posPart f)) a✝¹ = (toSimpleFunc f) a✝¹ ⊔ 0

Tactic:
convert h₂ using 1

Result:
case h.e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = (toSimpleFunc f) a ⊔ 0
a✝¹ : α
a✝ : (toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = ↑↑↑f a✝¹ ⊔ 0
h₃ : (toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
⊢ (toSimpleFunc f) a✝¹ ⊔ 0 = ↑↑↑f a✝¹ ⊔ 0