-- 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
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

Tactic:
rw [condExpIndSMul]

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)
⊢ ↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ⋯ hμst 1))) =ᶠ[ae μ] fun x_1 =>
    ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm ht hμt x) x_1

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)
⊢ ↑↑((compLpL 2 μ (toSpanSingleton ℝ x))
          ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1) +
              (condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1))) =ᶠ[ae μ]
    fun x_1 => ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm ht hμt x) x_1

Tactic:
push_cast

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)
⊢ ↑↑((compLpL 2 μ (toSpanSingleton ℝ x))
          (↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) +
            ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1)))) =ᶠ[ae μ]
    fun x_1 => ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm ht hμt x) x_1

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)
⊢ ↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) +
      ↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1))) =ᶠ[ae μ]
    fun x_1 => ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm ht hμt x) x_1

Tactic:
filter_upwards with y using rfl

Result:
no goals

Proof state:
α : 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 = condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm ht hμt x

Tactic:
ext1

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
⊢ ↑↑(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)
ht_eq : ↑↑(condExpIndL1Fin hm ht hμt x) =ᶠ[ae μ] ↑↑(condExpIndSMul hm ht hμt x)
⊢ ↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ⋯ hμst 1))) =ᶠ[ae μ] fun x_1 =>
    ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm ht hμt x) x_1

Tactic:
rw [indicatorConstLp_disjoint_union hs ht hμs hμt hst (1 : ℝ)]

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)
⊢ ↑↑((compLpL 2 μ (toSpanSingleton ℝ x))
          ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1 + indicatorConstLp 2 ht hμt 1))) =ᶠ[ae μ]
    fun x_1 => ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm ht hμt x) x_1

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) ≠ ⊤
⊢ ↑↑(condExpIndSMul hm ⋯ hμst x) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x) + ↑↑(condExpIndL1Fin hm ht hμt x)

Tactic:
have hs_eq := condExpIndL1Fin_ae_eq_condExpIndSMul hm hs hμs 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)
⊢ ↑↑(condExpIndSMul hm ⋯ hμst x) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x) + ↑↑(condExpIndL1Fin hm ht hμt x)