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
⊢ ∀ᵐ (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:
have h_ae : ∀ᵐ t ∂(fst κ a), (a, t) ∈ {p : α × β | η p (range e)ᶜ = 0} := by
    rw [← h_fst]
    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
    rw [← hη', compProd_null] at h_compProd
    swap; · exact (MeasurableSet.univ.prod he.measurableSet_range).compl
    simp only [preimage_compl, mem_univ, mk_preimage_prod_right] at h_compProd
    exact h_compProd
-- 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 :
  ∀ᵐ (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)
h :
  ∀ (a_1 : β)
    (ha :
      Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
        (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      ((((borelMarkovFromReal Ω η : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' t) :
        ℝ≥0∞)
      ((((η.comapRight he : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' t) :
        ℝ≥0∞)
⊢ (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)

Tactic:
filter_upwards [h_ae] with a ha
-- 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_1 : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae :
  ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a_1 : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a_1, t)
a : β
ha :
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞)
    ((((piecewise (s :=
                  preimage (β := ℝ≥0∞)
                    (fun (a : α × β) ↦
                      (((η : (a : α × β) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
                    {0})
                  ⋯ η
                  (deterministic (fun (x : α × β) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)
                    ⋯) :
                (a : α × β) → Measure ℝ)
              (a_1, a) :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
h₁ h₂ : MeasurableSet (Prod.mk a ⁻¹' t)
⊢ Eq (α := ℝ≥0∞)
    ((((borelMarkovFromReal Ω η : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
    ((((η.comapRight he : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)

Tactic:
rw [borelMarkovFromReal, comapRight_apply', comapRight_apply']

Premises used: ProbabilityTheory.Kernel.borelMarkovFromReal, ProbabilityTheory.Kernel.comapRight_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_1 : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae :
  ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a_1 : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a_1, t)
a : β
ha :
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ MeasurableSet (Prod.mk a ⁻¹' t)

Tactic:
measurable_prodMk_left ht

Premises used: measurable_prodMk_left
-- 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_1 : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae :
  ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a_1 : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a_1, t)
a : β
ha :
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ MeasurableSet (Prod.mk a ⁻¹' t)

Tactic:
exact measurable_prodMk_left ht

Premises used: measurable_prodMk_left
-- 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_1 : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae :
  ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a_1 : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a_1, t)
a : β
ha :
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
h :
  Membership.mem (γ := Set (α × β))
    (preimage (β := ℝ≥0∞)
      (fun (a : α × β) ↦
        (((η : (a : α × β) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
      {0})
    (a_1, a)
⊢ Eq (α := ℝ≥0∞)
    ((((piecewise (s :=
                  preimage (β := ℝ≥0∞)
                    (fun (a : α × β) ↦
                      (((η : (a : α × β) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
                    {0})
                  ⋯ η
                  (deterministic (fun (x : α × β) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)
                    ⋯) :
                (a : α × β) → Measure ℝ)
              (a_1, a) :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)

Tactic:
rw [piecewise_apply, if_pos]

Premises used: ProbabilityTheory.Kernel.piecewise_apply, if_pos
-- 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_1 : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae :
  ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a_1 : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a_1, t)
a : β
ha :
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Membership.mem (γ := Set (α × β))
    (preimage (β := ℝ≥0∞)
      (fun (a : α × β) ↦
        (((η : (a : α × β) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
      {0})
    (a_1, a)

Tactic:
ha

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton
-- 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_1 : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae :
  ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a_1 : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a_1, t)
a : β
ha :
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Membership.mem (γ := Set (α × β))
    (preimage (β := ℝ≥0∞)
      (fun (a : α × β) ↦
        (((η : (a : α × β) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
      {0})
    (a_1, a)

Tactic:
exact ha
-- 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 :
  ∀ (c : α) (t : Set (β × Ω)),
    MeasurableSet t →
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t : ℝ≥0∞)
        ((((κ'.comapRight h_prod_embed : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t :
          ℝ≥0∞)
⊢ κ = κ'.comapRight h_prod_embed

Tactic:
ext c t : 2
-- 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)
c : α
t : Set (β × Ω)
h_1 : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t : ℝ≥0∞)
    ((((comapRight (κ.map (Prod.map id e)) h_prod_embed : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) :
          (a : Set (β × Ω)) → ℝ≥0∞)
        t :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ'.comapRight h_prod_embed : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t :
      ℝ≥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)
c : α
t : Set (β × Ω)
h : 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)
c : α
t : Set (β × Ω)
h_1 : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t : ℝ≥0∞)
    ((Measure.comap (Prod.map id e)
            (((κ.map (Prod.map id e) : Kernel.{u_1, u_2} α (β × ℝ)) : (a : α) → Measure (β × ℝ)) c) :
          (a : Set (β × Ω)) → ℝ≥0∞)
        t :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t : ℝ≥0∞)
    ((Measure.comap (Prod.map id e) (Measure.map (Prod.map id e) ((κ : (a : α) → Measure (β × Ω)) c)) :
          (a : Set (β × Ω)) → ℝ≥0∞)
        t :
      ℝ≥0∞)
h₂ h₃ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t : ℝ≥0∞)
    ((((comapRight (κ.map (Prod.map id e)) h_prod_embed : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) :
          (a : Set (β × Ω)) → ℝ≥0∞)
        t :
      ℝ≥0∞)

Tactic:
rw [comapRight_apply, map_apply _ (by fun_prop), h_prod_embed.comap_map]

Premises used: ProbabilityTheory.Kernel.map_apply, MeasurableEmbedding.comap_map, ProbabilityTheory.Kernel.comapRight_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)
⊢ κ = κ'.comapRight h_prod_embed

Tactic:
have : κ = comapRight κ' h_prod_embed := by
    ext c t : 2
    unfold κ'
    rw [comapRight_apply, map_apply _ (by fun_prop), h_prod_embed.comap_map]
-- 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)
this : κ = κ'.comapRight h_prod_embed
rw : (κ'.fst ⊗ₖ η).comapRight h_prod_embed
| κ

Tactic:
rw [this, ← hη']
-- 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)
this : κ = κ'.comapRight h_prod_embed
conv_rhs : κ.fst ⊗ₖ borelMarkovFromReal Ω η = (κ'.fst ⊗ₖ η).comapRight h_prod_embed
⊢ κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ

Tactic:
conv_rhs => rw [this, ← hη']
-- 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)
this : κ = κ'.comapRight h_prod_embed
⊢ κ.fst ⊗ₖ borelMarkovFromReal Ω η = (κ'.fst ⊗ₖ η).comapRight h_prod_embed

Tactic:
compProd_fst_borelMarkovFromReal_eq_comapRight_compProd κ η hη

Premises used: ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal_eq_comapRight_compProd
-- 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)
this : κ = κ'.comapRight h_prod_embed
⊢ κ.fst ⊗ₖ borelMarkovFromReal Ω η = (κ'.fst ⊗ₖ η).comapRight h_prod_embed

Tactic:
exact compProd_fst_borelMarkovFromReal_eq_comapRight_compProd κ η hη

Premises used: ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal_eq_comapRight_compProd
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
κ : Kernel α (γ × Ω)
inst_3 : IsFiniteKernel κ
⊢ IsMarkovKernel (mα := Prod.instMeasurableSpace) (mβ := mΩ)
    (borelMarkovFromReal Ω (condKernelReal (κ.map (Prod.map id (embeddingReal Ω)))))

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
κ : Kernel α (γ × Ω)
inst_3 : IsFiniteKernel κ
rw : κ.fst ⊗ₖ borelMarkovFromReal Ω (condKernelReal (κ.map (Prod.map id (embeddingReal Ω)))) = κ
rw₁ rw₂ : κ = κ
⊢ κ.fst ⊗ₖ κ.condKernelBorel = κ

Tactic:
rw [condKernelBorel, compProd_fst_borelMarkovFromReal _ _ (compProd_fst_condKernelReal _)]

Premises used: ProbabilityTheory.Kernel.condKernelBorel, ProbabilityTheory.Kernel.compProd_fst_condKernelReal, ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal