awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
hμ : SFinite μ
pos :
  bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) =
    μ ⊗ₘ (η ∘ₖ κ)
pos₁ :
  Eq (α := Measure (α × γ))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)))
    ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
pos₂ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∥ₖ η ∘ₖ (Kernel.id ×ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
    ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
⊢ (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
have pos₃ : Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∘ₖ Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
  ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
Tactic: rw [Measure.compProd_eq_comp_prod, Measure.compProd_eq_comp_prod, Measure.comp_assoc,
    Kernel.parallelComp_comp_prod, Kernel.id_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
hμ : SFinite μ
pos :
  bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) =
    μ ⊗ₘ (η ∘ₖ κ)
pos₁ :
  Eq (α := Measure (α × γ))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)))
    ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
pos₂ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∥ₖ η ∘ₖ (Kernel.id ×ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
    ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
pos₃ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∘ₖ Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
    ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
⊢ (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
have pos₄ : Eq (α := Measure (α × γ)) ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
  ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
Tactic: rw [Measure.compProd_eq_comp_prod, Measure.compProd_eq_comp_prod, Measure.comp_assoc,
    Kernel.parallelComp_comp_prod, Kernel.id_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
⊢ Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
have rw : Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
  ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.id ×ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
Tactic: rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
      Kernel.id_comp, Kernel.deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
rw :
  Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.id ×ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
⊢ Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
have rw₁ : Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
  ((⇑(Kernel.id ∘ₖ Kernel.id ×ₖ (Kernel.deterministic f hf ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
Tactic: rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
      Kernel.id_comp, Kernel.deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
rw :
  Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.id ×ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
rw₁ :
  Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    ((⇑(Kernel.id ∘ₖ Kernel.id ×ₖ (Kernel.deterministic f hf ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
⊢ Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
have rw₂ : Eq (α := Measure (α × γ)) ((⇑(Kernel.id ×ₖ κ.map f) : (a : α) → Measure (α × γ)) ∘ₘ μ)
  ((⇑(Kernel.id ∘ₖ Kernel.id ×ₖ (Kernel.deterministic f hf ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
Tactic: rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
      Kernel.id_comp, Kernel.deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
rw :
  Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.id ×ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
rw₁ :
  Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    ((⇑(Kernel.id ∘ₖ Kernel.id ×ₖ (Kernel.deterministic f hf ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
rw₂ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ×ₖ κ.map f) : (a : α) → Measure (α × γ)) ∘ₘ μ)
    ((⇑(Kernel.id ∘ₖ Kernel.id ×ₖ (Kernel.deterministic f hf ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
⊢ Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
have rw₃ : Eq (α := Measure (α × γ)) ((⇑(Kernel.id ×ₖ κ.map f) : (a : α) → Measure (α × γ)) ∘ₘ μ)
  ((⇑(Kernel.id ×ₖ (Kernel.deterministic f hf ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
Tactic: rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
      Kernel.id_comp, Kernel.deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
rw :
  Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.id ×ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
rw₁ :
  Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    ((⇑(Kernel.id ∘ₖ Kernel.id ×ₖ (Kernel.deterministic f hf ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
rw₂ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ×ₖ κ.map f) : (a : α) → Measure (α × γ)) ∘ₘ μ)
    ((⇑(Kernel.id ∘ₖ Kernel.id ×ₖ (Kernel.deterministic f hf ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
rw₃ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ×ₖ κ.map f) : (a : α) → Measure (α × γ)) ∘ₘ μ)
    ((⇑(Kernel.id ×ₖ (Kernel.deterministic f hf ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
⊢ Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
have rw₄ : Eq (α := Measure (α × γ)) ((⇑(Kernel.id ×ₖ κ.map f) : (a : α) → Measure (α × γ)) ∘ₘ μ)
  ((⇑(Kernel.id ×ₖ κ.map f) : (a : α) → Measure (α × γ)) ∘ₘ μ)
Tactic: rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
      Kernel.id_comp, Kernel.deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
⊢ Eq (α := Measure (α × γ))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
    ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
have rw : Eq (α := Measure (α × γ))
  (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
    (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
  (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
    (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
Tactic: rw [compProd_eq_comp_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
⊢ Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
    (map (Prod.map id f) (μ ⊗ₘ κ))
have rw : Eq (α := Measure (α × γ))
  ((⇑(Kernel.deterministic id sorry ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
  (map (Prod.map id f) (μ ⊗ₘ κ))
Tactic: rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
rw :
  Eq (α := Measure (α × γ))
    ((⇑(Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
    (map (Prod.map id f) (μ ⊗ₘ κ))
⊢ Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
    (map (Prod.map id f) (μ ⊗ₘ κ))
have rw₁ : Eq (α := Measure (α × γ)) ((⇑(Kernel.deterministic (Prod.map id f) sorry) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
  (map (Prod.map id f) (μ ⊗ₘ κ))
Tactic: rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
rw :
  Eq (α := Measure (α × γ))
    ((⇑(Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
    (map (Prod.map id f) (μ ⊗ₘ κ))
rw₁ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.deterministic (Prod.map id f) ⋯) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
    (map (Prod.map id f) (μ ⊗ₘ κ))
⊢ Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
    (map (Prod.map id f) (μ ⊗ₘ κ))
have rw₂ : Eq (α := Measure (α × γ)) (map (Prod.map id f) (μ ⊗ₘ κ)) (map (Prod.map id f) (μ ⊗ₘ κ))
Tactic: rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
⊢ Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f) (map (Prod.map id f) (μ ⊗ₘ κ))
have calc : Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
  (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
    (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
Tactic: calc μ ⊗ₘ (κ.map f)
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ×ₖ κ) ∘ₘ μ := by
    rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
      Kernel.id_comp, Kernel.deterministic_comp_eq_map]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_eq_comp_prod]
  _ = (μ ⊗ₘ κ).map (Prod.map id f) := by
    rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
calc :
  Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
⊢ Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f) (map (Prod.map id f) (μ ⊗ₘ κ))
have calc₁ : Eq (α := Measure (α × γ))
  (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
    (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
  ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
Tactic: calc μ ⊗ₘ (κ.map f)
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ×ₖ κ) ∘ₘ μ := by
    rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
      Kernel.id_comp, Kernel.deterministic_comp_eq_map]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_eq_comp_prod]
  _ = (μ ⊗ₘ κ).map (Prod.map id f) := by
    rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
calc :
  Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
calc₁ :
  Eq (α := Measure (α × γ))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
    ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
⊢ Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f) (map (Prod.map id f) (μ ⊗ₘ κ))
have calc₂ : Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
  (map (Prod.map id f) (μ ⊗ₘ κ))
Tactic: calc μ ⊗ₘ (κ.map f)
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ×ₖ κ) ∘ₘ μ := by
    rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
      Kernel.id_comp, Kernel.deterministic_comp_eq_map]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_eq_comp_prod]
  _ = (μ ⊗ₘ κ).map (Prod.map id f) := by
    rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map]
-- 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
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((Measure.map f ((κ : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [map_apply _ hf, Measure.map_apply hf hs]
-- 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
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((Measure.map f ((κ : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [map_apply _ hf, Measure.map_apply hf hs]
-- 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 α β
f : β → γ
hf : Measurable f
g : γ → δ
hg : Measurable g
⊢ Eq (α := Kernel α δ) (κ.map (g ∘ f)) (map (mβ := mγ) (κ.map f) g)
have h : ∀ (x : α),
  Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (((map (mβ := mγ) (κ.map f) g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
Tactic: ext1 x
-- 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 α β
f : β → γ
hf : Measurable f
g : γ → δ
hg : Measurable g
x : α
⊢ Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (((map (mβ := mγ) (κ.map f) g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
have h : Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
  (Measure.map g (((κ.map f : Kernel α γ) : (a : α) → Measure γ) x) : Measure δ)
Tactic: rw [map_apply _ hg, map_apply _ hf, Measure.map_map hg hf, ← map_apply _ (hg.comp hf)]
-- 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 α β
f : β → γ
hf : Measurable f
g : γ → δ
hg : Measurable g
x : α
h :
  Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (Measure.map g (((κ.map f : Kernel α γ) : (a : α) → Measure γ) x) : Measure δ)
⊢ Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (((map (mβ := mγ) (κ.map f) g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
have h₁ : Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
  (Measure.map g (Measure.map f ((κ : (a : α) → Measure β) x)) : Measure δ)
Tactic: rw [map_apply _ hg, map_apply _ hf, Measure.map_map hg hf, ← map_apply _ (hg.comp hf)]
-- 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 α β
f : β → γ
hf : Measurable f
g : γ → δ
hg : Measurable g
x : α
h :
  Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (Measure.map g (((κ.map f : Kernel α γ) : (a : α) → Measure γ) x) : Measure δ)
h₁ :
  Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (Measure.map g (Measure.map f ((κ : (a : α) → Measure β) x)) : Measure δ)
⊢ Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (((map (mβ := mγ) (κ.map f) g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
have h₂ : Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
  (Measure.map (g ∘ f) ((κ : (a : α) → Measure β) x) : Measure δ)
Tactic: rw [map_apply _ hg, map_apply _ hf, Measure.map_map hg hf, ← map_apply _ (hg.comp hf)]
-- 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 α β
f : β → γ
hf : Measurable f
g : γ → δ
hg : Measurable g
x : α
h :
  Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (Measure.map g (((κ.map f : Kernel α γ) : (a : α) → Measure γ) x) : Measure δ)
h₁ :
  Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (Measure.map g (Measure.map f ((κ : (a : α) → Measure β) x)) : Measure δ)
h₂ :
  Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (Measure.map (g ∘ f) ((κ : (a : α) → Measure β) x) : Measure δ)
⊢ Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (((map (mβ := mγ) (κ.map f) g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
have h₃ : Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
  (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
Tactic: rw [map_apply _ hg, map_apply _ hf, Measure.map_map hg hf, ← map_apply _ (hg.comp hf)]
-- 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
mγ : MeasurableSpace γ
f : β → γ
⊢ Eq (α := Kernel α γ) (map (mβ := mβ) 0 f) 0
have h : ∀ (a : α) (s : Set γ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((map (mβ := mβ) 0 f : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      (((((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- 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
mγ : MeasurableSpace γ
f : β → γ
a : α
s : Set γ
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((map (mβ := mβ) 0 f : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∀ (hf : Measurable f),
  Eq (α := ℝ≥0∞) ((((map (mβ := mβ) 0 f : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: by_cases hf : Measurable f