-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_bot' [hμ : NeZero μ] (f : α → E) :
    μ[f|⊥] = fun _ => (μ Set.univ).toReal⁻¹ • ∫ x, f x ∂μ

Proof state:
case pos.intro
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
c : E
h_eq : μ[f|⊥] = fun x => c
h_integral : (μ Set.univ).toReal • c = ∫ (x : α), f x ∂μ
⊢ (fun x => c) = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
rw [← h_integral, ← smul_assoc, smul_eq_mul, inv_mul_cancel₀, one_smul]

Result:
case pos.intro
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
c : E
h_eq : μ[f|⊥] = fun x => c
h_integral : (μ Set.univ).toReal • c = ∫ (x : α), f x ∂μ
⊢ (μ Set.univ).toReal ≠ 0

Proof state:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : μ Set.univ = ⊤
h : ¬SigmaFinite (μ.trim ⋯)
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
rw [condExp_of_not_sigmaFinite bot_le h]

Result:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : μ Set.univ = ⊤
h : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Proof state:
case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
swap

Result:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Proof state:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
⊢ ¬SigmaFinite (μ.trim ⋯)

Tactic:
rwa [sigmaFinite_trim_bot_iff]

Result:
no goals

Proof state:
case pos.intro
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
c : E
h_eq : μ[f|⊥] = fun x => c
h_integral : (μ Set.univ).toReal • c = ∫ (x : α), f x ∂μ
⊢ ¬μ Set.univ = 0 ∧ ¬μ Set.univ = ⊤

Tactic:
exact ⟨NeZero.ne _, measure_ne_top μ Set.univ⟩

Result:
no goals