-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem memLp_add_of_disjoint {f g : α → E} (h : Disjoint (support f) (support g))
    (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
    MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ

Proof state:
case refine_2
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp g p μ

Tactic:
rw [← Set.indicator_add_eq_right h]

Result:
case refine_2
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp ((support g).indicator (f + g)) p μ

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ

Tactic:
borelize E

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ

Proof state:
case refine_1
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp ((support f).indicator (f + g)) p μ

Tactic:
exact hfg.indicator (measurableSet_support hf.measurable)

Result:
no goals

Proof state:
case refine_1
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp f p μ

Tactic:
rw [← Set.indicator_add_eq_left h]

Result:
case refine_1
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp ((support f).indicator (f + g)) p μ

Proof state:
case refine_2
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp ((support g).indicator (f + g)) p μ

Tactic:
exact hfg.indicator (measurableSet_support hg.measurable)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ

Tactic:
refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩

Result:
case refine_1
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp f p μ

case refine_2
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp g p μ