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 : 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)} μ
⊢ Tendsto (β := FiniteMeasure Ω) (fun (μ : FiniteMeasure Ω') ↦ comap f μ)
    (𝓝[{μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}] μ) (𝓝 (comap f μ))
have 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))
Tactic: rw [tendsto_iff_forall_integral_tendsto]
-- 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 : 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 : Ω →ᵇ ℝ
⊢ 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))
have 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))
Tactic: obtain ⟨g', -, hg'⟩ : ∃ g' : Ω' →ᵇ ℝ, ‖g'‖ = ‖g‖ ∧ g' ∘ f = g :=
    exists_extension_norm_eq_of_isClosedEmbedding g hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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 : Ω) → ℝ)
⊢ 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))
have 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']
-- 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 : 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) : ℝ)
⊢ 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))
have 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 Ω')))
Tactic: simp only [comap, toMeasure_mk, A, ← MeasurableEmbedding.integral_map hf.measurableEmbedding,
    MeasurableEmbedding.map_comap hf.measurableEmbedding]
-- 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 : 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 Ω'))
have e_μ : (↑ν : Measure Ω').restrict (range f) = (↑ν : Measure Ω')
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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)
⊢ (↑ν : Measure Ω').restrict (range f) = (↑ν : Measure Ω')
have hν₁ : Eq (α := ℝ≥0∞) (((↑ν : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (range f)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [null_iff_toMeasure_null] at hν
Cleared hypotheses: hν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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) : ℝ)
⊢ 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 Ω')))
have 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 Ω'))
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ν
-- 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 : 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 (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 Ω')))
have 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 Ω')))
Tactic: rw [B hμ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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 Ω')))
have A₁ : 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 _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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 (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 Ω')))
have 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 Ω')))
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
-- 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 : 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 Ω')))
⊢ 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 Ω')))
have 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 Ω')
Tactic: apply Tendsto.congr' _ this
-- 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 : 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 Ω' | 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 Ω')
have 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
Tactic: filter_upwards [self_mem_nhdsWithin] with ν hν using (B hν).symm
-- 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 : 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
⊢ (𝓝[{μ : 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 Ω')
have h₁ : ∀ (a : FiniteMeasure Ω'),
  Eq (α := ℝ≥0) ((a : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0) →
    Eq (α := ℝ) (∫ (y : Ω'), (g' : (a : Ω') → ℝ) y ∂(↑a : Measure Ω'))
      (∫ (y : Ω') in range f, (g' : (a : Ω') → ℝ) y ∂(↑a : Measure Ω'))
Tactic: filter_upwards [self_mem_nhdsWithin] with ν hν using (B hν).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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 : FiniteMeasure Ω') : (a : Set Ω') → ℝ≥0) A : ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) (f ⁻¹' A) : ℝ≥0)
have key : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
f_mble : Measurable f
ν₁ ν₂ : FiniteMeasure Ω
⊢ (ν₁ + ν₂).map f = HAdd.hAdd (α := FiniteMeasure Ω') (ν₁.map f) (ν₂.map f)
have 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∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
c : ℝ≥0
ν : FiniteMeasure Ω
⊢ (c • ν).map f = HSMul.hSMul (β := FiniteMeasure Ω') c (ν.map f)
have 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∞)
Tactic: ext s _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
⊢ mass (μ.map f) ≤ μ.mass
have simp : LE.le (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞)
  (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: simp only [mass, coeFn_def, toMeasure_map, ne_eq, measure_ne_top, not_false_eq_true,
    ENNReal.toNNReal_le_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
⊢ LE.le (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
have pos : ∀ (hf : AEMeasurable f (↑μ : Measure Ω)),
  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 μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞) (((Measure.map f (↑μ : Measure Ω) : Measure Ω') : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
have neg : ∀ (hf : ¬AEMeasurable f (↑μ : Measure Ω)),
  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 μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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∞)
have pos : LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' univ) : ℝ≥0∞)
  (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [Measure.map_apply_of_aemeasurable hf MeasurableSet.univ]