awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : TopologicalSpace Ω'
inst_4 : BorelSpace Ω
inst_5 : BorelSpace Ω'
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ :
  Membership.mem (γ := Set (FiniteMeasure Ω'))
    {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)} μ
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : Eq (α := Ω → ℝ) ((⇑g' : (a : Ω') → ℝ) ∘ f) (⇑g : (a : Ω) → ℝ)
A : ∀ (x : Ω), Eq (α := ℝ) ((g : (a : Ω) → ℝ) x : ℝ) ((g' : (a : Ω') → ℝ) (f x) : ℝ)
B :
  ∀ {ν : FiniteMeasure Ω'} (hν : Eq (α := ℝ≥0) ((ν : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)),
    Eq (α := ℝ) (∫ (y : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
      (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
this :
  Tendsto (β := ℝ) (fun (ν : FiniteMeasure Ω') ↦ ∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
    (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ)
    (𝓝 (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑μ : Measure Ω')))
apply :
  (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ).EventuallyEq (β :=
    ℝ) (fun (ν : FiniteMeasure Ω') ↦ ∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω')) fun (i : FiniteMeasure Ω') ↦
    ∫ (y : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑i : Measure Ω')
⊢ Tendsto (β := ℝ) (fun (i : FiniteMeasure Ω') ↦ ∫ (y : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑i : Measure Ω'))
    (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ)
    (𝓝 (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑μ : Measure Ω')))

Tactic:
apply Tendsto.congr' _ this

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : TopologicalSpace Ω'
inst_4 : BorelSpace Ω
inst_5 : BorelSpace Ω'
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ :
  Membership.mem (γ := Set (FiniteMeasure Ω'))
    {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)} μ
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : Eq (α := Ω → ℝ) ((⇑g' : (a : Ω') → ℝ) ∘ f) (⇑g : (a : Ω) → ℝ)
A : ∀ (x : Ω), Eq (α := ℝ) ((g : (a : Ω) → ℝ) x : ℝ) ((g' : (a : Ω') → ℝ) (f x) : ℝ)
B :
  ∀ {ν : FiniteMeasure Ω'} (hν : Eq (α := ℝ≥0) ((ν : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)),
    Eq (α := ℝ) (∫ (y : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
      (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
this :
  Tendsto (β := ℝ) (fun (ν : FiniteMeasure Ω') ↦ ∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
    (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ)
    (𝓝 (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑μ : Measure Ω')))
ν : FiniteMeasure Ω'
hν : Eq (α := ℝ≥0) ((ν : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)
⊢ Eq (α := ℝ) (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
    (∫ (y : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))

Tactic:
(B hν).symm

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : TopologicalSpace Ω'
inst_4 : BorelSpace Ω
inst_5 : BorelSpace Ω'
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ :
  Membership.mem (γ := Set (FiniteMeasure Ω'))
    {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)} μ
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : Eq (α := Ω → ℝ) ((⇑g' : (a : Ω') → ℝ) ∘ f) (⇑g : (a : Ω) → ℝ)
A : ∀ (x : Ω), Eq (α := ℝ) ((g : (a : Ω) → ℝ) x : ℝ) ((g' : (a : Ω') → ℝ) (f x) : ℝ)
B :
  ∀ {ν : FiniteMeasure Ω'} (hν : Eq (α := ℝ≥0) ((ν : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)),
    Eq (α := ℝ) (∫ (y : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
      (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
this :
  Tendsto (β := ℝ) (fun (ν : FiniteMeasure Ω') ↦ ∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
    (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ)
    (𝓝 (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑μ : Measure Ω')))
h :
  ∀ (a : FiniteMeasure Ω'),
    Membership.mem (γ := Set (FiniteMeasure Ω'))
      {x : FiniteMeasure Ω' |
        Membership.mem (γ := Set (FiniteMeasure Ω'))
            {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)} x →
          Membership.mem (γ := Set (FiniteMeasure Ω'))
            {x : FiniteMeasure Ω' |
              (fun (x : FiniteMeasure Ω') ↦
                  Eq (α := ℝ)
                    ((fun (ν : FiniteMeasure Ω') ↦ (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω') : ℝ)) x)
                    ((fun (i : FiniteMeasure Ω') ↦
                        (∫ (y : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑i : Measure Ω') : ℝ))
                      x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (ν : FiniteMeasure Ω') (hν : Eq (α := ℝ≥0) ((ν : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)),
    Eq (α := ℝ) (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
      (∫ (y : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
⊢ (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ).EventuallyEq (β :=
    ℝ) (fun (ν : FiniteMeasure Ω') ↦ ∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω')) fun (i : FiniteMeasure Ω') ↦
    ∫ (y : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑i : Measure Ω')

Tactic:
filter_upwards [self_mem_nhdsWithin] with ν hν using (B hν).symm

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
ν : FiniteMeasure Ω
f : Ω → Ω'
⊢ Eq (α := Measure Ω') (↑(ν.map f) : Measure Ω') (Measure.map f (↑ν : Measure Ω))

Tactic:
rfl

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

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

Tactic:
(ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr key

Premises used: Iff.mpr, ENNReal.toNNReal_eq_toNNReal_iff', MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
ν : FiniteMeasure Ω
f : Ω → Ω'
f_aemble : AEMeasurable f (↑ν : Measure Ω)
A : Set Ω'
A_mble : MeasurableSet A
key :
  Eq (α := ℝ≥0∞) ((((↑(ν.map f) : Measure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) A : ℝ≥0∞)
    (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' A) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0) (((ν.map f : FiniteMeasure Ω') : (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 key

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

Tactic:
map_apply_of_aemeasurable ν f_mble.aemeasurable A_mble

Premises used: Measurable.aemeasurable, MeasureTheory.FiniteMeasure.map_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
f_mble : Measurable f
ν₁ ν₂ : FiniteMeasure Ω
h :
  ∀ (s : Set Ω'),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((↑((ν₁ + ν₂).map f) : Measure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
        (((↑(HAdd.hAdd (α := FiniteMeasure Ω') (ν₁.map f) (ν₂.map f)) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
⊢ (ν₁ + ν₂).map f = HAdd.hAdd (α := FiniteMeasure Ω') (ν₁.map f) (ν₂.map f)

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
f_mble : Measurable f
ν₁ ν₂ : FiniteMeasure Ω
s : Set Ω'
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((↑((ν₁ + ν₂).map f) : Measure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
    (((↑(HAdd.hAdd (α := FiniteMeasure Ω') (ν₁.map f) (ν₂.map f)) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
c : ℝ≥0
ν : FiniteMeasure Ω
h :
  ∀ (s : Set Ω'),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((↑((c • ν).map f) : Measure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
        (((↑(HSMul.hSMul (β := FiniteMeasure Ω') c (ν.map f)) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
⊢ (c • ν).map f = HSMul.hSMul (β := FiniteMeasure Ω') c (ν.map f)

Tactic:
ext s _
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
c : ℝ≥0
ν : FiniteMeasure Ω
s : Set Ω'
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((↑((c • ν).map f) : Measure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
    (((↑(HSMul.hSMul (β := FiniteMeasure Ω') c (ν.map f)) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [toMeasure_smul]

Premises used: MeasureTheory.FiniteMeasure.toMeasure_smul
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
simp :
  LE.le (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ mass (μ.map f) ≤ μ.mass

Tactic:
simp only [mass, coeFn_def, toMeasure_map, ne_eq, measure_ne_top, not_false_eq_true,
    ENNReal.toNNReal_le_toNNReal]

Premises used: MeasureTheory.FiniteMeasure.mass, ENNReal.toNNReal_le_toNNReal, MeasureTheory.measure_ne_top, MeasureTheory.FiniteMeasure.coeFn_def, ne_eq, MeasureTheory.FiniteMeasure.toMeasure_map, not_false_eq_true
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
pos :
  ∀ (hf : AEMeasurable f (↑μ : Measure Ω)),
    LE.le (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
neg :
  ∀ (hf : ¬AEMeasurable f (↑μ : Measure Ω)),
    LE.le (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
by_cases hf : AEMeasurable f μ

Premises used: AEMeasurable, MeasureTheory.FiniteMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
hf : AEMeasurable f (↑μ : Measure Ω)
pos :
  LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' univ) : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [Measure.map_apply_of_aemeasurable hf MeasurableSet.univ]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
hf : AEMeasurable f (↑μ : Measure Ω)
⊢ LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' univ) : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
measure_mono (subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
hf : AEMeasurable f (↑μ : Measure Ω)
⊢ LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' univ) : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
exact measure_mono (subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
hf : ¬AEMeasurable f (↑μ : Measure Ω)
⊢ LE.le (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp [Measure.map_of_not_aemeasurable hf]

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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 : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim : Tendsto νs L (𝓝 ν)
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
rw :
  ∀
    (lim :
      ∀ (f : Ω →ᵇ ℝ≥0),
        Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
          (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω))))
    {f : Ω → Ω'} (f_cont : Continuous[inst_2, inst_4] f) (f_1 : Ω' →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω'), (↑((f_1 : (a : Ω') → ℝ≥0) x) : ℝ≥0∞) ∂(↑((νs i).map f) : Measure Ω')) L
      (𝓝 (∫⁻ (x : Ω'), (↑((f_1 : (a : Ω') → ℝ≥0) x) : ℝ≥0∞) ∂(↑(ν.map f) : Measure Ω')))
⊢ Tendsto (β := FiniteMeasure Ω') (fun (i : ι) ↦ (νs i).map f) L (𝓝 (ν.map f))

Tactic:
rw [FiniteMeasure.tendsto_iff_forall_lintegral_tendsto] at lim ⊢

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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 : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
⊢ Tendsto
    (fun (i : ι) ↦
      ∫⁻ (x : Ω),
        (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) x) :
          ℝ≥0∞) ∂(↑(νs i) : Measure Ω))
    L
    (𝓝
      (∫⁻ (x : Ω),
        (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) x) :
          ℝ≥0∞) ∂(↑ν : Measure Ω)))

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

Premises used: ContinuousMap.mk, BoundedContinuousFunction.compContinuous
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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 : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
h :
  ∀ (x : ι),
    ∫⁻ (x : Ω'), (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞) ∂(↑((νs x).map f) : Measure Ω') =
      ∫⁻ (x : Ω),
        (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) x) :
          ℝ≥0∞) ∂(↑(νs x) : Measure Ω)
h₁ :
  ∫⁻ (x : Ω'), (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞) ∂(↑(ν.map f) : Measure Ω') =
    ∫⁻ (x : Ω),
      (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) x) :
        ℝ≥0∞) ∂(↑ν : Measure Ω)
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω'), (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞) ∂(↑((νs i).map f) : Measure Ω')) L
    (𝓝 (∫⁻ (x : Ω'), (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞) ∂(↑(ν.map f) : Measure Ω')))

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

Premises used: ContinuousMap.mk, BoundedContinuousFunction.compContinuous
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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 : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
x : ι
h :
  ∫⁻ (x : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) x) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsFiniteMeasure μ) (Measure.map f (↑(νs x) : Measure Ω)) ⋯) :
        Measure Ω') =
    ∫⁻ (x : Ω), (↑((g : (a : Ω') → ℝ≥0) (f x)) : ℝ≥0∞) ∂(↑(νs x) : Measure Ω)
⊢ ∫⁻ (x : Ω'), (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞) ∂(↑((νs x).map f) : Measure Ω') =
    ∫⁻ (x : Ω),
      (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) x) :
        ℝ≥0∞) ∂(↑(νs x) : Measure Ω)

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

Premises used: MeasureTheory.FiniteMeasure.map, ContinuousMap.coe_mk, BoundedContinuousFunction.compContinuous_apply
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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 : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
x : ι
⊢ ∫⁻ (x : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) x) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsFiniteMeasure μ) (Measure.map f (↑(νs x) : Measure Ω)) ⋯) :
        Measure Ω') =
    ∫⁻ (x : Ω), (↑((g : (a : Ω') → ℝ≥0) (f x)) : ℝ≥0∞) ∂(↑(νs x) : Measure Ω)

Tactic:
lintegral_map ?_ f_cont.measurable

Premises used: Continuous.measurable, MeasureTheory.lintegral_map, MeasureTheory.FiniteMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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 : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
x : ι
h : Measurable (β := ℝ≥0∞) fun (x : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞)
⊢ ∫⁻ (x : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) x) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsFiniteMeasure μ) (Measure.map f (↑(νs x) : Measure Ω)) ⋯) :
        Measure Ω') =
    ∫⁻ (x : Ω), (↑((g : (a : Ω') → ℝ≥0) (f x)) : ℝ≥0∞) ∂(↑(νs x) : Measure Ω)

Tactic:
refine lintegral_map ?_ f_cont.measurable

Premises used: Continuous.measurable, MeasureTheory.lintegral_map
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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 : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
x : ι
⊢ Measurable (β := ℝ≥0∞) fun (x : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥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.FiniteMeasure
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 : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
x : ι
⊢ Measurable (β := ℝ≥0∞) fun (x : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞)

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

Premises used: Continuous.comp, BoundedContinuousFunction.continuous, Continuous.measurable, ENNReal.continuous_coe