awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ map (fun (x : α) ↦ x) μ = μ

Tactic:
map_id

Premises used: MeasureTheory.Measure.map_id
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : Measurable g
hf : Measurable f
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map g (map f μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [hf, hg, hs, hg hs, hg.comp hf, ← preimage_comp]

Premises used: Measurable.comp, Set.preimage_comp
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
f : α → β
h : μ ≤ ν
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((map f ν : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [hf.aemeasurable, hs, h _]

Premises used: Measurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
h : s ⊆ toMeasurable (map f μ) s
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' toMeasurable (map f μ) s) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
⊢ s ⊆ toMeasurable (map f μ) s

Tactic:
apply subset_toMeasurable

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)

Tactic:
(measure_mono (subset_preimage_image f s)).trans (le_map_apply hf _)

Premises used: MeasureTheory.Measure.le_map_apply, MeasureTheory.measure_mono, LE.le.trans, Set.subset_preimage_image
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
nonpos_iff_eq_zero.mp <| (le_map_apply hf s).trans_eq hs

Premises used: LE.le.trans_eq, MeasureTheory.Measure.le_map_apply, Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ Tendsto f (ae μ) (ae (F := Measure β) (map f μ))

Tactic:
fun _ hs => preimage_null_of_map_null hf hs

Premises used: Set.Mem, setOf, Set.preimage, Filter.Tendsto, MeasureTheory.Measure.preimage_null_of_map_null, Not
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : MeasurableSet s
⊢ s ∈ ae (F := Measure β) (map f μ) ↔ f ⁻¹' s ∈ ae μ

Tactic:
simp only [mem_ae_iff, map_apply_of_aemeasurable hf hs.compl, preimage_compl]

Premises used: MeasurableSet.compl, MeasureTheory.Measure.map_apply_of_aemeasurable, MeasureTheory.mem_ae_iff, Set.preimage_compl
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : s ∈ ae (F := Measure β) (map f μ)
⊢ f ⁻¹' s ∈ ae μ

Tactic:
(tendsto_ae_map hf).eventually hs

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.Measure.tendsto_ae_map, Set.preimage, Filter.Tendsto.eventually
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
p : β → Prop
hp : MeasurableSet.{u_2} (α := β) {x : β | p x}
⊢ (∀ᵐ (y : β) ∂map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ, p (f x)

Tactic:
mem_ae_map_iff hf hp

Premises used: MeasureTheory.mem_ae_map_iff, Set.Mem, Filter.Eventually, setOf, Set.preimage
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
p : β → Prop
h : ∀ᵐ (y : β) ∂map f μ, p y
⊢ ∀ᵐ (x : α) ∂μ, p (f x)

Tactic:
mem_ae_of_mem_ae_map hf h

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.mem_ae_of_mem_ae_map, Set.preimage
-- Module: Mathlib.MeasureTheory.Measure.Map
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
neg : ∀ (h : ¬AEMeasurable f μ), ∀ᵐ (x : β) ∂map f μ, x ∈ range f
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f

Tactic:
by_cases h : AEMeasurable f μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
pos : f ⁻¹' range f ∈ ae μ
⊢ range f ∈ ae (F := Measure β) (map f μ)

Tactic:
rw [mem_ae_map_iff h hf]

Premises used: MeasureTheory.mem_ae_map_iff
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ ∀ (a : α), a ∈ f ⁻¹' range f

Tactic:
mem_range_self

Premises used: Set.mem_range_self, Set.Mem, setOf, Set.preimage, Set.range
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
pos pos₁ : ∀ (a : α), a ∈ f ⁻¹' range f
⊢ f ⁻¹' range f ∈ ae μ

Tactic:
filter_upwards using mem_range_self

Premises used: Set.mem_range_self
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : ¬AEMeasurable f μ
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f

Tactic:
simp [map_of_not_aemeasurable h]

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
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∞)

Tactic:
le_antisymm ?_ (le_map_apply hf.measurable.aemeasurable s)

Premises used: Measurable.aemeasurable, le_antisymm, MeasureTheory.Measure.le_map_apply, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
refine :
  LE.le (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥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)

Premises used: Measurable.aemeasurable, le_antisymm, MeasureTheory.Measure.le_map_apply, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Measure.Map
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)ᶜ
⊢ MeasurableSet t

Tactic:
have htm : MeasurableSet t :=
    (hf.measurableSet_image.2 <| measurableSet_toMeasurable _ _).union
      hf.measurableSet_range.compl
-- Module: Mathlib.MeasureTheory.Measure.Map
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
rw : f '' f ⁻¹' s ⊆ f '' toMeasurable μ (f ⁻¹' s)
⊢ s ⊆ t

