awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
μs_lim : Tendsto μs F (𝓝 μ)
⊢ Tendsto (fun (i : γ) ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)

Tactic:
exact ⟨tendsto_normalize_of_tendsto μs_lim nonzero, μs_lim.mass⟩
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
ν : ProbabilityMeasure Ω
f : Ω → Ω'
hf : AEMeasurable f (↑ν : Measure Ω)
⊢ (↑(ν.map hf) : Measure Ω') = Measure.map f (↑ν : Measure Ω)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
ν : ProbabilityMeasure Ω
f : Ω → Ω'
f_aemble : AEMeasurable f (↑ν : Measure Ω)
A : Set Ω'
A_mble : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) (((↑(ν.map f_aemble) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) A : ℝ≥0∞)
    (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' A) : ℝ≥0∞)

Tactic:
Measure.map_apply_of_aemeasurable f_aemble A_mble

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
ν : ProbabilityMeasure Ω
f : Ω → Ω'
f_aemble : AEMeasurable f (↑ν : Measure Ω)
A : Set Ω'
A_mble : MeasurableSet A
⊢ Eq (α := ℝ≥0) ((ν.map f_aemble : (a : Set Ω') → ℝ≥0) A : ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) (f ⁻¹' A) : ℝ≥0)

Tactic:
(ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr <|
    ν.map_apply' f_aemble A_mble

Premises used: Iff.mpr, ENNReal.toNNReal_eq_toNNReal_iff', MeasureTheory.measure_ne_top, MeasureTheory.ProbabilityMeasure.map_apply'
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
ν : ProbabilityMeasure Ω
f : Ω → Ω'
f_aemble : AEMeasurable f (↑ν : Measure Ω)
A : Set Ω'
A_mble : MeasurableSet A
⊢ Eq (α := ℝ≥0) ((ν.map f_aemble : (a : Set Ω') → ℝ≥0) A : ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) (f ⁻¹' A) : ℝ≥0)

Tactic:
exact (ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr <|
    ν.map_apply' f_aemble A_mble

Premises used: Iff.mpr, ENNReal.toNNReal_eq_toNNReal_iff', MeasureTheory.measure_ne_top, MeasureTheory.ProbabilityMeasure.map_apply'
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
ν : ProbabilityMeasure Ω
f : Ω → Ω'
f_aemble : AEMeasurable f (↑ν : Measure Ω)
A : Set Ω'
A_mble : MeasurableSet A
⊢ Eq (α := ℝ≥0) ((ν.map f_aemble : (a : Set Ω') → ℝ≥0) A : ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) (f ⁻¹' A) : ℝ≥0)

Tactic:
map_apply_of_aemeasurable ν f_aemble A_mble

Premises used: MeasureTheory.ProbabilityMeasure.map_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim : Tendsto νs L (𝓝 ν)
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
rw :
  ∀
    (lim :
      ∀ (f : Ω →ᵇ ℝ≥0),
        Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
          (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω))))
    {f : Ω → Ω'} (f_cont : Continuous[inst_2, inst_4] f) (f_1 : Ω' →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω'), (↑((f_1 : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑((νs i).map ⋯) : Measure Ω')) L
      (𝓝 (∫⁻ (ω : Ω'), (↑((f_1 : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(ν.map ⋯) : Measure Ω')))
⊢ Tendsto (β := ProbabilityMeasure Ω') (fun (i : ι) ↦ (νs i).map ⋯) L (𝓝 (ν.map ⋯))

Tactic:
rw [ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto] at lim ⊢

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
⊢ Tendsto
    (fun (i : ι) ↦
      ∫⁻ (ω : Ω),
        (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) ω) :
          ℝ≥0∞) ∂(↑(νs i) : Measure Ω))
    L
    (𝓝
      (∫⁻ (ω : Ω),
        (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) ω) :
          ℝ≥0∞) ∂(↑ν : Measure Ω)))

Tactic:
lim (g.compContinuous ⟨f, f_cont⟩)

Premises used: ContinuousMap.mk, BoundedContinuousFunction.compContinuous
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
h :
  ∀ (x : ι),
    ∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑((νs x).map ⋯) : Measure Ω') =
      ∫⁻ (ω : Ω),
        (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) ω) :
          ℝ≥0∞) ∂(↑(νs x) : Measure Ω)
