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

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ (toSimpleFunc (-f)) a ⊔ 0 = (-toSimpleFunc f) a ⊔ 0

Tactic:
rw [h₂]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ (-⇑(toSimpleFunc f)) a ⊔ 0 = (-toSimpleFunc f) a ⊔ 0

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

Tactic:
rw [SimpleFunc.negPart, MeasureTheory.SimpleFunc.negPart]

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

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

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

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ ∀ (a : α),
    (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a →
      (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a → (toSimpleFunc (posPart (-f))) a = (-toSimpleFunc f).posPart a

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ (toSimpleFunc (-f)).posPart a = (-toSimpleFunc f).posPart a

Tactic:
show max _ _ = max _ _

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ (toSimpleFunc (-f)) a ⊔ 0 = (-toSimpleFunc f) a ⊔ 0

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ (toSimpleFunc (posPart (-f))) a = (-toSimpleFunc f).posPart a

Tactic:
rw [h₁]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ (toSimpleFunc (-f)).posPart a = (-toSimpleFunc f).posPart a

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ (-⇑(toSimpleFunc f)) a ⊔ 0 = (-toSimpleFunc f) a ⊔ 0

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ ∀ (a : α),
    (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a →
      (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a → (toSimpleFunc (posPart (-f))) a = (-toSimpleFunc f).posPart a

Tactic:
intro a h₁ h₂

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ (toSimpleFunc (posPart (-f))) a = (-toSimpleFunc f).posPart a