-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_const (c : E) : ∫ _ : α, c ∂μ = (μ univ).toReal • c

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
c : E
hμ : IsFiniteMeasure μ
⊢ ∫ (x : α), c ∂μ = (μ univ).toReal • c

Tactic:
simp only [integral, hE, L1.integral]

Result:
case pos
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
c : E
hμ : IsFiniteMeasure μ
⊢ (if h : True then if hf : Integrable (fun x => c) μ then L1.integralCLM (Integrable.toL1 (fun x => c) hf) else 0
    else 0) =
    (μ univ).toReal • c

Proof state:
case neg
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
c : E
hμ : ¬IsFiniteMeasure μ
⊢ ∫ (x : α), c ∂μ = (μ univ).toReal • c

Tactic:
by_cases hc : c = 0

Result:
case pos
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
c : E
hμ : ¬IsFiniteMeasure μ
hc : c = 0
⊢ ∫ (x : α), c ∂μ = (μ univ).toReal • c

case neg
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
c : E
hμ : ¬IsFiniteMeasure μ
hc : ¬c = 0
⊢ ∫ (x : α), c ∂μ = (μ univ).toReal • c

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
c : E
⊢ ∫ (x : α), c ∂μ = (μ univ).toReal • c

Tactic:
by_cases hμ : IsFiniteMeasure μ

Result:
case pos
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
c : E
hμ : IsFiniteMeasure μ
⊢ ∫ (x : α), c ∂μ = (μ univ).toReal • c

case neg
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
c : E
hμ : ¬IsFiniteMeasure μ
⊢ ∫ (x : α), c ∂μ = (μ univ).toReal • c

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
c : E
hμ : ¬IsFiniteMeasure μ
hc : c = 0
⊢ ∫ (x : α), c ∂μ = (μ univ).toReal • c

Tactic:
simp [hc, integral_zero]

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
c : E
hμ : IsFiniteMeasure μ
⊢ (if h : True then if hf : Integrable (fun x => c) μ then L1.integralCLM (Integrable.toL1 (fun x => c) hf) else 0
    else 0) =
    (μ univ).toReal • c

Tactic:
exact setToFun_const (dominatedFinMeasAdditive_weightedSMul _) _

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
c : E
hμ : ¬IsFiniteMeasure μ
hc : ¬c = 0
⊢ ∫ (x : α), c ∂μ = (μ univ).toReal • c

Tactic:
simp [(integrable_const_iff_isFiniteMeasure hc).not.2 hμ,
  integral_undef, MeasureTheory.not_isFiniteMeasure_iff.mp hμ]

Result:
no goals