Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos.refine_2
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ (c : E) ⦃s_1 : Set Ω⦄,
    MeasurableSet s_1 →
      μ s_1 < ∞ → μ.real s • ∫ (x : Ω), s_1.indicator (fun x ↦ c) x ∂μ = ∫ (x : Ω) in s, s_1.indicator (fun x ↦ c) x ∂μ

pp: case pos.refine_3
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f 1 μ →
        MemLp g 1 μ →
          StronglyMeasurable f →
            StronglyMeasurable g →
              μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
                μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ →
                  μ.real s • ∫ (x : Ω), (f + g) x ∂μ = ∫ (x : Ω) in s, (f + g) x ∂μ

pp: case pos.refine_4
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ IsClosed {f | μ.real s • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}

pp: case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    f =ᵐ[μ] g →
      MemLp f 1 μ →
        μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ → μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ

Tactic:
· intro c t hmt _
    rw [Indep_iff] at hindp
    rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, measureReal_def,
      measureReal_def, ← ENNReal.toReal_mul,
      mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
      Set.inter_comm, measureReal_def]

Goal state after:
case pos.refine_3
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f 1 μ →
        MemLp g 1 μ →
          StronglyMeasurable f →
            StronglyMeasurable g →
              μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
                μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ →
                  μ.real s • ∫ (x : Ω), (f + g) x ∂μ = ∫ (x : Ω) in s, (f + g) x ∂μ

case pos.refine_4
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ IsClosed {f | μ.real s • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}

case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    f =ᵐ[μ] g →
      MemLp f 1 μ →
        μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ → μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