awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
⊢ ∃ (t : Set α), MeasurableSet t ∧ t =ᵐ[μ] s ∧ f ⁻¹' t = t

Tactic:
⟨limsup (f^[·] ⁻¹' t) atTop, ?_, ?_, ?_⟩

Premises used: Nat.iterate, Filter.limsup, Filter.atTop, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
refine_1 : MeasurableSet.{u_1} (α := α) (limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop)
refine_2 : limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop =ᵐ[μ] s
refine_3 : f ⁻¹' limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop = limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop
⊢ ∃ (t : Set α), MeasurableSet t ∧ t =ᵐ[μ] s ∧ f ⁻¹' t = t

Tactic:
refine ⟨limsup (f^[·] ⁻¹' t) atTop, ?_, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
⊢ MeasurableSet.{u_1} (α := α) (limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop)

Tactic:
.measurableSet_limsup fun n ↦ h.measurable.iterate n htm

Premises used: Measurable.iterate, MeasurableSet.measurableSet_limsup, MeasureTheory.Measure.QuasiMeasurePreserving.measurable
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
⊢ MeasurableSet.{u_1} (α := α) (limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop)

Tactic:
exact .measurableSet_limsup fun n ↦ h.measurable.iterate n htm
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
⊢ f ⁻¹' t =ᵐ[μ] t

Tactic:
have : f ⁻¹' t =ᵐ[μ] t := (h.preimage_ae_eq ht.symm).trans (hs'.trans ht)
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
this : f ⁻¹' t =ᵐ[μ] t
⊢ limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop =ᵐ[μ] s

Tactic:
limsup_ae_eq_of_forall_ae_eq _ fun n ↦ .trans (h.preimage_iterate_ae_eq _ this) ht.symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_iterate_ae_eq, MeasureTheory.limsup_ae_eq_of_forall_ae_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
this : f ⁻¹' t =ᵐ[μ] t
⊢ limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop =ᵐ[μ] s

Tactic:
exact limsup_ae_eq_of_forall_ae_eq _ fun n ↦ .trans (h.preimage_iterate_ae_eq _ this) ht.symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_iterate_ae_eq, MeasureTheory.limsup_ae_eq_of_forall_ae_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
refine_3 : f ⁻¹' limsup (fun (x : ℕ) ↦ (preimage f)^[x] t) atTop = limsup (fun (x : ℕ) ↦ (preimage f)^[x] t) atTop
⊢ f ⁻¹' limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop = limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop

Tactic:
simp only [Set.preimage_iterate_eq]

Premises used: Set.preimage_iterate_eq
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
⊢ f ⁻¹' limsup (fun (x : ℕ) ↦ (preimage f)^[x] t) atTop = limsup (fun (x : ℕ) ↦ (preimage f)^[x] t) atTop

Tactic:
CompleteLatticeHom.apply_limsup_iterate (CompleteLatticeHom.setPreimage f) t

Premises used: Filter.limsSup, CompleteLatticeHom.apply_limsup_iterate, Set.Mem, setOf, CompleteLatticeHom.setPreimage, Filter.limsup, Set.preimage
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
⊢ f ⁻¹' limsup (fun (x : ℕ) ↦ (preimage f)^[x] t) atTop = limsup (fun (x : ℕ) ↦ (preimage f)^[x] t) atTop

Tactic:
exact CompleteLatticeHom.apply_limsup_iterate (CompleteLatticeHom.setPreimage f) t

Premises used: CompleteLatticeHom.apply_limsup_iterate, CompleteLatticeHom.setPreimage
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
s t : Set α
μ : Measure α
g : G
h_qmp : QuasiMeasurePreserving (fun (x : α) ↦ g⁻¹ • x) μ μ
h_ae_eq : s =ᵐ[μ] t
⊢ g • s =ᵐ[μ] g • t

Tactic:
simpa only [← preimage_smul_inv] using h_qmp.ae_eq h_ae_eq

Premises used: Set.preimage_smul_inv, MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
rw : ¬g₂ = g₁
⊢ g ≠ 1

Tactic:
rw [Ne, inv_mul_eq_one]

Premises used: Ne, inv_mul_eq_one
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ ¬g₂ = g₁

Tactic:
hg.symm

Premises used: Ne.symm
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ ¬g₂ = g₁

Tactic:
exact hg.symm

Premises used: Ne.symm
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ g ≠ 1

Tactic:
replace hg : g ≠ 1 := by
    rw [Ne, inv_mul_eq_one]
    exact hg.symm
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
rw : g • s ∩ s = (fun (x : α) ↦ g₂⁻¹ • x) '' (g₁ • s ∩ g₂ • s)
rw₁ : g • s ∩ s = g₂⁻¹ • (g₁ • s ∩ g₂ • s)
rw₂ : g • s ∩ s = g₂⁻¹ • g₁ • s ∩ g₂⁻¹ • g₂ • s
rw₃ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ g₂⁻¹ • g₂ • s
rw₄ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ (g₂⁻¹ * g₂) • s
rw₅ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ HSMul.hSMul.{u_5, u_6, u_6} (α := G) 1 s
rw₆ rw₇ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ s
⊢ (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s

Tactic:
rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
      smul_smul, inv_mul_cancel, one_smul]

Premises used: Set.image_smul, inv_mul_cancel, Set.smul_set_inter, MulAction.bijective, smul_smul, Set.preimage_eq_iff_eq_image, one_smul, Inv.inv
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
⊢ (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s

Tactic:
have : (g₂⁻¹ • ·) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s := by
    rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
      smul_smul, inv_mul_cancel, one_smul]
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
this : (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
change : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (g₁ • s ∩ g₂ • s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (AEDisjoint μ on fun (g : G) ↦ g • s) g₁ g₂

Tactic:
change μ (g₁ • s ∩ g₂ • s) = 0

Premises used: Inter.inter, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
this : (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (g₁ • s ∩ g₂ • s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
this ▸ (h_qmp g₂⁻¹).preimage_null (h_ae_disjoint g hg)

Premises used: Eq.rec, Inv.inv, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
this : (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (g₁ • s ∩ g₂ • s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact this ▸ (h_qmp g₂⁻¹).preimage_null (h_ae_disjoint g hg)
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → β
g : β → γ
hg : NullMeasurable g ν
hf : QuasiMeasurePreserving f μ ν
⊢ NullMeasurable (g ∘ f) μ

Tactic:
fun _s hs ↦ (hg hs).preimage hf

Premises used: Set.Mem, setOf, MeasureTheory.NullMeasurableSet.preimage, Set.preimage, MeasureTheory.NullMeasurable
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
h : NullMeasurableSet s μ
hle : ν ≪ μ
⊢ NullMeasurableSet s ν

Tactic:
h.preimage <| (QuasiMeasurePreserving.id μ).mono_left hle

Premises used: Set.Mem, setOf, MeasureTheory.NullMeasurableSet.preimage, Set.preimage, MeasureTheory.Measure.QuasiMeasurePreserving.id, MeasureTheory.Measure.QuasiMeasurePreserving.mono_left
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
h : NullMeasurableSet s μ
hle : ν ≤ μ
⊢ NullMeasurableSet s ν

Tactic:
h.mono_ac hle.absolutelyContinuous

Premises used: LE.le.absolutelyContinuous, MeasureTheory.NullMeasurableSet.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
c : ℝ≥0∞
⊢ NullMeasurableSet s (c • μ)

Tactic:
h.mono_ac (Measure.AbsolutelyContinuous.rfl.smul_left c)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.NullMeasurableSet.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0∞
hc : c ≠ 0
⊢ NullMeasurableSet s (c • μ) ↔ NullMeasurableSet s μ

Tactic:
⟨fun h ↦ h.mono_ac (Measure.absolutelyContinuous_smul hc), fun h ↦ h.smul_measure c⟩

Premises used: MeasureTheory.NullMeasurableSet.smul_measure, MeasureTheory.Measure.absolutelyContinuous_smul, Iff.intro, MeasureTheory.NullMeasurableSet.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → β
s t : Set β
ht : AEDisjoint ν s t
hf : QuasiMeasurePreserving f μ ν
⊢ AEDisjoint μ (f ⁻¹' s) (f ⁻¹' t)

Tactic:
hf.preimage_null ht

Premises used: Set.Mem, setOf, Set.inter, MeasureTheory.AEDisjoint, Set.preimage, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
hg : Measurable.{u_2, u_1} (α := β) (β := α) (⇑e.symm : (a : β) → α)
hf : Measurable.{u_1, u_2} (α := α) (β := β) (⇑e : (a : α) → β)
⊢ Measure.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (Measure.map (⇑e : (a : α) → β) μ) ≪ μ

Tactic:
rw [Measure.map_map, e.symm_comp_self, Measure.map_id]

Premises used: MeasureTheory.Measure.map_id, MeasurableEquiv.symm_comp_self, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measurable.{u_2, u_1} (α := β) (β := α) (⇑e.symm : (a : β) → α)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measurable.{u_1, u_2} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.real s = 0 ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.real, ENNReal.toReal_eq_zero_iff]

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
or_iff_left h

Premises used: or_iff_left
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact or_iff_left h

Premises used: or_iff_left
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s ≠ 0 ↔ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [measureReal_eq_zero_iff, h]

Premises used: MeasureTheory.measureReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := (s : Set α) → ℝ) (Measure.real (m := x) 0) 0

Tactic:
rfl

Premises used: MeasureTheory.Measure.real, ENNReal.toReal, NNReal.toReal, rfl
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
s : Set α
⊢ Measure.real (m := x) 0 s = 0

Tactic:
rfl

Premises used: MeasureTheory.Measure.real, ENNReal.toReal, NNReal.toReal, rfl
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
⊢ 0 ≤ μ.real s

Tactic:
ENNReal.toReal_nonneg

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
⊢ μ.real ∅ = 0

Tactic:
simp [Measure.real]

Premises used: MeasureTheory.Measure.real
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
inst_1 : NeZero μ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
inst_1 : NeZero μ
⊢ μ.real univ ≠ 0

Tactic:
measureReal_univ_pos.ne'

Premises used: LT.lt.ne', MeasureTheory.measureReal_univ_pos
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.ofReal (μ.real s) = (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
simp [measureReal_def, h]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
h : μ.real s ≠ 0
⊢ s.Nonempty

Tactic:
nonempty_iff_ne_empty.2 fun h' ↦ h <| h'.symm ▸ measureReal_empty

Premises used: Iff.mpr, MeasureTheory.measureReal_empty, Eq.rec, Set.nonempty_iff_ne_empty, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0∞
⊢ (c • μ).real s = c.toReal * μ.real s

Tactic:
simp [Measure.real]

Premises used: MeasureTheory.Measure.real
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0
⊢ (c • μ).real s = (↑c : ℝ) * μ.real s

Tactic:
simp [measureReal_def]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measure.real (m := inst) (map f μ) s = μ.real (f ⁻¹' s)

Tactic:
map_measureReal_apply_of_aemeasurable hf.aemeasurable hs

Premises used: Measurable.aemeasurable, MeasureTheory.map_measureReal_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₁ ⊆ s₂
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s₁ ≤ μ.real s₂

Tactic:
ENNReal.toReal_mono h₂ (measure_mono h)

Premises used: MeasureTheory.Measure.real, MeasureTheory.measure_mono, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
s : Set α
m : MeasurableSpace β
ν : Measure β
t : Set β
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s = ν.real t ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp [measureReal_def, ENNReal.toReal_eq_toReal_iff' h₁ h₂]

Premises used: ENNReal.toReal_eq_toReal_iff', MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t (μ.restrict s)
⊢ (μ.restrict s).real t = μ.real (t ∩ s)

Tactic:
simp only [measureReal_def, restrict_apply₀ ht]

Premises used: MeasureTheory.Measure.restrict_apply₀, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
⊢ (μ.restrict s).real t = μ.real (t ∩ s)

Tactic:
simp only [measureReal_def, restrict_apply ht]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
⊢ (μ.restrict s).real univ = μ.real s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ (μ.restrict s).real t = μ.real (t ∩ s)

Tactic:
simp only [measureReal_def, restrict_apply' hs]

Premises used: MeasureTheory.measureReal_def, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
simp only [restrict_apply₀' hs]

Premises used: MeasureTheory.Measure.restrict_apply₀'
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
⊢ (μ.restrict s).real s = μ.real s

Tactic:
simp [measureReal_def]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₁ ⊆ s₂
h₂ : μ.real s₂ = 0
h'₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [measureReal_eq_zero_iff h'₂] at h₂

Premises used: MeasureTheory.measureReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₁ ⊆ s₂
h₂ : μ.real s₂ = 0
h'₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
h₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [measureReal_eq_zero_iff h'₂] at h₂

Premises used: MeasureTheory.measureReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₁ ⊆ s₂
h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (0 : ℝ≥0∞)
h'₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s₁ = 0

Tactic:
simp [Measure.real, measure_mono_null h h₂]

Premises used: MeasureTheory.Measure.real, MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
inl : ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), μ.real s ≤ μ.real (s ∪ t)
inr : ∀ (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), μ.real s ≤ μ.real (s ∪ t)
⊢ μ.real s ≤ μ.real (s ∪ t)

Tactic:
rcases eq_top_or_lt_top (μ s) with hs | hs

Premises used: DFunLike.coe, eq_top_or_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s ≤ μ.real (s ∪ t)

Tactic:
simp [Measure.real, hs]

Premises used: MeasureTheory.Measure.real
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s ≤ μ.real (s ∪ t)

Tactic:
measureReal_mono subset_union_left (measure_union_lt_top hs h.lt_top).ne

Premises used: MeasureTheory.measure_union_lt_top, MeasureTheory.measureReal_mono, Set.subset_union_left, Ne.lt_top, LT.lt.ne