-- 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_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 < ⊤
u v : Ω → E
huv : u =ᶠ[ae μ] v
a✝ : MemLp u 1 μ
hueq : (μ s).toReal • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ (μ s).toReal • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ

Tactic:
rwa [← integral_congr_ae huv, ←
  (setIntegral_congr_ae (hle₂ _ hms) _ : ∫ x in s, u x ∂μ = ∫ x in s, v x ∂μ)]

Result:
Ω : 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
huv : u =ᶠ[ae μ] v
a✝ : MemLp u 1 μ
hueq : (μ s).toReal • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → u x = v x

Proof state:
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 μ
⊢ 0 =ᶠ[ae μ] fun x => 0

Tactic:
rfl

Result:
no goals

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

Tactic:
rw [heq₁]

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 ∂μ) ∘ ⇑(lpMeas E ℝ m₁ 1 μ).subtypeL)

Proof state:
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 =ᶠ[ae μ] g →
      MemLp f 1 μ →
        (μ s).toReal • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
          (μ s).toReal • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ

Tactic:
intro u v huv _ hueq

Result:
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 < ⊤
u v : Ω → E
huv : u =ᶠ[ae μ] v
a✝ : MemLp u 1 μ
hueq : (μ s).toReal • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ (μ s).toReal • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ

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₂ μ
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
f : ↥(lpMeas E ℝ m₁ 1 μ)
x✝ : Ω
⊢ True

Tactic:
trivial

Result:
no goals

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 < ⊤
⊢ IsClosed {f | (μ s).toReal • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}

Tactic:
have heq₁ : (fun f : lpMeas E ℝ m₁ 1 μ => ∫ x, (f : Ω → E) x ∂μ) =
    (fun f : Lp E 1 μ => ∫ x, f x ∂μ) ∘ Submodule.subtypeL _ := by
  refine funext fun f => integral_congr_ae ?_
  simp_rw [Submodule.coe_subtypeL', Submodule.coe_subtype]; norm_cast

Result:
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
⊢ IsClosed {f | (μ s).toReal • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}

Proof state:
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 ∂μ

Tactic:
rw [condExp_of_not_integrable hfint, integral_undef hfint]

Result:
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 μ
⊢ 0 =ᶠ[ae μ] fun x => 0

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 < ⊤
⊢ ∫ (x : Ω) in s, ∫ (x : Ω), f x ∂μ ∂μ = ∫ (x : Ω) in s, f x ∂μ

Tactic:
rw [setIntegral_const]

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