-- Mathlib/MeasureTheory/Integral/Average.lean
theorem average_union_mem_segment {f : α → E} {s t : Set α} (hd : AEDisjoint μ s t)
    (ht : NullMeasurableSet t μ) (hsμ : μ s ≠ ∞) (htμ : μ t ≠ ∞) (hfs : IntegrableOn f s μ)
    (hft : IntegrableOn f t μ) :
    ⨍ x in s ∪ t, f x ∂μ ∈ [⨍ x in s, f x ∂μ -[ℝ] ⨍ x in t, f x ∂μ]

Proof state:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : s =ᶠ[ae μ] ∅
⊢ ⨍ (x : α) in t, f x ∂μ ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]

Tactic:
exact right_mem_segment _ _ _

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : s =ᶠ[ae μ] ∅
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]

Tactic:
rw [restrict_congr_set (hse.union EventuallyEq.rfl), empty_union]

Result:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : s =ᶠ[ae μ] ∅
⊢ ⨍ (x : α) in t, f x ∂μ ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]

Proof state:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : ¬μ s = 0
⊢ 0 < (μ s).toReal + (μ t).toReal

Tactic:
calc
  0 < (μ s).toReal := ENNReal.toReal_pos hse hsμ
  _ ≤ _ := le_add_of_nonneg_right ENNReal.toReal_nonneg

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : μ s = 0
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]

Tactic:
rw [← ae_eq_empty] at hse

Result:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : s =ᶠ[ae μ] ∅
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]

Tactic:
by_cases hse : μ s = 0

Result:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : μ s = 0
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]

case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : ¬μ s = 0
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]

Proof state:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : ¬μ s = 0
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]

Tactic:
refine
  mem_segment_iff_div.mpr
    ⟨(μ s).toReal, (μ t).toReal, ENNReal.toReal_nonneg, ENNReal.toReal_nonneg, ?_,
      (average_union hd ht hsμ htμ hfs hft).symm⟩

Result:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : ¬μ s = 0
⊢ 0 < (μ s).toReal + (μ t).toReal