case h
α : Type u_1
E : Type u_2
F : Type ?u.709397
G : Type ?u.709400
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs✝ : MeasurableSet s✝
hμs✝ : ↑↑μ s✝ ≠ ⊤
c✝ : E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : ↑↑μ s ≠ ⊤
hμt : ↑↑μ t ≠ ⊤
hst : s ∩ t = ∅
c : E
⊢ ↑↑(indicatorConstLp p (_ : MeasurableSet (s ∪ t)) (_ : ↑↑μ (s ∪ t) ≠ ⊤) c) =ᵐ[μ]
    ↑↑(indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c)
α : Type u_1
E : Type u_2
F : Type ?u.709397
G : Type ?u.709400
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs✝ : MeasurableSet s✝
hμs✝ : ↑↑μ s✝ ≠ ⊤
c✝ : E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : ↑↑μ s ≠ ⊤
hμt : ↑↑μ t ≠ ⊤
hst : s ∩ t = ∅
c : E
⊢ indicatorConstLp p (_ : MeasurableSet (s ∪ t)) (_ : ↑↑μ (s ∪ t) ≠ ⊤) c =
    indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c
ext1
case h
α : Type u_1
E : Type u_2
F : Type ?u.709397
G : Type ?u.709400
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs✝ : MeasurableSet s✝
hμs✝ : ↑↑μ s✝ ≠ ⊤
c✝ : E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : ↑↑μ s ≠ ⊤
hμt : ↑↑μ t ≠ ⊤
hst : s ∩ t = ∅
c : E
⊢ (Set.indicator (s ∪ t) fun x => c) =ᵐ[μ] ↑↑(indicatorConstLp p hs hμs c) + ↑↑(indicatorConstLp p ht hμt c)
case h
α : Type u_1
E : Type u_2
F : Type ?u.709397
G : Type ?u.709400
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs✝ : MeasurableSet s✝
hμs✝ : ↑↑μ s✝ ≠ ⊤
c✝ : E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : ↑↑μ s ≠ ⊤
hμt : ↑↑μ t ≠ ⊤
hst : s ∩ t = ∅
c : E
⊢ ↑↑(indicatorConstLp p (_ : MeasurableSet (s ∪ t)) (_ : ↑↑μ (s ∪ t) ≠ ⊤) c) =ᵐ[μ]
    ↑↑(indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c)
refine' indicatorConstLp_coeFn.trans (EventuallyEq.trans _ (Lp.coeFn_add _ _).symm)
case h
α : Type u_1
E : Type u_2
F : Type ?u.709397
G : Type ?u.709400
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs✝ : MeasurableSet s✝
hμs✝ : ↑↑μ s✝ ≠ ⊤
c✝ : E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : ↑↑μ s ≠ ⊤
hμt : ↑↑μ t ≠ ⊤
hst : s ∩ t = ∅
c : E
⊢ (Set.indicator (s ∪ t) fun x => c) =ᵐ[μ] fun x => Set.indicator s (fun x => c) x + Set.indicator t (fun x => c) x
case h
α : Type u_1
E : Type u_2
F : Type ?u.709397
G : Type ?u.709400
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs✝ : MeasurableSet s✝
hμs✝ : ↑↑μ s✝ ≠ ⊤
c✝ : E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : ↑↑μ s ≠ ⊤
hμt : ↑↑μ t ≠ ⊤
hst : s ∩ t = ∅
c : E
⊢ (Set.indicator (s ∪ t) fun x => c) =ᵐ[μ] ↑↑(indicatorConstLp p hs hμs c) + ↑↑(indicatorConstLp p ht hμt c)
refine'
  EventuallyEq.trans _
    (EventuallyEq.add indicatorConstLp_coeFn.symm indicatorConstLp_coeFn.symm)
no goals
case h
α : Type u_1
E : Type u_2
F : Type ?u.709397
G : Type ?u.709400
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs✝ : MeasurableSet s✝
hμs✝ : ↑↑μ s✝ ≠ ⊤
c✝ : E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : ↑↑μ s ≠ ⊤
hμt : ↑↑μ t ≠ ⊤
hst : s ∩ t = ∅
c : E
⊢ (Set.indicator (s ∪ t) fun x => c) =ᵐ[μ] fun x => Set.indicator s (fun x => c) x + Set.indicator t (fun x => c) x
rw [Set.indicator_union_of_disjoint (Set.disjoint_iff_inter_eq_empty.mpr hst) _]