awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
f : α → β
hf : Measurable f
⊢ map f (μ + ν) = HAdd.hAdd (α := Measure β) (map f μ) (map f ν)

Tactic:
simp [← mapₗ_apply_of_measurable hf]

Premises used: MeasureTheory.Measure.mapₗ_apply_of_measurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
pos : ∀ (hf : AEMeasurable (_m := mα) f 0), Eq (α := Measure β) (map f 0) 0
neg : ∀ (hf : ¬AEMeasurable (_m := mα) f 0), Eq (α := Measure β) (map f 0) 0
⊢ Eq (α := Measure β) (map f 0) 0

Tactic:
by_cases hf : AEMeasurable f (0 : Measure α)

Premises used: AEMeasurable, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable (_m := mα) f 0
⊢ Eq (α := Measure β) (map f 0) 0

Tactic:
simp [map, hf]

Premises used: MeasureTheory.Measure.map
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : ¬AEMeasurable (_m := mα) f 0
⊢ Eq (α := Measure β) (map f 0) 0

Tactic:
simp [map, hf]

Premises used: MeasureTheory.Measure.map
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure α
hf : ¬AEMeasurable f μ
⊢ Eq (α := Measure β) (map f μ) 0

Tactic:
simp [map, hf]

Premises used: MeasureTheory.Measure.map
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure α
hf : Ne (α := Measure β) (map f μ) 0
⊢ AEMeasurable f μ

Tactic:
not_imp_comm.1 map_of_not_aemeasurable hf

Premises used: not_imp_comm, Iff.mp, MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
pos : ∀ (hf : AEMeasurable f μ), Eq (α := Measure β) (map f μ) (map g μ)
neg : ∀ (hf : ¬AEMeasurable f μ), Eq (α := Measure β) (map f μ) (map g μ)
⊢ Eq (α := Measure β) (map f μ) (map g μ)

Tactic:
by_cases hf : AEMeasurable f μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f μ
⊢ AEMeasurable g μ

