awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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:
have : κ a (s ×ˢ t) = (Kernel.fst κ ⊗ₖ Kernel.condKernel κ) a (s ×ˢ t) := by
    congr; exact (κ.disintegrate _).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
this :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) :
      ℝ≥0∞)
⊢ ∫⁻ (b : β) in s,
      (((κ.condKernel : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        t ∂(κ.fst : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t)

Tactic:
simpa [this] using (Kernel.compProd_apply_prod hs ht).symm

Premises used: Eq.symm, ProbabilityTheory.Kernel.compProd_apply_prod
-- 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 κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
rw : ∫⁻ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a
| ∫⁻ (x : β × Ω), f x ∂(κ : (a : α) → Measure (β × Ω)) a

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 κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
conv_rhs :
  ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (x : β × Ω), f x ∂(κ : (a : α) → Measure (β × Ω)) a

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 κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
rw rw₁ :
  ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (b : β), ∫⁻ (c : Ω), f (b, c) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a

Tactic:
rw [Kernel.lintegral_compProd _ _ _ hf]

Premises used: ProbabilityTheory.Kernel.lintegral_compProd
-- 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 κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
rw : ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a
| ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂(κ : (a : α) → Measure (β × Ω)) a

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 κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
conv_rhs :
  ∫⁻ (b : β) in s,
      ∫⁻ (ω : Ω) in t, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a
⊢ ∫⁻ (b : β) in s,
      ∫⁻ (ω : Ω) in t, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂(κ : (a : α) → Measure (β × Ω)) a

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 κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
rw rw₁ :
  ∫⁻ (b : β) in s,
      ∫⁻ (ω : Ω) in t, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (x : β) in s,
      ∫⁻ (y : Ω) in t, f (x, y) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, x) ∂(κ.fst : (a : α) → Measure β) a
⊢ ∫⁻ (b : β) in s,
      ∫⁻ (ω : Ω) in t, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a

Tactic:
rw [Kernel.setLIntegral_compProd _ _ _ hf hs ht]

Premises used: ProbabilityTheory.Kernel.setLIntegral_compProd
-- 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 κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
rw :
  ∫⁻ (b : β) in s,
      ∫⁻ (ω : Ω), f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a
⊢ ∫⁻ (b : β) in s,
      ∫⁻ (ω : Ω), f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (x : β × Ω) in SProd.sprod (β := Set Ω) s Set.univ, f x ∂(κ : (a : α) → Measure (β × Ω)) a

Tactic:
rw [← setLIntegral_condKernel hf a hs MeasurableSet.univ]

Premises used: ProbabilityTheory.setLIntegral_condKernel, MeasurableSet.univ
-- 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 κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s,
      ∫⁻ (ω : Ω), f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a

Tactic:
simp_rw [Measure.restrict_univ]

Premises used: MeasureTheory.Measure.restrict_univ
-- 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 κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
t : Set Ω
ht : MeasurableSet t
rw :
  ∫⁻ (b : β),
      ∫⁻ (ω : Ω) in t, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (b : β) in Set.univ,
      ∫⁻ (ω : Ω) in t, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a
⊢ ∫⁻ (b : β),
      ∫⁻ (ω : Ω) in t, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (x : β × Ω) in SProd.sprod (α := Set β) Set.univ t, f x ∂(κ : (a : α) → Measure (β × Ω)) a

Tactic:
rw [← setLIntegral_condKernel hf a MeasurableSet.univ ht]

Premises used: ProbabilityTheory.setLIntegral_condKernel, MeasurableSet.univ
-- 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 κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β),
      ∫⁻ (ω : Ω) in t, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (b : β) in Set.univ,
      ∫⁻ (ω : Ω) in t, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a

Tactic:
simp_rw [Measure.restrict_univ]

Premises used: MeasureTheory.Measure.restrict_univ
-- 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 κ
E : Type u_4
f : β × Ω → E
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
a : α
hf : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ : (a : α) → Measure (β × Ω)) a)
⊢ AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a)

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

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 κ
E : Type u_4
f : β × Ω → E
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
a : α
hf : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a)
⊢ AEStronglyMeasurable.{u_2, u_4} (β := E) (m₀ := mβ)
    (fun (x : β) ↦ @integral _ _ _ _ inst ((κ.condKernel : (a : α × β) → Measure Ω) (a, x)) fun (y : Ω) ↦ f (x, y))
    ((κ.fst : (a : α) → Measure β) a)

Tactic:
AEStronglyMeasurable.integral_kernel_compProd hf

Premises used: MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd
-- 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 κ
E : Type u_4
f : β × Ω → E
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
a : α
hf : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a)
⊢ AEStronglyMeasurable.{u_2, u_4} (β := E) (m₀ := mβ)
    (fun (x : β) ↦ @integral _ _ _ _ inst ((κ.condKernel : (a : α × β) → Measure Ω) (a, x)) fun (y : Ω) ↦ f (x, y))
    ((κ.fst : (a : α) → Measure β) a)

Tactic:
exact AEStronglyMeasurable.integral_kernel_compProd hf

Premises used: MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd
-- 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 κ
E : Type u_4
f : β × Ω → E
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
a : α
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ : (a : α) → Measure (β × Ω)) a)
rw :
  @integral _ _ _ _ Prod.instMeasurableSpace ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a) fun (x : β × Ω) ↦
    f x
