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_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∞)
    (((if
                Membership.mem (γ := Set (α × β))
                  (preimage (β := ℝ≥0∞)
                    (fun (a : α × β) ↦
                      (((η : (a : α × β) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
                    {0})
                  (a_1, a) then
              (η : (a : α × β) → Measure ℝ) (a_1, a)
            else
              ((deterministic (fun (x : α × β) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) ⋯ :
                    Kernel (α × β) ℝ) :
                  (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∞)
⊢ 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∞)
have h₁ : Eq (α := ℝ≥0∞)
  ((((η : (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: classical
  rw [piecewise_apply, if_pos]
  exact ha
-- 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 ⊗ₖ η = κ'
⊢ κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ
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)
⊢ κ = κ'.comapRight h_prod_embed
have 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∞)
Tactic: ext c t : 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)
c : α
t : Set (β × Ω)
h : MeasurableSet t
⊢ 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∞)
have 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∞)
Tactic: rw [comapRight_apply, map_apply _ (by fun_prop), h_prod_embed.comap_map]
-- 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)
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∞)
⊢ 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∞)
have 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∞)
Tactic: rw [comapRight_apply, map_apply _ (by fun_prop), h_prod_embed.comap_map]
-- 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)
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∞)
⊢ 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∞)
have h₂ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t : ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × Ω)) c : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [comapRight_apply, map_apply _ (by fun_prop), h_prod_embed.comap_map]
-- 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 Ω η = κ
have this : κ = κ'.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]
-- 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)
this : κ = κ'.comapRight h_prod_embed
| κ
have rw : (κ'.fst ⊗ₖ η).comapRight h_prod_embed
Tactic: rw [this, ← hη']
-- 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)
this : κ = κ'.comapRight h_prod_embed
⊢ κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ
have conv_rhs : κ.fst ⊗ₖ borelMarkovFromReal Ω η = (κ'.fst ⊗ₖ η).comapRight h_prod_embed
Tactic: conv_rhs => rw [this, ← 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 : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernelBorel = κ
have rw : κ.fst ⊗ₖ borelMarkovFromReal Ω (condKernelReal (κ.map (Prod.map id (embeddingReal Ω)))) = κ
Tactic: rw [condKernelBorel, compProd_fst_borelMarkovFromReal _ _ (compProd_fst_condKernelReal _)]
-- 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 : IsFiniteKernel κ
rw : κ.fst ⊗ₖ borelMarkovFromReal Ω (condKernelReal (κ.map (Prod.map id (embeddingReal Ω)))) = κ
⊢ κ.fst ⊗ₖ κ.condKernelBorel = κ
have rw₁ : κ = κ
Tactic: rw [condKernelBorel, compProd_fst_borelMarkovFromReal _ _ (compProd_fst_condKernelReal _)]
-- 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 Unit (α × Ω)
inst_3 : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernelUnitBorel = κ
have rw : κ.fst ⊗ₖ borelMarkovFromReal Ω (condKernelUnitReal (κ.map (Prod.map id (embeddingReal Ω)))) = κ
Tactic: rw [condKernelUnitBorel, compProd_fst_borelMarkovFromReal _ _ (disintegrate _ _)]
-- 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 Unit (α × Ω)
inst_3 : IsFiniteKernel κ
rw : κ.fst ⊗ₖ borelMarkovFromReal Ω (condKernelUnitReal (κ.map (Prod.map id (embeddingReal Ω)))) = κ
⊢ κ.fst ⊗ₖ κ.condKernelUnitBorel = κ
have rw₁ : κ = κ
Tactic: rw [condKernelUnitBorel, compProd_fst_borelMarkovFromReal _ _ (disintegrate _ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
Ω : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
ρ : Measure (α × Ω)
inst_2 : IsFiniteMeasure ρ
a : α
⊢ Eq.{u_4 + 1} (α := Measure Ω) ((ρ.condKernel : (a : α) → Measure Ω) a : Measure Ω)
    ((condKernelUnitBorel (const Unit ρ) : (a : Unit × α) → Measure Ω) ((), a) : Measure Ω)
have rw : Eq.{u_4 + 1} (α := Measure Ω)
  (((condKernelUnitBorel (const Unit ρ)).comap (fun (a : α) ↦ ((), a)) sorry : (a : α) → Measure Ω) a : Measure Ω)
  ((condKernelUnitBorel (const Unit ρ) : (a : Unit × α) → Measure Ω) ((), a) : Measure Ω)
Tactic: rw [Measure.condKernel]
-- 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 Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
⊢ Eq (α := Kernel Unit α) (const Unit ρ.fst) (fst (const Unit ρ))
have h : ∀ (a : Unit) (s : Set α),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((const Unit ρ.fst : (a : Unit) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((((fst (const Unit ρ) : (a : Unit) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (hypothesis)
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 Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
⊢ ρ.fst ⊗ₘ ρ.condKernel = ρ
have h1 : Eq (α := Kernel Unit α) (const Unit ρ.fst) (fst (const Unit ρ))
Tactic: have h1 : const Unit (Measure.fst ρ) = fst (const Unit ρ) := by
      ext
      simp only [fst_apply, Measure.fst, const_apply]
-- 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 Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
h1 : Eq (α := Kernel Unit α) (const Unit ρ.fst) (fst (const Unit ρ))
⊢ prodMkLeft Unit ρ.condKernel = condKernelUnitBorel (const Unit ρ)
have h : ∀ (a : Unit × α) (s : Set Ω),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      (((((prodMkLeft Unit ρ.condKernel : Kernel.{u_1, u_4} (Unit × α) Ω) : (a : Unit × α) → Measure Ω) a : Measure Ω) :
            (a : Set Ω) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((condKernelUnitBorel (const Unit ρ) : (a : Unit × α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s :
        ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (hypothesis)
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 Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
h1 : Eq (α := Kernel Unit α) (const Unit ρ.fst) (fst (const Unit ρ))
⊢ ρ.fst ⊗ₘ ρ.condKernel = ρ
have h2 : prodMkLeft Unit ρ.condKernel = condKernelUnitBorel (const Unit ρ)
Tactic: have h2 : prodMkLeft Unit (Measure.condKernel ρ) = condKernelUnitBorel (const Unit ρ) := by
      ext
      simp only [prodMkLeft_apply, Measure.condKernel_apply]
-- 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 Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
h1 : Eq (α := Kernel Unit α) (const Unit ρ.fst) (fst (const Unit ρ))
h2 : prodMkLeft Unit ρ.condKernel = condKernelUnitBorel (const Unit ρ)
⊢ ρ.fst ⊗ₘ ρ.condKernel = ρ
have rw : (const Unit ρ : (a : Unit) → Measure (α × Ω)) () = ρ
Tactic: rw [Measure.compProd, h1, h2, disintegrate]
-- 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 Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
⊢ IsMarkovKernel ρ.condKernel
have rw : IsMarkovKernel ((condKernelUnitBorel (const Unit ρ)).comap (fun (a : α) ↦ ((), a)) sorry)
Tactic: rw [Measure.condKernel]
-- 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 Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
⊢ IsMarkovKernel κ.condKernel
have rw : IsMarkovKernel (α := α × β) (β := Ω) (mα := Prod.instMeasurableSpace) (mβ := mΩ)
  (if hα : Countable α then condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) sorry
  else κ.condKernelBorel)
Tactic: rw [condKernel_def]
-- 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 Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
⊢ IsMarkovKernel (α := α × β) (β := Ω) (mα := Prod.instMeasurableSpace) (mβ := mΩ)
    (if hα : Countable α then
      condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯
    else κ.condKernelBorel)
have pos : ∀ (h : Countable α),
  IsMarkovKernel (α := α × β) (β := Ω) (mα := Prod.instMeasurableSpace) (mβ := mΩ)
    (condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) sorry)
Tactic: split_ifs
-- 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 Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
pos :
  ∀ (h : Countable α),
    IsMarkovKernel (α := α × β) (β := Ω) (mα := Prod.instMeasurableSpace) (mβ := mΩ)
      (condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯)
⊢ IsMarkovKernel (α := α × β) (β := Ω) (mα := Prod.instMeasurableSpace) (mβ := mΩ)
    (if hα : Countable α then
      condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯
    else κ.condKernelBorel)
have neg : ∀ (h_1 : ¬Countable α), IsMarkovKernel κ.condKernelBorel
Tactic: split_ifs
-- 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 Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernel = κ
have rw : (κ.fst ⊗ₖ
    if hα : Countable α then
      condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) sorry
    else κ.condKernelBorel) =
  κ
Tactic: rw [condKernel_def]
-- 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 Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
⊢ (κ.fst ⊗ₖ
      if hα : Countable α then
        condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯
      else κ.condKernelBorel) =
    κ
have pos : ∀ (hα : Countable α),
  κ.fst ⊗ₖ condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) sorry = κ
Tactic: split_ifs with hα