Tactic:
have hg : AEMeasurable g μ := hf.congr h
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
pos :
  Eq.{u_2 + 1} (α := Measure β)
    (((mapₗ (AEMeasurable.mk f hf) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)
    (((mapₗ (AEMeasurable.mk g hg) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)
⊢ Eq (α := Measure β) (map f μ) (map g μ)

Tactic:
simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hg]

Premises used: MeasureTheory.Measure.mapₗ_mk_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ Eq.{u_2 + 1} (α := Measure β)
    (((mapₗ (AEMeasurable.mk f hf) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)
    (((mapₗ (AEMeasurable.mk g hg) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)

Tactic:
mapₗ_congr hf.measurable_mk hg.measurable_mk (hf.ae_eq_mk.symm.trans (h.trans hg.ae_eq_mk))

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.mapₗ_congr, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ Eq.{u_2 + 1} (α := Measure β)
    (((mapₗ (AEMeasurable.mk f hf) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)
    (((mapₗ (AEMeasurable.mk g hg) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)

Tactic:
exact
      mapₗ_congr hf.measurable_mk hg.measurable_mk (hf.ae_eq_mk.symm.trans (h.trans hg.ae_eq_mk))

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.mapₗ_congr, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f μ
⊢ ¬AEMeasurable g μ

Tactic:
simpa [← aemeasurable_congr h] using hf

Premises used: aemeasurable_congr
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f μ
⊢ ¬AEMeasurable g μ

Tactic:
have hg : ¬AEMeasurable g μ := by simpa [← aemeasurable_congr h] using hf
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f μ
hg : ¬AEMeasurable g μ
⊢ Eq (α := Measure β) (map f μ) (map g μ)

Tactic:
simp [map_of_not_aemeasurable, hf, hg]

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
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∞
c : R
μ : Measure α
f : α → β
this : ∀ (c : ℝ≥0∞), map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)

Tactic:
simpa using this (c • 1)

Premises used: HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Map
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∞
c : R
μ : Measure α
f : α → β
suffices : ∀ (c : ℝ≥0∞), map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)

Tactic:
suffices ∀ c : ℝ≥0∞, (c • μ).map f = c • μ.map f by simpa using this (c • 1)
-- Module: Mathlib.MeasureTheory.Measure.Map
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∞
inl : map f (HSMul.hSMul (α := ℝ≥0∞) 0 μ) = HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) 0 (map f μ)
inr : ∀ (hc : c ≠ 0), map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.Map
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 : α → β
⊢ map f (HSMul.hSMul (α := ℝ≥0∞) 0 μ) = HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) 0 (map f μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Map
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
pos : ∀ (hf : AEMeasurable f μ), map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
neg : ∀ (hf : ¬AEMeasurable f μ), map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)

Tactic:
by_cases hf : AEMeasurable f μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
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 μ
⊢ AEMeasurable f (c • μ)

Tactic:
have hfc : AEMeasurable f (c • μ) :=
      ⟨hf.mk f, hf.measurable_mk, (ae_ennreal_smul_measure_iff hc).2 hf.ae_eq_mk⟩
-- Module: Mathlib.MeasureTheory.Measure.Map
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 • μ)
pos :
  HSMul.hSMul (β := Measure β) c
      (((mapₗ (AEMeasurable.mk f hfc) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
            (a : Measure α) → Measure β)
          μ :
        Measure β) =
    HSMul.hSMul (β := Measure β) c
      (((mapₗ (AEMeasurable.mk f hf) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
            (a : Measure α) → Measure β)
          μ :
        Measure β)
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)

Tactic:
simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hfc, map_smulₛₗ,
      RingHom.id_apply]

Premises used: RingHom.id_apply, MulActionSemiHomClass.map_smulₛₗ, MeasureTheory.Measure.mapₗ_mk_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
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 • μ)
pos :
  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 β)
⊢ HSMul.hSMul (β := Measure β) c
      (((mapₗ (AEMeasurable.mk f hfc) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
            (a : Measure α) → Measure β)
          μ :
        Measure β) =
    HSMul.hSMul (β := Measure β) c
      (((mapₗ (AEMeasurable.mk f hf) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
            (a : Measure α) → Measure β)
          μ :
        Measure β)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.Map
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 • μ)
pos : AEMeasurable.mk f hfc =ᶠ[ae μ] AEMeasurable.mk f hf
⊢ 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 β)

Tactic:
apply mapₗ_congr hfc.measurable_mk hf.measurable_mk

Premises used: MeasureTheory.Measure.mapₗ_congr, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.Map
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 • μ)
⊢ AEMeasurable.mk f hfc =ᶠ[ae μ] AEMeasurable.mk f hf

Tactic:
.trans ((ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk.symm) hf.ae_eq_mk

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.ae_ennreal_smul_measure_iff, Iff.mp, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Map
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 • μ)
⊢ AEMeasurable.mk f hfc =ᶠ[ae μ] AEMeasurable.mk f hf

Tactic:
exact .trans ((ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk.symm) hf.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.Map
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 • μ)
⊢ False

Tactic:
hf ⟨hfc.mk f, hfc.measurable_mk, (ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk⟩

Premises used: AEMeasurable.mk, MeasureTheory.Measure.ae_ennreal_smul_measure_iff, And.intro, Exists.intro, Iff.mp, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.Map
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 • μ)
⊢ False

Tactic:
exact hf ⟨hfc.mk f, hfc.measurable_mk, (ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk⟩

Premises used: AEMeasurable.mk, MeasureTheory.Measure.ae_ennreal_smul_measure_iff, And.intro, Exists.intro, Iff.mp, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.Map
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 μ
⊢ ¬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⟩
-- Module: Mathlib.MeasureTheory.Measure.Map
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 • μ)
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)

Tactic:
simp [map_of_not_aemeasurable hf, map_of_not_aemeasurable hfc]

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s (map f μ)
rw :
  ∀
    (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∞)
⊢ Eq (α := ℝ≥0∞) (((map f μ : 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 ⊢

Premises used: MeasureTheory.Measure.mapₗ, dif_pos, MeasureTheory.Measure.map, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.Map
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 β) μ)
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∞)
⊢ Eq (α := ℝ≥0∞)
    ((((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯ : (a : Measure α) → Measure β) μ : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [liftLinear_apply₀ _ hs, measure_congr (hf.ae_eq_mk.preimage s)]

Premises used: MeasureTheory.measure_congr, MeasureTheory.Measure.liftLinear_apply₀, Filter.EventuallyEq.preimage, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.Map
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∞)
    ((((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:
rfl
-- 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
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)

Tactic:
map_apply₀ hf hs.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.map_apply₀
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)

Tactic:
map_apply_of_aemeasurable hf.aemeasurable hs

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
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∞)
⊢ toOuterMeasure (map f μ) =
    OuterMeasure.trim ((OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure)

Tactic:
rw [← trimmed, OuterMeasure.trim_eq_trim_iff]

Premises used: MeasureTheory.Measure.trimmed, MeasureTheory.OuterMeasure.trim_eq_trim_iff
-- 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
⊢ Eq (α := ℝ≥0∞) ((toOuterMeasure (map f μ) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure : OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp [hf, hs]
-- Module: Mathlib.MeasureTheory.Measure.Map
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∞)
simp_rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' univ) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := Measure β) (map f μ) 0 ↔ μ = 0

Tactic:
simp_rw [← measure_univ_eq_zero, map_apply_of_aemeasurable hf .univ, preimage_univ]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable, Set.preimage_univ, MeasureTheory.Measure.measure_univ_eq_zero, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
rw : Eq (α := Measure β) (map f μ) 0 ↔ μ = 0
rw₁ rw₂ : μ = 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

Tactic:
rw [mapₗ_apply_of_measurable hf, map_eq_zero_iff hf.aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.map_eq_zero_iff, MeasureTheory.Measure.mapₗ_apply_of_measurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
rw : NullMeasurableSet s (map f μ)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← map_apply₀ hfm, hf]

Premises used: MeasureTheory.Measure.map_apply₀
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
rwa rwa₁ rwa₂ rwa₃ : NullMeasurableSet s μ
⊢ NullMeasurableSet s (map f μ)

Tactic:
rwa [hf]
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : ¬AEMeasurable f μ
rw :
  ∀ (hf : 0 = μ) {s : Set α} (hs : NullMeasurableSet s μ) (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∞)

Tactic:
rw [map_of_not_aemeasurable hfm] at hf

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : 0 = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : ¬AEMeasurable f μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [← hf]
-- Module: Mathlib.MeasureTheory.Measure.Map
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∞)
if₁ :
  ∀ (hfm : ¬AEMeasurable f μ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
if₂ :
  ∀ (hfm : AEMeasurable f μ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
if₃ 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∞)

Tactic:
if hfm : AEMeasurable f μ then
    rw [← map_apply₀ hfm, hf]
    rwa [hf]
  else
    rw [map_of_not_aemeasurable hfm] at hf
    simp [← hf]

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ Ne (α := Measure β) (map f μ) 0 ↔ μ ≠ 0

Tactic:
(map_eq_zero_iff hf).not

Premises used: MeasureTheory.Measure.map_eq_zero_iff, Iff.not
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
⊢ Ne.{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

Tactic:
(mapₗ_eq_zero_iff hf).not

Premises used: Iff.not, MeasureTheory.Measure.mapₗ_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ map id μ = μ

Tactic:
ext fun _ => map_apply measurable_id

Premises used: MeasureTheory.Measure.map_apply, measurable_id, MeasureTheory.Measure.ext