-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_smul_measure (f : α → G) (c : ℝ≥0∞) :
    ∫ x, f x ∂c • μ = c.toReal • ∫ x, f x ∂μ

Proof state:
case pos.inl
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
⊢ ∫ (x : α), f x ∂⊤ • μ = ⊤.toReal • ∫ (x : α), f x ∂μ

Tactic:
rw [ENNReal.top_toReal, zero_smul, integral_eq_setToFun, setToFun_top_smul_measure]

Result:
no goals

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
⊢ ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : ¬CompleteSpace G
⊢ ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ

Tactic:
swap

Result:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : ¬CompleteSpace G
⊢ ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ

case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
⊢ ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ

Proof state:
case pos.inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
hc : c ≠ ⊤
hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ)) c.toReal
hdfma_smul : DominatedFinMeasAdditive (c • μ) (weightedSMul (c • μ)) 1
⊢ setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f = setToFun μ (fun s => c.toReal • weightedSMul μ s) ⋯ f

Tactic:
rw [← setToFun_congr_smul_measure c hc hdfma hdfma_smul f]

Result:
case pos.inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
hc : c ≠ ⊤
hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ)) c.toReal
hdfma_smul : DominatedFinMeasAdditive (c • μ) (weightedSMul (c • μ)) 1
⊢ setToFun μ (weightedSMul (c • μ)) hdfma f = setToFun μ (fun s => c.toReal • weightedSMul μ s) ⋯ f

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
⊢ ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
⊢ ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : ¬CompleteSpace G
⊢ ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
⊢ ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ

Tactic:
rcases eq_or_ne c ∞ with (rfl | hc)

Result:
case pos.inl
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
⊢ ∫ (x : α), f x ∂⊤ • μ = ⊤.toReal • ∫ (x : α), f x ∂μ

case pos.inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
hc : c ≠ ⊤
⊢ ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : ¬CompleteSpace G
⊢ ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ

Tactic:
simp [integral, hG]

Result:
no goals

Proof state:
case pos.inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
hc : c ≠ ⊤
⊢ setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f = setToFun μ (fun s => c.toReal • weightedSMul μ s) ⋯ f

Tactic:
have hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ) : Set α → G →L[ℝ] G) c.toReal :=
  mul_one c.toReal ▸ (dominatedFinMeasAdditive_weightedSMul (c • μ)).of_smul_measure hc

Result:
case pos.inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
hc : c ≠ ⊤
hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ)) c.toReal
⊢ setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f = setToFun μ (fun s => c.toReal • weightedSMul μ s) ⋯ f

Proof state:
case pos.inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
hc : c ≠ ⊤
hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ)) c.toReal
hdfma_smul : DominatedFinMeasAdditive (c • μ) (weightedSMul (c • μ)) 1
⊢ setToFun μ (weightedSMul (c • μ)) hdfma f = setToFun μ (fun s => c.toReal • weightedSMul μ s) ⋯ f

Tactic:
exact setToFun_congr_left' _ _ (fun s _ _ => weightedSMul_smul_measure μ c) f

Result:
no goals

Proof state:
case pos.inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
hc : c ≠ ⊤
⊢ ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ

Tactic:
simp_rw [integral_eq_setToFun, ← setToFun_smul_left]

Result:
case pos.inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
hc : c ≠ ⊤
⊢ setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f = setToFun μ (fun s => c.toReal • weightedSMul μ s) ⋯ f

Proof state:
case pos.inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
hc : c ≠ ⊤
hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ)) c.toReal
⊢ setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f = setToFun μ (fun s => c.toReal • weightedSMul μ s) ⋯ f

Tactic:
have hdfma_smul := dominatedFinMeasAdditive_weightedSMul (F := G) (c • μ)

Result:
case pos.inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hG : CompleteSpace G
hc : c ≠ ⊤
hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ)) c.toReal
hdfma_smul : DominatedFinMeasAdditive (c • μ) (weightedSMul (c • μ)) 1
⊢ setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f = setToFun μ (fun s => c.toReal • weightedSMul μ s) ⋯ f