awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
h : SProd.sprod (β := Set β) (countablePartitionSet n x) univ = ⋃ (n_1 : ℕ), countablePartitionSet n x ×ˢ seq n_1
⊢ Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) univ)) :
      Filter ℝ≥0∞)

Tactic:
convert! tendsto_measure_iUnion_atTop (monotone_const.set_prod hseq)

Premises used: monotone_const, MeasureTheory.tendsto_measure_iUnion_atTop, Monotone.set_prod
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
h :
  SProd.sprod (β := Set β) (countablePartitionSet n x) univ =
    SProd.sprod (β := Set β) (countablePartitionSet n x) (⋃ (i : ℕ), seq i)
h₁ h₂ :
  SProd.sprod (β := Set β) (countablePartitionSet n x) univ = SProd.sprod (β := Set β) (countablePartitionSet n x) univ
⊢ SProd.sprod (β := Set β) (countablePartitionSet n x) univ = ⋃ (n_1 : ℕ), countablePartitionSet n x ×ˢ seq n_1

Tactic:
rw [← prod_iUnion, hseq_iUnion]

Premises used: Set.prod_iUnion
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞) ∨
    Ne (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
Or.inr h0

Premises used: Or.inr
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞) ∨
    Ne (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
exact Or.inr h0

Premises used: Or.inr
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h :
  ∀ (x : γ) (hx : κ.densityProcess κ.fst n a x univ = 1),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 1)
⊢ ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 1)

Tactic:
filter_upwards [densityProcess_fst_univ_ae κ n a] with x hx

Premises used: ProbabilityTheory.Kernel.densityProcess_fst_univ_ae
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
x : γ
hx : κ.densityProcess κ.fst n a x univ = 1
h : Tendsto (fun (m : ℕ) ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 (κ.densityProcess κ.fst n a x univ))
⊢ Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 1)

Tactic:
rw [← hx]
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
x : γ
hx : κ.densityProcess κ.fst n a x univ = 1
⊢ Tendsto (fun (m : ℕ) ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 (κ.densityProcess κ.fst n a x univ))

Tactic:
tendsto_densityProcess_fst_atTop_univ_of_monotone κ n a x seq hseq hseq_iUnion

Premises used: ProbabilityTheory.Kernel.tendsto_densityProcess_fst_atTop_univ_of_monotone
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
x : γ
hx : κ.densityProcess κ.fst n a x univ = 1
⊢ Tendsto (fun (m : ℕ) ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 (κ.densityProcess κ.fst n a x univ))

Tactic:
exact tendsto_densityProcess_fst_atTop_univ_of_monotone κ n a x seq hseq hseq_iUnion

Premises used: ProbabilityTheory.Kernel.tendsto_densityProcess_fst_atTop_univ_of_monotone
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
⊢ ∀ (n : ℕ), ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), κ.densityProcess κ.fst n a x univ = 1

Tactic:
have h := fun n ↦ densityProcess_fst_univ_ae κ n a
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
h : ∀ (n : ℕ), ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), κ.densityProcess κ.fst n a x univ = 1
⊢ ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1

Tactic:
rw [← ae_all_iff] at h

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
h : ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1
h₁ : ∀ (x : γ) (hx : ∀ (i : ℕ), κ.densityProcess κ.fst i a x univ = 1), κ.density κ.fst a x univ = 1
⊢ ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), κ.density κ.fst a x univ = 1

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
h : ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1
x : γ
hx : ∀ (i : ℕ), κ.densityProcess κ.fst i a x univ = 1
⊢ κ.density κ.fst a x univ = 1

Tactic:
simp [density, hx]

Premises used: ProbabilityTheory.Kernel.density
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.density κ.fst a x (seq m)) atTop (𝓝 1)

Tactic:
tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_

Premises used: MeasureTheory.tendsto_of_integral_tendsto_of_monotone, MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
refine_1 :
  ∀ (n : ℕ), @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density κ.fst a x (seq n)) ((κ.fst : (a : α) → Measure γ) a)
refine_2 :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density κ.fst a a_1 (seq i))
    atTop (𝓝 (@integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a : γ) ↦ 1))
refine_3 :
  ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
    Monotone (β := ℝ) fun (i : ℕ) ↦ κ.density κ.fst a a_1 (seq i)
refine_4 : ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), ∀ (i : ℕ), κ.density κ.fst a a_1 (seq i) ≤ 1
⊢ ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.density κ.fst a x (seq m)) atTop (𝓝 1)

Tactic:
refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_

Premises used: MeasureTheory.tendsto_of_integral_tendsto_of_monotone, MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ (n : ℕ), @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density κ.fst a x (seq n)) ((κ.fst : (a : α) → Measure γ) a)

Tactic:
fun m ↦ integrable_density le_rfl _ (hseq_meas m)

