case inl
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ < ⊤
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c

case inr
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ = ⊤
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c
cases' (@le_top _ _ _ (μ univ)).lt_or_eq with hμ hμ
case inl
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ < ⊤
this : IsFiniteMeasure μ
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c
case inl
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ < ⊤
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c
haveI : IsFiniteMeasure μ := ⟨hμ⟩
case inl
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ < ⊤
this : IsFiniteMeasure μ
⊢ (if hf : Integrable fun x => c then ↑L1.integralCLM (Integrable.toL1 (fun x => c) hf) else 0) =
    ENNReal.toReal (↑↑μ univ) • c
case inl
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ < ⊤
this : IsFiniteMeasure μ
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c
simp only [integral, L1.integral]
no goals
case inl
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ < ⊤
this : IsFiniteMeasure μ
⊢ (if hf : Integrable fun x => c then ↑L1.integralCLM (Integrable.toL1 (fun x => c) hf) else 0) =
    ENNReal.toReal (↑↑μ univ) • c
exact setToFun_const (dominatedFinMeasAdditive_weightedSMul _) _
case pos
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ = ⊤
hc : c = 0
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c

case neg
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ = ⊤
hc : ¬c = 0
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c
case inr
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ = ⊤
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c
by_cases hc : c = 0
no goals
case pos
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ = ⊤
hc : c = 0
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c
simp [hc, integral_zero]
case neg
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ = ⊤
hc : ¬c = 0
this : ¬Integrable fun x => c
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c
case neg
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ = ⊤
hc : ¬c = 0
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c
have : ¬Integrable (fun _ : α => c) μ := by
  simp only [integrable_const_iff, not_or]
  exact ⟨hc, hμ.not_lt⟩
no goals
case neg
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ = ⊤
hc : ¬c = 0
this : ¬Integrable fun x => c
⊢ (∫ (x : α), c ∂μ) = ENNReal.toReal (↑↑μ univ) • c
simp [integral_undef, *]
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ = ⊤
hc : ¬c = 0
⊢ ¬c = 0 ∧ ¬↑↑μ univ < ⊤
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ = ⊤
hc : ¬c = 0
⊢ ¬Integrable fun x => c
simp only [integrable_const_iff, not_or]
no goals
α : Type u_2
E : Type u_1
F : Type ?u.1256042
𝕜 : Type ?u.1256045
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1258736
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
c : E
hμ : ↑↑μ univ = ⊤
hc : ¬c = 0
⊢ ¬c = 0 ∧ ¬↑↑μ univ < ⊤
exact ⟨hc, hμ.not_lt⟩