awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : AEMeasurable f μ
hfc : AEMeasurable f (c • μ)
⊢ Eq.{u_2 + 1} (α := Measure β)
    (((mapₗ (AEMeasurable.mk f hfc) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)
    (((mapₗ (AEMeasurable.mk f hf) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)
have pos : AEMeasurable.mk f hfc =ᶠ[ae μ] AEMeasurable.mk f hf
Tactic: apply mapₗ_congr hfc.measurable_mk hf.measurable_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : ¬AEMeasurable f μ
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
have hfc : ¬AEMeasurable f (c • μ)
Tactic: have hfc : ¬AEMeasurable f (c • μ) := by
      intro hfc
      exact hf ⟨hfc.mk f, hfc.measurable_mk, (ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s (map f μ)
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw : ∀ (hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) sorry : (a : Measure α) → Measure β) μ)),
  Eq (α := ℝ≥0∞)
    ((((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) sorry : (a : Measure α) → Measure β) μ : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [map, dif_pos hf, mapₗ, dif_pos hf.measurable_mk] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯ : (a : Measure α) → Measure β) μ)
⊢ Eq (α := ℝ≥0∞)
    ((((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯ : (a : Measure α) → Measure β) μ : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((((OuterMeasure.map (AEMeasurable.mk f hf) : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure :
          OuterMeasure β) :
        (a : Set β) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (AEMeasurable.mk f hf ⁻¹' s) : ℝ≥0∞)
Tactic: rw [liftLinear_apply₀ _ hs, measure_congr (hf.ae_eq_mk.preimage s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ toOuterMeasure (map f μ) =
    OuterMeasure.trim ((OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure)
have rw : ∀ (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((toOuterMeasure (map f μ) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure : OuterMeasure β) :
            (a : Set β) → ℝ≥0∞)
          s :
        ℝ≥0∞)
Tactic: rw [← trimmed, OuterMeasure.trim_eq_trim_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ Eq (α := Measure β) (map f μ) 0 ↔ μ = 0
have simp_rw : Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [← measure_univ_eq_zero, map_apply_of_aemeasurable hf .univ, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
simp_rw :
  Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := Measure β) (map f μ) 0 ↔ μ = 0
have simp_rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' univ) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [← measure_univ_eq_zero, map_apply_of_aemeasurable hf .univ, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
⊢ Eq.{u_2 + 1} (α := Measure β)
      (((mapₗ f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) : (a : Measure α) → Measure β)
          μ :
        Measure β)
      (0 : Measure β) ↔
    μ = 0
have rw : Eq (α := Measure β) (map f μ) 0 ↔ μ = 0
Tactic: rw [mapₗ_apply_of_measurable hf, map_eq_zero_iff hf.aemeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
rw : Eq (α := Measure β) (map f μ) 0 ↔ μ = 0
⊢ Eq.{u_2 + 1} (α := Measure β)
      (((mapₗ f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) : (a : Measure α) → Measure β)
          μ :
        Measure β)
      (0 : Measure β) ↔
    μ = 0
have rw₁ : μ = 0 ↔ μ = 0
Tactic: rw [mapₗ_apply_of_measurable hf, map_eq_zero_iff hf.aemeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : NullMeasurableSet s (map f μ)
Tactic: rw [← map_apply₀ hfm, hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : ¬AEMeasurable f μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∀ (hf : 0 = μ) {s : Set α} (hs : NullMeasurableSet s μ) (hfm : ¬AEMeasurable f μ),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_of_not_aemeasurable hfm] at hf
Cleared hypotheses: hf, s, hs, hfm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have if : ∀ (hfm : AEMeasurable f μ),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: if hfm : AEMeasurable f μ then
    rw [← map_apply₀ hfm, hf]
    rwa [hf]
  else
    rw [map_of_not_aemeasurable hfm] at hf
    simp [← hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
if :
  ∀ (hfm : AEMeasurable f μ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have if₁ : ∀ (hfm : ¬AEMeasurable f μ),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: if hfm : AEMeasurable f μ then
    rw [← map_apply₀ hfm, hf]
    rwa [hf]
  else
    rw [map_of_not_aemeasurable hfm] at hf
    simp [← hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' toMeasurable (map f μ) s) : ℝ≥0∞)
have h : s ⊆ toMeasurable (map f μ) s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f
have pos : ∀ (h : AEMeasurable f μ), ∀ᵐ (x : β) ∂map f μ, x ∈ range f
Tactic: by_cases h : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
pos : ∀ (h : AEMeasurable f μ), ∀ᵐ (x : β) ∂map f μ, x ∈ range f
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f
have neg : ∀ (h : ¬AEMeasurable f μ), ∀ᵐ (x : β) ∂map f μ, x ∈ range f
Tactic: by_cases h : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ range f ∈ ae (F := Measure β) (map f μ)
have pos : f ⁻¹' range f ∈ ae μ
Tactic: rw [mem_ae_map_iff h hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ f ⁻¹' range f ∈ ae μ
have pos : ∀ (a : α), a ∈ f ⁻¹' range f
Tactic: filter_upwards using mem_range_self
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: refine le_antisymm ?_ (le_map_apply hf.measurable.aemeasurable s)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
⊢ LE.le (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have htm : MeasurableSet t
Tactic: have htm : MeasurableSet t :=
    (hf.measurableSet_image.2 <| measurableSet_toMeasurable _ _).union
      hf.measurableSet_range.compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
⊢ s ⊆ t
have rw : f '' f ⁻¹' s ⊆ f '' toMeasurable μ (f ⁻¹' s)
Tactic: rw [subset_union_compl_iff_inter_subset, ← image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
⊢ LE.le (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have hst : s ⊆ t
Tactic: have hst : s ⊆ t := by
    rw [subset_union_compl_iff_inter_subset, ← image_preimage_eq_inter_range]
    exact image_mono (subset_toMeasurable _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
⊢ f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
have rw : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ f ⁻¹' (range f)ᶜ = toMeasurable μ (f ⁻¹' s)
Tactic: rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      hf.injective.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
rw : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ f ⁻¹' (range f)ᶜ = toMeasurable μ (f ⁻¹' s)
⊢ f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
have rw₁ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ (f ⁻¹' range f)ᶜ = toMeasurable μ (f ⁻¹' s)
Tactic: rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      hf.injective.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
rw : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ f ⁻¹' (range f)ᶜ = toMeasurable μ (f ⁻¹' s)
rw₁ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ (f ⁻¹' range f)ᶜ = toMeasurable μ (f ⁻¹' s)
⊢ f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
have rw₂ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ univᶜ = toMeasurable μ (f ⁻¹' s)
Tactic: rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      hf.injective.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
rw : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ f ⁻¹' (range f)ᶜ = toMeasurable μ (f ⁻¹' s)
rw₁ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ (f ⁻¹' range f)ᶜ = toMeasurable μ (f ⁻¹' s)
rw₂ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ univᶜ = toMeasurable μ (f ⁻¹' s)
⊢ f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
have rw₃ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ ∅ = toMeasurable μ (f ⁻¹' s)
Tactic: rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      hf.injective.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
rw : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ f ⁻¹' (range f)ᶜ = toMeasurable μ (f ⁻¹' s)
rw₁ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ (f ⁻¹' range f)ᶜ = toMeasurable μ (f ⁻¹' s)
rw₂ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ univᶜ = toMeasurable μ (f ⁻¹' s)
rw₃ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ ∅ = toMeasurable μ (f ⁻¹' s)
⊢ f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
have rw₄ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) = toMeasurable μ (f ⁻¹' s)
Tactic: rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      hf.injective.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
rw : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ f ⁻¹' (range f)ᶜ = toMeasurable μ (f ⁻¹' s)
rw₁ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ (f ⁻¹' range f)ᶜ = toMeasurable μ (f ⁻¹' s)
rw₂ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ univᶜ = toMeasurable μ (f ⁻¹' s)
rw₃ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ ∅ = toMeasurable μ (f ⁻¹' s)
rw₄ : f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) = toMeasurable μ (f ⁻¹' s)
⊢ f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
have rw₅ : toMeasurable μ (f ⁻¹' s) = toMeasurable μ (f ⁻¹' s)
Tactic: rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      hf.injective.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
⊢ LE.le (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
Tactic: have hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s) := by
    rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      hf.injective.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [map_apply hf.measurable htm, hft, measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (f ⁻¹' s)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [map_apply hf.measurable htm, hft, measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (f ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [map_apply hf.measurable htm, hft, measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
⊢ LE.le (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have f₁ : LE.le (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: calc
    μ.map f s ≤ μ.map f t := by gcongr
    _ = μ (f ⁻¹' s) := by rw [map_apply hf.measurable htm, hft, measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
f₁ :
  LE.le (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have f₂ : Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: calc
    μ.map f s ≤ μ.map f t := by gcongr
    _ = μ (f ⁻¹' s) := by rw [map_apply hf.measurable htm, hft, measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
h : Eq (α := Measure β) (map f μ) (map f ν)
⊢ μ = ν
have h₁ : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
h : Eq (α := Measure β) (map f μ) (map f ν)
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
  (((map f ν : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
Tactic: rw [← Set.preimage_image_eq s hf.injective, ← hf.map_apply, ← hf.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
e : α ≃ᵐ β
μ₁ μ₂ : Measure α
hμ : Eq.{u_2 + 1} (α := Measure β) (map (⇑e : (a : α) → β) μ₁) (map (⇑e : (a : α) → β) μ₂)
⊢ μ₁ = μ₂
have hμ₁ : Eq.{u_1 + 1} (α := Measure α) (map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) μ₁))
  (map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) μ₂))
Tactic: apply_fun Measure.map e.symm at hμ
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
ν : Measure β
e : α ≃ᵐ β
⊢ map (⇑e : (a : α) → β) μ = ν ↔ μ = map (⇑e.symm : (a : β) → α) ν
have rw : map (⇑e : (a : α) → β) μ = ν ↔
  Eq.{u_2 + 1} (α := Measure β) (map (⇑e : (a : α) → β) μ)
    (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) ν))
Tactic: rw [← (map_measurableEquiv_injective e).eq_iff, map_map_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
ν : Measure β
e : α ≃ᵐ β
rw :
  map (⇑e : (a : α) → β) μ = ν ↔
    Eq.{u_2 + 1} (α := Measure β) (map (⇑e : (a : α) → β) μ)
      (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) ν))
⊢ map (⇑e : (a : α) → β) μ = ν ↔ μ = map (⇑e.symm : (a : β) → α) ν
have rw₁ : map (⇑e : (a : α) → β) μ = ν ↔ map (⇑e : (a : α) → β) μ = ν
Tactic: rw [← (map_measurableEquiv_injective e).eq_iff, map_map_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
⊢ Filter.map (⇑f : (a : α) → β) (ae μ) = ae (F := Measure β) (map (⇑f : (a : α) → β) μ)
have h : ∀ (s : Set β),
  Membership.mem (γ := Filter β) (Filter.map (⇑f : (a : α) → β) (ae μ)) s ↔
    s ∈ ae (F := Measure β) (map (⇑f : (a : α) → β) μ)
Tactic: ext s