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 γ
s : Set (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
      (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)) 0
have rw : Measurable (β := ℝ≥0∞) fun (b : β) ↦
  (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: rw [Kernel.compProd_apply hs, lintegral_eq_zero_iff]
-- 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 (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
h :
  Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)) 0
have obtain : ∀ (t : Set (β × γ)) (hst : s ⊆ t) (mt : MeasurableSet t)
  (ht :
    Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
      (0 : ℝ≥0∞)),
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)) 0
Tactic: obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
h :
  Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (0 : ℝ≥0∞)
t : Set (β × γ)
hst : s ⊆ t
mt : MeasurableSet t
ht :
  Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)) 0
have ht₁ : (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
  (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' t)) 0
Tactic: simp_rw [compProd_null a mt] at ht
Cleared hypotheses: ht
-- 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 (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
h :
  Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (0 : ℝ≥0∞)
t : Set (β × γ)
hst : s ⊆ t
mt : MeasurableSet t
ht :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' t)) 0
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)) 0
have rw : (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)) 0 ∧
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞) 0 fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: rw [Filter.eventuallyLE_antisymm_iff]
-- 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 γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet (α := β × γ) {x : β × γ | p x}
h :
  ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ), p (b, c)
⊢ ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc
have pos : ∀ (hκ : IsSFiniteKernel κ), ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc
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 γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet (α := β × γ) {x : β × γ | p x}
h :
  ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ), p (b, c)
pos : ∀ (hκ : IsSFiniteKernel κ), ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc
⊢ ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc
have neg : ∀ (hκ : ¬IsSFiniteKernel κ), ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc
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 γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet (α := β × γ) {x : β × γ | p x}
h :
  ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ), p (b, c)
hκ : IsSFiniteKernel κ
⊢ ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc
have pos : ∀ (hη : IsSFiniteKernel η), ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc
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 γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet (α := β × γ) {x : β × γ | p x}
h :
  ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ), p (b, c)
hκ : IsSFiniteKernel κ
pos : ∀ (hη : IsSFiniteKernel η), ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc
⊢ ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc
have neg : ∀ (hη : ¬IsSFiniteKernel η), ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc
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 γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet (α := β × γ) {x : β × γ | p x}
h :
  ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ), p (b, c)
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc
have pos : ∀
  (h :
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
          {a_1 : β |
            ¬Eq (α := ℝ≥0∞)
                ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) {a : γ | ¬p (a_1, a)} :
                  ℝ≥0∞)
                (0 : ℝ≥0∞)} :
        ℝ≥0∞)
      (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {a : β × γ | ¬p a} : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: simp_rw [ae_iff] at h ⊢
Cleared hypotheses: 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 γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet (α := β × γ) {x : β × γ | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {a_1 : β |
          ¬Eq (α := ℝ≥0∞)
              ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) {a : γ | ¬p (a_1, a)} : ℝ≥0∞)
              (0 : ℝ≥0∞)} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {a : β × γ | ¬p a} : ℝ≥0∞)
    (0 : ℝ≥0∞)
have pos : (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
  (fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' {a : β × γ | ¬p a}))
  0
Tactic: rw [compProd_null]
-- 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 γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet (α := β × γ) {x : β × γ | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {a_1 : β |
          ¬Eq (α := ℝ≥0∞)
              ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) {a : γ | ¬p (a_1, a)} : ℝ≥0∞)
              (0 : ℝ≥0∞)} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
pos :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' {a : β × γ | ¬p a}))
    0
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {a : β × γ | ¬p a} : ℝ≥0∞)
    (0 : ℝ≥0∞)
have pos₁ : MeasurableSet (α := β × γ) {a : β × γ | ¬p a}
Tactic: rw [compProd_null]
-- 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 α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ κ.restrict (s := s) hs ⊗ₖ η.restrict (s := t) ht = (κ ⊗ₖ η).restrict (s := s ×ˢ t) ⋯
have h : ∀ (a : α) (u : Set (β × γ)) (hu : MeasurableSet u),
  Eq (α := ℝ≥0∞)
    ((((κ.restrict (s := s) hs ⊗ₖ η.restrict (s := t) ht : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        u :
      ℝ≥0∞)
    (((((κ ⊗ₖ η).restrict (s := s ×ˢ t) sorry : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        u :
      ℝ≥0∞)
Tactic: ext a u hu
-- 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 α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞)
    ((((κ.restrict (s := s) hs ⊗ₖ η.restrict (s := t) ht : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        u :
      ℝ≥0∞)
    (((((κ ⊗ₖ η).restrict (s := s ×ˢ t) ⋯ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        u :
      ℝ≥0∞)
have h : ∫⁻ (b : β),
    (((η.restrict (s := t) ht : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' u) ∂(κ.restrict (s := s) hs : (a : α) → Measure β) a =
  ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' (u ∩ s ×ˢ t)) ∂(κ : (a : α) → Measure β) a
Tactic: rw [compProd_apply hu, restrict_apply' _ _ _ hu, compProd_apply (hu.inter (hs.prod ht))]
-- 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 α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
⊢ ∫⁻ (b : β),
      (((η.restrict (s := t) ht : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' u) ∂(κ.restrict (s := s) hs : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' (u ∩ s ×ˢ t)) ∂(κ : (a : α) → Measure β) a
have h : ∫⁻ (b : β) in s,
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      ({x : γ | (b, x) ∈ u} ∩ t) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      {x : γ | (b, x) ∈ u ∧ b ∈ s ∧ x ∈ t} ∂(κ : (a : α) → Measure β) a
Tactic: simp only [restrict_apply, Set.preimage, Measure.restrict_apply' ht, Set.mem_inter_iff,
    Set.mem_prod]
-- 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 α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
      ℝ≥0∞)
    (if b ∈ s then (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t)
      else 0 :
      ℝ≥0∞)
have pos : ∀ (h : b ∈ s),
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t) : ℝ≥0∞)
Tactic: split_ifs with 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 α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
pos :
  ∀ (h : b ∈ s),
    Eq (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
        ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
      ℝ≥0∞)
    (if b ∈ s then (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t)
      else 0 :
      ℝ≥0∞)
have neg : ∀ (h : b ∉ s),
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: split_ifs with 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 α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
      ℝ≥0∞)
    (s.indicator
        (fun (b : β) ↦
          (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t))
        b :
      ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
    ℝ≥0∞)
  (if b ∈ s then (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t)
    else 0 :
    ℝ≥0∞)
Tactic: classical
    rw [Set.indicator_apply]
    split_ifs with h
    · simp only [h, true_and, Set.inter_def, Set.mem_setOf]
    · simp only [h, false_and, and_false, Set.setOf_false, measure_empty]
-- 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 α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
rw rw₁ rw₂ :
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
      ℝ≥0∞)
    (if b ∈ s then (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t)
      else 0 :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
      ℝ≥0∞)
    (s.indicator
        (fun (b : β) ↦
          (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t))
        b :
      ℝ≥0∞)
have pos : ∀ (h : b ∈ s),
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t) : ℝ≥0∞)
Tactic: classical
    rw [Set.indicator_apply]
    split_ifs with h
    · simp only [h, true_and, Set.inter_def, Set.mem_setOf]
    · simp only [h, false_and, and_false, Set.setOf_false, measure_empty]
-- 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 α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
rw rw₁ rw₂ :
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
      ℝ≥0∞)
    (if b ∈ s then (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t)
      else 0 :
      ℝ≥0∞)
pos :
  ∀ (h : b ∈ s),
    Eq (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
        ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
      ℝ≥0∞)
    (s.indicator
        (fun (b : β) ↦
          (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t))
        b :
      ℝ≥0∞)
have neg : ∀ (h : b ∉ s),
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: classical
    rw [Set.indicator_apply]
    split_ifs with h
    · simp only [h, true_and, Set.inter_def, Set.mem_setOf]
    · simp only [h, false_and, and_false, Set.setOf_false, measure_empty]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
⊢ ∫⁻ (b : β) in s,
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        ({x : γ | (b, x) ∈ u} ∩ t) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {x : γ | (b, x) ∈ u ∧ b ∈ s ∧ x ∈ t} ∂(κ : (a : α) → Measure β) a
have this : ∀ (b : β),
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
      ℝ≥0∞)
    (s.indicator
        (fun (b : β) ↦
          (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t))
        b :
      ℝ≥0∞)
Tactic: have (b : _) : η (a, b) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} =
      s.indicator (fun b => η (a, b) ({c : γ | (b, c) ∈ u} ∩ t)) b := by
    classical
    rw [Set.indicator_apply]
    split_ifs with h
    · simp only [h, true_and, Set.inter_def, Set.mem_setOf]
    · simp only [h, false_and, and_false, Set.setOf_false, measure_empty]
-- 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 α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
this :
  ∀ (b : β),
    Eq (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
        ℝ≥0∞)
      (s.indicator
          (fun (b : β) ↦
            (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t))
          b :
        ℝ≥0∞)
⊢ ∫⁻ (b : β) in s,
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        ({x : γ | (b, x) ∈ u} ∩ t) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {x : γ | (b, x) ∈ u ∧ b ∈ s ∧ x ∈ t} ∂(κ : (a : α) → Measure β) a
have h : ∫⁻ (b : β) in s,
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      ({x : γ | (b, x) ∈ u} ∩ t) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (b : β),
    s.indicator
      (fun (b : β) ↦
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t))
      b ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [this]