awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (b : α × α), ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η : (a : α × α) → Measure (β × γ)) b ∂Measure.dirac (a, a) =
    ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(η : (a : α) → Measure γ) a ∂(κ : (a : α) → Measure β) a
have rw : ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η : (a : α × α) → Measure (β × γ)) (a, a) =
  ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(η : (a : α) → Measure γ) a ∂(κ : (a : α) → Measure β) a
Tactic: rw [lintegral_dirac' _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η : (a : α × α) → Measure (β × γ)) (a, a) =
    ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(η : (a : α) → Measure γ) a ∂(κ : (a : α) → Measure β) a
have simp_rw : ∫⁻ (c : β × γ), g c ∂Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) =
  ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(η : (a : α) → Measure γ) a ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [parallelComp_apply, MeasureTheory.lintegral_prod _ hg.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ ×ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂(κ : (a : α) → Measure β) a ∂(η : (a : α) → Measure γ) a
have rw : ∫⁻ (c : β × γ), g c ∂Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) =
  ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂(κ : (a : α) → Measure β) a ∂(η : (a : α) → Measure γ) a
Tactic: rw [prod_apply, MeasureTheory.lintegral_prod_symm _ hg.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (c : β × γ), g c ∂Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) =
    ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂(κ : (a : α) → Measure β) a ∂(η : (a : α) → Measure γ) a