Tactic:
rw [subset_union_compl_iff_inter_subset, ← image_preimage_eq_inter_range]

Premises used: Set.subset_union_compl_iff_inter_subset, Set.image_preimage_eq_inter_range
-- Module: Mathlib.MeasureTheory.Measure.Map
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
⊢ f '' f ⁻¹' s ⊆ f '' toMeasurable μ (f ⁻¹' s)

Tactic:
image_mono (subset_toMeasurable _ _)

Premises used: Set.image_mono, MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
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
⊢ f '' f ⁻¹' s ⊆ f '' toMeasurable μ (f ⁻¹' s)

Tactic:
exact image_mono (subset_toMeasurable _ _)

Premises used: Set.image_mono, MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
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

Tactic:
have hst : s ⊆ t := by
    rw [subset_union_compl_iff_inter_subset, ← image_preimage_eq_inter_range]
    exact image_mono (subset_toMeasurable _ _)
-- Module: Mathlib.MeasureTheory.Measure.Map
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)
rw₅ rw₆ : toMeasurable μ (f ⁻¹' s) = toMeasurable μ (f ⁻¹' s)
⊢ f ⁻¹' t = toMeasurable μ (f ⁻¹' s)

Tactic:
rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      hf.injective.preimage_image]

Premises used: Set.union_empty, Set.preimage_range, Set.compl_univ, Set.preimage_union, MeasurableEmbedding.injective, Function.Injective.preimage_image, Set.preimage_compl
-- Module: Mathlib.MeasureTheory.Measure.Map
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)

Tactic:
have hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s) := by
    rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      hf.injective.preimage_image]
-- Module: Mathlib.MeasureTheory.Measure.Map
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∞)
    (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Map
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∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (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∞)

Tactic:
rw [map_apply hf.measurable htm, hft, measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
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∞)
f₂ : Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥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]

Premises used: Set.preimage, MeasureTheory.Measure.map, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
h : Eq (α := Measure β) (map f μ) (map f ν)
h₁ :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Map
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
h₁ :
  Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((map f ν : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← Set.preimage_image_eq s hf.injective, ← hf.map_apply, ← hf.map_apply]

Premises used: MeasurableEmbedding.injective, MeasurableEmbedding.map_apply, Set.preimage_image_eq
-- Module: Mathlib.MeasureTheory.Measure.Map
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∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((map f ν : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α ≃ᵐ β
s : Set β
⊢ Eq (α := ℝ≥0∞) (((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' s) : ℝ≥0∞)

Tactic:
f.measurableEmbedding.map_apply _ _

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.map_apply
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) μ) = μ

Tactic:
simp [map_map e.symm.measurable e.measurable]

Premises used: MeasurableEquiv.symm, MeasurableEquiv.measurable, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
ν : Measure β
e : α ≃ᵐ β
⊢ map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) ν) = ν

Tactic:
simp [map_map e.measurable e.symm.measurable]

Premises used: MeasurableEquiv.symm, MeasurableEquiv.measurable, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Measure.Map
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 : α) → β) μ₂)
⊢ 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μ

Premises used: MeasurableEquiv.symm, MeasureTheory.Measure.map, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
e : α ≃ᵐ β
μ₁ μ₂ : Measure α
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:
simpa [map_symm_map e] using hμ

Premises used: MeasurableEquiv.map_symm_map
-- Module: Mathlib.MeasureTheory.Measure.Map
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 : β) → α) ν))
rw₁ rw₂ : map (⇑e : (a : α) → β) μ = ν ↔ map (⇑e : (a : α) → β) μ = ν
⊢ map (⇑e : (a : α) → β) μ = ν ↔ μ = map (⇑e.symm : (a : β) → α) ν

Tactic:
rw [← (map_measurableEquiv_injective e).eq_iff, map_map_symm]

