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 : 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 : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) x) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsFiniteMeasure μ) (Measure.map f (↑ν : Measure Ω)) ⋯) :
        Measure Ω') =
    ∫⁻ (x : Ω), (↑((g : (a : Ω') → ℝ≥0) (f x)) : ℝ≥0∞) ∂(↑ν : Measure Ω)
⊢ ∫⁻ (x : Ω'), (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞) ∂(↑(ν.map f) : Measure Ω') =
    ∫⁻ (x : Ω),
      (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) x) :
        ℝ≥0∞) ∂(↑ν : 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 : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) x) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsFiniteMeasure μ) (Measure.map f (↑ν : Measure Ω)) ⋯) :
        Measure Ω') =
    ∫⁻ (x : Ω), (↑((g : (a : Ω') → ℝ≥0) (f x)) : ℝ≥0∞) ∂(↑ν : 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
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 (↑ν : Measure Ω)) ⋯) :
        Measure Ω') =
    ∫⁻ (x : Ω), (↑((g : (a : Ω') → ℝ≥0) (f x)) : ℝ≥0∞) ∂(↑ν : 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
⊢ 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
⊢ 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
-- 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 Ω'
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
rw : ∀ (x : FiniteMeasure Ω), ContinuousAt.{u_1, u_2} (Y := FiniteMeasure Ω') (fun (ν : FiniteMeasure Ω) ↦ ν.map f) x
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (ν : FiniteMeasure Ω) ↦ ν.map f

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- 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 Ω'
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
⊢ ∀ (x : FiniteMeasure Ω), ContinuousAt.{u_1, u_2} (Y := FiniteMeasure Ω') (fun (ν : FiniteMeasure Ω) ↦ ν.map f) x

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

Premises used: ContinuousAt, id, Continuous.continuousAt, continuous_id, MeasureTheory.FiniteMeasure.tendsto_map_of_tendsto_of_continuous
-- 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 Ω'
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
⊢ ∀ (x : FiniteMeasure Ω), ContinuousAt.{u_1, u_2} (Y := FiniteMeasure Ω') (fun (ν : FiniteMeasure Ω) ↦ ν.map f) x

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

Premises used: id, Continuous.continuousAt, continuous_id, MeasureTheory.FiniteMeasure.tendsto_map_of_tendsto_of_continuous
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
⊢ IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))

Tactic:
have A : IsEmbedding (Subtype.val : M → FiniteMeasure Ω') := IsEmbedding.subtypeVal
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
refine : μ.map f ∈ M
⊢ (↑M : Type u_2)

Tactic:
refine ⟨μ.map f, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
simp :
  Eq (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (range f)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.map f ∈ M

Tactic:
simp only [null_iff_toMeasure_null, mem_setOf_eq, toMeasure_map, M]

Premises used: Set.mem_setOf_eq, MeasureTheory.FiniteMeasure.toMeasure_map, MeasureTheory.FiniteMeasure.null_iff_toMeasure_null
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
rw : Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' (range f)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (range f)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.map_apply hf.continuous.measurable hf.isClosed_range.isOpen_compl.measurableSet]

Premises used: IsClosed.isOpen_compl, MeasureTheory.Measure.map_apply, IsOpen.measurableSet, Topology.IsClosedEmbedding.continuous, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
⊢ Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' (range f)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
h :
  ∀ (s : Set Ω) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((↑(M.restrict (π := fun (μ : FiniteMeasure Ω') ↦ FiniteMeasure Ω) (fun (μ : FiniteMeasure Ω') ↦ comap f μ)
                    ((fun (μ : FiniteMeasure Ω) ↦
                        (Subtype.mk (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M) (μ.map f) ⋯ :
                          { x : FiniteMeasure Ω' // x ∈ M }))
                      μ)) :
                Measure Ω) :
              Measure Ω) :
            (a : Set Ω) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ M.restrict (π := fun (μ : FiniteMeasure Ω') ↦ FiniteMeasure Ω) (fun (μ : FiniteMeasure Ω') ↦ comap f μ)
      ((fun (μ : FiniteMeasure Ω) ↦
          (Subtype.mk (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M) (μ.map f) ⋯ : { x : FiniteMeasure Ω' // x ∈ M }))
        μ) =
    μ

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
h : Function.Injective f
h₁ : Measurable f
h₂ : MeasurableSet (f '' s)
h₃ : Function.Injective f
h₄ : ∀ (s : Set Ω), MeasurableSet s → MeasurableSet (f '' s)
h₅ : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f (Measure.map f (↑μ : Measure Ω)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.comap_apply, Measure.map_apply, preimage_image_eq]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.comap_apply, Set.preimage_image_eq
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ Function.Injective f

Tactic:
hf.injective

Premises used: Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ Function.Injective f

Tactic:
exact hf.injective

Premises used: Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ Measurable f

Tactic:
hf.continuous.measurable

Premises used: Topology.IsClosedEmbedding.continuous, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ Measurable f

Tactic:
exact hf.continuous.measurable

Premises used: Topology.IsClosedEmbedding.continuous, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet (f '' s)

Tactic:
hf.measurableEmbedding.measurableSet_image' hs

Premises used: MeasurableEmbedding.measurableSet_image', Topology.IsClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet (f '' s)

Tactic:
exact hf.measurableEmbedding.measurableSet_image' hs

Premises used: MeasurableEmbedding.measurableSet_image', Topology.IsClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ ∀ (s : Set Ω), MeasurableSet s → MeasurableSet (f '' s)

Tactic:
fun t ht ↦ hf.measurableEmbedding.measurableSet_image' ht

Premises used: MeasurableEmbedding.measurableSet_image', Topology.IsClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ ∀ (s : Set Ω), MeasurableSet s → MeasurableSet (f '' s)

Tactic:
exact fun t ht ↦ hf.measurableEmbedding.measurableSet_image' ht

Premises used: MeasurableEmbedding.measurableSet_image', Topology.IsClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
hs
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
exact hs
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : (↑M : Type u_2)
a :
  ∀ (s : Set Ω') (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((↑(↑((fun (μ : FiniteMeasure Ω) ↦
                          (Subtype.mk (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M) (μ.map f) ⋯ :
                            { x : FiniteMeasure Ω' // x ∈ M }))
                        (M.restrict (π := fun (μ : FiniteMeasure Ω') ↦ FiniteMeasure Ω)
                          (fun (μ : FiniteMeasure Ω') ↦ comap f μ) μ)) :
                    FiniteMeasure Ω') :
                Measure Ω') :
              Measure Ω') :
            (a : Set Ω') → ℝ≥0∞)
          s :
        ℝ≥0∞)
      (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
⊢ (fun (μ : FiniteMeasure Ω) ↦
        (Subtype.mk (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M) (μ.map f) ⋯ : { x : FiniteMeasure Ω' // x ∈ M }))
      (M.restrict (π := fun (μ : FiniteMeasure Ω') ↦ FiniteMeasure Ω) (fun (μ : FiniteMeasure Ω') ↦ comap f μ) μ) =
    μ

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : (↑M : Type u_2)
s : Set Ω'
hs : MeasurableSet s
a :
  Eq (α := ℝ≥0∞)
    ((((↑(comap f (↑μ : FiniteMeasure Ω')) : Measure Ω) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map f (↑(comap f (↑μ : FiniteMeasure Ω')) : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
    (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.map_apply hf.continuous.measurable hs]

Premises used: MeasureTheory.Measure.map_apply, Topology.IsClosedEmbedding.continuous, Continuous.measurable