α : Type u_2
β : Type ?u.1643027
E✝ : Type ?u.1643030
F : Type ?u.1643033
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ c = 0 ∨ ↑↑(Measure.restrict μ s) univ ≠ ⊤
α : Type u_2
β : Type ?u.1643027
E✝ : Type ?u.1643030
F : Type ?u.1643033
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ Integrable ↑↑(indicatorConstLp p hs hμs c)
rw [integrable_congr indicatorConstLp_coeFn, integrable_indicator_iff hs, IntegrableOn,
  integrable_const_iff, lt_top_iff_ne_top]
case h
α : Type u_2
β : Type ?u.1643027
E✝ : Type ?u.1643030
F : Type ?u.1643033
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ ↑↑(Measure.restrict μ s) univ ≠ ⊤
α : Type u_2
β : Type ?u.1643027
E✝ : Type ?u.1643030
F : Type ?u.1643033
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ c = 0 ∨ ↑↑(Measure.restrict μ s) univ ≠ ⊤
right
no goals
case h
α : Type u_2
β : Type ?u.1643027
E✝ : Type ?u.1643030
F : Type ?u.1643033
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ ↑↑(Measure.restrict μ s) univ ≠ ⊤
simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply] using hμs