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 κ
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)
⊢ 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, ω))

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 : α
t : Set Ω
ht : MeasurableSet t
hf :
  IntegrableOn (mα := Prod.instMeasurableSpace) f (SProd.sprod (α := Set β) Set.univ t)
    ((κ : (a : α) → Measure (β × Ω)) a)
rw :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ.fst : (a : α) → Measure β) a) fun (b : β) ↦
      @integral _ _ _ _ inst (Measure.restrict ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) t) fun (ω : Ω) ↦
        f (b, ω))
    (@integral _ _ _ _ mβ (Measure.restrict ((κ.fst : (a : α) → Measure β) a) Set.univ) fun (b : β) ↦
      @integral _ _ _ _ inst (Measure.restrict ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) t) fun (ω : Ω) ↦
        f (b, ω))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ.fst : (a : α) → Measure β) a) fun (b : β) ↦
      @integral _ _ _ _ inst (Measure.restrict ((κ.condKernel : (a : α × β) → Measure Ω) (a, b)) t) fun (ω : Ω) ↦
        f (b, ω))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict ((κ : (a : α) → Measure (β × Ω)) a) (SProd.sprod (α := Set β) Set.univ t)) fun (x : β × Ω) ↦
      f x)

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

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

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
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
s : Set (β × Ω)
hs : MeasurableSet s
rw : ((ρ.fst ⊗ₘ ρ.condKernel : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
| ((ρ : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
s : Set (β × Ω)
hs : MeasurableSet s
conv_rhs :
  ∫⁻ (x : β), (((ρ.condKernel : (a : β) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {y : Ω | (x, y) ∈ s} ∂ρ.fst =
    (ρ.fst ⊗ₘ ρ.condKernel : (a : Set (β × Ω)) → ℝ≥0∞) s
⊢ ∫⁻ (x : β), (((ρ.condKernel : (a : β) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {y : Ω | (x, y) ∈ s} ∂ρ.fst =
    (ρ : (a : Set (β × Ω)) → ℝ≥0∞) s

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
s : Set (β × Ω)
hs : MeasurableSet s
simp_rw :
  ∫⁻ (x : β), (((ρ.condKernel : (a : β) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {y : Ω | (x, y) ∈ s} ∂ρ.fst =
    ∫⁻ (a : β), (((ρ.condKernel : (a : β) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ρ.fst
⊢ ∫⁻ (x : β), (((ρ.condKernel : (a : β) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {y : Ω | (x, y) ∈ s} ∂ρ.fst =
    (ρ.fst ⊗ₘ ρ.condKernel : (a : Set (β × Ω)) → ℝ≥0∞) s

Tactic:
simp_rw [compProd_apply hs]

Premises used: MeasureTheory.Measure.compProd_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), (((ρ.condKernel : (a : β) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {y : Ω | (x, y) ∈ s} ∂ρ.fst =
    ∫⁻ (a : β), (((ρ.condKernel : (a : β) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ρ.fst

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
e_a : ρ = ρ.fst ⊗ₘ ρ.condKernel
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((ρ.fst ⊗ₘ ρ.condKernel : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ρ = ρ.fst ⊗ₘ ρ.condKernel

Tactic:
(ρ.disintegrate _).symm

Premises used: MeasureTheory.Measure.disintegrate, Eq.symm
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ρ = ρ.fst ⊗ₘ ρ.condKernel

Tactic:
exact (ρ.disintegrate _).symm

Premises used: MeasureTheory.Measure.disintegrate, Eq.symm
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((ρ.fst ⊗ₘ ρ.condKernel : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)

Tactic:
have : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t) := by
    congr; exact (ρ.disintegrate _).symm
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((ρ.fst ⊗ₘ ρ.condKernel : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
⊢ ∫⁻ (b : β) in s, (((ρ.condKernel : (a : β) → Measure Ω) b : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t ∂ρ.fst =
    (ρ : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t)

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

Premises used: MeasureTheory.Measure.compProd_apply_prod, Eq.symm
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
rw : ∫⁻ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel
| ∫⁻ (x : β × Ω), f x ∂ρ

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
conv_rhs :
  ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst = ∫⁻ (x : β × Ω), f x ∂ρ

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
rw rw₁ :
  ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (a : β), ∫⁻ (b : Ω), f (a, b) ∂(ρ.condKernel : (a : β) → Measure Ω) a ∂ρ.fst
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel

Tactic:
rw [lintegral_compProd hf]

Premises used: MeasureTheory.Measure.lintegral_compProd
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
rw : ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
| ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
conv_rhs :
  ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
rw rw₁ :
  ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (a : β) in s, ∫⁻ (b : Ω) in t, f (a, b) ∂(ρ.condKernel : (a : β) → Measure Ω) a ∂ρ.fst
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel

Tactic:
rw [setLIntegral_compProd hf hs ht]

Premises used: MeasureTheory.Measure.setLIntegral_compProd
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
rw :
  ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (x : β × Ω) in SProd.sprod (β := Set Ω) s Set.univ, f x ∂ρ

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

Premises used: MeasureTheory.Measure.setLIntegral_condKernel, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst

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
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
t : Set Ω
ht : MeasurableSet t
rw :
  ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (b : β) in Set.univ, ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (x : β × Ω) in SProd.sprod (α := Set β) Set.univ t, f x ∂ρ

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

Premises used: MeasureTheory.Measure.setLIntegral_condKernel, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (b : β) in Set.univ, ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst

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
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
hf : AEStronglyMeasurable f ρ
⊢ AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ AEStronglyMeasurable.{u_1, u_3} (β := E)
    (fun (x : β) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)) ρ.fst

Tactic:
AEStronglyMeasurable.integral_kernel_compProd hf

Premises used: MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd, MeasureTheory.Measure.fst
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ AEStronglyMeasurable.{u_1, u_3} (β := E)
    (fun (x : β) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)) ρ.fst

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
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
hf : Integrable f ρ
rw : ∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel
| ∫ (x : β × Ω), f x ∂ρ

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
hf : Integrable f ρ
conv_rhs :
  Eq.{u_3 + 1} (α := E)
    (∫ (b : β), @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel)
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β), @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω), f x ∂ρ)

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
hf : Integrable f ρ
⊢ Integrable f (ρ.fst ⊗ₘ ρ.condKernel)

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
hf : Integrable f (ρ.fst ⊗ₘ ρ.condKernel)
rw rw₁ :
  Eq.{u_3 + 1} (α := E)
    (∫ (b : β), @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (a : β), @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) a) fun (b : Ω) ↦ f (a, b) ∂ρ.fst)
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β), @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel)

Tactic:
rw [integral_compProd hf]

Premises used: MeasureTheory.Measure.integral_compProd
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ρ
rw : ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
| ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ρ
conv_rhs :
  Eq.{u_3 + 1} (α := E)
    (∫ (b : β) in s,
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel)
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β) in s,
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ)

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ρ
⊢ IntegrableOn f (s ×ˢ t) (ρ.fst ⊗ₘ ρ.condKernel)

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

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) (ρ.fst ⊗ₘ ρ.condKernel)
rw rw₁ :
  Eq.{u_3 + 1} (α := E)
    (∫ (b : β) in s,
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (a : β) in s,
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) a) t) fun (b : Ω) ↦ f (a, b) ∂ρ.fst)
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β) in s,
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel)

Tactic:
rw [setIntegral_compProd hs ht hf]

Premises used: MeasureTheory.Measure.setIntegral_compProd