-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProd_restrict {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) :
    Kernel.restrict κ hs ⊗ₖ Kernel.restrict η ht = Kernel.restrict (κ ⊗ₖ η) (hs.prod ht)

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
this :
  ∀ (b : β), (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = s.indicator (fun b => (η (a, b)) ({c | (b, c) ∈ u} ∩ t)) b
⊢ ∫⁻ (b : β) in s, (η (a, b)) ({c | (b, c) ∈ u} ∩ t) ∂κ a =
    ∫⁻ (b : β), s.indicator (fun b => (η (a, b)) ({c | (b, c) ∈ u} ∩ t)) b ∂κ a

Tactic:
rw [lintegral_indicator hs]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
h : b ∉ s
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = 0

Tactic:
simp only [h, false_and, and_false, Set.setOf_false, measure_empty]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = s.indicator (fun b => (η (a, b)) ({c | (b, c) ∈ u} ∩ t)) b

Tactic:
rw [Set.indicator_apply]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = if b ∈ s then (η (a, b)) ({c | (b, c) ∈ u} ∩ t) else 0

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
this :
  ∀ (b : β), (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = s.indicator (fun b => (η (a, b)) ({c | (b, c) ∈ u} ∩ t)) b
⊢ ∫⁻ (b : β) in s, (η (a, b)) ({c | (b, c) ∈ u} ∩ t) ∂κ a = ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} ∂κ a

Tactic:
simp_rw [this]

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
this :
  ∀ (b : β), (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = s.indicator (fun b => (η (a, b)) ({c | (b, c) ∈ u} ∩ t)) b
⊢ ∫⁻ (b : β) in s, (η (a, b)) ({c | (b, c) ∈ u} ∩ t) ∂κ a =
    ∫⁻ (b : β), s.indicator (fun b => (η (a, b)) ({c | (b, c) ∈ u} ∩ t)) b ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
⊢ ∀ (b : β), (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = s.indicator (fun b => (η (a, b)) ({c | (b, c) ∈ u} ∩ t)) b

Tactic:
intro b

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = s.indicator (fun b => (η (a, b)) ({c | (b, c) ∈ u} ∩ t)) b

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
h : b ∈ s
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = (η (a, b)) ({c | (b, c) ∈ u} ∩ t)

Tactic:
simp only [h, true_and, Set.inter_def, Set.mem_setOf]

Result:
no goals

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
⊢ ((κ.restrict hs ⊗ₖ η.restrict ht) a) u = (((κ ⊗ₖ η).restrict ⋯) a) u

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

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
⊢ ∫⁻ (b : β), ((η.restrict ht) (a, b)) {c | (b, c) ∈ u} ∂(κ.restrict hs) a =
    ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ u ∩ s ×ˢ t} ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = if b ∈ s then (η (a, b)) ({c | (b, c) ∈ u} ∩ t) else 0

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
h : b ∈ s
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = (η (a, b)) ({c | (b, c) ∈ u} ∩ t)

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
h : b ∉ s
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = 0