-- 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 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)
⊢ condExpL1 hm μ g = condExpL1 hm μ f

Tactic:
have hn_eq : ∀ n, condExpL1 hm μ (gs n) = condExpL1 hm μ (fs n) := by
  intro n
  ext1
  refine (condExp_ae_eq_condExpL1 hm (gs n)).symm.trans ((hfg n).symm.trans ?_)
  exact condExp_ae_eq_condExpL1 hm (fs n)

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)
hn_eq : ∀ (n : ℕ), condExpL1 hm μ (gs n) = condExpL1 hm μ (fs n)
⊢ condExpL1 hm μ g = condExpL1 hm μ f

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₀
hμm : SigmaFinite (μ.trim hm)
hn_eq : ∀ (n : ℕ), condExpL1 hm μ (gs n) = condExpL1 hm μ (fs n)
⊢ condExpL1 hm μ g = condExpL1 hm μ f

Tactic:
have hcond_fs : Tendsto (fun n => condExpL1 hm μ (fs n)) atTop (𝓝 (condExpL1 hm μ f)) :=
  tendsto_condExpL1_of_dominated_convergence hm _ (fun n => (hfs_int n).1) h_int_bound_fs
    hfs_bound hfs

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)
hn_eq : ∀ (n : ℕ), condExpL1 hm μ (gs n) = condExpL1 hm μ (fs n)
hcond_fs : Tendsto (fun n => condExpL1 hm μ (fs n)) atTop (𝓝 (condExpL1 hm μ f))
⊢ condExpL1 hm μ g = condExpL1 hm μ f

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₀
hμm : SigmaFinite (μ.trim hm)
hn_eq : ∀ (n : ℕ), condExpL1 hm μ (gs n) = condExpL1 hm μ (fs n)
hcond_fs : Tendsto (fun n => condExpL1 hm μ (fs n)) atTop (𝓝 (condExpL1 hm μ f))
⊢ condExpL1 hm μ g = condExpL1 hm μ f

Tactic:
have hcond_gs : Tendsto (fun n => condExpL1 hm μ (gs n)) atTop (𝓝 (condExpL1 hm μ g)) :=
  tendsto_condExpL1_of_dominated_convergence hm _ (fun n => (hgs_int n).1) h_int_bound_gs
    hgs_bound hgs

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)
hn_eq : ∀ (n : ℕ), condExpL1 hm μ (gs n) = condExpL1 hm μ (fs n)
hcond_fs : Tendsto (fun n => condExpL1 hm μ (fs n)) atTop (𝓝 (condExpL1 hm μ f))
hcond_gs : Tendsto (fun n => condExpL1 hm μ (gs n)) atTop (𝓝 (condExpL1 hm μ g))
⊢ condExpL1 hm μ g = condExpL1 hm μ f