awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsMarkovKernel η
⊢ IsMarkovKernel (mβ := mΩ) (borelMarkovFromReal Ω η)

Tactic:
IsMarkovKernel.comapRight _ (measurableEmbedding_embeddingReal Ω) (fun a ↦ ?_)

Premises used: MeasureTheory.measurableEmbedding_embeddingReal, ProbabilityTheory.Kernel.IsMarkovKernel.comapRight, ProbabilityTheory.Kernel.borelMarkovFromReal
-- 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 : IsMarkovKernel η
refine :
  ∀ (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 :
              Measure ℝ) :
            (a : Set ℝ) → ℝ≥0∞)
          (range (embeddingReal Ω)) :
        ℝ≥0∞)
      (1 : ℝ≥0∞)
⊢ IsMarkovKernel (mβ := mΩ) (borelMarkovFromReal Ω η)

Tactic:
refine IsMarkovKernel.comapRight _ (measurableEmbedding_embeddingReal Ω) (fun a ↦ ?_)

Premises used: MeasureTheory.measurableEmbedding_embeddingReal, ProbabilityTheory.Kernel.IsMarkovKernel.comapRight
-- 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 : IsMarkovKernel η
a : α
pos :
  ∀
    (h :
      Membership.mem (γ := Set α)
        (preimage (β := ℝ≥0∞)
          (fun (a : α) ↦ (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
          {0})
        a),
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω)) : ℝ≥0∞)
      (1 : ℝ≥0∞)
