mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x ↦ κ.densityProcess ν n a x s

Tactic:
exact measurable_densityProcess_right κ ν n a hs

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
b : β
hbs : b ∉ s
⊢ s.indicator (fun x ↦ r) b ≤ s.indicator (fun b ↦ (κCond (a, b)) univ) b

Tactic:
· simp [hbs]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
h_2_le : (s.indicator fun x ↦ r) ≤ s.indicator fun b ↦ (κCond (a, b)) univ
h_ne_zero : (κ.fst a) {x | r ≤ (κCond (a, x)) univ} ≠ 0
| (κ.fst a) s

Tactic:
← one_mul (κ.fst a s)

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
h_2_le : (s.indicator fun x ↦ r) ≤ s.indicator fun b ↦ (κCond (a, b)) univ
h_ne_zero : (κ.fst a) {x | r ≤ (κCond (a, x)) univ} ≠ 0
| 1 * (κ.fst a) s
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝¹ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
⊢ cov[fun ω ↦
      ⟪∑ x_1, ((EuclideanSpace.basisFun ι ℝ).repr x).ofLp x_1 • (EuclideanSpace.basisFun ι ℝ) x_1,
        (toLp 2 ∘ fun ω i ↦ X i ω) ω⟫,
      fun ω ↦
      ⟪∑ x, ((EuclideanSpace.basisFun κ ℝ).repr y).ofLp x • (EuclideanSpace.basisFun κ ℝ) x,
        (toLp 2 ∘ fun ω j ↦ Y j ω) ω⟫;
      P] =
    0

Tactic:
sum_inner,

Goal state after:
case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝¹ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
⊢ cov[fun ω ↦
      ∑ i,
        ⟪((EuclideanSpace.basisFun ι ℝ).repr x).ofLp i • (EuclideanSpace.basisFun ι ℝ) i, (toLp 2 ∘ fun ω i ↦ X i ω) ω⟫,
      fun ω ↦
      ∑ i,
        ⟪((EuclideanSpace.basisFun κ ℝ).repr y).ofLp i • (EuclideanSpace.basisFun κ ℝ) i, (toLp 2 ∘ fun ω j ↦ Y j ω) ω⟫;
      P] =
    0
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
b : β
hbs : b ∉ s
⊢ s.indicator (fun b ↦ (κCond (a, b)) univ) b ≤ s.indicator (fun x ↦ r) b

Tactic:
· simp [hbs]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
h_2_le : (s.indicator fun b ↦ (κCond (a, b)) univ) ≤ s.indicator fun x ↦ r
h_ne_zero : (κ.fst a) {x | (κCond (a, x)) univ ≤ r} ≠ 0
| (κ.fst a) s

Tactic:
← one_mul (κ.fst a s)

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
h_2_le : (s.indicator fun b ↦ (κCond (a, b)) univ) ≤ s.indicator fun x ↦ r
h_ne_zero : (κ.fst a) {x | (κCond (a, x)) univ ≤ r} ≠ 0
| 1 * (κ.fst a) s
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd : ((κ'.fst ⊗ₖ η) a) (univ ×ˢ range e)ᶜ = 0
⊢ ∀ᵐ (t : β) ∂κ'.fst a, (a, t) ∈ {p | (η p) (range e)ᶜ = 0}

Tactic:
compProd_null

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd : (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' (univ ×ˢ range e)ᶜ)) =ᵐ[κ'.fst a] 0
⊢ ∀ᵐ (t : β) ∂κ'.fst a, (a, t) ∈ {p | (η p) (range e)ᶜ = 0}

case hs
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd : ((κ'.fst ⊗ₖ η) a) (univ ×ˢ range e)ᶜ = 0
⊢ MeasurableSet (univ ×ˢ range e)ᶜ
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: case h_basic
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ t ∈ ⋃ a, {Iic ↑a}, (κ x) t = (ρ.condKernel x) t

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Goal state after:
case h_basic
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ (a : ℚ), (κ x) (Iic ↑a) = (ρ.condKernel x) (Iic ↑a)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ Integrable (fun a ↦ ((condDistrib Y X μ) (X a)).real s) μ

Tactic:
refine integrable_toReal_of_lintegral_ne_top ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ AEMeasurable (fun a ↦ ((condDistrib Y X μ) (X a)) s) μ

case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ((condDistrib Y X μ) (X x)) s ∂μ ≠ ∞
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a : ℕ
⊢ partialTraj κ a (a + 1) = (Kernel.id ×ₖ (κ a).map ⇑(piSingleton a)).map (_root_.IicProdIoc a (a + 1))

Tactic:
partialTraj_succ_of_le le_rfl,

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a : ℕ
⊢ (Kernel.id ×ₖ (κ a).map ⇑(piSingleton a) ∘ₖ partialTraj κ a a).map (_root_.IicProdIoc a (a + 1)) =
    (Kernel.id ×ₖ (κ a).map ⇑(piSingleton a)).map (_root_.IicProdIoc a (a + 1))
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
⊢ setBer(u, p) ({a | i ∈ a} ∩ {a | i ∉ u}) = 0

Tactic:
by_cases hi : i ∈ u

Goal state after:
case pos
ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∈ u
⊢ setBer(u, p) ({a | i ∈ a} ∩ {a | i ∉ u}) = 0

case neg
ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∉ u
⊢ setBer(u, p) ({a | i ∈ a} ∩ {a | i ∉ u}) = 0
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n ↦ f n a
h_sum : Summable fun n ↦ f n
a : α
s : Set β
hs : MeasurableSet s
this : ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b ↦ f n a b) b ∂κ a
⊢ ∫⁻ (b : β) in s, ∑' (n : ι), (fun b ↦ f n a b) b ∂κ a = ∑' (n : ι), ((κ.withDensity (f n)) a) s

Tactic:
lintegral_tsum fun n => by fun_prop

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n ↦ f n a
h_sum : Summable fun n ↦ f n
a : α
s : Set β
hs : MeasurableSet s
this : ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b ↦ f n a b) b ∂κ a
⊢ ∑' (i : ι), ∫⁻ (a_1 : β) in s, f i a a_1 ∂κ a = ∑' (n : ι), ((κ.withDensity (f n)) a) s
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : ¬Measurable (Function.uncurry f)
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
rw [withDensity_of_not_measurable _ hf]; infer_instance

Goal state after:
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
by
  -- We already have that for `f` bounded from above and a `κ` a finite kernel,
  -- `withDensity κ f` is finite. We write any function as a countable sum of bounded
  -- functions, and decompose an s-finite kernel as a sum of finite kernels. We then use that
  -- `withDensity` commutes with sums for both arguments and get a sum of finite kernels.
  by_cases hf : Measurable (Function.uncurry f)
  swap; · rw [withDensity_of_not_measurable _ hf]; infer_instance
  let fs : ℕ → α → β → ℝ≥0∞ := fun n a b => min (f a b) (n + 1) - min (f a b) n
  have h_le : ∀ a b n, ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ n := by
    intro a b n hn
    have : (f a b).toReal ≤ n := Nat.le_of_ceil_le hn
    rw [← ENNReal.le_ofReal_iff_toReal_le (hf_ne_top a b) _] at this
    · simpa
    · exact n.cast_nonneg
  have h_zero : ∀ a b n, ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0 := by
    intro a b n hn
    suffices min (f a b) (n + 1) = f a b ∧ min (f a b) n = f a b by
      simp_rw [fs, this.1, this.2, tsub_self (f a b)]
    exact ⟨min_eq_left ((h_le a b n hn).trans (le_add_of_nonneg_right zero_le_one)),
      min_eq_left (h_le a b n hn)⟩
  have hf_eq_tsum : f = ∑' n, fs n := by
    have h_sum_a : ∀ a, Summable fun n => fs n a :=
      fun _ => Pi.summable.mpr fun _ => ENNReal.summable
    ext a b : 2
    rw [tsum_apply (Pi.summable.mpr h_sum_a), tsum_apply (h_sum_a a),
      ENNReal.tsum_eq_liminf_sum_nat]
    have h_finsetSum : ∀ n, ∑ i ∈ Finset.range n, fs i a b = min (f a b) n := fun n ↦ by
      induction n with
      | zero => simp
      | succ n hn =>
        rw [Finset.sum_range_succ, hn]
        simp [fs]
    simp_rw [h_finsetSum]
    refine (Filter.Tendsto.liminf_eq ?_).symm
    refine Filter.Tendsto.congr' ?_ tendsto_const_nhds
    rw [Filter.EventuallyEq, Filter.eventually_atTop]
    exact ⟨⌈(f a b).toReal⌉₊, fun n hn => (min_eq_left (h_le a b n hn)).symm⟩
  rw [hf_eq_tsum, withDensity_tsum _ fun n : ℕ => _]
  swap; · fun_prop
  refine isSFiniteKernel_sum (hκs := fun n => ?_)
  suffices IsFiniteKernel (withDensity κ (fs n)) by infer_instance
  refine isFiniteKernel_withDensity_of_bounded _ (ENNReal.coe_ne_top : ↑n + 1 ≠ ∞) fun a b => ?_
  -- After https://github.com/leanprover/lean4/pull/2734, we need to do beta reduction before `norm_cast`
  beta_reduce
  norm_cast
  calc
    fs n a b ≤ min (f a b) (n + 1) := tsub_le_self
    _ ≤ n + 1 := min_le_right _ _
    _ = ↑(n + 1) := by norm_cast

Goal state after:
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝ : IsFiniteKernel η
hκη : κ ≤ η
a : α
⊢ κ.rnDerivAux η a ≤ᵐ[η a] 1

Tactic:
filter_upwards [Measure.rnDeriv_le_one_of_le (hκη a)] with x hx_le_one

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝ : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : (∂κ a/∂η a) x ≤ 1 x
⊢ κ.rnDerivAux η a x ≤ 1 x
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : ⋂ n, B n = ∅
n : ℕ
| (piContent μ) (cylinder (s n) (S n))

Tactic:
piContent_cylinder μ (mS n),

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : ⋂ n, B n = ∅
n : ℕ
| (Measure.pi fun i ↦ μ ↑i) (S n)
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ⟂ₘ η a
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
⊢ ∫⁻ (a : α), (η a) (Prod.mk a ⁻¹' s) ∂ν = 0 ∧ ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' sᶜ) ∂μ = 0

Tactic:
have h1 a : η a (Prod.mk a ⁻¹' s) = 0 := by rw [h_eq, Kernel.measure_mutuallySingularSetSlice]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ⟂ₘ η a
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 : ∀ (a : α), (η a) (Prod.mk a ⁻¹' s) = 0
⊢ ∫⁻ (a : α), (η a) (Prod.mk a ⁻¹' s) ∂ν = 0 ∧ ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' sᶜ) ∂μ = 0
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ IsDeterministic (copy α)

Tactic:
unfold copy

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ IsDeterministic (deterministic Function.diag ⋯)
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
inst✝ : IsMarkovKernel κ
⊢ ⇑κ =ᵐ[⇑(κ†μ) ∘ₘ ⇑κ ∘ₘ μ] ⇑((κ†μ)†(⇑κ ∘ₘ μ))

Tactic:
refine ae_eq_posterior_of_compProd_eq_swap_comp κ ?_

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
inst✝ : IsMarkovKernel κ
⊢ (⇑(κ†μ) ∘ₘ ⇑κ ∘ₘ μ) ⊗ₘ κ = ⇑(Kernel.swap 𝓧 Ω) ∘ₘ (⇑κ ∘ₘ μ) ⊗ₘ κ†μ
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
| (Kernel.id ×ₖ (traj κ a).map (Set.Ioi a).domRestrict).map (frestrictLe b ∘ ⇑(IicProdIoi a))

Tactic:
2

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
| frestrictLe b ∘ ⇑(IicProdIoi a)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
| (traj κ a).map ((fun x i ↦ x ⟨↑i, ⋯⟩) ∘ (Set.Ioi a).domRestrict)

Tactic:
2

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
| (fun x i ↦ x ⟨↑i, ⋯⟩) ∘ (Set.Ioi a).domRestrict
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case hfm
X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
mf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ AEStronglyMeasurable f (Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀))

Tactic:
convert! mf
    rw [traj_map_updateFinset]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : PMF α
a : α
h : MeasurableSet {a}
⊢ p.toMeasure {a} = p a

Tactic:
simp [p.toMeasure_apply_eq_toOuterMeasure_apply h, toOuterMeasure_apply_singleton]

Goal state after: