-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_congr_ae (h : f =ᵐ[μ] g) : μ[f|m] =ᵐ[μ] μ[g|m]

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

Tactic:
by_cases hμm : SigmaFinite (μ.trim hm)

Result:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]

Result:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᶠ[ae μ] 0

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ 0 =ᶠ[ae μ] 0

Tactic:
rfl

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᶠ[ae μ] 0

Tactic:
rfl

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

Tactic:
simp_rw [condExp_of_not_le hm]

Result:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ 0 =ᶠ[ae μ] 0

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

Tactic:
swap

Result:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

Tactic:
exact (condExp_ae_eq_condExpL1 hm f).trans
  (Filter.EventuallyEq.trans (by rw [condExpL1_congr_ae hm h])
    (condExp_ae_eq_condExpL1 hm g).symm)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ ↑↑(condExpL1 hm μ f) =ᶠ[ae μ] ↑↑(condExpL1 hm μ g)

Tactic:
rw [condExpL1_congr_ae hm h]

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

Tactic:
swap

Result:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

Tactic:
by_cases hm : m ≤ m₀

Result:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]