awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
⊢ μ.trim ⋯ = μ

Tactic:
simp [Measure.trim]

Premises used: MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
rw : (μ.toMeasure ⋯).toOuterMeasure = μ.trim
rw₁ rw₂ : μ.trim = μ.trim
⊢ (μ.trim hm).toOuterMeasure = μ.trim

Tactic:
rw [Measure.trim, toMeasure_toOuterMeasure (ms := m)]

Premises used: MeasureTheory.Measure.trim, MeasureTheory.toMeasure_toOuterMeasure
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
hm : m ≤ m0
⊢ Measure.trim 0 hm = 0

Tactic:
simp [Measure.trim, @OuterMeasure.toMeasure_zero _ m]

Premises used: MeasureTheory.Measure.trim, MeasureTheory.OuterMeasure.toMeasure_zero
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((μ.toMeasure ⋯ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.trim, toMeasure_apply (ms := m) _ _ hs, Measure.coe_toOuterMeasure]

Premises used: MeasureTheory.Measure.trim, MeasureTheory.Measure.coe_toOuterMeasure, MeasureTheory.toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.toMeasure ⋯ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
@le_toMeasure_apply _ m _ _ _

Premises used: MeasureTheory.le_toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.toMeasure ⋯ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact @le_toMeasure_apply _ m _ _ _

Premises used: MeasureTheory.le_toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
⊢ μ.trim hm = Measure.map id μ

Tactic:
@Measure.ext α m _ _ (fun s hs ↦ ?_)

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
refine :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map id μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.trim hm = Measure.map id μ

Tactic:
refine @Measure.ext α m _ _ (fun s hs ↦ ?_)

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' s) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' s) : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map id μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.map_apply (measurable_id'' hm) hs, trim_measurableSet_eq hm hs, Set.preimage_id]