Premises used: le_rfl, ProbabilityTheory.Kernel.integrable_density
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ (n : ℕ), @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density κ.fst a x (seq n)) ((κ.fst : (a : α) → Measure γ) a)

Tactic:
exact fun m ↦ integrable_density le_rfl _ (hseq_meas m)

Premises used: le_rfl, ProbabilityTheory.Kernel.integrable_density
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
refine_2 :
  Tendsto
    (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density κ.fst a a_1 (seq i))
    atTop (𝓝 (Measure.real.{u_3} (α := γ) (m := mγ) ((κ.fst : (a : α) → Measure γ) a) univ))
⊢ Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density κ.fst a a_1 (seq i))
    atTop (𝓝 (@integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a : γ) ↦ 1))

Tactic:
rw [MeasureTheory.integral_const, smul_eq_mul, mul_one]

Premises used: MeasureTheory.integral_const, smul_eq_mul, mul_one
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto
    (fun (m : ℕ) ↦ @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (x : γ) ↦ κ.density κ.fst a x (seq m))
    atTop (𝓝 (Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ))

Tactic:
tendsto_integral_density_of_monotone (κ := κ) le_rfl a seq hseq hseq_iUnion hseq_meas

Premises used: le_rfl, ProbabilityTheory.Kernel.tendsto_integral_density_of_monotone
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h :
  Measure.real.{u_3} (α := γ) (m := mγ) ((κ.fst : (a : α) → Measure γ) a) univ =
    Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ
⊢ Tendsto
    (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density κ.fst a a_1 (seq i))
    atTop (𝓝 (Measure.real.{u_3} (α := γ) (m := mγ) ((κ.fst : (a : α) → Measure γ) a) univ))

Tactic:
convert! tendsto_integral_density_of_monotone (κ := κ) le_rfl a seq hseq hseq_iUnion hseq_meas

Premises used: le_rfl, ProbabilityTheory.Kernel.tendsto_integral_density_of_monotone
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h :
  ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | Membership.mem (γ := Set γ) univ p.1}) =
    ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
⊢ ENNReal.toReal ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ) =
    ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)

Tactic:
rw [fst_apply' _ _ MeasurableSet.univ]

Premises used: ProbabilityTheory.Kernel.fst_apply', MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | Membership.mem (γ := Set γ) univ p.1}) =
    ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)

Tactic:
simp only [mem_univ, setOf_true]

Premises used: Set.mem_univ, Set.setOf_true
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
    Monotone (β := ℝ) fun (i : ℕ) ↦ κ.density κ.fst a a_1 (seq i)

Tactic:
ae_of_all _ (fun c n m hnm ↦ density_mono_set le_rfl a c (hseq hnm))

Premises used: le_rfl, MeasureTheory.ae_of_all, ProbabilityTheory.Kernel.density_mono_set
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
    Monotone (β := ℝ) fun (i : ℕ) ↦ κ.density κ.fst a a_1 (seq i)

Tactic:
exact ae_of_all _ (fun c n m hnm ↦ density_mono_set le_rfl a c (hseq hnm))

Premises used: le_rfl, MeasureTheory.ae_of_all, ProbabilityTheory.Kernel.density_mono_set
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), ∀ (i : ℕ), κ.density κ.fst a a_1 (seq i) ≤ 1

Tactic:
ae_of_all _ (fun x m ↦ density_le_one le_rfl a x (seq m))

Premises used: le_rfl, ProbabilityTheory.Kernel.density_le_one, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), ∀ (i : ℕ), κ.density κ.fst a a_1 (seq i) ≤ 1

Tactic:
exact ae_of_all _ (fun x m ↦ density_le_one le_rfl a x (seq m))

Premises used: le_rfl, ProbabilityTheory.Kernel.density_le_one, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
rw : ((((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
| ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← κ.disintegrate κ.condKernel]

Premises used: ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
conv_rhs :
  ∫⁻ (x : β),
      (((κ.condKernel : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ.fst : (a : α) → Measure β) a =
    (((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s
⊢ ∫⁻ (x : β),
      (((κ.condKernel : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ.fst : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s

Tactic:
conv_rhs => rw [← κ.disintegrate κ.condKernel]

Premises used: ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β),
      (((κ.condKernel : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ.fst : (a : α) → Measure β) a =
    (((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s

Tactic:
simp_rw [Kernel.compProd_apply hs]

Premises used: ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
e_a : κ = κ.fst ⊗ₖ κ.condKernel
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) :
      ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ κ = κ.fst ⊗ₖ κ.condKernel

Tactic:
(κ.disintegrate _).symm

Premises used: ProbabilityTheory.Kernel.disintegrate, Eq.symm
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ κ = κ.fst ⊗ₖ κ.condKernel

Tactic:
exact (κ.disintegrate _).symm

Premises used: ProbabilityTheory.Kernel.disintegrate, Eq.symm