awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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
neg : ∀ (hη : ¬IsSFiniteKernel η), ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc
⊢ ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc

Tactic:
by_cases hη : IsSFiniteKernel η

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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

Tactic:
simp [compProd_of_not_isSFiniteKernel_right _ _ hη]

Premises used: ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 η
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∞)
⊢ ∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc

Tactic:
simp_rw [ae_iff] at h ⊢

Premises used: MeasureTheory.ae_iff
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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
pos₁ : MeasurableSet (α := β × γ) {a : β × γ | ¬p a}
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {a : β × γ | ¬p a} : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [compProd_null]

Premises used: ProbabilityTheory.Kernel.compProd_null
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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∞)
⊢ (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:
h

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, Set.preimage, Not
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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∞)
⊢ (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:
exact h
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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∞)
⊢ MeasurableSet (α := β × γ) {a : β × γ | ¬p a}

Tactic:
hp.compl

Premises used: Set.Mem, setOf, MeasurableSet.compl
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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∞)
⊢ MeasurableSet (α := β × γ) {a : β × γ | ¬p a}

Tactic:
exact hp.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
p : β × γ → Prop
hp : MeasurableSet (α := β × γ) {x : β × γ | p x}
⊢ (∀ᵐ (bc : β × γ) ∂((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)), p bc) ↔
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ), p (b, c)

Tactic:
⟨fun h ↦ ae_ae_of_ae_compProd h, fun h ↦ ae_compProd_of_ae_ae hp h⟩

Premises used: ProbabilityTheory.Kernel.ae_compProd_of_ae_ae, ProbabilityTheory.Kernel.ae_ae_of_ae_compProd, Iff.intro
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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
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) ⋯ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
            (a : Set (β × γ)) → ℝ≥0∞)
          u :
        ℝ≥0∞)
⊢ κ.restrict (s := s) hs ⊗ₖ η.restrict (s := t) ht = (κ ⊗ₖ η).restrict (s := s ×ˢ t) ⋯

Tactic:
ext a u hu
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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
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
⊢ 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∞)

Tactic:
rw [compProd_apply hu, restrict_apply' _ _ _ hu, compProd_apply (hu.inter (hs.prod ht))]

Premises used: ProbabilityTheory.Kernel.restrict_apply', MeasurableSet.prod, ProbabilityTheory.Kernel.compProd_apply, MeasurableSet.inter
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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
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
⊢ ∫⁻ (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:
simp only [restrict_apply, Set.preimage, Measure.restrict_apply' ht, Set.mem_inter_iff,
    Set.mem_prod]

Premises used: ProbabilityTheory.Kernel.restrict_apply, Set.mem_inter_iff, Set.mem_prod, Set.preimage, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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∞)
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∞)
⊢ 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:
split_ifs with h
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : β
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:
simp only [h, true_and, Set.inter_def, Set.mem_setOf]

Premises used: Set.mem_setOf, Set.inter_def, true_and
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : β
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:
simp only [h, false_and, and_false, Set.setOf_false, measure_empty]

Premises used: false_and, MeasureTheory.measure_empty, Set.setOf_false, and_false
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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∞)
neg 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∞)
⊢ 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:
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]

Premises used: Set.indicator_apply, false_and, MeasureTheory.measure_empty, Set.mem_setOf, Set.inter_def, Set.setOf_false, and_false, true_and
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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∞)

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]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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∞)
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
⊢ ∫⁻ (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_rw [this]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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∞)
h h₁ :
  ∫⁻ (b : β) in s,
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        ({x : γ | (b, x) ∈ u} ∩ t) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (a_1 : β) in s,
      (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        ({c : γ | (a_1, c) ∈ u} ∩ t) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (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:
rw [lintegral_indicator hs]

Premises used: MeasureTheory.lintegral_indicator
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 β
hs : MeasurableSet s
rw : κ.restrict (s := s) hs ⊗ₖ η = κ.restrict (s := s) hs ⊗ₖ η.restrict (s := Set.univ) ⋯
⊢ κ.restrict (s := s) hs ⊗ₖ η = (κ ⊗ₖ η).restrict (s := SProd.sprod (β := Set γ) s Set.univ) ⋯

Tactic:
rw [← compProd_restrict hs MeasurableSet.univ]

Premises used: ProbabilityTheory.Kernel.compProd_restrict, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 β
hs : MeasurableSet s
e_η : η = η.restrict (s := Set.univ) ⋯
⊢ κ.restrict (s := s) hs ⊗ₖ η = κ.restrict (s := s) hs ⊗ₖ η.restrict (s := Set.univ) ⋯

Tactic:
congr
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 β
hs : MeasurableSet s
⊢ η = η.restrict (s := Set.univ) ⋯

Tactic:
Kernel.restrict_univ.symm

Premises used: Eq.symm, ProbabilityTheory.Kernel.restrict_univ
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 β
hs : MeasurableSet s
⊢ η = η.restrict (s := Set.univ) ⋯

Tactic:
exact Kernel.restrict_univ.symm

Premises used: Eq.symm, ProbabilityTheory.Kernel.restrict_univ
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
rw : κ ⊗ₖ η.restrict (s := t) ht = κ.restrict (s := Set.univ) ⋯ ⊗ₖ η.restrict (s := t) ht
⊢ κ ⊗ₖ η.restrict (s := t) ht = (κ ⊗ₖ η).restrict (s := SProd.sprod (α := Set β) Set.univ t) ⋯

Tactic:
rw [← compProd_restrict MeasurableSet.univ ht]

Premises used: ProbabilityTheory.Kernel.compProd_restrict, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
e_κ : κ = κ.restrict (s := Set.univ) ⋯
⊢ κ ⊗ₖ η.restrict (s := t) ht = κ.restrict (s := Set.univ) ⋯ ⊗ₖ η.restrict (s := t) ht

Tactic:
congr
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ κ = κ.restrict (s := Set.univ) ⋯

Tactic:
Kernel.restrict_univ.symm

Premises used: Eq.symm, ProbabilityTheory.Kernel.restrict_univ
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ κ = κ.restrict (s := Set.univ) ⋯

Tactic:
exact Kernel.restrict_univ.symm

Premises used: Eq.symm, ProbabilityTheory.Kernel.restrict_univ
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
⊢ ∀ (a : β × γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) a = Function.uncurry f a

Tactic:
have h : ∀ a, ⨆ n, F n a = Function.uncurry f a := SimpleFunc.iSup_eapprox_apply hf