awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst : ∀ (b : α), IsMarkovKernel (κ.sectR b)
x : α × β
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((((κ.sectR x.1 : (a : β) → Measure γ) x.2 : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [← sectR_apply, measure_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst : ∀ (b : α), IsMarkovKernel (κ.sectR b)
x : α × β
rw :
  Eq (α := ℝ≥0∞) ((((κ.sectR x.1 : (a : β) → Measure γ) x.2 : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [← sectR_apply, measure_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
f : δ → β
hf : Measurable f
⊢ (κ.sectR a).comap f hf = κ.comap (fun (d : δ) ↦ (a, f d)) ⋯
have h : ∀ (d : δ) (s : Set γ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) (((((κ.sectR a).comap f hf : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ.comap (fun (d : δ) ↦ (a, f d)) sorry : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext d s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
f : δ → β
hf : Measurable f
d : δ
s : Set γ
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((((κ.sectR a).comap f hf : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (a, f d)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((((κ.sectR a : (a : β) → Measure γ) (f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ.comap (fun (d : δ) ↦ (a, f d)) sorry : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, sectR_apply, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
f : δ → β
hf : Measurable f
d : δ
s : Set γ
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((κ.sectR a : (a : β) → Measure γ) (f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (a, f d)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((((κ.sectR a).comap f hf : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (a, f d)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) (a, f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ.comap (fun (d : δ) ↦ (a, f d)) sorry : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, sectR_apply, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
f : δ → β
hf : Measurable f
d : δ
s : Set γ
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((κ.sectR a : (a : β) → Measure γ) (f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (a, f d)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) (a, f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (a, f d)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((((κ.sectR a).comap f hf : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (a, f d)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) (a, f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α × β) → Measure γ) (a, f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, sectR_apply, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft γ κ) ↔ IsSFiniteKernel κ
have inhabit : ∀ (inhabited_h : Inhabited γ), IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft γ κ) ↔ IsSFiniteKernel κ
Tactic: inhabit γ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft γ κ) ↔ IsSFiniteKernel κ
have refine : ∀ (h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft γ κ)), IsSFiniteKernel κ
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft γ κ)
⊢ IsSFiniteKernel κ
have rw : IsSFiniteKernel (sectR (mα := mγ) (prodMkLeft γ κ) default)
Tactic: rw [← sectR_prodMkLeft γ κ default]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight γ κ) ↔ IsSFiniteKernel κ
have inhabit : ∀ (inhabited_h : Inhabited γ), IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight γ κ) ↔ IsSFiniteKernel κ
Tactic: inhabit γ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight γ κ) ↔ IsSFiniteKernel κ
have refine : ∀ (h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight γ κ)), IsSFiniteKernel κ
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight γ κ)
⊢ IsSFiniteKernel κ
have rw : IsSFiniteKernel (sectL (mβ := mγ) (prodMkRight γ κ) default)
Tactic: rw [← sectL_prodMkRight γ κ default]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
⊢ Eq.{u_2 + 1} (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
    ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) ())
have rw : Eq.{u_2 + 1} (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
  (bind.{u_1, u_2} (α := α) (mα := mα) ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) (⇑κ : (a : α) → Measure β))
Tactic: rw [Kernel.comp_apply, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
rw :
  Eq.{u_2 + 1} (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
    (bind.{u_1, u_2} (α := α) (mα := mα) ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) (⇑κ : (a : α) → Measure β))
⊢ Eq.{u_2 + 1} (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
    ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) ())
have rw₁ : Eq.{u_2 + 1} (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
Tactic: rw [Kernel.comp_apply, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : Countable α
inst_1 : MeasurableSingletonClass α
⊢ Eq.{u_2 + 1} (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
    (sum fun (ω : α) ↦
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {ω} : ℝ≥0∞)
        ((κ : (a : α) → Measure β) ω : Measure β))
have h : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (ω : α) ↦
              HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {ω} : ℝ≥0∞)
                ((κ : (a : α) → Measure β) ω : Measure β) :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : Countable α
inst_1 : MeasurableSingletonClass α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (ω : α) ↦
              HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {ω} : ℝ≥0∞)
                ((κ : (a : α) → Measure β) ω : Measure β) :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s ∂μ =
  ∑' (i : α),
    (HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {i} : ℝ≥0∞)
          ((κ : (a : α) → Measure β) i : Measure β) :
        (a : Set β) → ℝ≥0∞)
      s
Tactic: rw [Measure.sum_apply _ hs, Measure.bind_apply hs (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
⊢ (μ ⊗ₘ κ).snd = (⇑κ : (a : α) → Measure β) ∘ₘ μ
have h : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' Prod.snd ⁻¹' s) ∂μ =
  ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s ∂μ
Tactic: rw [bind_apply hs κ.aemeasurable, snd_apply hs, compProd_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
h :
  ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' Prod.snd ⁻¹' s) ∂μ =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s ∂μ
⊢ Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : MeasurableSet (α := α × β) (Prod.snd ⁻¹' s)
Tactic: rw [bind_apply hs κ.aemeasurable, snd_apply hs, compProd_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
h : ∀ᵐ (ω : β) ∂(⇑κ : (a : α) → Measure β) ∘ₘ μ, p ω
⊢ ∀ᵐ (ω' : α) ∂μ, ∀ᵐ (ω : β) ∂((κ : (a : α) → Measure β) ω' : Measure β), p ω
have h₁ : ∀ᵐ (ω : β) ∂((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β), p ω
Tactic: rw [comp_eq_comp_const_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
hp : MeasurableSet.{u_2} (α := β) {z : β | p z}
h : ∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂((κ : (a : α) → Measure β) y : Measure β), p z
⊢ ∀ᵐ (z : β) ∂(⇑κ : (a : α) → Measure β) ∘ₘ μ, p z
have rw : ∀ᵐ (z : β) ∂((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β), p z
Tactic: rw [comp_eq_comp_const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
⊢ SFinite.{u_2} (α := β) (m0 := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
have rw : SFinite (μ ⊗ₘ κ).snd
Tactic: rw [← snd_compProd]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
⊢ IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
have rw : IsFiniteMeasure (μ ⊗ₘ κ).snd
Tactic: rw [← snd_compProd]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst : IsProbabilityMeasure μ
inst_1 : IsMarkovKernel κ
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
have rw : IsProbabilityMeasure (μ ⊗ₘ κ).snd
Tactic: rw [← snd_compProd]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst : IsZeroOrProbabilityMeasure μ
inst_1 : IsZeroOrMarkovKernel κ
⊢ IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
have rw : IsZeroOrProbabilityMeasure (μ ⊗ₘ κ).snd
Tactic: rw [← snd_compProd]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
⊢ Eq (α := Measure γ) (map f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)) ((⇑(κ.map f) : (a : α) → Measure γ) ∘ₘ μ)
have h : ∀ (s : Set γ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((map f ((⇑κ : (a : α) → Measure β) ∘ₘ μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((⇑(κ.map f) : (a : α) → Measure γ) ∘ₘ μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map f ((⇑κ : (a : α) → Measure β) ∘ₘ μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((⇑(κ.map f) : (a : α) → Measure γ) ∘ₘ μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) ∂μ =
  ∫⁻ (a : α), ((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂μ
Tactic: rw [Measure.map_apply hf hs, Measure.bind_apply (hf hs) κ.aemeasurable,
    Measure.bind_apply hs (Kernel.aemeasurable _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ (⇑(Kernel.discard α) : (a : α) → Measure PUnit.{1}) ∘ₘ μ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure Unit) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (dirac ())
have h : ∀ (s : Set PUnit.{1}) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((⇑(Kernel.discard α) : (a : α) → Measure PUnit.{1}) ∘ₘ μ : (a : Set PUnit.{1}) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (β := Measure Unit) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (dirac ()) :
          (a : Set PUnit.{1}) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ Eq (α := Measure (β × β)) (bind (mα := mβ) (map f μ) (⇑(Kernel.copy β) : (a : β) → Measure (β × β)))
    (map (fun (a : α) ↦ (f a, f a)) μ)
have rw : Eq (α := Measure (β × β)) (map ((fun (x : β) ↦ (x, x)) ∘ f) μ) (map (fun (a : α) ↦ (f a, f a)) μ)
Tactic: rw [Kernel.copy, deterministic_comp_eq_map, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = (⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ
have rw : Eq (α := Measure (α × β)) ((Kernel.id ×ₖ κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
  ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ : Measure (α × β))
Tactic: rw [compProd, Kernel.compProd_prodMkLeft_eq_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
⊢ μ ⊗ₘ Kernel.id = (⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ
have rw : Eq (α := Measure (α × α)) (map (fun (x : α) ↦ (x, x)) μ) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
Tactic: rw [compProd_id, Kernel.copy, deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
rw : Eq (α := Measure (α × α)) (map (fun (x : α) ↦ (x, x)) μ) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
⊢ μ ⊗ₘ Kernel.id = (⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ
have rw₁ : Eq (α := Measure (α × α)) (map (fun (x : α) ↦ (x, x)) μ)
  ((⇑(Kernel.deterministic (fun (x : α) ↦ (x, x)) sorry) : (a : α) → Measure (α × α)) ∘ₘ μ)
Tactic: rw [compProd_id, Kernel.copy, deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
rw : Eq (α := Measure (α × α)) (map (fun (x : α) ↦ (x, x)) μ) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
rw₁ :
  Eq (α := Measure (α × α)) (map (fun (x : α) ↦ (x, x)) μ)
    ((⇑(Kernel.deterministic (fun (x : α) ↦ (x, x)) ⋯) : (a : α) → Measure (α × α)) ∘ₘ μ)
⊢ μ ⊗ₘ Kernel.id = (⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ
have rw₂ : Eq (α := Measure (α × α)) (map (fun (x : α) ↦ (x, x)) μ) (map (fun (x : α) ↦ (x, x)) μ)
Tactic: rw [compProd_id, Kernel.copy, deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ))
have pos : ∀ (hκ : IsSFiniteKernel κ),
  Eq.{u_3 + 1} (α := Measure γ) ((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ))
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
pos :
  ∀ (hκ : IsSFiniteKernel κ),
    Eq.{u_3 + 1} (α := Measure γ) ((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
      (snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ))
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ))
have neg : ∀ (hκ : ¬IsSFiniteKernel κ),
  Eq.{u_3 + 1} (α := Measure γ) ((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ))
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ))
have pos : ∀ (s : Set γ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s :
      ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s :
      ℝ≥0∞)
have pos : ∫⁻ (a : α),
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a ∂μ =
  ∫⁻ (a : α),
    (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) ∂μ
Tactic: rw [Measure.bind_apply hs η.aemeasurable, Measure.snd_apply hs,
    Measure.bind_apply _ (Kernel.aemeasurable _), Measure.lintegral_compProd (η.measurable_coe hs)]