awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
f : X →ᵇ ℝ
⊢ Continuous[instTopologicalSpace, _] fun (μ : FiniteMeasure X) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂(↑μ : Measure X)

Tactic:
continuous_iff_forall_continuous_integral.1 continuous_id _

Premises used: continuous_id, Iff.mp, MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_integral
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
X : Type u_2
inst_3 : TopologicalSpace X
μs : X → FiniteMeasure Ω
inst_4 : CompactSpace Ω
⊢ Continuous[inst_3, instTopologicalSpace] μs ↔
    ∀ (f : C(Ω, ℝ≥0)),
      Continuous[inst_3, _] fun (x : X) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(μs x) : Measure Ω)

Tactic:
continuous_iff_forall_continuous_lintegral.trans
    (ContinuousMap.equivBoundedOfCompact ..).symm.forall_congr_left

Premises used: ContinuousMap.equivBoundedOfCompact, Equiv.forall_congr_left, MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_lintegral, Iff.trans, Equiv.symm
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
X : Type u_2
inst_3 : TopologicalSpace X
μs : X → FiniteMeasure Ω
inst_4 : CompactSpace Ω
⊢ Continuous[inst_3, instTopologicalSpace] μs ↔
    ∀ (f : C(Ω, ℝ)), Continuous[inst_3, _] fun (x : X) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs x) : Measure Ω)

Tactic:
continuous_iff_forall_continuous_integral.trans
    (ContinuousMap.equivBoundedOfCompact ..).symm.forall_congr_left

Premises used: ContinuousMap.equivBoundedOfCompact, Equiv.forall_congr_left, Iff.trans, Equiv.symm, MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_integral
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
F : Type u_3
inst_4 : FunLike F X ℝ≥0
inst_5 : ContinuousMapClass F X ℝ≥0
f : F
⊢ Continuous[instTopologicalSpace, _] fun (μ : FiniteMeasure X) ↦
    ∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure X)

Tactic:
continuous_iff_forall_continuousMap_continuous_lintegral.1 continuous_id ⟨f, map_continuous f⟩

Premises used: ContinuousMap.mk, MeasureTheory.FiniteMeasure.continuous_iff_forall_continuousMap_continuous_lintegral, continuous_id, Iff.mp, ContinuousMapClass.map_continuous, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
F : Type u_3
inst_4 : FunLike F X ℝ
inst_5 : ContinuousMapClass F X ℝ
f : F
⊢ Continuous[instTopologicalSpace, _] fun (μ : FiniteMeasure X) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂(↑μ : Measure X)

Tactic:
continuous_iff_forall_continuousMap_continuous_integral.1 continuous_id ⟨f, map_continuous f⟩

