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

Proof state:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedField 𝕜
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)

Tactic:
refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) ?_

Result:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedField 𝕜
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(simpleFunc E 1 μ)
⊢ ⇑(toSimpleFunc (c • f)) =ᶠ[ae μ] ⇑(c • toSimpleFunc f)

Proof state:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedField 𝕜
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = c • SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
rw [← SimpleFunc.setToSimpleFunc_smul T h_add h_smul c (SimpleFunc.integrable f)]

Result:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedField 𝕜
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)

Proof state:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedField 𝕜
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(simpleFunc E 1 μ)
⊢ ⇑(toSimpleFunc (c • f)) =ᶠ[ae μ] ⇑(c • toSimpleFunc f)

Tactic:
exact smul_toSimpleFunc c f

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedField 𝕜
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(simpleFunc E 1 μ)
⊢ setToL1S T (c • f) = c • setToL1S T f

Tactic:
simp_rw [setToL1S]

Result:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedField 𝕜
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = c • SimpleFunc.setToSimpleFunc T (toSimpleFunc f)