awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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∞)
⊢ 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∞)
have 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 Ω))) sorry) sorry : Kernel α ℝ) :
                (a : α) → Measure ℝ)
              a :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (range (embeddingReal Ω)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω)) : ℝ≥0∞)
    (1 : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rwa [← prob_compl_eq_zero_iff (measurableEmbedding_embeddingReal Ω).measurableSet_range]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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 : α
⊢ 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∞)
have 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 Ω))) sorry) sorry :
                  Kernel α ℝ) :
                (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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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∞)
⊢ 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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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∞)
⊢ 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∞)
have 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 Ω))) sorry) sorry : Kernel α ℝ) :
                (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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (hypothesis)
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 ⊗ₖ η = κ'
⊢ Eq (α := Kernel α (β × Ω)) (κ.fst ⊗ₖ borelMarkovFromReal Ω η)
    ((fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η).comapRight (f :=
      Prod.map id (embeddingReal Ω)) ⋯)
have h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
Tactic: have h_prod_embed : MeasurableEmbedding (Prod.map (id : β → β) e) :=
    MeasurableEmbedding.id.prodMap he
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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 ⊗ₖ borelMarkovFromReal Ω η = (κ'.fst ⊗ₖ η).comapRight h_prod_embed
have rw : κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ'.fst ⊗ₖ η.comapRight he
Tactic: rw [comapRight_compProd_id_prod _ _ he]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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
have 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∞)
Tactic: ext a u
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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∞)
    (((((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∞)
have 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∞)
Tactic: rw [fst_apply, map_apply _ (by fun_prop),
      Measure.map_map measurable_fst h_prod_embed.measurable, fst_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (hypothesis)
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 ⊗ₖ borelMarkovFromReal Ω η = κ'.fst ⊗ₖ η.comapRight he
have h_fst : κ'.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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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
⊢ κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ'.fst ⊗ₖ η.comapRight he
have rw : κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ.fst ⊗ₖ η.comapRight he
Tactic: rw [h_fst]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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
⊢ κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ.fst ⊗ₖ η.comapRight he
have 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∞)
Tactic: ext a t ht : 2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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∞)
    ((((κ.fst ⊗ₖ borelMarkovFromReal Ω η : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((((κ.fst ⊗ₖ η.comapRight he : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t : ℝ≥0∞)
have 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
Tactic: simp_rw [compProd_apply ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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
have 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)
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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)
have 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)
Tactic: rw [← h_fst]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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∞)
    (((((κ.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∞)
have rw : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞)
      (Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rw [map_apply' _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
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∞)
⊢ 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∞)
have hs : MeasurableSet (SProd.sprod (α := Set β) univ (range e))ᶜ
Tactic: rw [map_apply' _ (by fun_prop)]