Premises used: MeasureTheory.Measure.map_apply, Set.preimage_id, MeasureTheory.trim_measurableSet_eq, measurable_id''
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((Measure.map f (μ.trim ⋯) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure β) (Measure.map f (μ.trim ⋯)) (Measure.map f μ)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
h : MeasurableSet (f ⁻¹' s)
rw : Measurable f
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (μ.trim ⋯) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.map_apply hf hs, Measure.map_apply _ hs, trim_measurableSet_eq]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.trim_measurableSet_eq
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
⟨s, hs, rfl⟩

Premises used: MeasurableSet, And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
exact ⟨s, hs, rfl⟩
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable f

Tactic:
Measurable.of_comap_le le_rfl

Premises used: le_rfl, Measurable.of_comap_le
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable f

Tactic:
exact Measurable.of_comap_le le_rfl

Premises used: le_rfl, Measurable.of_comap_le
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((Measure.map f (μ.trim ⋯) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← map_trim_comap hf, Measure.map_apply (Measurable.of_comap_le le_rfl) hs]

Premises used: le_rfl, MeasureTheory.Measure.map_apply, Measurable.of_comap_le, MeasureTheory.map_trim_comap
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
p : β → Prop
hp : MeasurableSet.{u_2} (α := β) {x : β | p x}
rw : (∀ᵐ (y : β) ∂Measure.map f (μ.trim ⋯), p y) ↔ ∀ᵐ (x : α) ∂μ.trim ⋯, p (f x)
rw₁ rw₂ : (∀ᵐ (x : α) ∂μ.trim ⋯, p (f x)) ↔ ∀ᵐ (x : α) ∂μ.trim ⋯, p (f x)
⊢ (∀ᵐ (y : β) ∂Measure.map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ.trim ⋯, p (f x)

Tactic:
rw [← map_trim_comap hf, ae_map_iff (Measurable.of_comap_le le_rfl).aemeasurable hp]

Premises used: le_rfl, Measurable.aemeasurable, Measurable.of_comap_le, MeasureTheory.ae_map_iff, MeasureTheory.map_trim_comap
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((μ + ν).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.trim hm + ν.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [trim_measurableSet_eq hm hs]

Premises used: MeasureTheory.trim_measurableSet_eq
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
h : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
grw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
grw₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
grw₂ grw₃ : LE.le (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
grw [← nonpos_iff_eq_zero, ← h, le_trim hm]

Premises used: MeasureTheory.le_trim, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs rwa rwa₁ rwa₂ rwa₃ : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (toMeasurable (μ.trim hm) s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rwa [@measure_toMeasurable _ m]

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
hm : m ≤ m0
μ : Measure α
P : α → Prop
h : ∀ᵐ (x : α) ∂μ.trim hm, P x
⊢ ∀ᵐ (x : α) ∂μ, P x

Tactic:
measure_eq_zero_of_trim_eq_zero hm h

Premises used: Set.Mem, MeasureTheory.measure_eq_zero_of_trim_eq_zero, Filter.Eventually, setOf
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_3
hm : m ≤ m0
f₁ f₂ : α → E
h12 : f₁ =ᶠ[ae (μ.trim hm)] f₂
⊢ f₁ =ᶠ[ae μ] f₂

Tactic:
measure_eq_zero_of_trim_eq_zero hm h12

Premises used: Set.Mem, MeasureTheory.measure_eq_zero_of_trim_eq_zero, Filter.Eventually, setOf, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : LE E
hm : m ≤ m0
f₁ f₂ : α → E
h12 : f₁ ≤ᶠ[ae (μ.trim hm)] f₂
⊢ f₁ ≤ᶠ[ae μ] f₂

Tactic:
measure_eq_zero_of_trim_eq_zero hm h12

Premises used: Set.Mem, MeasureTheory.measure_eq_zero_of_trim_eq_zero, Filter.Eventually, setOf, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
⊢ (μ.trim hm₂).trim hm₁₂ = μ.trim ⋯

Tactic:
@Measure.ext _ m₁ _ _ (fun t ht => ?_)

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
refine :
  ∀ (t : Set α) (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞) (((μ.trim hm₂).trim hm₁₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ.trim hm₂).trim hm₁₂ = μ.trim ⋯

Tactic:
refine @Measure.ext _ m₁ _ _ (fun t ht => ?_)

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
t : Set α
ht : MeasurableSet t
rw : Eq (α := ℝ≥0∞) ((μ.trim hm₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ.trim hm₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.trim hm₂).trim hm₁₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [trim_measurableSet_eq hm₁₂ ht, trim_measurableSet_eq (hm₁₂.trans hm₂) ht,
    trim_measurableSet_eq hm₂ (hm₁₂ t ht)]

Premises used: MeasureTheory.trim_measurableSet_eq, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
⊢ (μ.trim hm).restrict s = (μ.restrict s).trim hm

Tactic:
@Measure.ext _ m _ _ (fun t ht => ?_)

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
refine :
  ∀ (t : Set α) (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞) (((μ.trim hm).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      (((μ.restrict s).trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ.trim hm).restrict s = (μ.restrict s).trim hm

Tactic:
refine @Measure.ext _ m _ _ (fun t ht => ?_)

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
rw :
  Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (((μ.restrict s).trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₃ rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.trim hm).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [@Measure.restrict_apply α m _ _ _ ht, trim_measurableSet_eq hm ht,
    Measure.restrict_apply (hm t ht),
    trim_measurableSet_eq hm (@MeasurableSet.inter α m t s ht hs)]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.trim_measurableSet_eq, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
β : Type u_2
m m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
s : Set α
hm : m ≤ m0
inst : IsFiniteMeasure μ
rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [trim_measurableSet_eq hm (@MeasurableSet.univ _ m)]

Premises used: MeasureTheory.trim_measurableSet_eq, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
β : Type u_2
m m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
s : Set α
hm : m ≤ m0
inst : IsFiniteMeasure μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_lt_top _ _

Premises used: MeasureTheory.measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
β : Type u_2
m m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
s : Set α
hm : m ≤ m0
inst : IsFiniteMeasure μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_lt_top _ _

Premises used: MeasureTheory.measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
⊢ SigmaFinite (μ.trim hm)

Tactic:
⟨⟨?_⟩⟩

Premises used: Nonempty.intro, MeasureTheory.SigmaFinite.mk
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
refine : (μ.trim hm).FiniteSpanningSetsIn Set.univ
⊢ SigmaFinite (μ.trim hm)

Tactic:
refine ⟨⟨?_⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
set : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ.trim hm).FiniteSpanningSetsIn Set.univ

Tactic:
refine
    { set := spanningSets (μ.trim (hm₂.trans hm))
      set_mem := fun _ => Set.mem_univ _
      finite := fun i => ?_
      spanning := iUnion_spanningSets _ }
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
i : ℕ
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
    ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
    (((μ.trim hm).trim hm₂ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)

Tactic:
rw [@trim_measurableSet_eq α m₂ m (μ.trim hm) _ hm₂ (measurableSet_spanningSets _ _)]

Premises used: MeasureTheory.measurableSet_spanningSets, MeasureTheory.trim_measurableSet_eq
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
i : ℕ
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
    ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.trim hm).trim hm₂ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
    ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)

Tactic:
rw [@trim_trim _ _ μ _ _ hm₂ hm]

Premises used: MeasureTheory.trim_trim
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
i : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_spanningSets_lt_top _ _

Premises used: MeasureTheory.measure_spanningSets_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
i : ℕ
rw :
  Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
    (((μ.trim hm).trim hm₂ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) (((μ.trim hm).trim hm₂ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
    ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
calc
    (μ.trim hm) (spanningSets (μ.trim (hm₂.trans hm)) i) =
        ((μ.trim hm).trim hm₂) (spanningSets (μ.trim (hm₂.trans hm)) i) := by
      rw [@trim_measurableSet_eq α m₂ m (μ.trim hm) _ hm₂ (measurableSet_spanningSets _ _)]
    _ = (μ.trim (hm₂.trans hm)) (spanningSets (μ.trim (hm₂.trans hm)) i) := by
      rw [@trim_trim _ _ μ _ _ hm₂ hm]
    _ < ∞ := measure_spanningSets_lt_top _ _

Premises used: MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.Measure.trim, LE.le.trans, DFunLike.coe, MeasureTheory.spanningSets
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
rw : SigmaFinite (μ.trim ⋯)
⊢ SigmaFinite μ

Tactic:
rw [← trim_eq_self (μ := μ)]

Premises used: MeasureTheory.trim_eq_self
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
sigmaFiniteTrim_mono le_rfl hm

Premises used: le_rfl, MeasureTheory.sigmaFiniteTrim_mono
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
exact sigmaFiniteTrim_mono le_rfl hm

Premises used: le_rfl, MeasureTheory.sigmaFiniteTrim_mono
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
rw : IsFiniteMeasure (m0 := ⊥) (μ.trim ⋯) ↔ IsFiniteMeasure μ
⊢ SigmaFinite (m0 := ⊥) (μ.trim ⋯) ↔ IsFiniteMeasure μ

Tactic:
rw [sigmaFinite_bot_iff]

Premises used: MeasureTheory.sigmaFinite_bot_iff
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ IsFiniteMeasure (m0 := ⊥) (μ.trim ⋯) ↔ IsFiniteMeasure μ

Tactic:
⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩

Premises used: Iff.intro, MeasureTheory.IsFiniteMeasure.mk
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
refine_1 :
  ∀ (h : IsFiniteMeasure (m0 := ⊥) (μ.trim ⋯)), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 :
  ∀ (h : IsFiniteMeasure μ),
    LT.lt (α := ℝ≥0∞) (((μ.trim ⋯ : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure (m0 := ⊥) (μ.trim ⋯) ↔ IsFiniteMeasure μ

Tactic:
refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (m0 := ⊥) (μ.trim ⋯)
⊢ LT.lt (α := ℝ≥0∞) (((μ.trim ⋯ : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have h_univ := h.measure_univ_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have h_univ := h.measure_univ_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (m0 := ⊥) (μ.trim ⋯)
h_univ : LT.lt (α := ℝ≥0∞) (((μ.trim ⋯ : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 refine_1₁ refine_1₂ refine_1₃ :
  ∀ (h_univ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [trim_measurableSet_eq bot_le MeasurableSet.univ] at h_univ

Premises used: MeasureTheory.trim_measurableSet_eq, bot_le, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
h_univ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 refine_2₁ refine_2₂ refine_2₃ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((μ.trim ⋯ : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [trim_measurableSet_eq bot_le MeasurableSet.univ]

Premises used: MeasureTheory.trim_measurableSet_eq, bot_le, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
⊢ μ.trim hm ≪ ν.trim hm

Tactic:
Measure.AbsolutelyContinuous.mk (fun s hs hsν ↦ ?_)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
refine :
  ∀ (s : Set α) (hs : MeasurableSet s) (hsν : Eq (α := ℝ≥0∞) ((ν.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.trim hm ≪ ν.trim hm

Tactic:
refine Measure.AbsolutelyContinuous.mk (fun s hs hsν ↦ ?_)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
hsν : Eq (α := ℝ≥0∞) ((ν.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  ∀ (hsν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [trim_measurableSet_eq hm hs] at hsν ⊢

Premises used: MeasureTheory.trim_measurableSet_eq
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
hsν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hμν hsν
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
hsν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact hμν hsν
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_3
β : Type u_4
m m0 : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace β
inst_1 : MeasurableEq β
hm : m ≤ m0
f g : α → β
hf : Measurable f
hg : Measurable g
hfg : f =ᶠ[ae μ] g
rwa : MeasurableSet.{u_3} (α := α) {a : α | ¬f a = g a}
⊢ f =ᶠ[ae (μ.trim hm)] g

Tactic:
rwa [Filter.EventuallyEq, ae_iff, trim_measurableSet_eq hm _]

Premises used: Filter.EventuallyEq, MeasureTheory.ae_iff, MeasureTheory.trim_measurableSet_eq