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
δ : 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))
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))
⊢ 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)) ((η : (a : β) → Measure δ) (f 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 δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α δ
inst_1 : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
⊢ Eq (α := Kernel α (γ × ε)) (κ.map f ×ₖ η.map g) ((κ ×ₖ η).map (Prod.map f g))
have h : ∀ (x : α),
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (((κ ×ₖ η).map (Prod.map f g) : (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 δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α δ
inst_1 : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
⊢ Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (((κ ×ₖ η).map (Prod.map f g) : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
have h : Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
  (Measure.map (Prod.map f g) ((κ ×ₖ η : (a : α) → Measure (β × δ)) x) : Measure (γ × ε))
Tactic: rw [map_apply _ (hf.prodMap hg), prod_apply κ, ← Measure.map_prod_map _ _ hf hg, prod_apply,
    map_apply _ hf, map_apply _ hg]
-- 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 δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α δ
inst_1 : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
h :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.map (Prod.map f g) ((κ ×ₖ η : (a : α) → Measure (β × δ)) x) : Measure (γ × ε))
⊢ Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (((κ ×ₖ η).map (Prod.map f g) : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
have h₁ : Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
  (Measure.map (Prod.map f g) (Measure.prod ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure δ) x)) :
    Measure (γ × ε))
Tactic: rw [map_apply _ (hf.prodMap hg), prod_apply κ, ← Measure.map_prod_map _ _ hf hg, prod_apply,
    map_apply _ hf, map_apply _ hg]
-- 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 δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α δ
inst_1 : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
h :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.map (Prod.map f g) ((κ ×ₖ η : (a : α) → Measure (β × δ)) x) : Measure (γ × ε))
h₁ :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.map (Prod.map f g) (Measure.prod ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure δ) x)) :
      Measure (γ × ε))
⊢ Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (((κ ×ₖ η).map (Prod.map f g) : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
have h₂ : Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
  (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)) :
    Measure (γ × ε))
Tactic: rw [map_apply _ (hf.prodMap hg), prod_apply κ, ← Measure.map_prod_map _ _ hf hg, prod_apply,
    map_apply _ hf, map_apply _ hg]
-- 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 δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α δ
inst_1 : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
h :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.map (Prod.map f g) ((κ ×ₖ η : (a : α) → Measure (β × δ)) x) : Measure (γ × ε))
h₁ :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.map (Prod.map f g) (Measure.prod ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure δ) x)) :
      Measure (γ × ε))
h₂ :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)) :
      Measure (γ × ε))
⊢ Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (((κ ×ₖ η).map (Prod.map f g) : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
have h₃ : Eq (α := Measure (γ × ε))
  (Measure.prod (((κ.map f : Kernel α γ) : (a : α) → Measure γ) x) (((η.map g : Kernel α ε) : (a : α) → Measure ε) x))
  (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)))
Tactic: rw [map_apply _ (hf.prodMap hg), prod_apply κ, ← Measure.map_prod_map _ _ hf hg, prod_apply,
    map_apply _ hf, map_apply _ hg]
-- 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 δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α δ
inst_1 : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
h :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.map (Prod.map f g) ((κ ×ₖ η : (a : α) → Measure (β × δ)) x) : Measure (γ × ε))
h₁ :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.map (Prod.map f g) (Measure.prod ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure δ) x)) :
      Measure (γ × ε))
h₂ :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)) :
      Measure (γ × ε))
h₃ :
  Eq (α := Measure (γ × ε))
    (Measure.prod (((κ.map f : Kernel α γ) : (a : α) → Measure γ) x) (((η.map g : Kernel α ε) : (a : α) → Measure ε) x))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)))
⊢ Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (((κ ×ₖ η).map (Prod.map f g) : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
have h₄ : Eq (α := Measure (γ × ε))
  (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (((η.map g : Kernel α ε) : (a : α) → Measure ε) x))
  (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)))
Tactic: rw [map_apply _ (hf.prodMap hg), prod_apply κ, ← Measure.map_prod_map _ _ hf hg, prod_apply,
    map_apply _ hf, map_apply _ hg]
-- 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 δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α δ
inst_1 : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
h :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.map (Prod.map f g) ((κ ×ₖ η : (a : α) → Measure (β × δ)) x) : Measure (γ × ε))
h₁ :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.map (Prod.map f g) (Measure.prod ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure δ) x)) :
      Measure (γ × ε))
h₂ :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)) :
      Measure (γ × ε))
h₃ :
  Eq (α := Measure (γ × ε))
    (Measure.prod (((κ.map f : Kernel α γ) : (a : α) → Measure γ) x) (((η.map g : Kernel α ε) : (a : α) → Measure ε) x))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)))
h₄ :
  Eq (α := Measure (γ × ε))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (((η.map g : Kernel α ε) : (a : α) → Measure ε) x))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)))
⊢ Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (((κ ×ₖ η).map (Prod.map f g) : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
have h₅ : Eq (α := Measure (γ × ε))
  (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)))
  (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)))
