awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a_1 : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a_1, a) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s ×ˢ t) : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a_1, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) a : ℝ≥0∞)
have pos : ∀ (ha : a ∈ s),
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a_1, a) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s ×ˢ t) : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a_1, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) a : ℝ≥0∞)
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a_1 : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
pos :
  ∀ (ha : a ∈ s),
    Eq (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a_1, a) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s ×ˢ t) : ℝ≥0∞)
      (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a_1, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) a :
        ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a_1, a) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s ×ˢ t) : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a_1, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) a : ℝ≥0∞)
have neg : ∀ (ha : a ∉ s),
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a_1, a) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s ×ˢ t) : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a_1, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) a : ℝ≥0∞)
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst : IsSFiniteKernel η
inst_1 : IsSFiniteKernel η'
h :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
⊢ κ ⊗ₖ η = κ ⊗ₖ η'
have pos : ∀ (hκ : IsSFiniteKernel κ), κ ⊗ₖ η = κ ⊗ₖ η'
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst : IsSFiniteKernel η
inst_1 : IsSFiniteKernel η'
h :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
pos : ∀ (hκ : IsSFiniteKernel κ), κ ⊗ₖ η = κ ⊗ₖ η'
⊢ κ ⊗ₖ η = κ ⊗ₖ η'
have neg : ∀ (hκ : ¬IsSFiniteKernel κ), κ ⊗ₖ η = κ ⊗ₖ η'
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst : IsSFiniteKernel η
inst_1 : IsSFiniteKernel η'
h :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
hκ : IsSFiniteKernel κ
⊢ κ ⊗ₖ η = κ ⊗ₖ η'
have pos : ∀ (a : α) (s : Set (β × γ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ ⊗ₖ η' : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst : IsSFiniteKernel η
inst_1 : IsSFiniteKernel η'
h :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ ⊗ₖ η' : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (b : β),
    (((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
Tactic: rw [compProd_apply hs, compProd_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst : IsSFiniteKernel η
inst_1 : IsSFiniteKernel η'
h :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
have pos : (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
  (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))
  fun (b : β) ↦ (((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst : IsSFiniteKernel η
inst_1 : IsSFiniteKernel η'
h :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
b : β
hb :
  Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
    ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
    ((((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
  ((((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
Tactic: rw [hb]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst : IsSFiniteKernel η
inst_1 : IsSFiniteKernel η'
h :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))
    fun (b : β) ↦ (((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
have h₁ : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (b : β) ↦
                Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
                  ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ))
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                Eq (α := ℝ≥0∞)
                  ((fun (b : β) ↦
                      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) :
                        ℝ≥0∞))
                    x)
                  ((fun (b : β) ↦
                      ((((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) :
                        ℝ≥0∞))
                    x))
              x}
          x}
    a_1
Tactic: filter_upwards [h a] with b hb using by rw [hb]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst : IsSFiniteKernel η
inst_1 : IsSFiniteKernel η'
h :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
h₁ :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
                    ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq (α := ℝ≥0∞)
                    ((fun (b : β) ↦
                        ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) :
                          ℝ≥0∞))
                      x)
                    ((fun (b : β) ↦
                        ((((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) :
                          ℝ≥0∞))
                      x))
                x}
            x}
      a_1
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))
    fun (b : β) ↦ (((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
have h₂ : ∀ (a_1 : β),
  Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ)
      ((η' : (a : α × β) → Measure γ) (a, a_1) : Measure γ) →
    Eq (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' s) : ℝ≥0∞)
      ((((η' : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' s) : ℝ≥0∞)
Tactic: filter_upwards [h a] with b hb using by rw [hb]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
⊢ 0 ⊗ₖ κ = 0
have pos : ∀ (h : IsSFiniteKernel κ), 0 ⊗ₖ κ = 0
Tactic: by_cases h : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
pos : ∀ (h : IsSFiniteKernel κ), 0 ⊗ₖ κ = 0
⊢ 0 ⊗ₖ κ = 0
have neg : ∀ (h : ¬IsSFiniteKernel κ), 0 ⊗ₖ κ = 0
Tactic: by_cases h : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : IsSFiniteKernel κ
⊢ 0 ⊗ₖ κ = 0
have pos : ∀ (a : α) (s : Set (β × γ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((0 ⊗ₖ κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((0 ⊗ₖ κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∫⁻ (b : β),
    (((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂((0 : Kernel α β) : (a : α) → Measure β) a =
  (((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s
Tactic: rw [Kernel.compProd_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : ¬IsSFiniteKernel κ
⊢ 0 ⊗ₖ κ = 0
have neg : Eq (α := Kernel α (β × γ)) 0 0
Tactic: rw [Kernel.compProd_of_not_isSFiniteKernel_right _ _ h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
⊢ Eq (α := Kernel α (β × γ)) (κ ⊗ₖ 0) 0
have pos : ∀ (h : IsSFiniteKernel κ), Eq (α := Kernel α (β × γ)) (κ ⊗ₖ 0) 0
Tactic: by_cases h : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
pos : ∀ (h : IsSFiniteKernel κ), Eq (α := Kernel α (β × γ)) (κ ⊗ₖ 0) 0
⊢ Eq (α := Kernel α (β × γ)) (κ ⊗ₖ 0) 0
have neg : ∀ (h : ¬IsSFiniteKernel κ), Eq (α := Kernel α (β × γ)) (κ ⊗ₖ 0) 0
Tactic: by_cases h : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
h : IsSFiniteKernel κ
⊢ Eq (α := Kernel α (β × γ)) (κ ⊗ₖ 0) 0
have pos : ∀ (a : α) (s : Set (β × γ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((κ ⊗ₖ 0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ ⊗ₖ 0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∫⁻ (b : β),
    (((0 : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
  (((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s
Tactic: rw [Kernel.compProd_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
h : ¬IsSFiniteKernel κ
⊢ Eq (α := Kernel α (β × γ)) (κ ⊗ₖ 0) 0
have neg : Eq (α := Kernel α (β × γ)) 0 0
Tactic: rw [Kernel.compProd_of_not_isSFiniteKernel_left _ _ h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
⊢ κ ⊗ₖ η = 0 ↔
    ∀ (a : α),
      ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)
have refine_1 : ∀ (h : κ ⊗ₖ η = 0) (a : α),
  ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
refine_1 :
  ∀ (h : κ ⊗ₖ η = 0) (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)
⊢ κ ⊗ₖ η = 0 ↔
    ∀ (a : α),
      ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)
have refine_2 : ∀
  (h :
    ∀ (a : α),
      ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)),
  κ ⊗ₖ η = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
⊢ ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)
have refine_1 : ∀ (a : α),
  ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (0 : ℝ≥0∞)
Tactic: simp_rw [← Measure.measure_univ_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
⊢ ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        (0 : ℝ≥0∞)
have refine_1 : ∀ (a : α),
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ
Tactic: refine fun a ↦ (lintegral_eq_zero_iff ?_).mp ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
refine_1 :
  ∀ (a : α),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ
⊢ ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        (0 : ℝ≥0∞)
have refine_1₁ : ∀ (a : α),
  ∫⁻ (a_1 : β),
      (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        Set.univ ∂(κ : (a : α) → Measure β) a =
    0
Tactic: refine fun a ↦ (lintegral_eq_zero_iff ?_).mp ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ ∫⁻ (a_1 : β),
      (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        Set.univ ∂(κ : (a : α) → Measure β) a =
    0
have refine_1 : Eq (α := ℝ≥0∞)
  ((((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
      (SProd.sprod (α := Set β) (β := Set γ) Set.univ Set.univ) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rw [← setLIntegral_univ, ← Kernel.compProd_apply_prod .univ .univ, h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
h :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)
⊢ κ ⊗ₖ η = 0
have refine_2 : κ ⊗ₖ η = κ ⊗ₖ 0
Tactic: rw [← Kernel.compProd_zero_right κ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
x : α
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have simp_rw : ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      {x : γ | b ∈ s} ∂(κ : (a : α) → Measure β) x =
  (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
Tactic: simp_rw [compProd_apply (measurable_fst hs), ← Set.preimage_comp, Prod.fst_comp_mk, Set.preimage,
    Function.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
x : α
b : β
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
    (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)
have pos : ∀ (hb : b ∈ s),
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
    (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)
Tactic: by_cases hb : b ∈ s