⊢ ∫⁻ (c : β × γ), g c ∂(κ ×ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂(κ : (a : α) → Measure β) a ∂(η : (a : α) → Measure γ) a
have rw₁ : ∫⁻ (y : γ), ∫⁻ (x : β), g (x, y) ∂(κ : (a : α) → Measure β) a ∂(η : (a : α) → Measure γ) a =
  ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂(κ : (a : α) → Measure β) a ∂(η : (a : α) → Measure γ) a
Tactic: rw [prod_apply, MeasureTheory.lintegral_prod_symm _ hg.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
κ : Kernel α γ
inst : IsSFiniteKernel κ
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (p : β × γ), g p ∂(deterministic f hf ×ₖ κ : (a : α) → Measure (β × γ)) a =
    ∫⁻ (c : γ), g (f a, c) ∂(κ : (a : α) → Measure γ) a
have rw : ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(κ : (a : α) → Measure γ) a ∂(deterministic f hf : (a : α) → Measure β) a =
  ∫⁻ (c : γ), g (f a, c) ∂(κ : (a : α) → Measure γ) a
Tactic: rw [lintegral_prod _ _ _ hg, lintegral_deterministic' _ hg.lintegral_prod_right']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
κ : Kernel α γ
inst : IsSFiniteKernel κ
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(κ : (a : α) → Measure γ) a ∂(deterministic f hf : (a : α) → Measure β) a =
    ∫⁻ (c : γ), g (f a, c) ∂(κ : (a : α) → Measure γ) a
⊢ ∫⁻ (p : β × γ), g p ∂(deterministic f hf ×ₖ κ : (a : α) → Measure (β × γ)) a =
    ∫⁻ (c : γ), g (f a, c) ∂(κ : (a : α) → Measure γ) a
have rw₁ : ∫⁻ (y : γ), g (f a, y) ∂(κ : (a : α) → Measure γ) a = ∫⁻ (c : γ), g (f a, c) ∂(κ : (a : α) → Measure γ) a
Tactic: rw [lintegral_prod _ _ _ hg, lintegral_deterministic' _ hg.lintegral_prod_right']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → γ
hf : Measurable f
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (p : β × γ), g p ∂(κ ×ₖ deterministic f hf : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), g (b, f a) ∂(κ : (a : α) → Measure β) a
have rw : ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂(κ : (a : α) → Measure β) a ∂(deterministic f hf : (a : α) → Measure γ) a =
  ∫⁻ (b : β), g (b, f a) ∂(κ : (a : α) → Measure β) a
Tactic: rw [lintegral_prod_symm _ _ _ hg, lintegral_deterministic' _ hg.lintegral_prod_left']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → γ
hf : Measurable f
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂(κ : (a : α) → Measure β) a ∂(deterministic f hf : (a : α) → Measure γ) a =
    ∫⁻ (b : β), g (b, f a) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (p : β × γ), g p ∂(κ ×ₖ deterministic f hf : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), g (b, f a) ∂(κ : (a : α) → Measure β) a
have rw₁ : ∫⁻ (x : β), g (x, f a) ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), g (b, f a) ∂(κ : (a : α) → Measure β) a
Tactic: rw [lintegral_prod_symm _ _ _ hg, lintegral_deterministic' _ hg.lintegral_prod_left']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
⊢ ∫⁻ (p : α × β), f p ∂(Kernel.id ×ₖ κ : (a : α) → Measure (α × β)) a =
    ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a
have rw : ∫⁻ (p : α × β), f p ∂(deterministic id sorry ×ₖ κ : (a : α) → Measure (α × β)) a =
  ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: rw [Kernel.id, lintegral_deterministic_prod _ _ _ hf, id_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
rw :
  ∫⁻ (p : α × β), f p ∂(deterministic id ⋯ ×ₖ κ : (a : α) → Measure (α × β)) a =
    ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (p : α × β), f p ∂(Kernel.id ×ₖ κ : (a : α) → Measure (α × β)) a =
    ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a
have rw₁ : ∫⁻ (c : β), f (id a, c) ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: rw [Kernel.id, lintegral_deterministic_prod _ _ _ hf, id_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
rw :
  ∫⁻ (p : α × β), f p ∂(deterministic id ⋯ ×ₖ κ : (a : α) → Measure (α × β)) a =
    ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a
rw₁ : ∫⁻ (c : β), f (id a, c) ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (p : α × β), f p ∂(Kernel.id ×ₖ κ : (a : α) → Measure (α × β)) a =
    ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a
have rw₂ : ∫⁻ (c : β), f (a, c) ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: rw [Kernel.id, lintegral_deterministic_prod _ _ _ hf, id_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel β α
inst : IsSFiniteKernel κ
b : β
⊢ ∫⁻ (p : α × β), f p ∂(κ ×ₖ Kernel.id : (a : β) → Measure (α × β)) b =
    ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b
have rw : ∫⁻ (p : α × β), f p ∂(κ ×ₖ deterministic id sorry : (a : β) → Measure (α × β)) b =
  ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b
Tactic: rw [Kernel.id, lintegral_prod_deterministic _ _ _ hf, id_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel β α
inst : IsSFiniteKernel κ
b : β
rw :
  ∫⁻ (p : α × β), f p ∂(κ ×ₖ deterministic id ⋯ : (a : β) → Measure (α × β)) b =
    ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b
⊢ ∫⁻ (p : α × β), f p ∂(κ ×ₖ Kernel.id : (a : β) → Measure (α × β)) b =
    ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b
have rw₁ : ∫⁻ (b_1 : α), f (b_1, id b) ∂(κ : (a : β) → Measure α) b = ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b
Tactic: rw [Kernel.id, lintegral_prod_deterministic _ _ _ hf, id_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel β α
inst : IsSFiniteKernel κ
b : β
rw :
  ∫⁻ (p : α × β), f p ∂(κ ×ₖ deterministic id ⋯ : (a : β) → Measure (α × β)) b =
    ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b
rw₁ : ∫⁻ (b_1 : α), f (b_1, id b) ∂(κ : (a : β) → Measure α) b = ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b
⊢ ∫⁻ (p : α × β), f p ∂(κ ×ₖ Kernel.id : (a : β) → Measure (α × β)) b =
    ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b
have rw₂ : ∫⁻ (b_1 : α), f (b_1, b) ∂(κ : (a : β) → Measure α) b = ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b
Tactic: rw [Kernel.id, lintegral_prod_deterministic _ _ _ hf, id_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((deterministic f mf ×ₖ κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
have hf : Measurable (β := ℝ≥0∞) fun (b : β) ↦ (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: rw [prod_apply' _ _ _ hs, lintegral_deterministic']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
s : Set (α × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.id ×ₖ κ : (a : α) → Measure (α × β)) a : Measure (α × β)) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((((deterministic id sorry ×ₖ κ : (a : α) → Measure (α × β)) a : Measure (α × β)) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
Tactic: rw [Kernel.id, deterministic_prod_apply' _ _ _ hs, id_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
s : Set (α × β)
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞)
    ((((deterministic id ⋯ ×ₖ κ : (a : α) → Measure (α × β)) a : Measure (α × β)) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.id ×ₖ κ : (a : α) → Measure (α × β)) a : Measure (α × β)) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk (id a) ⁻¹' s) : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
Tactic: rw [Kernel.id, deterministic_prod_apply' _ _ _ hs, id_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
s : Set (α × β)
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞)
    ((((deterministic id ⋯ ×ₖ κ : (a : α) → Measure (α × β)) a : Measure (α × β)) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk (id a) ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.id ×ₖ κ : (a : α) → Measure (α × β)) a : Measure (α × β)) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
Tactic: rw [Kernel.id, deterministic_prod_apply' _ _ _ hs, id_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (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 α β
h : IsZeroOrMarkovKernel κ
η : Kernel α γ
inst : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel (κ ×ₖ η)
have inl : ∀ [h : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
  IsZeroOrMarkovKernel (β := β × γ) (mβ := Prod.instMeasurableSpace) (0 ×ₖ η)
Tactic: rcases eq_zero_or_isMarkovKernel κ with rfl | h
Cleared hypotheses: κ, h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (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 α β
h : IsZeroOrMarkovKernel κ
η : Kernel α γ
inst : IsZeroOrMarkovKernel η
inl :
  ∀ [h : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    IsZeroOrMarkovKernel (β := β × γ) (mβ := Prod.instMeasurableSpace) (0 ×ₖ η)
⊢ IsZeroOrMarkovKernel (κ ×ₖ η)
have inr : ∀ (h : IsMarkovKernel κ), IsZeroOrMarkovKernel (κ ×ₖ η)
Tactic: rcases eq_zero_or_isMarkovKernel κ with rfl | h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (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 α β
h_1 : IsZeroOrMarkovKernel κ
η : Kernel α γ
inst : IsZeroOrMarkovKernel η
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ ×ₖ η)
have inr : ∀ [IsZeroOrMarkovKernel.{u_1, u_4} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0],
  IsZeroOrMarkovKernel (β := β × γ) (mβ := Prod.instMeasurableSpace) (κ ×ₖ 0)
Tactic: rcases eq_zero_or_isMarkovKernel η with rfl | h'
Cleared hypotheses: η, inst
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (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 α β
h_1 : IsZeroOrMarkovKernel κ
η : Kernel α γ
inst : IsZeroOrMarkovKernel η
h : IsMarkovKernel κ
inr :
  ∀ [IsZeroOrMarkovKernel.{u_1, u_4} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0],
    IsZeroOrMarkovKernel (β := β × γ) (mβ := Prod.instMeasurableSpace) (κ ×ₖ 0)
⊢ IsZeroOrMarkovKernel (κ ×ₖ η)
have inr₁ : ∀ (h' : IsMarkovKernel η), IsZeroOrMarkovKernel (κ ×ₖ η)
Tactic: rcases eq_zero_or_isMarkovKernel η with rfl | h'
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsMarkovKernel η
⊢ (κ ×ₖ η).fst = κ
have rw : (κ ∥ₖ η).fst ∘ₖ copy α = κ
Tactic: rw [prod, fst_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsMarkovKernel η
⊢ (κ ∥ₖ η).fst ∘ₖ copy α = κ
have h : ∀ (a : α),
  Eq.{u_2 + 1} (α := Measure β) (((κ ∥ₖ η).fst ∘ₖ copy α : (a : α) → Measure β) a : Measure β)
    ((κ : (a : α) → Measure β) a : Measure β)
Tactic: ext a : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsMarkovKernel η
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) (((κ ∥ₖ η).fst ∘ₖ copy α : (a : α) → Measure β) a : Measure β)
    ((κ : (a : α) → Measure β) a : Measure β)
have h : Eq.{u_2 + 1} (α := Measure β)
  (Measure.map (α := β × γ) Prod.fst
    (Measure.prod ((κ : (a : α) → Measure β) (a, a).1) ((η : (a : α) → Measure γ) (a, a).2)))
  ((κ : (a : α) → Measure β) a)
Tactic: rw [comp_apply, copy_apply, Measure.dirac_bind (by fun_prop), fst_apply, parallelComp_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsMarkovKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
⊢ (κ ×ₖ η).snd = η
have h : ∀ (x : α) (s : Set γ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) (((((κ ×ₖ η).snd : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst : IsSFiniteKernel κ
η : Kernel β δ
inst_1 : IsSFiniteKernel η
f : α → β
hf : Measurable f
⊢ (κ ×ₖ η).comap f hf = κ.comap f hf ×ₖ η.comap f hf
have h : ∀ (x : α),
  Eq (α := Measure (γ × δ)) (((κ ×ₖ η).comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst : IsSFiniteKernel κ
η : Kernel β δ
inst_1 : IsSFiniteKernel η
f : α → β
hf : Measurable f
x : α
⊢ Eq (α := Measure (γ × δ)) (((κ ×ₖ η).comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
have h : Eq (α := Measure (γ × δ)) ((κ ×ₖ η : (a : β) → Measure (γ × δ)) (f x) : Measure (γ × δ))
  ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
Tactic: rw [comap_apply, prod_apply, prod_apply, comap_apply, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst : IsSFiniteKernel κ
η : Kernel β δ
inst_1 : IsSFiniteKernel η
f : α → β
hf : Measurable f
x : α
h :
  Eq (α := Measure (γ × δ)) ((κ ×ₖ η : (a : β) → Measure (γ × δ)) (f x) : Measure (γ × δ))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
⊢ Eq (α := Measure (γ × δ)) (((κ ×ₖ η).comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
have h₁ : Eq (α := Measure (γ × δ)) (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η : (a : β) → Measure δ) (f x)))
  ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x)
Tactic: rw [comap_apply, prod_apply, prod_apply, comap_apply, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst : IsSFiniteKernel κ
η : Kernel β δ
inst_1 : IsSFiniteKernel η
f : α → β
hf : Measurable f
x : α
h :
  Eq (α := Measure (γ × δ)) ((κ ×ₖ η : (a : β) → Measure (γ × δ)) (f x) : Measure (γ × δ))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
h₁ :
  Eq (α := Measure (γ × δ)) (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η : (a : β) → Measure δ) (f x)))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x)
⊢ Eq (α := Measure (γ × δ)) (((κ ×ₖ η).comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
have h₂ : Eq (α := Measure (γ × δ)) (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η : (a : β) → Measure δ) (f x)))
  (Measure.prod ((κ.comap f hf : (a : α) → Measure γ) x) ((η.comap f hf : (a : α) → Measure δ) x))
Tactic: rw [comap_apply, prod_apply, prod_apply, comap_apply, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst : IsSFiniteKernel κ
η : Kernel β δ
inst_1 : IsSFiniteKernel η
f : α → β
hf : Measurable f
x : α
h :
  Eq (α := Measure (γ × δ)) ((κ ×ₖ η : (a : β) → Measure (γ × δ)) (f x) : Measure (γ × δ))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
h₁ :
  Eq (α := Measure (γ × δ)) (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η : (a : β) → Measure δ) (f x)))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x)
h₂ :
  Eq (α := Measure (γ × δ)) (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η : (a : β) → Measure δ) (f x)))
    (Measure.prod ((κ.comap f hf : (a : α) → Measure γ) x) ((η.comap f hf : (a : α) → Measure δ) x))
⊢ Eq (α := Measure (γ × δ)) (((κ ×ₖ η).comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
have h₃ : Eq (α := Measure (γ × δ)) (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η : (a : β) → Measure δ) (f x)))
  (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η.comap f hf : (a : α) → Measure δ) x))
Tactic: rw [comap_apply, prod_apply, prod_apply, comap_apply, comap_apply]