| @integral _ _ _ _ Prod.instMeasurableSpace ((κ : (a : α) → Measure (β × Ω)) a) fun (x : β × Ω) ↦ f x

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 κ
E : Type u_4
f : β × Ω → E
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
a : α
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ : (a : α) → Measure (β × Ω)) a)
conv_rhs :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ.fst : (a : α) → Measure β) a) fun (b : β) ↦
      @integral _ _ _ _ inst ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) fun (ω : Ω) ↦ f (b, ω))
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a)
      fun (x : β × Ω) ↦ f x)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ.fst : (a : α) → Measure β) a) fun (b : β) ↦
      @integral _ _ _ _ inst ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) fun (ω : Ω) ↦ f (b, ω))
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ : (a : α) → Measure (β × Ω)) a) fun (x : β × Ω) ↦ f x)

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 κ
E : Type u_4
f : β × Ω → E
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
a : α
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ : (a : α) → Measure (β × Ω)) a)
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a)

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

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 κ
E : Type u_4
f : β × Ω → E
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
a : α
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a)
rw rw₁ :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ.fst : (a : α) → Measure β) a) fun (b : β) ↦
      @integral _ _ _ _ inst ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) fun (ω : Ω) ↦ f (b, ω))
    (@integral _ _ _ _ mβ ((κ.fst : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ inst ((κ.condKernel : (a : α × β) → Measure Ω) (a, x)) fun (y : Ω) ↦ f (x, y))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ.fst : (a : α) → Measure β) a) fun (b : β) ↦
      @integral _ _ _ _ inst ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) fun (ω : Ω) ↦ f (b, ω))
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a)
      fun (x : β × Ω) ↦ f x)

Tactic:
rw [integral_compProd hf]

Premises used: ProbabilityTheory.integral_compProd
-- 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 κ
E : Type u_4
f : β × Ω → E
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ : (a : α) → Measure (β × Ω)) a)
rw :
  @integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.restrict ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a) (s ×ˢ t)) fun (x : β × Ω) ↦ f x
| @integral _ _ _ _ Prod.instMeasurableSpace (Measure.restrict ((κ : (a : α) → Measure (β × Ω)) a) (s ×ˢ t))
    fun (x : β × Ω) ↦ f x

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 κ
E : Type u_4
f : β × Ω → E
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ : (a : α) → Measure (β × Ω)) a)
conv_rhs :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ.fst : (a : α) → Measure β) a) s) fun (b : β) ↦
      @integral _ _ _ _ inst (Measure.restrict ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) t) fun (ω : Ω) ↦
        f (b, ω))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a) (s ×ˢ t)) fun (x : β × Ω) ↦ f x)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ.fst : (a : α) → Measure β) a) s) fun (b : β) ↦
      @integral _ _ _ _ inst (Measure.restrict ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) t) fun (ω : Ω) ↦
        f (b, ω))
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.restrict ((κ : (a : α) → Measure (β × Ω)) a) (s ×ˢ t))
      fun (x : β × Ω) ↦ f x)

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 κ
E : Type u_4
f : β × Ω → E
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ : (a : α) → Measure (β × Ω)) a)
⊢ IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a)

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

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 κ
E : Type u_4
f : β × Ω → E
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a)
rw rw₁ :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ.fst : (a : α) → Measure β) a) s) fun (b : β) ↦
      @integral _ _ _ _ inst (Measure.restrict ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) t) fun (ω : Ω) ↦
        f (b, ω))
    (@integral _ _ _ _ mβ (Measure.restrict ((κ.fst : (a : α) → Measure β) a) s) fun (x : β) ↦
      @integral _ _ _ _ inst (Measure.restrict ((κ.condKernel : (a : α × β) → Measure Ω) (a, x)) t) fun (y : Ω) ↦
        f (x, y))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ.fst : (a : α) → Measure β) a) s) fun (b : β) ↦
      @integral _ _ _ _ inst (Measure.restrict ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) t) fun (ω : Ω) ↦
        f (b, ω))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a) (s ×ˢ t)) fun (x : β × Ω) ↦ f x)

Tactic:
rw [setIntegral_compProd hs ht hf]

Premises used: ProbabilityTheory.setIntegral_compProd
-- 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 κ
E : Type u_4
f : β × Ω → E
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
a : α
s : Set β
hs : MeasurableSet s
hf :
  IntegrableOn (mα := Prod.instMeasurableSpace) f (SProd.sprod (β := Set Ω) s Set.univ)
    ((κ : (a : α) → Measure (β × Ω)) a)
rw :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ.fst : (a : α) → Measure β) a) s) fun (b : β) ↦
      @integral _ _ _ _ inst ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) fun (ω : Ω) ↦ f (b, ω))
    (@integral _ _ _ _ mβ (Measure.restrict ((κ.fst : (a : α) → Measure β) a) s) fun (b : β) ↦
      @integral _ _ _ _ inst (Measure.restrict ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) Set.univ) fun (ω : Ω) ↦
        f (b, ω))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ.fst : (a : α) → Measure β) a) s) fun (b : β) ↦
      @integral _ _ _ _ inst ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) fun (ω : Ω) ↦ f (b, ω))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict ((κ : (a : α) → Measure (β × Ω)) a) (SProd.sprod (β := Set Ω) s Set.univ)) fun (x : β × Ω) ↦
      f x)

Tactic:
rw [← setIntegral_condKernel a hs MeasurableSet.univ hf]

Premises used: ProbabilityTheory.setIntegral_condKernel, MeasurableSet.univ