[GOAL]
⊢ ConcreteCategory MeasCat
[PROOFSTEP]
unfold MeasCat
[GOAL]
⊢ ConcreteCategory (Bundled MeasurableSpace)
[PROOFSTEP]
infer_instance
[GOAL]
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ ∫⁻ (x : ℝ≥0∞), x ∂Measure.join μ = ∫⁻ (x : ℝ≥0∞), x ∂Measure.map (fun m => ∫⁻ (x : ℝ≥0∞), x ∂m) μ
[PROOFSTEP]
rw [Measure.lintegral_join, lintegral_map]
[GOAL]
case hf
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun x => x
[PROOFSTEP]
apply_rules [measurable_id, Measure.measurable_lintegral]
[GOAL]
case hg
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun m => ∫⁻ (x : ℝ≥0∞), x ∂m
[PROOFSTEP]
apply_rules [measurable_id, Measure.measurable_lintegral]
[GOAL]
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun x => x
[PROOFSTEP]
apply_rules [measurable_id, Measure.measurable_lintegral]
