-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpIndL1Fin_disjoint_union (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ∞)
    (hμt : μ t ≠ ∞) (hst : Disjoint s t) (x : G) :
    condExpIndL1Fin hm (hs.union ht) ((measure_union_le s t).trans_lt
      (lt_top_iff_ne_top.mpr (ENNReal.add_ne_top.mpr ⟨hμs, hμt⟩))).ne x =
    condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm ht hμt x

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
⊢ ↑↑(condExpIndL1Fin hm ⋯ ⋯ x) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm ht hμt x)

Tactic:
have hμst := measure_union_ne_top hμs hμt

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
hμst : μ (s ∪ t) ≠ ⊤
⊢ ↑↑(condExpIndL1Fin hm ⋯ ⋯ x) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm ht hμt x)

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
hμst : μ (s ∪ t) ≠ ⊤
hs_eq : ↑↑(condExpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condExpIndSMul hm hs hμs x)
⊢ ↑↑(condExpIndSMul hm ⋯ hμst x) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x) + ↑↑(condExpIndL1Fin hm ht hμt x)

Tactic:
have ht_eq := condExpIndL1Fin_ae_eq_condExpIndSMul hm ht hμt x

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
hμst : μ (s ∪ t) ≠ ⊤
hs_eq : ↑↑(condExpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condExpIndSMul hm hs hμs x)
ht_eq : ↑↑(condExpIndL1Fin hm ht hμt x) =ᶠ[ae μ] ↑↑(condExpIndSMul hm ht hμt x)
⊢ ↑↑(condExpIndSMul hm ⋯ hμst x) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x) + ↑↑(condExpIndL1Fin hm ht hμt x)

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
hμst : μ (s ∪ t) ≠ ⊤
hs_eq : ↑↑(condExpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condExpIndSMul hm hs hμs x)
ht_eq : ↑↑(condExpIndL1Fin hm ht hμt x) =ᶠ[ae μ] ↑↑(condExpIndSMul hm ht hμt x)
⊢ ↑↑(condExpIndSMul hm ⋯ hμst x) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x) + ↑↑(condExpIndL1Fin hm ht hμt x)

Tactic:
refine EventuallyEq.trans ?_ (EventuallyEq.add hs_eq.symm ht_eq.symm)

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
hμst : μ (s ∪ t) ≠ ⊤
hs_eq : ↑↑(condExpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condExpIndSMul hm hs hμs x)
ht_eq : ↑↑(condExpIndL1Fin hm ht hμt x) =ᶠ[ae μ] ↑↑(condExpIndSMul hm ht hμt x)
⊢ ↑↑(condExpIndSMul hm ⋯ hμst x) =ᶠ[ae μ] fun x_1 =>
    ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm ht hμt x) x_1