awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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
⊢ Tendsto (β := FiniteMeasure Ω') (fun (i : ι) ↦ (νs i).map f) L (𝓝 (ν.map f))
have 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 Ω')))
Tactic: rw [FiniteMeasure.tendsto_iff_forall_lintegral_tendsto] at lim ⊢
Cleared hypotheses: lim, f, f_cont
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 : (a : Ω') → ℝ≥0) x) : ℝ≥0∞) ∂(↑((νs i).map f) : Measure Ω')) L
    (𝓝 (∫⁻ (x : Ω'), (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞) ∂(↑(ν.map f) : Measure Ω')))
have 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 Ω)
Tactic: convert! lim (g.compContinuous ⟨f, f_cont⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω)
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω'), (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞) ∂(↑((νs i).map f) : Measure Ω')) L
    (𝓝 (∫⁻ (x : Ω'), (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞) ∂(↑(ν.map f) : Measure Ω')))
have 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 Ω)
Tactic: convert! lim (g.compContinuous ⟨f, f_cont⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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∞) ∂(↑((νs x).map f) : Measure Ω') =
    ∫⁻ (x : Ω),
      (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) x) :
        ℝ≥0∞) ∂(↑(νs x) : Measure Ω)
have h : ∫⁻ (x : Ω'),
    (↑((g : (a : Ω') → ℝ≥0) x) :
      ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsFiniteMeasure μ) (Measure.map f (↑(νs x) : Measure Ω)) sorry) :
      Measure Ω') =
  ∫⁻ (x : Ω), (↑((g : (a : Ω') → ℝ≥0) (f x)) : ℝ≥0∞) ∂(↑(νs x) : Measure Ω)
Tactic: simp only [map, compContinuous_apply, ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω)
have h : Measurable (β := ℝ≥0∞) fun (x : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞)
Tactic: refine lintegral_map ?_ f_cont.measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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∞) ∂(↑(ν.map f) : Measure Ω') =
    ∫⁻ (x : Ω),
      (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) x) :
        ℝ≥0∞) ∂(↑ν : Measure Ω)
have h : ∫⁻ (x : Ω'),
    (↑((g : (a : Ω') → ℝ≥0) x) :
      ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsFiniteMeasure μ) (Measure.map f (↑ν : Measure Ω)) sorry) :
      Measure Ω') =
  ∫⁻ (x : Ω), (↑((g : (a : Ω') → ℝ≥0) (f x)) : ℝ≥0∞) ∂(↑ν : Measure Ω)
Tactic: simp only [map, compContinuous_apply, ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω)
have h : Measurable (β := ℝ≥0∞) fun (x : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) x) : ℝ≥0∞)
Tactic: refine lintegral_map ?_ f_cont.measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (ν : FiniteMeasure Ω) ↦ ν.map f
have rw : ∀ (x : FiniteMeasure Ω), ContinuousAt.{u_1, u_2} (Y := FiniteMeasure Ω') (fun (ν : FiniteMeasure Ω) ↦ ν.map f) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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_3, u_2} (Y := FiniteMeasure Ω') fun (μ : FiniteMeasure Ω) ↦ μ.map f
have A : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω
⊢ (↑M : Type u_2)
have refine : μ.map f ∈ M
Tactic: refine ⟨μ.map f, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω
⊢ μ.map f ∈ M
have simp : Eq (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (range f)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [null_iff_toMeasure_null, mem_setOf_eq, toMeasure_map, M]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (range f)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' (range f)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Measure.map_apply hf.continuous.measurable hf.isClosed_range.isOpen_compl.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω
⊢ 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 }))
        μ) =
    μ
have 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) sorry :
                        { x : FiniteMeasure Ω' // x ∈ M }))
                    μ)) :
              Measure Ω) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f (Measure.map f (↑μ : Measure Ω)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
have h : Function.Injective f
Tactic: rw [Measure.comap_apply, Measure.map_apply, preimage_image_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f (Measure.map f (↑μ : Measure Ω)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Measurable f
Tactic: rw [Measure.comap_apply, Measure.map_apply, preimage_image_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f (Measure.map f (↑μ : Measure Ω)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : MeasurableSet (f '' s)
Tactic: rw [Measure.comap_apply, Measure.map_apply, preimage_image_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f (Measure.map f (↑μ : Measure Ω)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
have h₄ : ∀ (s : Set Ω), MeasurableSet s → MeasurableSet (f '' s)
Tactic: rw [Measure.comap_apply, Measure.map_apply, preimage_image_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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)
⊢ (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 μ) μ) =
    μ
have a : ∀ (s : Set Ω') (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((↑(↑((fun (μ : FiniteMeasure Ω) ↦
                        (Subtype.mk (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M) (μ.map f) sorry :
                          { 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∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map f (↑(comap f (↑μ : FiniteMeasure Ω')) : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
    (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
have a : Eq (α := ℝ≥0∞) ((((↑(comap f (↑μ : FiniteMeasure Ω')) : Measure Ω) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Measure.map_apply hf.continuous.measurable hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap f (↑(↑μ : FiniteMeasure Ω') : Measure Ω') : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
have a : Eq (α := ℝ≥0∞) (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
  (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Measure.comap_apply _ hf.injective, image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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∞) (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
    (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap f (↑(↑μ : FiniteMeasure Ω') : Measure Ω') : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
have a₁ : ∀ (s : Set Ω), MeasurableSet s → MeasurableSet (f '' s)
Tactic: rw [Measure.comap_apply _ hf.injective, image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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∞) (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
    (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
a₁ : ∀ (s : Set Ω), MeasurableSet s → MeasurableSet (f '' s)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap f (↑(↑μ : FiniteMeasure Ω') : Measure Ω') : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
have a₂ : MeasurableSet (f ⁻¹' s)
Tactic: rw [Measure.comap_apply _ hf.injective, image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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
⊢ Eq (α := ℝ≥0∞) (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
    (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
have a : ∀ᵐ (x : Ω') ∂(↑(↑μ : FiniteMeasure Ω') : Measure Ω'), x ∈ range f
Tactic: rw [← Measure.restrict_apply hs, Measure.restrict_eq_self_of_ae_mem]