awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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
⊢ ∫⁻ (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
have 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
Tactic: rw [Kernel.setLIntegral_compProd _ _ _ hf hs ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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 =
    ∫⁻ (x : β × Ω) in SProd.sprod (β := Set Ω) s Set.univ, f x ∂(κ : (a : α) → Measure (β × Ω)) a
have 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
Tactic: rw [← setLIntegral_condKernel hf a hs MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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 =
    ∫⁻ (x : β × Ω) in SProd.sprod (α := Set β) Set.univ t, f x ∂(κ : (a : α) → Measure (β × Ω)) a
have 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
Tactic: rw [← setLIntegral_condKernel hf a MeasurableSet.univ ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
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.{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)
have hf₁ : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a)
Tactic: rw [← κ.disintegrate κ.condKernel] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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)
| @integral _ _ _ _ Prod.instMeasurableSpace ((κ : (a : α) → Measure (β × Ω)) a) fun (x : β × Ω) ↦ f x
have rw : @integral _ _ _ _ Prod.instMeasurableSpace ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a) fun (x : β × Ω) ↦ f x
Tactic: rw [← κ.disintegrate κ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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)
⊢ 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)
have 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)
Tactic: conv_rhs => rw [← κ.disintegrate κ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
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)
⊢ 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)
have hf₁ : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a)
Tactic: rw [← κ.disintegrate κ.condKernel] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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)
⊢ 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)
have 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))
Tactic: rw [integral_compProd hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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)
| @integral _ _ _ _ Prod.instMeasurableSpace (Measure.restrict ((κ : (a : α) → Measure (β × Ω)) a) (s ×ˢ t))
    fun (x : β × Ω) ↦ f x
have rw : @integral _ _ _ _ Prod.instMeasurableSpace
  (Measure.restrict ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a) (s ×ˢ t)) fun (x : β × Ω) ↦ f x
Tactic: rw [← κ.disintegrate κ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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)
⊢ 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)
have 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)
Tactic: conv_rhs => rw [← κ.disintegrate κ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
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)
⊢ 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)
have hf₁ : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a)
Tactic: rw [← κ.disintegrate κ.condKernel] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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)
⊢ 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)
have 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))
Tactic: rw [setIntegral_compProd hs ht hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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 _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict ((κ : (a : α) → Measure (β × Ω)) a) (SProd.sprod (β := Set Ω) s Set.univ)) fun (x : β × Ω) ↦
      f x)
have 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, ω))
Tactic: rw [← setIntegral_condKernel a hs MeasurableSet.univ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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 _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict ((κ : (a : α) → Measure (β × Ω)) a) (SProd.sprod (α := Set β) Set.univ t)) fun (x : β × Ω) ↦
      f x)
have 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, ω))
Tactic: rw [← setIntegral_condKernel a MeasurableSet.univ ht hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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
| ((ρ : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ((ρ.fst ⊗ₘ ρ.condKernel : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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 : Set (β × Ω)) → ℝ≥0∞) s
have conv_rhs : ∫⁻ (x : β), (((ρ.condKernel : (a : β) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {y : Ω | (x, y) ∈ s} ∂ρ.fst =
  (ρ.fst ⊗ₘ ρ.condKernel : (a : Set (β × Ω)) → ℝ≥0∞) s
Tactic: conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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 =
    (ρ.fst ⊗ₘ ρ.condKernel : (a : Set (β × Ω)) → ℝ≥0∞) s
have 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
Tactic: simp_rw [compProd_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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∞)
have e_a : ρ = ρ.fst ⊗ₘ ρ.condKernel
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
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
⊢ ∫⁻ (b : β) in s, (((ρ.condKernel : (a : β) → Measure Ω) b : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t ∂ρ.fst =
    (ρ : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t)
have this : 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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
| ∫⁻ (x : β × Ω), f x ∂ρ
have rw : ∫⁻ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel
Tactic: rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst = ∫⁻ (x : β × Ω), f x ∂ρ
have conv_rhs : ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
  ∫⁻ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel
Tactic: conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel
have rw : ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
  ∫⁻ (a : β), ∫⁻ (b : Ω), f (a, b) ∂(ρ.condKernel : (a : β) → Measure Ω) a ∂ρ.fst
Tactic: rw [lintegral_compProd hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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
| ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ
have rw : ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
Tactic: rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ
have conv_rhs : ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
  ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
Tactic: conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
have 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
Tactic: rw [setLIntegral_compProd hf hs ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
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 =
    ∫⁻ (x : β × Ω) in SProd.sprod (β := Set Ω) s Set.univ, f x ∂ρ
have rw : ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
  ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst
Tactic: rw [← setLIntegral_condKernel hf hs MeasurableSet.univ]