-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1S_neg {T : Set α → E →L[ℝ] F} (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0)
    (h_add : FinMeasAdditive μ T) (f : α →₁ₛ[μ] E) : setToL1S T (-f) = -setToL1S T f

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : ↥(simpleFunc E 1 μ)
this : ⇑(toSimpleFunc (-f)) =ᶠ[ae μ] ⇑(-toSimpleFunc f)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
rw [SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) this]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : ↥(simpleFunc E 1 μ)
this : ⇑(toSimpleFunc (-f)) =ᶠ[ae μ] ⇑(-toSimpleFunc f)
⊢ SimpleFunc.setToSimpleFunc T (-toSimpleFunc f) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : ↥(simpleFunc E 1 μ)
this : ⇑(toSimpleFunc (-f)) =ᶠ[ae μ] ⇑(-toSimpleFunc f)
⊢ SimpleFunc.setToSimpleFunc T (-toSimpleFunc f) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
exact SimpleFunc.setToSimpleFunc_neg T h_add (SimpleFunc.integrable f)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
have : simpleFunc.toSimpleFunc (-f) =ᵐ[μ] ⇑(-simpleFunc.toSimpleFunc f) :=
  neg_toSimpleFunc f

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : ↥(simpleFunc E 1 μ)
this : ⇑(toSimpleFunc (-f)) =ᶠ[ae μ] ⇑(-toSimpleFunc f)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S T (-f) = -setToL1S T f

Tactic:
simp_rw [setToL1S]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)