h₁ :
  ∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(ν.map ⋯) : Measure Ω') =
    ∫⁻ (ω : Ω),
      (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑ν : Measure Ω)
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑((νs i).map ⋯) : Measure Ω')) L
    (𝓝 (∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(ν.map ⋯) : Measure Ω')))

Tactic:
convert! lim (g.compContinuous ⟨f, f_cont⟩)

Premises used: ContinuousMap.mk, BoundedContinuousFunction.compContinuous
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
x : ι
h :
  ∫⁻ (ω : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsProbabilityMeasure μ) (Measure.map f (↑(νs x) : Measure Ω))
            ⋯) :
        Measure Ω') =
    ∫⁻ (ω : Ω), (↑((g : (a : Ω') → ℝ≥0) (f ω)) : ℝ≥0∞) ∂(↑(νs x) : Measure Ω)
⊢ ∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑((νs x).map ⋯) : Measure Ω') =
    ∫⁻ (ω : Ω),
      (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑(νs x) : Measure Ω)

Tactic:
simp only [map, compContinuous_apply, ContinuousMap.coe_mk]

Premises used: ContinuousMap.coe_mk, BoundedContinuousFunction.compContinuous_apply, MeasureTheory.ProbabilityMeasure.map
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
x : ι
⊢ ∫⁻ (ω : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsProbabilityMeasure μ) (Measure.map f (↑(νs x) : Measure Ω))
            ⋯) :
        Measure Ω') =
    ∫⁻ (ω : Ω), (↑((g : (a : Ω') → ℝ≥0) (f ω)) : ℝ≥0∞) ∂(↑(νs x) : Measure Ω)

Tactic:
lintegral_map ?_ f_cont.measurable

Premises used: Continuous.measurable, MeasureTheory.lintegral_map, MeasureTheory.ProbabilityMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
x : ι
h : Measurable (β := ℝ≥0∞) fun (ω : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞)
⊢ ∫⁻ (ω : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsProbabilityMeasure μ) (Measure.map f (↑(νs x) : Measure Ω))
            ⋯) :
        Measure Ω') =
    ∫⁻ (ω : Ω), (↑((g : (a : Ω') → ℝ≥0) (f ω)) : ℝ≥0∞) ∂(↑(νs x) : Measure Ω)

Tactic:
refine lintegral_map ?_ f_cont.measurable

Premises used: Continuous.measurable, MeasureTheory.lintegral_map
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
x : ι
⊢ Measurable (β := ℝ≥0∞) fun (ω : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞)

Tactic:
(ENNReal.continuous_coe.comp g.continuous).measurable

Premises used: ENNReal.ofNNReal, Continuous.comp, BoundedContinuousFunction.continuous, WithTop.some, Continuous.measurable, ENNReal.continuous_coe
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
x : ι
⊢ Measurable (β := ℝ≥0∞) fun (ω : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞)

Tactic:
exact (ENNReal.continuous_coe.comp g.continuous).measurable

Premises used: Continuous.comp, BoundedContinuousFunction.continuous, Continuous.measurable, ENNReal.continuous_coe
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
h :
  ∫⁻ (ω : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsProbabilityMeasure μ) (Measure.map f (↑ν : Measure Ω)) ⋯) :
        Measure Ω') =
    ∫⁻ (ω : Ω), (↑((g : (a : Ω') → ℝ≥0) (f ω)) : ℝ≥0∞) ∂(↑ν : Measure Ω)
⊢ ∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(ν.map ⋯) : Measure Ω') =
    ∫⁻ (ω : Ω),
      (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑ν : Measure Ω)

Tactic:
simp only [map, compContinuous_apply, ContinuousMap.coe_mk]

Premises used: ContinuousMap.coe_mk, BoundedContinuousFunction.compContinuous_apply, MeasureTheory.ProbabilityMeasure.map
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsProbabilityMeasure μ) (Measure.map f (↑ν : Measure Ω)) ⋯) :
        Measure Ω') =
    ∫⁻ (ω : Ω), (↑((g : (a : Ω') → ℝ≥0) (f ω)) : ℝ≥0∞) ∂(↑ν : Measure Ω)

Tactic:
lintegral_map ?_ f_cont.measurable

Premises used: Continuous.measurable, MeasureTheory.lintegral_map, MeasureTheory.ProbabilityMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
h : Measurable (β := ℝ≥0∞) fun (ω : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞)
⊢ ∫⁻ (ω : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsProbabilityMeasure μ) (Measure.map f (↑ν : Measure Ω)) ⋯) :
        Measure Ω') =
    ∫⁻ (ω : Ω), (↑((g : (a : Ω') → ℝ≥0) (f ω)) : ℝ≥0∞) ∂(↑ν : Measure Ω)

Tactic:
refine lintegral_map ?_ f_cont.measurable

Premises used: Continuous.measurable, MeasureTheory.lintegral_map
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
⊢ Measurable (β := ℝ≥0∞) fun (ω : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞)

Tactic:
(ENNReal.continuous_coe.comp g.continuous).measurable

Premises used: ENNReal.ofNNReal, Continuous.comp, BoundedContinuousFunction.continuous, WithTop.some, Continuous.measurable, ENNReal.continuous_coe
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
⊢ Measurable (β := ℝ≥0∞) fun (ω : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞)

Tactic:
exact (ENNReal.continuous_coe.comp g.continuous).measurable

Premises used: Continuous.comp, BoundedContinuousFunction.continuous, Continuous.measurable, ENNReal.continuous_coe
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
rw :
  ∀ (x : ProbabilityMeasure Ω),
    ContinuousAt.{u_1, u_2} (Y := ProbabilityMeasure Ω') (fun (ν : ProbabilityMeasure Ω) ↦ ν.map ⋯) x
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (ν : ProbabilityMeasure Ω) ↦ ν.map ⋯

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
⊢ ∀ (x : ProbabilityMeasure Ω),
    ContinuousAt.{u_1, u_2} (Y := ProbabilityMeasure Ω') (fun (ν : ProbabilityMeasure Ω) ↦ ν.map ⋯) x

Tactic:
fun _ ↦ tendsto_map_of_tendsto_of_continuous _ _ continuous_id.continuousAt f_cont

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous, ContinuousAt, id, Continuous.continuousAt, continuous_id
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
⊢ ∀ (x : ProbabilityMeasure Ω),
    ContinuousAt.{u_1, u_2} (Y := ProbabilityMeasure Ω') (fun (ν : ProbabilityMeasure Ω) ↦ ν.map ⋯) x

Tactic:
exact fun _ ↦ tendsto_map_of_tendsto_of_continuous _ _ continuous_id.continuousAt f_cont

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous, id, Continuous.continuousAt, continuous_id
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_1
inst : MeasurableSpace α
m : Measure (Measure α)
inst_1 : IsProbabilityMeasure m
hm : ∀ᵐ (μ : Measure α) ∂m, IsProbabilityMeasure μ
simp : ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) univ ∂m = 1
⊢ IsProbabilityMeasure m.join

Tactic:
simp only [isProbabilityMeasure_iff, MeasurableSet.univ, Measure.join_apply]

Premises used: MeasureTheory.isProbabilityMeasure_iff, MeasureTheory.Measure.join_apply, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_1
inst : MeasurableSpace α
m : Measure (Measure α)
inst_1 : IsProbabilityMeasure m
hm : ∀ᵐ (μ : Measure α) ∂m, IsProbabilityMeasure μ
⊢ ∀ᵐ (μ : Measure α) ∂m, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp_rw [isProbabilityMeasure_iff] at hm

Premises used: MeasureTheory.isProbabilityMeasure_iff
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_1
inst : MeasurableSpace α
m : Measure (Measure α)
inst_1 : IsProbabilityMeasure m
hm : ∀ᵐ (μ : Measure α) ∂m, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) univ ∂m = 1

Tactic:
lintegral_eq_const hm

Premises used: MeasureTheory.lintegral_eq_const
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_1
inst : MeasurableSpace α
m : Measure (Measure α)
inst_1 : IsProbabilityMeasure m
hm : ∀ᵐ (μ : Measure α) ∂m, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) univ ∂m = 1

Tactic:
exact lintegral_eq_const hm

Premises used: MeasureTheory.lintegral_eq_const
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
m : Measure α
inst_2 : IsProbabilityMeasure m
f : α → Measure β
hf₀ : AEMeasurable f m
hf₁ : ∀ᵐ (μ : α) ∂m, IsProbabilityMeasure (f μ)
simp : ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) univ ∂m = 1
⊢ IsProbabilityMeasure (m.bind f)

Tactic:
simp only [isProbabilityMeasure_iff, MeasurableSet.univ, Measure.bind_apply _ hf₀]

Premises used: MeasureTheory.Measure.bind_apply, MeasureTheory.isProbabilityMeasure_iff, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
m : Measure α
inst_2 : IsProbabilityMeasure m
f : α → Measure β
hf₀ : AEMeasurable f m
hf₁ : ∀ᵐ (μ : α) ∂m, IsProbabilityMeasure (f μ)
⊢ ∀ᵐ (μ : α) ∂m, Eq (α := ℝ≥0∞) ((f μ : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp_rw [isProbabilityMeasure_iff] at hf₁

Premises used: MeasureTheory.isProbabilityMeasure_iff
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
m : Measure α
inst_2 : IsProbabilityMeasure m
f : α → Measure β
hf₀ : AEMeasurable f m
hf₁ : ∀ᵐ (μ : α) ∂m, Eq (α := ℝ≥0∞) ((f μ : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) univ ∂m = 1

Tactic:
lintegral_eq_const hf₁

Premises used: MeasureTheory.lintegral_eq_const
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
m : Measure α
inst_2 : IsProbabilityMeasure m
f : α → Measure β
hf₀ : AEMeasurable f m
hf₁ : ∀ᵐ (μ : α) ∂m, Eq (α := ℝ≥0∞) ((f μ : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) univ ∂m = 1

Tactic:
exact lintegral_eq_const hf₁

Premises used: MeasureTheory.lintegral_eq_const
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s : Set (α × β)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ∅)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s_1 s : Set (α × β)
hs :
  Membership.mem (γ := Set (Set (α × β)))
    (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t}) s
basic :
  ∀ (s : Set α) (hs : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s) (t : Set β),
    Measurable (β := ℝ≥0∞) fun (x : α) ↦
      (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)

Tactic:
obtain ⟨s, hs, t, -, rfl⟩ := hs

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s_1 : Set (α × β)
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s
t : Set β
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦
    (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t)

Tactic:
simpa only [mk_preimage_prod_right_eq_if, measure_if]
      using measurable_const.indicator hs

Premises used: Measurable.indicator, Set.mk_preimage_prod_right_eq_if, MeasureTheory.measure_if, measurable_const