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

Tactic:
refine funext fun f => integral_congr_ae ?_

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 < ⊤
f : ↥(lpMeas E ℝ m₁ 1 μ)
⊢ ↑↑↑f =ᶠ[ae μ] ↑↑((lpMeas E ℝ m₁ 1 μ).subtypeL 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 < ⊤
⊢ ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f 1 μ →
        MemLp g 1 μ →
          StronglyMeasurable f →
            StronglyMeasurable g →
              (μ s).toReal • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
                (μ s).toReal • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ →
                  (μ s).toReal • ∫ (x : Ω), (f + g) x ∂μ = ∫ (x : Ω) in s, (f + g) x ∂μ

Tactic:
intro u v _ huint hvint hu hv hu_eq hv_eq

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

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

Tactic:
refine (ae_eq_condExp_of_forall_setIntegral_eq hle₂ hfint
  (fun s _ hs => integrableOn_const.2 (Or.inr hs)) (fun s hms hs => ?_)
    stronglyMeasurable_const.aestronglyMeasurable).symm

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

Proof state:
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 : ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ⊤
c : E
t : Set Ω
hmt : MeasurableSet t
a✝ : μ t < ⊤
⊢ (μ s).toReal • ∫ (x : Ω), t.indicator (fun x => c) x ∂μ = ∫ (x : Ω) in s, t.indicator (fun x => c) x ∂μ

Tactic:
rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, ← ENNReal.toReal_mul,
  mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
  Set.inter_comm]

Result:
no goals

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

Tactic:
rw [heq₂]

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

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

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

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