Premises used: Function.Injective.eq_iff, MeasurableEquiv.map_map_symm, MeasurableEquiv.map_measurableEquiv_injective
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
h :
  ∀ (s : Set β),
    Membership.mem (γ := Filter β) (Filter.map (⇑f : (a : α) → β) (ae μ)) s ↔
      s ∈ ae (F := Measure β) (map (⇑f : (a : α) → β) μ)
⊢ Filter.map (⇑f : (a : α) → β) (ae μ) = ae (F := Measure β) (map (⇑f : (a : α) → β) μ)

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
s : Set β
h : (⇑f : (a : α) → β) ⁻¹' s ∈ ae μ ↔ s ∈ ae (F := Measure β) (map (⇑f : (a : α) → β) μ)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) (((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) (((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Membership.mem (γ := Filter β) (Filter.map (⇑f : (a : α) → β) (ae μ)) s ↔
    s ∈ ae (F := Measure β) (map (⇑f : (a : α) → β) μ)

Tactic:
simp_rw [mem_map, mem_ae_iff, ← preimage_compl, f.map_apply]

Premises used: MeasurableEquiv.map_apply, MeasureTheory.mem_ae_iff, Set.preimage_compl, Filter.mem_map
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ (ae μ).IsMeasurablyGenerated

Tactic:
⟨fun _s hs =>
    let ⟨t, hst, htm, htμ⟩ := exists_measurable_superset_of_null hs
    ⟨tᶜ, compl_mem_ae_iff.2 htμ, htm.compl, compl_subset_comm.1 hst⟩⟩

Premises used: MeasureTheory.ae, Iff.mpr, MeasurableSet, Compl.compl, Membership.mem, Exists, Set.compl_subset_comm, HasSubset.Subset, MeasurableSet.compl, And, _private.0.MeasureTheory.ae_isMeasurablyGenerated.match_1, And.intro, Exists.intro, Iff.mp, Filter.IsMeasurablyGenerated.mk, MeasureTheory.exists_measurable_superset_of_null, MeasureTheory.compl_mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : LinearOrder α
a b : α
P : α → Prop
⊢ (∀ᵐ (x : α) ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ (x : α) ∂μ, x ∈ Ioc a b → P x) ∧ ∀ᵐ (x : α) ∂μ, x ∈ Ioc b a → P x

Tactic:
simp only [uIoc_eq_union, mem_union, or_imp, eventually_and]

Premises used: Set.mem_union, Filter.eventually_and, or_imp, Set.uIoc_eq_union
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
hd : Disjoint s₁ s₂
h : MeasurableSet s₂
⊢ (μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)

Tactic:
measure_union₀ h.nullMeasurableSet hd.aedisjoint

Premises used: MeasurableSet.nullMeasurableSet, Disjoint.aedisjoint, MeasureTheory.measure_union₀
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
hd : Disjoint s₁ s₂
h : MeasurableSet s₁
⊢ (μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)

Tactic:
measure_union₀' h.nullMeasurableSet hd.aedisjoint

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measure_union₀', Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
measure_inter_add_diff₀ _ ht.nullMeasurableSet

Premises used: MeasureTheory.measure_inter_add_diff₀, MeasurableSet.nullMeasurableSet
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
(add_comm _ _).trans (measure_inter_add_diff s ht)

Premises used: add_comm, MeasureTheory.measure_inter_add_diff, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
contrapose! :
  ∀ (hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
contrapose! hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
((measure_mono (subset_diff_union s t)).trans_lt
    ((measure_union_le _ _).trans_lt (ENNReal.add_lt_top.2 ⟨hs.lt_top, ht.lt_top⟩))).ne

Premises used: Iff.mpr, Ne.lt_top, And.intro, MeasureTheory.measure_mono, Set.subset_diff_union, ENNReal.add_lt_top, LE.le.trans_lt, MeasureTheory.measure_union_le, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ((measure_mono (subset_diff_union s t)).trans_lt
    ((measure_union_le _ _).trans_lt (ENNReal.add_lt_top.2 ⟨hs.lt_top, ht.lt_top⟩))).ne

Premises used: Iff.mpr, Ne.lt_top, And.intro, MeasureTheory.measure_mono, Set.subset_diff_union, ENNReal.add_lt_top, LE.le.trans_lt, MeasureTheory.measure_union_le, LT.lt.ne