awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h :
  (ae (F := Measure β) ((κ.fst : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦
      (((borelMarkovFromReal Ω η : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk b ⁻¹' t))
    fun (b : β) ↦
    (((η.comapRight he : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk b ⁻¹' t)
⊢ ∫⁻ (b : β),
      (((borelMarkovFromReal Ω η : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η.comapRight he : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(κ.fst : (a : α) → Measure β) a

Tactic:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
rw :
  ∀ᵐ (t : β) ∂((κ'.fst : (a : α) → Measure β) a : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a, t)
⊢ ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a, t)

Tactic:
rw [← h_fst]
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
unfold :
  Eq (α := ℝ≥0∞)
    (((((κ.map (Prod.map id e) : Kernel.{u_1, u_2} α (β × ℝ)) : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) :
          (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) univ (range e))ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((κ' : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) univ (range e))ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
unfold κ'
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
⊢ Measurable (α := β × Ω) (Prod.map id e)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
rw :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞)
        (Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
hs : MeasurableSet (SProd.sprod (α := Set β) univ (range e))ᶜ
⊢ Eq (α := ℝ≥0∞)
    (((((κ.map (Prod.map id e) : Kernel.{u_1, u_2} α (β × ℝ)) : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) :
          (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) univ (range e))ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [map_apply' _ (by fun_prop)]

Premises used: ProbabilityTheory.Kernel.map_apply'
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
⊢ MeasurableSet (SProd.sprod (α := Set β) univ (range e))ᶜ

Tactic:
(MeasurableSet.univ.prod he.measurableSet_range).compl

Premises used: Set.Mem, setOf, MeasurableSet.prod, MeasurableSet.compl, MeasurableEmbedding.measurableSet_range, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
⊢ MeasurableSet (SProd.sprod (α := Set β) univ (range e))ᶜ

Tactic:
exact (MeasurableSet.univ.prod he.measurableSet_range).compl

Premises used: MeasurableSet.prod, MeasurableSet.compl, MeasurableEmbedding.measurableSet_range, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
this : Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ = ∅
rw : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) ∅) 0
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞)
        (Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [this]
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
this : Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ = ∅
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) ∅) 0

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
suffices : Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ = ∅
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞)
        (Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
suffices Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ = ∅ by rw [this]; simp
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h :
  ∀ (x : β × Ω),
    x ∈ Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ ↔ Membership.mem (γ := Set (β × Ω)) ∅ x
⊢ Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ = ∅

Tactic:
ext x
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
x : β × Ω
⊢ x ∈ Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ ↔ Membership.mem (γ := Set (β × Ω)) ∅ x

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞)
    ((((κ' : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) univ (range e))ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
have h_compProd : κ' a (univ ×ˢ range e)ᶜ = 0 := by
      unfold κ'
      rw [map_apply' _ (by fun_prop)]
      swap; · exact (MeasurableSet.univ.prod he.measurableSet_range).compl
      suffices Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ = ∅ by rw [this]; simp
      ext x
      simp
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd :
  Eq (α := ℝ≥0∞)
    ((((κ' : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) univ (range e))ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
rw :
  ∀
    (h_compProd :
      (ae (F := Measure β) ((κ'.fst : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
        (fun (b : β) ↦
          (((η : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
            (Prod.mk b ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ))
        0),
    ∀ᵐ (t : β) ∂((κ'.fst : (a : α) → Measure β) a : Measure β),
      Membership.mem (γ := Set (α × β))
        {p : α × β |
          Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞)}
        (a, t)
hs :
  ∀
    (h_compProd :
      Eq (α := ℝ≥0∞)
        ((((κ'.fst ⊗ₖ η : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
            (SProd.sprod (α := Set β) univ (range e))ᶜ :
          ℝ≥0∞)
        (0 : ℝ≥0∞)),
    MeasurableSet (SProd.sprod (α := Set β) univ (range e))ᶜ
⊢ ∀ᵐ (t : β) ∂((κ'.fst : (a : α) → Measure β) a : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a, t)

Tactic:
rw [← hη', compProd_null] at h_compProd

Premises used: ProbabilityTheory.Kernel.compProd_null
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd :
  Eq (α := ℝ≥0∞)
    ((((κ'.fst ⊗ₖ η : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) univ (range e))ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ MeasurableSet (SProd.sprod (α := Set β) univ (range e))ᶜ

Tactic:
(MeasurableSet.univ.prod he.measurableSet_range).compl

Premises used: Set.Mem, setOf, MeasurableSet.prod, MeasurableSet.compl, MeasurableEmbedding.measurableSet_range, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd :
  Eq (α := ℝ≥0∞)
    ((((κ'.fst ⊗ₖ η : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) univ (range e))ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ MeasurableSet (SProd.sprod (α := Set β) univ (range e))ᶜ

Tactic:
exact (MeasurableSet.univ.prod he.measurableSet_range).compl

Premises used: MeasurableSet.prod, MeasurableSet.compl, MeasurableEmbedding.measurableSet_range, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd :
  (ae (F := Measure β) ((κ'.fst : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦
      (((η : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ))
    0
⊢ (ae (F := Measure β) ((κ'.fst : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ) 0

Tactic:
simp only [preimage_compl, mem_univ, mk_preimage_prod_right] at h_compProd

Premises used: Set.mem_univ, Set.mk_preimage_prod_right, Set.preimage_compl
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd :
  (ae (F := Measure β) ((κ'.fst : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ) 0
⊢ ∀ᵐ (t : β) ∂((κ'.fst : (a : α) → Measure β) a : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a, t)

Tactic:
h_compProd

Premises used: Set.Mem, setOf, Filter.EventuallyEq
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd :
  (ae (F := Measure β) ((κ'.fst : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ) 0
⊢ ∀ᵐ (t : β) ∂((κ'.fst : (a : α) → Measure β) a : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a, t)

Tactic:
exact h_compProd