-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem tendsto_condExp_unique (fs gs : ℕ → α → E) (f g : α → E)
    (hfs_int : ∀ n, Integrable (fs n) μ) (hgs_int : ∀ n, Integrable (gs n) μ)
    (hfs : ∀ᵐ x ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x)))
    (hgs : ∀ᵐ x ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))) (bound_fs : α → ℝ)
    (h_int_bound_fs : Integrable bound_fs μ) (bound_gs : α → ℝ)
    (h_int_bound_gs : Integrable bound_gs μ) (hfs_bound : ∀ n, ∀ᵐ x ∂μ, ‖fs n x‖ ≤ bound_fs x)
    (hgs_bound : ∀ n, ∀ᵐ x ∂μ, ‖gs n x‖ ≤ bound_gs x) (hfg : ∀ n, μ[fs n|m] =ᵐ[μ] μ[gs n|m]) :
    μ[f|m] =ᵐ[μ] μ[g|m]

Proof state:
case h
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
n : ℕ
⊢ ↑↑(condExpL1 hm μ (gs n)) =ᶠ[ae μ] ↑↑(condExpL1 hm μ (fs n))

Tactic:
refine (condExp_ae_eq_condExpL1 hm (gs n)).symm.trans ((hfg n).symm.trans ?_)

Result:
case h
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
n : ℕ
⊢ μ[fs n|m] =ᶠ[ae μ] ↑↑(condExpL1 hm μ (fs n))

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]
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 α
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]
hm : ¬m ≤ m₀
⊢ 0 =ᶠ[ae μ] 0

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]
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 α
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]
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 α
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f|m] =ᶠ[ae μ] μ[g|m]

Proof state:
case h
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
n : ℕ
⊢ μ[fs n|m] =ᶠ[ae μ] ↑↑(condExpL1 hm μ (fs n))

Tactic:
exact condExp_ae_eq_condExpL1 hm (fs n)

Result:
no goals