-- Mathlib/Probability/ConditionalExpectation.lean
theorem condExp_indep_eq (hle₁ : m₁ ≤ m) (hle₂ : m₂ ≤ m) [SigmaFinite (μ.trim hle₂)]
    (hf : StronglyMeasurable[m₁] f) (hindp : Indep m₁ m₂ μ) : μ[f|m₂] =ᵐ[μ] fun _ => μ[f]

Proof state:
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 < ⊤
u v : Ω → E
a✝ : Disjoint (Function.support u) (Function.support v)
huint : MemLp u 1 μ
hvint : MemLp v 1 μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : (μ s).toReal • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
hv_eq : (μ s).toReal • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
⊢ (μ s).toReal • ∫ (x : Ω), (u + v) x ∂μ = ∫ (x : Ω) in s, (u + v) x ∂μ

Tactic:
rw [memLp_one_iff_integrable] at huint hvint

Result:
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 < ⊤
u v : Ω → E
a✝ : Disjoint (Function.support u) (Function.support v)
huint : Integrable u μ
hvint : Integrable v μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : (μ s).toReal • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
hv_eq : (μ s).toReal • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
⊢ (μ s).toReal • ∫ (x : Ω), (u + v) x ∂μ = ∫ (x : Ω) in s, (u + v) x ∂μ

Proof state:
case pos
Ω : 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 : Integrable f μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ⊤
⊢ (μ s).toReal • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ

Tactic:
rw [← memLp_one_iff_integrable] at hfint

Result:
case pos
Ω : 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 < ⊤
⊢ (μ s).toReal • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ

Proof state:
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 < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ⇑(lpMeas E ℝ m₁ 1 μ).subtypeL
heq₂ : (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ⇑(lpMeas E ℝ m₁ 1 μ).subtypeL
⊢ IsClosed {f | (μ s).toReal • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}

Tactic:
refine isClosed_eq (Continuous.const_smul ?_ _) ?_

Result:
case pos.refine_4.refine_1
Ω : 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 < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ⇑(lpMeas E ℝ m₁ 1 μ).subtypeL
heq₂ : (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ⇑(lpMeas E ℝ m₁ 1 μ).subtypeL
⊢ Continuous fun f => ∫ (x : Ω), ↑↑↑f x ∂μ

case pos.refine_4.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 < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ⇑(lpMeas E ℝ m₁ 1 μ).subtypeL
heq₂ : (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ⇑(lpMeas E ℝ m₁ 1 μ).subtypeL
⊢ Continuous fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ

Proof state:
case pos.refine_4.refine_1
Ω : 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 < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ⇑(lpMeas E ℝ m₁ 1 μ).subtypeL
heq₂ : (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ⇑(lpMeas E ℝ m₁ 1 μ).subtypeL
⊢ Continuous ((fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ⇑(lpMeas E ℝ m₁ 1 μ).subtypeL)

Tactic:
exact continuous_integral.comp (ContinuousLinearMap.continuous _)

Result:
no goals

Proof state:
Ω : 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₂ μ
⊢ μ[f|m₂] =ᶠ[ae μ] fun x => ∫ (x : Ω), f x ∂μ

Tactic:
by_cases hfint : Integrable f μ

Result:
case pos
Ω : 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 : Integrable f μ
⊢ μ[f|m₂] =ᶠ[ae μ] fun x => ∫ (x : Ω), f x ∂μ

case neg
Ω : 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 : ¬Integrable f μ
⊢ μ[f|m₂] =ᶠ[ae μ] fun x => ∫ (x : Ω), f x ∂μ