Premises used: ContinuousMap.mk, continuous_id, Iff.mp, ContinuousMapClass.map_continuous, MeasureTheory.FiniteMeasure.continuous_iff_forall_continuousMap_continuous_integral, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω'
⊢ IsFiniteMeasure (m0 := inst) (Measure.comap f (↑μ : Measure Ω'))

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω'
⊢ Eq (α := Measure Ω) (↑(comap f μ) : Measure Ω) (Measure.comap f (↑μ : Measure Ω'))

Tactic:
rfl

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

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

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

Tactic:
apply (Measure.comap_apply_le _ _ nullMeasurableSet_univ).trans (measure_mono (subset_univ _))

Premises used: Set.subset_univ, MeasureTheory.nullMeasurableSet_univ, MeasureTheory.Measure.comap_apply_le, MeasureTheory.measure_mono, LE.le.trans
-- 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)} μ
rw :
  ∀ (f_1 : Ω →ᵇ ℝ),
    Tendsto (β := ℝ)
      (fun (i : FiniteMeasure Ω') ↦
        @integral _ _ _ _ inst (↑(comap f i) : Measure Ω) fun (x : Ω) ↦ (f_1 : (a : Ω) → ℝ) x)
      (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ)
      (𝓝 (@integral _ _ _ _ inst (↑(comap f μ) : Measure Ω) fun (x : Ω) ↦ (f_1 : (a : Ω) → ℝ) x))
⊢ Tendsto (β := FiniteMeasure Ω) (fun (μ : FiniteMeasure Ω') ↦ comap f μ)
    (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ) (𝓝 (comap f μ))

Tactic:
rw [tendsto_iff_forall_integral_tendsto]

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto
-- 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' : Ω' →ᵇ ℝ), ‖g'‖ = ‖g‖ ∧ Eq (α := Ω → ℝ) ((⇑g' : (a : Ω') → ℝ) ∘ f) (⇑g : (a : Ω) → ℝ)

Tactic:
exists_extension_norm_eq_of_isClosedEmbedding g hf

Premises used: BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding
-- 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 : Ω →ᵇ ℝ
obtain :
  ∀ (g' : Ω' →ᵇ ℝ) (hg' : Eq (α := Ω → ℝ) ((⇑g' : (a : Ω') → ℝ) ∘ f) (⇑g : (a : Ω) → ℝ)),
    Tendsto (β := ℝ)
      (fun (i : FiniteMeasure Ω') ↦ @integral _ _ _ _ inst (↑(comap f i) : Measure Ω) fun (x : Ω) ↦ (g : (a : Ω) → ℝ) x)
      (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ)
      (𝓝 (@integral _ _ _ _ inst (↑(comap f μ) : Measure Ω) fun (x : Ω) ↦ (g : (a : Ω) → ℝ) x))
⊢ Tendsto (β := ℝ)
    (fun (i : FiniteMeasure Ω') ↦ @integral _ _ _ _ inst (↑(comap f i) : Measure Ω) fun (x : Ω) ↦ (g : (a : Ω) → ℝ) x)
    (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ)
    (𝓝 (@integral _ _ _ _ inst (↑(comap f μ) : Measure Ω) fun (x : Ω) ↦ (g : (a : Ω) → ℝ) x))

Tactic:
obtain ⟨g', -, hg'⟩ : ∃ g' : Ω' →ᵇ ℝ, ‖g'‖ = ‖g‖ ∧ g' ∘ f = g :=
    exists_extension_norm_eq_of_isClosedEmbedding g hf

Premises used: BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding
-- 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 : Ω) → ℝ)
x : Ω
⊢ Eq (α := ℝ) ((g : (a : Ω) → ℝ) x : ℝ) (((⇑g' : (a : Ω') → ℝ) ∘ f) x : ℝ)

Tactic:
simp only [hg']
-- 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 : Ω) → ℝ)
⊢ ∀ (x : Ω), Eq (α := ℝ) ((g : (a : Ω) → ℝ) x : ℝ) ((g' : (a : Ω') → ℝ) (f x) : ℝ)

Tactic:
have A x : g x = g' (f x) := by change (⇑g) x = (⇑g' ∘ f) x; simp only [hg']
-- 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) : ℝ)
simp :
  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 : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑μ : Measure Ω')))
⊢ Tendsto (β := ℝ)
    (fun (i : FiniteMeasure Ω') ↦ @integral _ _ _ _ inst (↑(comap f i) : Measure Ω) fun (x : Ω) ↦ (g : (a : Ω) → ℝ) x)
    (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ)
    (𝓝 (@integral _ _ _ _ inst (↑(comap f μ) : Measure Ω) fun (x : Ω) ↦ (g : (a : Ω) → ℝ) x))

Tactic:
simp only [comap, toMeasure_mk, A, ← MeasurableEmbedding.integral_map hf.measurableEmbedding,
    MeasurableEmbedding.map_comap hf.measurableEmbedding]

Premises used: MeasurableEmbedding.integral_map, MeasureTheory.FiniteMeasure.comap, MeasureTheory.FiniteMeasure.toMeasure_mk, Topology.IsClosedEmbedding.measurableEmbedding, MeasurableEmbedding.map_comap
-- 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) : ℝ)
ν : FiniteMeasure Ω'
hν : Eq (α := ℝ≥0) ((ν : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)
e_μ : (↑ν : Measure Ω').restrict (range f) = (↑ν : Measure Ω')
⊢ Eq (α := ℝ) (∫ (y : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
    (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))

Tactic:
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) : ℝ)
ν : FiniteMeasure Ω'
hν : Eq (α := ℝ≥0) ((ν : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)
⊢ Eq (α := ℝ≥0∞) (((↑ν : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (range f)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [null_iff_toMeasure_null] at hν

Premises used: MeasureTheory.FiniteMeasure.null_iff_toMeasure_null
-- 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) : ℝ)
ν : FiniteMeasure Ω'
hν : Eq (α := ℝ≥0∞) (((↑ν : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (range f)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (↑ν : Measure Ω').restrict (range f) = (↑ν : Measure Ω')

Tactic:
Measure.restrict_eq_self_of_ae_mem hν

Premises used: MeasureTheory.Measure.restrict_eq_self_of_ae_mem
-- 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) : ℝ)
ν : FiniteMeasure Ω'
hν : Eq (α := ℝ≥0∞) (((↑ν : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (range f)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (↑ν : Measure Ω').restrict (range f) = (↑ν : Measure Ω')

Tactic:
exact Measure.restrict_eq_self_of_ae_mem hν

Premises used: MeasureTheory.Measure.restrict_eq_self_of_ae_mem
-- 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) : ℝ)
⊢ ∀ {ν : 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 Ω'))

Tactic:
have B {ν : FiniteMeasure Ω'} (hν : ν (range f)ᶜ = 0) :
      ∫ y in range f, g' y ∂ν = ∫ y, g' y ∂ν := by
    congr
    simp only [null_iff_toMeasure_null] at hν
    exact Measure.restrict_eq_self_of_ae_mem hν
-- 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 Ω'))
rw :
  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 Ω')))
⊢ 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 : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑μ : Measure Ω')))

Tactic:
rw [B hμ]
-- 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 Ω'))
⊢ Tendsto (β := ℝ) (fun (ν : FiniteMeasure Ω') ↦ ∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω')) (𝓝 μ)
    (𝓝 (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑μ : Measure Ω')))

Tactic:
have A : Tendsto (fun (ν : FiniteMeasure Ω') ↦ ∫ y, g' y ∂ν) (𝓝 μ) (𝓝 (∫ (y : Ω'), g' y ∂μ)) :=
      tendsto_iff_forall_integral_tendsto.1 tendsto_id _
-- 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_1 : ∀ (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 Ω'))
A :
  Tendsto (β := ℝ) (fun (ν : FiniteMeasure Ω') ↦ ∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω')) (𝓝 μ)
    (𝓝 (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑μ : Measure Ω')))
⊢ Tendsto (β := ℝ) (fun (ν : FiniteMeasure Ω') ↦ ∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
    (𝓝 μ ⊓ 𝓟 {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)})
    (𝓝 (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑μ : Measure Ω')))

Tactic:
Tendsto.mono_left A inf_le_left

Premises used: Filter.Tendsto.mono_left, inf_le_left
-- 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_1 : ∀ (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 Ω'))
A :
  Tendsto (β := ℝ) (fun (ν : FiniteMeasure Ω') ↦ ∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω')) (𝓝 μ)
    (𝓝 (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑μ : Measure Ω')))
⊢ Tendsto (β := ℝ) (fun (ν : FiniteMeasure Ω') ↦ ∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
    (𝓝 μ ⊓ 𝓟 {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)})
    (𝓝 (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑μ : Measure Ω')))

Tactic:
exact Tendsto.mono_left A inf_le_left

Premises used: Filter.Tendsto.mono_left, inf_le_left
-- 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 Ω'))
⊢ Tendsto (β := ℝ) (fun (ν : FiniteMeasure Ω') ↦ ∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑ν : Measure Ω'))
    (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ)
    (𝓝 (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑μ : Measure Ω')))

Tactic:
have : Tendsto (fun (ν : FiniteMeasure Ω') ↦ ∫ y, g' y ∂ν) (𝓝[{μ | μ (range f)ᶜ = 0}] μ)
      (𝓝 (∫ (y : Ω'), g' y ∂μ)) := by
    rw [nhdsWithin]
    have A : Tendsto (fun (ν : FiniteMeasure Ω') ↦ ∫ y, g' y ∂ν) (𝓝 μ) (𝓝 (∫ (y : Ω'), g' y ∂μ)) :=
      tendsto_iff_forall_integral_tendsto.1 tendsto_id _
    exact Tendsto.mono_left A inf_le_left