case h.h
α : Type u_1
β : Type u_2
ι : Type ?u.362955
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
h : ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → (∫⁻ (b : β), f b ∂↑κ a) = ∫⁻ (b : β), f b ∂↑η a
a : α
s : Set β
⊢ MeasurableSet s → ↑↑(↑κ a) s = ↑↑(↑η a) s
α : Type u_1
β : Type u_2
ι : Type ?u.362955
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
h : ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → (∫⁻ (b : β), f b ∂↑κ a) = ∫⁻ (b : β), f b ∂↑η a
⊢ κ = η
ext a s
case h.h
α : Type u_1
β : Type u_2
ι : Type ?u.362955
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
h : ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → (∫⁻ (b : β), f b ∂↑κ a) = ∫⁻ (b : β), f b ∂↑η a
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑κ a) s = ↑↑(↑η a) s
case h.h
α : Type u_1
β : Type u_2
ι : Type ?u.362955
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
h : ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → (∫⁻ (b : β), f b ∂↑κ a) = ∫⁻ (b : β), f b ∂↑η a
a : α
s : Set β
⊢ MeasurableSet s → ↑↑(↑κ a) s = ↑↑(↑η a) s
intro hs
case h.h
α : Type u_1
β : Type u_2
ι : Type ?u.362955
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
a : α
s : Set β
hs : MeasurableSet s
h : (∫⁻ (b : β), Set.indicator s (fun x => 1) b ∂↑κ a) = ∫⁻ (b : β), Set.indicator s (fun x => 1) b ∂↑η a
⊢ ↑↑(↑κ a) s = ↑↑(↑η a) s
case h.h
α : Type u_1
β : Type u_2
ι : Type ?u.362955
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
h : ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → (∫⁻ (b : β), f b ∂↑κ a) = ∫⁻ (b : β), f b ∂↑η a
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑κ a) s = ↑↑(↑η a) s
specialize h a (s.indicator fun _ => 1) (Measurable.indicator measurable_const hs)
case h.h
α : Type u_1
β : Type u_2
ι : Type ?u.362955
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
a : α
s : Set β
hs : MeasurableSet s
h : ↑↑(↑κ a) s = ↑↑(↑η a) s
⊢ ↑↑(↑κ a) s = ↑↑(↑η a) s
case h.h
α : Type u_1
β : Type u_2
ι : Type ?u.362955
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
a : α
s : Set β
hs : MeasurableSet s
h : (∫⁻ (b : β), Set.indicator s (fun x => 1) b ∂↑κ a) = ∫⁻ (b : β), Set.indicator s (fun x => 1) b ∂↑η a
⊢ ↑↑(↑κ a) s = ↑↑(↑η a) s
simp_rw [lintegral_indicator_const hs, one_mul] at h
no goals
case h.h
α : Type u_1
β : Type u_2
ι : Type ?u.362955
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
a : α
s : Set β
hs : MeasurableSet s
h : ↑↑(↑κ a) s = ↑↑(↑η a) s
⊢ ↑↑(↑κ a) s = ↑↑(↑η a) s
rw [h]