-- Mathlib/Probability/Kernel/Condexp.lean
lemma condExp_generateFrom_singleton (hs : MeasurableSet s) {f : Ω → F} (hf : Integrable f μ) :
    μ[f | generateFrom {s}] =ᵐ[μ.restrict s] fun _ ↦ ∫ x, f x ∂μ[|s]

Proof state:
case neg.refine_2.inr.inl
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = s
⊢ ∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in t, f x ∂μ.restrict s

Tactic:
simp only [h, cond, integral_smul_measure, ENNReal.toReal_inv, integral_const,
  MeasurableSet.univ, Measure.restrict_apply, univ_inter, Measure.restrict_apply_self]

Result:
case neg.refine_2.inr.inl
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = s
⊢ (μ s).toReal • (μ s).toReal⁻¹ • ∫ (x : Ω) in s, f x ∂μ = ∫ (x : Ω) in s, f x ∂μ.restrict s

Proof state:
case neg.refine_2
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
⊢ ∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in t, f x ∂μ.restrict s

Tactic:
obtain (h | h | h | h) := measurableSet_generateFrom_singleton_iff.1 ht

Result:
case neg.refine_2.inl
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = ∅
⊢ ∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in t, f x ∂μ.restrict s

case neg.refine_2.inr.inl
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = s
⊢ ∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in t, f x ∂μ.restrict s

case neg.refine_2.inr.inr.inl
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = sᶜ
⊢ ∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in t, f x ∂μ.restrict s

case neg.refine_2.inr.inr.inr
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = univ
⊢ ∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in t, f x ∂μ.restrict s

Proof state:
case neg.refine_1
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
⊢ ∫ (x : Ω), f x ∂μ[|s] = 0 ∨ (μ.restrict s) t < ⊤

Tactic:
exact Or.inr <| measure_lt_top (μ.restrict s) t

Result:
no goals

Proof state:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
⊢ μ[f|MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun x => ∫ (x : Ω), f x ∂μ[|s]

Tactic:
by_cases hμs : μ s = 0

Result:
case pos
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : μ s = 0
⊢ μ[f|MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun x => ∫ (x : Ω), f x ∂μ[|s]

case neg
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
⊢ μ[f|MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun x => ∫ (x : Ω), f x ∂μ[|s]

Proof state:
case neg.refine_2.inr.inr.inr
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = univ
⊢ ∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in t, f x ∂μ.restrict s

Tactic:
simp only [h, Measure.restrict_univ, cond, integral_smul_measure, ENNReal.toReal_inv,
  integral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
  smul_inv_smul₀ <| ENNReal.toReal_ne_zero.2 ⟨hμs, measure_ne_top _ _⟩]

Result:
no goals

Proof state:
case pos
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : μ s = 0
⊢ μ[f|MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun x => ∫ (x : Ω), f x ∂μ[|s]

Tactic:
rw [Measure.restrict_eq_zero.2 hμs]

Result:
case pos
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : μ s = 0
⊢ μ[f|MeasurableSpace.generateFrom {s}] =ᶠ[ae 0] fun x => ∫ (x : Ω), f x ∂μ[|s]