-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma tendsto_setIntegral_densityProcess (hκν : fst κ ≤ ν)
    [IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) (A : Set γ) :
    Tendsto (fun i ↦ ∫ x in A, densityProcess κ ν i a x s ∂(ν a)) atTop
      (𝓝 (∫ x in A, density κ ν a x s ∂(ν a)))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
n : ℕ
⊢ (fun x => κ.densityProcess ν n a x s) -
      Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) =ᶠ[ae (ν a)]
    (fun i x => κ.densityProcess ν i a x s) n - fun x => κ.density ν a x s

Tactic:
exact EventuallyEq.rfl.sub (density_ae_eq_limitProcess hκν a hs).symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
⊢ Tendsto (fun i => eLpNorm ((fun i x => κ.densityProcess ν i a x s) i - fun x => κ.density ν a x s) 1 (ν a)) atTop
    (𝓝 0)

Tactic:
refine (tendsto_congr fun n ↦ ?_).mp (tendsto_eLpNorm_one_densityProcess_limitProcess hκν a hs)

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
n : ℕ
⊢ eLpNorm
      ((fun x => κ.densityProcess ν n a x s) -
        Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a))
      1 (ν a) =
    eLpNorm ((fun i x => κ.densityProcess ν i a x s) n - fun x => κ.density ν a x s) 1 (ν a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
n : ℕ
⊢ eLpNorm
      ((fun x => κ.densityProcess ν n a x s) -
        Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a))
      1 (ν a) =
    eLpNorm ((fun i x => κ.densityProcess ν i a x s) n - fun x => κ.density ν a x s) 1 (ν a)

Tactic:
refine eLpNorm_congr_ae ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
n : ℕ
⊢ (fun x => κ.densityProcess ν n a x s) -
      Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) =ᶠ[ae (ν a)]
    (fun i x => κ.densityProcess ν i a x s) n - fun x => κ.density ν a x s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
⊢ Tendsto (fun i => ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop (𝓝 (∫ (x : γ) in A, κ.density ν a x s ∂ν a))

Tactic:
refine tendsto_setIntegral_of_L1' (μ := ν a) (fun x ↦ density κ ν a x s)
  (integrable_density hκν a hs) (F := fun i x ↦ densityProcess κ ν i a x s) (l := atTop)
  (Eventually.of_forall (fun n ↦ integrable_densityProcess hκν _ _ hs)) ?_ A

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
⊢ Tendsto (fun i => eLpNorm ((fun i x => κ.densityProcess ν i a x s) i - fun x => κ.density ν a x s) 1 (ν a)) atTop
    (𝓝 0)