neg :
  ∀
    (h :
      a ∉
        preimage (β := ℝ≥0∞)
          (fun (a : α) ↦ (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
          {0}),
    Eq (α := ℝ≥0∞)
      (((((deterministic (fun (x : α) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) ⋯ :
                    Kernel α ℝ) :
                  (a : α) → Measure ℝ)
                a :
              Measure ℝ) :
            (a : Set ℝ) → ℝ≥0∞)
          (range (embeddingReal Ω)) :
        ℝ≥0∞)
      (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((if
                Membership.mem (γ := Set α)
                  (preimage (β := ℝ≥0∞)
                    (fun (a : α) ↦
                      (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
                    {0})
                  a then
              (η : (a : α) → Measure ℝ) a
            else
              ((deterministic (fun (x : α) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) ⋯ :
                    Kernel α ℝ) :
                  (a : α) → Measure ℝ)
                a :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (range (embeddingReal Ω)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
split_ifs with h
-- 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 : IsMarkovKernel η
a : α
h :
  Membership.mem (γ := Set α)
    (preimage (β := ℝ≥0∞)
      (fun (a : α) ↦ (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ) {0})
    a
pos pos₁ pos₂ pos₃ :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω)) : ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
rwa [← prob_compl_eq_zero_iff (measurableEmbedding_embeddingReal Ω).measurableSet_range]

Premises used: MeasureTheory.measurableEmbedding_embeddingReal, MeasureTheory.prob_compl_eq_zero_iff, MeasurableEmbedding.measurableSet_range
-- 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 : IsMarkovKernel η
a : α
h :
  a ∉
    preimage (β := ℝ≥0∞)
      (fun (a : α) ↦ (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ) {0}
⊢ Eq (α := ℝ≥0∞)
    ((Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) : (a : Set ℝ) → ℝ≥0∞)
        (range (embeddingReal Ω)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
simp [(range_nonempty (embeddingReal Ω)).choose_spec]

Premises used: Exists.choose_spec, MeasureTheory.embeddingReal, Set.range_nonempty
-- 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 : IsMarkovKernel η
a : α
rw rw₁ rw₂ :
  Eq (α := ℝ≥0∞)
    (((if
                Membership.mem (γ := Set α)
                  (preimage (β := ℝ≥0∞)
                    (fun (a : α) ↦
                      (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
                    {0})
                  a then
              (η : (a : α) → Measure ℝ) a
            else
              ((deterministic (fun (x : α) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) ⋯ :
                    Kernel α ℝ) :
                  (a : α) → Measure ℝ)
                a :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (range (embeddingReal Ω)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
pos :
  ∀
    (h :
      Membership.mem (γ := Set α)
        (preimage (β := ℝ≥0∞)
          (fun (a : α) ↦ (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
          {0})
        a),
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω)) : ℝ≥0∞)
      (1 : ℝ≥0∞)
neg neg₁ :
  ∀
    (h :
      a ∉
        preimage (β := ℝ≥0∞)
          (fun (a : α) ↦ (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
          {0}),
    Eq (α := ℝ≥0∞)
      (((((deterministic (fun (x : α) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) ⋯ :
                    Kernel α ℝ) :
                  (a : α) → Measure ℝ)
                a :
              Measure ℝ) :
            (a : Set ℝ) → ℝ≥0∞)
          (range (embeddingReal Ω)) :
        ℝ≥0∞)
      (1 : ℝ≥0∞)
⊢ 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 :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (range (embeddingReal Ω)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
classical
  rw [piecewise_apply]
  split_ifs with h
  · rwa [← prob_compl_eq_zero_iff (measurableEmbedding_embeddingReal Ω).measurableSet_range]
  · rw [deterministic_apply]
    simp [(range_nonempty (embeddingReal Ω)).choose_spec]

Premises used: Exists.choose_spec, MeasureTheory.measurableEmbedding_embeddingReal, ProbabilityTheory.Kernel.deterministic_apply, MeasureTheory.embeddingReal, ProbabilityTheory.Kernel.piecewise_apply, MeasureTheory.prob_compl_eq_zero_iff, MeasurableEmbedding.measurableSet_range, Set.range_nonempty
-- 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)
⊢ κ'.fst ⊗ₖ η = κ'

Tactic:
have hη' : fst κ' ⊗ₖ η = κ' := 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 ⊗ₖ η = κ'
⊢ MeasurableEmbedding (α := β × Ω) (Prod.map id e)

Tactic:
have h_prod_embed : MeasurableEmbedding (Prod.map (id : β → β) e) :=
    MeasurableEmbedding.id.prodMap he
-- 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)
change : κ.fst ⊗ₖ borelMarkovFromReal Ω η = (κ'.fst ⊗ₖ η).comapRight h_prod_embed
⊢ Eq (α := Kernel α (β × Ω)) (κ.fst ⊗ₖ borelMarkovFromReal Ω η)
    ((fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η).comapRight (f :=
      Prod.map id (embeddingReal Ω)) ⋯)

Tactic:
change fst κ ⊗ₖ borelMarkovFromReal Ω η = comapRight (fst κ' ⊗ₖ η) h_prod_embed

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

Tactic:
rw [comapRight_compProd_id_prod _ _ he]

Premises used: ProbabilityTheory.Kernel.comapRight_compProd_id_prod
-- 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 :
  ∀ (a : α) (u : Set β),
    MeasurableSet u →
      Eq (α := ℝ≥0∞) ((((κ'.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞)
⊢ κ'.fst = κ.fst

Tactic:
ext a u
-- 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)
a : α
u : Set β
h_1 : MeasurableSet u
h :
  Eq (α := ℝ≥0∞)
    (((((fst (mγ := Real.measurableSpace) (κ.map (Prod.map id e)) : Kernel α β) : (a : α) → Measure β) a : Measure β) :
          (a : Set β) → ℝ≥0∞)
        u :
      ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ'.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) u : ℝ≥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)
a : α
u : Set β
h : MeasurableSet u
⊢ 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)
a : α
u : Set β
h_1 : MeasurableSet u
h :
  Eq (α := ℝ≥0∞)
    (((Measure.map (Prod.fst ∘ Prod.map id e) ((κ : (a : α) → Measure (β × Ω)) a) : Measure β) : (a : Set β) → ℝ≥0∞) u :
      ℝ≥0∞)
    (((Measure.map (α := β × Ω) Prod.fst ((κ : (a : α) → Measure (β × Ω)) a) : Measure β) : (a : Set β) → ℝ≥0∞) u :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((fst (mγ := Real.measurableSpace) (κ.map (Prod.map id e)) : Kernel α β) : (a : α) → Measure β) a : Measure β) :
          (a : Set β) → ℝ≥0∞)
        u :
      ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
rw [fst_apply, map_apply _ (by fun_prop),
      Measure.map_map measurable_fst h_prod_embed.measurable, fst_apply]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.fst_apply, MeasurableEmbedding.measurable, MeasureTheory.Measure.map_map, measurable_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)
a : α
u : Set β
h : MeasurableSet u
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (Prod.fst ∘ Prod.map id e) ((κ : (a : α) → Measure (β × Ω)) a) : Measure β) : (a : Set β) → ℝ≥0∞) u :
      ℝ≥0∞)
    (((Measure.map (α := β × Ω) Prod.fst ((κ : (a : α) → Measure (β × Ω)) a) : Measure β) : (a : Set β) → ℝ≥0∞) u :
      ℝ≥0∞)

Tactic:
congr
-- 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)
⊢ κ'.fst = κ.fst

Tactic:
have h_fst : fst κ' = fst κ := by
    ext a u
    unfold κ'
    rw [fst_apply, map_apply _ (by fun_prop),
      Measure.map_map measurable_fst h_prod_embed.measurable, fst_apply]
    congr
-- 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
rw : κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ.fst ⊗ₖ η.comapRight he
⊢ κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ'.fst ⊗ₖ η.comapRight he

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
h :
  ∀ (a : α) (t : Set (β × Ω)) (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞)
      ((((κ.fst ⊗ₖ borelMarkovFromReal Ω η : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      ((((κ.fst ⊗ₖ η.comapRight he : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t :
        ℝ≥0∞)
⊢ κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ.fst ⊗ₖ η.comapRight he

Tactic:
ext a t ht : 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)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h :
  ∫⁻ (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
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst ⊗ₖ borelMarkovFromReal Ω η : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((((κ.fst ⊗ₖ η.comapRight he : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp_rw [compProd_apply ht]

Premises used: ProbabilityTheory.Kernel.compProd_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
⊢ ∫⁻ (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:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae