-- 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.ha
Ω : 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 ≠ 0

Tactic:
exact 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 0] fun x => ∫ (x : Ω), f x ∂μ[|s]

Tactic:
rfl

Result:
no goals

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

Tactic:
simp only [h, integral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
  ((Measure.restrict_apply_eq_zero hs.compl).2 <| compl_inter_self s ▸ measure_empty),
  ENNReal.zero_toReal, zero_smul, setIntegral_zero_measure]

Result:
no goals

Proof state:
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]

Tactic:
refine ae_eq_trans (condExp_restrict_ae_eq_restrict
  (generateFrom_singleton_le hs)
  (measurableSet_generateFrom rfl) hf).symm ?_

Result:
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
⊢ μ.restrict s[f|MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun x => ∫ (x : Ω), f x ∂μ[|s]

Proof state:
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
⊢ μ.restrict s[f|MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun x => ∫ (x : Ω), f x ∂μ[|s]

Tactic:
refine (ae_eq_condExp_of_forall_setIntegral_eq (generateFrom_singleton_le hs) hf.restrict ?_ ?_
  stronglyMeasurable_const.aestronglyMeasurable).symm

Result:
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
⊢ ∀ (s_1 : Set Ω),
    MeasurableSet s_1 → (μ.restrict s) s_1 < ⊤ → IntegrableOn (fun x => ∫ (x : Ω), f x ∂μ[|s]) s_1 (μ.restrict s)

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
⊢ ∀ (s_1 : Set Ω),
    MeasurableSet s_1 →
      (μ.restrict s) s_1 < ⊤ →
        ∫ (x : Ω) in s_1, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in s_1, 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 Ω
⊢ IntegrableOn (fun x => ∫ (x : Ω), f x ∂μ[|s]) t (μ.restrict s)

Tactic:
rw [integrableOn_const]

Result:
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 < ⊤

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
⊢ ∀ (s_1 : Set Ω),
    MeasurableSet s_1 → (μ.restrict s) s_1 < ⊤ → IntegrableOn (fun x => ∫ (x : Ω), f x ∂μ[|s]) s_1 (μ.restrict s)

Tactic:
rintro t - -

Result:
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 Ω
⊢ IntegrableOn (fun x => ∫ (x : Ω), f x ∂μ[|s]) t (μ.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
⊢ ∀ (s_1 : Set Ω),
    MeasurableSet s_1 →
      (μ.restrict s) s_1 < ⊤ →
        ∫ (x : Ω) in s_1, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in s_1, f x ∂μ.restrict s

Tactic:
rintro t ht -

Result:
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

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
⊢ (μ s).toReal • (μ s).toReal⁻¹ • ∫ (x : Ω) in s, f x ∂μ = ∫ (x : Ω) in s, f x ∂μ.restrict s

Tactic:
rw [smul_inv_smul₀, Measure.restrict_restrict hs, inter_self]

Result:
case neg.refine_2.inr.inl.ha
Ω : 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 ≠ 0

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

Tactic:
simp [h]

Result:
no goals