-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma compProd_id [SFinite μ] : μ ⊗ₘ Kernel.id = μ.map (fun x ↦ (x, x))

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), ((fun x => (x, x)) ⁻¹' s).indicator 1 a ∂μ = μ ((fun x => (x, x)) ⁻¹' s)

Tactic:
rw [lintegral_indicator_one]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ MeasurableSet ((fun x => (x, x)) ⁻¹' s)

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), (Kernel.id a) (Prod.mk a ⁻¹' s) ∂μ = μ ((fun x => (x, x)) ⁻¹' s)

Tactic:
simp_rw [Kernel.id_apply, dirac_apply' _ (h_meas _)]

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), (Prod.mk a ⁻¹' s).indicator 1 a ∂μ = μ ((fun x => (x, x)) ⁻¹' s)

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (Kernel.id a) (Prod.mk a ⁻¹' s) ∂μ = μ ((fun x => (x, x)) ⁻¹' s)

Tactic:
have h_meas a : MeasurableSet (Prod.mk a ⁻¹' s) := measurable_prod_mk_left hs

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), (Kernel.id a) (Prod.mk a ⁻¹' s) ∂μ = μ ((fun x => (x, x)) ⁻¹' s)

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), (Prod.mk a ⁻¹' s).indicator 1 a ∂μ = μ ((fun x => (x, x)) ⁻¹' s)

Tactic:
calc ∫⁻ a, (Prod.mk a ⁻¹' s).indicator 1 a ∂μ
_ = ∫⁻ a, ((fun x ↦ (x, x)) ⁻¹' s).indicator 1 a ∂μ := rfl
_ = μ ((fun x ↦ (x, x)) ⁻¹' s) := by
  rw [lintegral_indicator_one]
  exact (measurable_id.prod measurable_id) hs

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ μ ⊗ₘ Kernel.id = map (fun x => (x, x)) μ

Tactic:
ext s hs

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
⊢ (μ ⊗ₘ Kernel.id) s = (map (fun x => (x, x)) μ) s

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
⊢ (μ ⊗ₘ Kernel.id) s = (map (fun x => (x, x)) μ) s

Tactic:
rw [compProd_apply hs, map_apply (measurable_id.prod measurable_id) hs]

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (Kernel.id a) (Prod.mk a ⁻¹' s) ∂μ = μ ((fun x => (x, x)) ⁻¹' s)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ MeasurableSet ((fun x => (x, x)) ⁻¹' s)

Tactic:
exact (measurable_id.prod measurable_id) hs

Result:
no goals