Tactic: rw [map_apply _ (hf.prodMap hg), prod_apply κ, ← Measure.map_prod_map _ _ hf hg, prod_apply,
    map_apply _ hf, map_apply _ hg]
-- 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
⊢ Eq (α := Kernel α (δ × γ)) (κ.map f ×ₖ η) ((κ ×ₖ η).map (Prod.map f id))
have rw : Eq (α := Kernel α (δ × γ)) (κ.map f ×ₖ η) (κ.map f ×ₖ η.map id)
Tactic: rw [← map_prod_map _ _ hf measurable_id, map_id]
-- 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
rw : Eq (α := Kernel α (δ × γ)) (κ.map f ×ₖ η) (κ.map f ×ₖ η.map id)
⊢ Eq (α := Kernel α (δ × γ)) (κ.map f ×ₖ η) ((κ ×ₖ η).map (Prod.map f id))
have rw₁ : Eq (α := Kernel α (δ × γ)) (κ.map f ×ₖ η) (κ.map f ×ₖ η)
Tactic: rw [← map_prod_map _ _ hf measurable_id, map_id]
-- 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 α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
⊢ (prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯ = (prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap
have rw : ∀ (a : α × γ) (f : δ × β → ℝ≥0∞),
  Measurable f →
    ∫⁻ (b : δ × β), f b ∂((prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap sorry : (a : α × γ) → Measure (δ × β)) a =
      ∫⁻ (b : δ × β), f b ∂((prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap : (a : α × γ) → Measure (δ × β)) a
Tactic: rw [ext_fun_iff]
-- 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 α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ × β), f b ∂((prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯ : (a : α × γ) → Measure (δ × β)) x =
    ∫⁻ (b : δ × β), f b ∂((prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap : (a : α × γ) → Measure (δ × β)) x
have rw : ∫⁻ (b : δ),
    ∫⁻ (c : β),
      f (b, c) ∂(prodMkLeft γ κ : (a : γ × α) → Measure β) x.swap ∂(prodMkRight α η : (a : γ × α) → Measure δ) x.swap =
  ∫⁻ (b : β),
    ∫⁻ (c : δ),
      f (b, c).swap ∂(prodMkLeft α η : (a : α × γ) → Measure δ) x ∂(prodMkRight γ κ : (a : α × γ) → Measure β) x
Tactic: rw [lintegral_comap, lintegral_map _ measurable_swap _ hf, lintegral_prod _ _ _ hf,
    lintegral_prod]
-- 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 α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
rw :
  ∫⁻ (b : δ),
      ∫⁻ (c : β),
        f
          (b,
            c) ∂(prodMkLeft γ κ : (a : γ × α) → Measure β) x.swap ∂(prodMkRight α η : (a : γ × α) → Measure δ) x.swap =
    ∫⁻ (b : β),
      ∫⁻ (c : δ),
        f (b, c).swap ∂(prodMkLeft α η : (a : α × γ) → Measure δ) x ∂(prodMkRight γ κ : (a : α × γ) → Measure β) x
⊢ ∫⁻ (b : δ × β), f b ∂((prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯ : (a : α × γ) → Measure (δ × β)) x =
    ∫⁻ (b : δ × β), f b ∂((prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap : (a : α × γ) → Measure (δ × β)) x
have hg : Measurable (β := ℝ≥0∞) fun (a : β × δ) ↦ f a.swap
Tactic: rw [lintegral_comap, lintegral_map _ measurable_swap _ hf, lintegral_prod _ _ _ hf,
    lintegral_prod]
-- 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 α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ),
      ∫⁻ (c : β),
        f
          (b,
            c) ∂(prodMkLeft γ κ : (a : γ × α) → Measure β) x.swap ∂(prodMkRight α η : (a : γ × α) → Measure δ) x.swap =
    ∫⁻ (b : β),
      ∫⁻ (c : δ),
        f (b, c).swap ∂(prodMkLeft α η : (a : α × γ) → Measure δ) x ∂(prodMkRight γ κ : (a : α × γ) → Measure β) x
have simp : ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(κ : (a : α) → Measure β) x.1 ∂(η : (a : γ) → Measure δ) x.2 =
  ∫⁻ (b : β), ∫⁻ (c : δ), f (c, b) ∂(η : (a : γ) → Measure δ) x.2 ∂(κ : (a : α) → Measure β) x.1
Tactic: simp only [prodMkRight_apply, Prod.fst_swap, Prod.swap_prod_mk, lintegral_prodMkLeft,
    Prod.snd_swap]
-- 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 α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(κ : (a : α) → Measure β) x.1 ∂(η : (a : γ) → Measure δ) x.2 =
    ∫⁻ (b : β), ∫⁻ (c : δ), f (c, b) ∂(η : (a : γ) → Measure δ) x.2 ∂(κ : (a : α) → Measure β) x.1
have refine : AEMeasurable (α := β × δ) (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace) (Function.uncurry fun (c : β) (b : δ) ↦ f (b, c))
  (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2))
Tactic: refine (lintegral_lintegral_swap ?_).symm
-- 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 α β
η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
⊢ (κ ×ₖ η).map Prod.swap = η ×ₖ κ
have rw : ∀ (a : α) (f : γ × β → ℝ≥0∞),
  Measurable f →
    ∫⁻ (b : γ × β), f b ∂((κ ×ₖ η).map Prod.swap : (a : α) → Measure (γ × β)) a =
      ∫⁻ (b : γ × β), f b ∂(η ×ₖ κ : (a : α) → Measure (γ × β)) a
Tactic: rw [ext_fun_iff]
-- 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 α β
η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : γ × β), f b ∂((κ ×ₖ η).map Prod.swap : (a : α) → Measure (γ × β)) x =
    ∫⁻ (b : γ × β), f b ∂(η ×ₖ κ : (a : α) → Measure (γ × β)) x
have rw : ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c).swap ∂(η : (a : α) → Measure γ) x ∂(κ : (a : α) → Measure β) x =
  ∫⁻ (b : γ), ∫⁻ (c : β), f (b, c) ∂(κ : (a : α) → Measure β) x ∂(η : (a : α) → Measure γ) x
Tactic: rw [lintegral_map _ measurable_swap _ hf, lintegral_prod, lintegral_prod _ _ _ hf]
-- 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 α β
η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
rw :
  ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c).swap ∂(η : (a : α) → Measure γ) x ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : γ), ∫⁻ (c : β), f (b, c) ∂(κ : (a : α) → Measure β) x ∂(η : (a : α) → Measure γ) x
⊢ ∫⁻ (b : γ × β), f b ∂((κ ×ₖ η).map Prod.swap : (a : α) → Measure (γ × β)) x =
    ∫⁻ (b : γ × β), f b ∂(η ×ₖ κ : (a : α) → Measure (γ × β)) x
have hg : Measurable (β := ℝ≥0∞) fun (a : β × γ) ↦ f a.swap
Tactic: rw [lintegral_map _ measurable_swap _ hf, lintegral_prod, lintegral_prod _ _ _ hf]
-- 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 α β
η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c).swap ∂(η : (a : α) → Measure γ) x ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : γ), ∫⁻ (c : β), f (b, c) ∂(κ : (a : α) → Measure β) x ∂(η : (a : α) → Measure γ) x
have refine : AEMeasurable (α := γ × β) (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
  (Function.uncurry fun (c : γ) (b : β) ↦ f (b, c).swap)
  (Measure.prod ((η : (a : α) → Measure γ) x) ((κ : (a : α) → Measure β) x))
Tactic: refine (lintegral_lintegral_swap ?_).symm
-- 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 η
⊢ swap β γ ∘ₖ (κ ×ₖ η) = η ×ₖ κ
have rw : (κ ×ₖ η).map Prod.swap = η ×ₖ κ
Tactic: rw [swap_comp_eq_map, map_prod_swap]
-- 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 η
rw : (κ ×ₖ η).map Prod.swap = η ×ₖ κ
⊢ swap β γ ∘ₖ (κ ×ₖ η) = η ×ₖ κ
have rw₁ : η ×ₖ κ = η ×ₖ κ
Tactic: rw [swap_comp_eq_map, map_prod_swap]
-- 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 : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
⊢ deterministic f hf ×ₖ deterministic g hg = deterministic (fun (a : α) ↦ (f a, g a)) ⋯
have h : ∀ (a : α) (s : Set (β × γ)),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((deterministic f hf ×ₖ deterministic g hg : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
            (a : Set (β × γ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((deterministic (fun (a : α) ↦ (f a, g a)) sorry : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
            (a : Set (β × γ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
Tactic: ext
-- 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 : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
a : α
s : Set (β × γ)
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((deterministic f hf ×ₖ deterministic g hg : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((deterministic (fun (a : α) ↦ (f a, g a)) ⋯ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  ((Measure.prod ((deterministic f hf : (a : α) → Measure β) a) ((deterministic g hg : (a : α) → Measure γ) a) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((((deterministic (fun (a : α) ↦ (f a, g a)) sorry : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: simp_rw [prod_apply, deterministic_apply, Measure.dirac_prod_dirac]
-- 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 : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
a : α
s : Set (β × γ)
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((Measure.prod ((deterministic f hf : (a : α) → Measure β) a) ((deterministic g hg : (a : α) → Measure γ) a) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((deterministic (fun (a : α) ↦ (f a, g a)) ⋯ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((deterministic f hf ×ₖ deterministic g hg : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((deterministic (fun (a : α) ↦ (f a, g a)) ⋯ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((Measure.prod (Measure.dirac (f a)) (Measure.dirac (g a)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
  ((Measure.dirac (f a, g a) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [prod_apply, deterministic_apply, Measure.dirac_prod_dirac]