awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : NoMaxOrder α
inst_2 : IsCountablyGenerated.{u_1} (α := α) atTop
μ : Measure α
a : α
rw :
  Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ico a x) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : α), Ico a b)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ico a x) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (Ici a)) : Filter ℝ≥0∞)

Tactic:
rw [← iUnion_Ico_right]

Premises used: Set.iUnion_Ico_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : NoMaxOrder α
inst_2 : IsCountablyGenerated.{u_1} (α := α) atTop
μ : Measure α
a : α
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ico a x) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : α), Ico a b)) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_iUnion_atTop (antitone_const.Ico monotone_id)

Premises used: MeasureTheory.tendsto_measure_iUnion_atTop, Antitone.Ico, monotone_id, antitone_const
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : NoMaxOrder α
inst_2 : IsCountablyGenerated.{u_1} (α := α) atTop
μ : Measure α
a : α
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ico a x) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : α), Ico a b)) : Filter ℝ≥0∞)

Tactic:
exact tendsto_measure_iUnion_atTop (antitone_const.Ico monotone_id)

Premises used: MeasureTheory.tendsto_measure_iUnion_atTop, Antitone.Ico, monotone_id, antitone_const
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : NoMinOrder α
inst_2 : IsCountablyGenerated.{u_1} (α := α) atBot
μ : Measure α
a : α
rw :
  Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ioc x a) : ℝ≥0∞)) atBot
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : α), Ioc b a)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ioc x a) : ℝ≥0∞)) atBot
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (Iic a)) : Filter ℝ≥0∞)

Tactic:
rw [← iUnion_Ioc_left]

Premises used: Set.iUnion_Ioc_left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : NoMinOrder α
inst_2 : IsCountablyGenerated.{u_1} (α := α) atBot
μ : Measure α
a : α
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ioc x a) : ℝ≥0∞)) atBot
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : α), Ioc b a)) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_iUnion_atBot (monotone_id.Ioc antitone_const)

Premises used: MeasureTheory.tendsto_measure_iUnion_atBot, monotone_id, Monotone.Ioc, antitone_const
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : NoMinOrder α
inst_2 : IsCountablyGenerated.{u_1} (α := α) atBot
μ : Measure α
a : α
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ioc x a) : ℝ≥0∞)) atBot
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : α), Ioc b a)) : Filter ℝ≥0∞)

Tactic:
exact tendsto_measure_iUnion_atBot (monotone_id.Ioc antitone_const)

Premises used: MeasureTheory.tendsto_measure_iUnion_atBot, monotone_id, Monotone.Ioc, antitone_const
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : IsCountablyGenerated.{u_1} (α := α) atTop
μ : Measure α
rw :
  Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Iic x) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (a : α), Iic a)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Iic x) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) univ) : Filter ℝ≥0∞)

Tactic:
rw [← iUnion_Iic]

Premises used: Set.iUnion_Iic
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : IsCountablyGenerated.{u_1} (α := α) atTop
μ : Measure α
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Iic x) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (a : α), Iic a)) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_iUnion_atTop monotone_Iic

Premises used: MeasureTheory.tendsto_measure_iUnion_atTop, monotone_Iic
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : IsCountablyGenerated.{u_1} (α := α) atTop
μ : Measure α
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Iic x) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (a : α), Iic a)) : Filter ℝ≥0∞)

Tactic:
exact tendsto_measure_iUnion_atTop monotone_Iic

Premises used: MeasureTheory.tendsto_measure_iUnion_atTop, monotone_Iic
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : IsCountablyGenerated.{u_1} (α := α) atBot
μ : Measure α
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ici x) : ℝ≥0∞)) atBot
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) univ) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_Iic_atTop (α := αᵒᵈ) μ

Premises used: Set.Ici, setOf, MeasureTheory.tendsto_measure_Iic_atTop, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : PartialOrder α
a : α
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Iic a \ {a} =ᶠ[ae μ] Iic a
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a ∩ {a}) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) 0 0
⊢ Iio a =ᶠ[ae μ] Iic a

Tactic:
rw [← Iic_diff_right, diff_ae_eq_self, measure_mono_null Set.inter_subset_right ha]

Premises used: MeasureTheory.measure_mono_null, MeasureTheory.diff_ae_eq_self, Set.Iic_diff_right, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : PartialOrder α
a : α
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ioi a =ᶠ[ae μ] Ici a

Tactic:
Iio_ae_eq_Iic' (α := αᵒᵈ) ha

Premises used: MeasureTheory.Iio_ae_eq_Iic', Set.Ioi, Set.Ici, setOf, OrderDual
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : PartialOrder α
a b : α
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ioo a b =ᶠ[ae μ] Ioc a b

Tactic:
(ae_eq_refl _).inter (Iio_ae_eq_Iic' hb)

Premises used: Set.Ioc, MeasureTheory.Iio_ae_eq_Iic', Set.Mem, setOf, Filter.EventuallyEq.inter, MeasureTheory.ae_eq_refl, Set.inter, Set.Ioo
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : PartialOrder α
a b : α
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ioc a b =ᶠ[ae μ] Icc a b

Tactic:
(Ioi_ae_eq_Ici' ha).inter (ae_eq_refl _)

Premises used: Set.Ioc, Set.Ioi, Set.Ici, Set.Mem, setOf, Filter.EventuallyEq.inter, MeasureTheory.ae_eq_refl, Set.inter, Set.Icc, MeasureTheory.Ioi_ae_eq_Ici'
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : PartialOrder α
a b : α
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ioo a b =ᶠ[ae μ] Ico a b

Tactic:
(Ioi_ae_eq_Ici' ha).inter (ae_eq_refl _)

Premises used: Set.Ioi, Set.Ici, Set.Mem, setOf, Filter.EventuallyEq.inter, MeasureTheory.ae_eq_refl, Set.inter, Set.Ico, MeasureTheory.Ioi_ae_eq_Ici', Set.Ioo
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : PartialOrder α
a b : α
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ioo a b =ᶠ[ae μ] Icc a b

Tactic:
(Ioi_ae_eq_Ici' ha).inter (Iio_ae_eq_Iic' hb)

Premises used: MeasureTheory.Iio_ae_eq_Iic', Set.Ioi, Set.Ici, Set.Mem, setOf, Filter.EventuallyEq.inter, Set.inter, Set.Icc, MeasureTheory.Ioi_ae_eq_Ici', Set.Ioo
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : PartialOrder α
a b : α
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ico a b =ᶠ[ae μ] Icc a b

Tactic:
(ae_eq_refl _).inter (Iio_ae_eq_Iic' hb)

Premises used: MeasureTheory.Iio_ae_eq_Iic', Set.Mem, setOf, Filter.EventuallyEq.inter, MeasureTheory.ae_eq_refl, Set.inter, Set.Ico, Set.Icc
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : PartialOrder α
a b : α
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ico a b =ᶠ[ae μ] Ioc a b

Tactic:
(Ioo_ae_eq_Ico' ha).symm.trans (Ioo_ae_eq_Ioc' hb)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Ioo_ae_eq_Ico', Filter.EventuallyEq.symm, MeasureTheory.Ioo_ae_eq_Ioc'
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_6
m : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ.real s = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)

Tactic:
rfl

Premises used: MeasureTheory.Measure.real, rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
⊢ μ.trim = μ.toOuterMeasure

Tactic:
le_antisymm μ.trim_le μ.1.le_trim

Premises used: MeasureTheory.OuterMeasure.le_trim, MeasureTheory.Measure.toOuterMeasure, le_antisymm, MeasureTheory.Measure.trim_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
rw :
  Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (f i) ⋯)
    (∑' (i : ℕ), (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (f i))
⊢ Eq (α := ℝ≥0∞) ((inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (iUnion f) : ℝ≥0∞)
    (∑' (i : ℕ), (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
rw [inducedOuterMeasure_eq m0 mU (MeasurableSet.iUnion hf), mU hf hd]

Premises used: MeasureTheory.inducedOuterMeasure_eq, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e_f :
  Eq (α := ℕ → ℝ≥0∞) (fun (i : ℕ) ↦ m (f i) ⋯) fun (i : ℕ) ↦
    (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (f i)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (f i) ⋯)
    (∑' (i : ℕ), (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (f i))

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e_f : ∀ (n : ℕ), m (f n) ⋯ = (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (f n)
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (i : ℕ) ↦ m (f i) ⋯) fun (i : ℕ) ↦
    (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (f i)

Tactic:
funext n
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
n : ℕ
e_f : m (f n) ⋯ = m (f n) ⋯
e_f₁ : MeasurableSet (f n)
e_f₂ : m (f n) ⋯ = m (f n) ⋯
e_f₃ : MeasurableSet (f n)
⊢ m (f n) ⋯ = (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (f n)

Tactic:
rw [inducedOuterMeasure_eq m0 mU]

Premises used: MeasureTheory.inducedOuterMeasure_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s_1 s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s : Set α
hs : MeasurableSet s
rw : (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) s ≤ m s hs
rw₁ rw₂ : m s hs ≤ m s hs
⊢ ((inducedOuterMeasure (P := MeasurableSet) m ⋯ m0).trim : (a : Set α) → ℝ≥0∞) s ≤ m s hs

Tactic:
rw [OuterMeasure.trim_eq _ hs, inducedOuterMeasure_eq m0 mU hs]

Premises used: MeasureTheory.inducedOuterMeasure_eq, MeasureTheory.OuterMeasure.trim_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s : Set α
hs : MeasurableSet s
⊢ (ofMeasurable m m0 mU : (a : Set α) → ℝ≥0∞) s = m s hs

Tactic:
inducedOuterMeasure_eq m0 mU hs

Premises used: MeasureTheory.inducedOuterMeasure_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ₁ μ₂ : Measure α
h :
  ∀ (s : Set α),
    MeasurableSet s → Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw : μ₁.trim = μ₂.toOuterMeasure
rw₁ : μ₂.trim = μ₂.toOuterMeasure
rw₂ rw₃ : μ₂.toOuterMeasure = μ₂.toOuterMeasure
⊢ μ₁.toOuterMeasure = μ₂.toOuterMeasure

Tactic:
rw [← trimmed, OuterMeasure.trim_congr (h _), trimmed]

Premises used: MeasureTheory.Measure.trimmed, MeasureTheory.OuterMeasure.trim_congr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ₁ : Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
m : OuterMeasure α
⊢ m ≤ μ.toOuterMeasure ↔
    ∀ (s : Set α),
      MeasurableSet s → LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa only [μ.trimmed] using OuterMeasure.le_trim_iff (m₂ := μ.1)

Premises used: MeasureTheory.Measure.trimmed, MeasureTheory.OuterMeasure.le_trim_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null h ht

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
⊢ Eq (α := (a : Set α) → ℝ≥0∞) (⇑μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) (⇑μ : (a : Set α) → ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [μ.trimmed, μ.coe_toOuterMeasure]

Premises used: MeasureTheory.Measure.coe_toOuterMeasure, MeasureTheory.Measure.trimmed
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) t)
    (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t)
    (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [measure_eq_trim, OuterMeasure.trim_eq_iInf, μ.coe_toOuterMeasure]

Premises used: MeasureTheory.Measure.coe_toOuterMeasure, MeasureTheory.measure_eq_trim, MeasureTheory.OuterMeasure.trim_eq_iInf
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
simp_rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (i : Set α), ⨅ (_ : s ⊆ i ∧ MeasurableSet i), (μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
simp_rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (i : Set α), ⨅ (_ : s ⊆ i), ⨅ (_ : MeasurableSet i), (μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : { t : Set α // s ⊆ t ∧ MeasurableSet t }), (μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞)

Tactic:
simp_rw [iInf_subtype, iInf_and, ← measure_eq_iInf]

Premises used: iInf_subtype, iInf_and, MeasureTheory.measure_eq_iInf
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((inducedOuterMeasure (P := MeasurableSet) (fun (s : Set α) (x : MeasurableSet s) ↦ (μ : (a : Set α) → ℝ≥0∞) s) ⋯
              ⋯ :
            OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
measure_eq_trim _

Premises used: MeasureTheory.measure_eq_trim
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
⊢ μ.toOuterMeasure =
    inducedOuterMeasure (P := MeasurableSet) (fun (s : Set α) (x : MeasurableSet s) ↦ (μ : (a : Set α) → ℝ≥0∞) s) ⋯ ⋯

Tactic:
μ.trimmed.symm

Premises used: MeasureTheory.Measure.trimmed, MeasureTheory.OuterMeasure.trim, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs h : MeasurableSet s
⊢ (μ : (a : Set α) → ℝ≥0∞) s =
    extend (P := fun (t : Set α) ↦ MeasurableSet t)
      (fun (t : Set α) (_ht : MeasurableSet t) ↦ (μ : (a : Set α) → ℝ≥0∞) t) s

Tactic:
rw [extend_eq]

Premises used: MeasureTheory.extend_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
exact hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.Nonempty

Tactic:
nonempty_iff_ne_empty.2 fun h' => h <| h'.symm ▸ measure_empty

Premises used: Iff.mpr, Eq.rec, MeasureTheory.measure_empty, Set.nonempty_iff_ne_empty, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₁ ⊆ s₂
h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
top_unique <| h₁ ▸ measure_mono h

Premises used: Eq.rec, top_unique, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)

Tactic:
μ.mono subset_union_left

Premises used: MeasureTheory.OuterMeasure.mono, Set.subset_union_left, MeasureTheory.Measure.toOuterMeasure
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)

Tactic:
μ.mono subset_union_right

Premises used: MeasureTheory.OuterMeasure.mono, Set.subset_union_right, MeasureTheory.Measure.toOuterMeasure
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ∃ (t : Set α),
    s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa only [← measure_eq_trim] using μ.toOuterMeasure.exists_measurable_superset_eq_trim s

Premises used: MeasureTheory.Measure.toOuterMeasure, MeasureTheory.measure_eq_trim, MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
ι : Sort u_5
inst : MeasurableSpace α
inst_1 : Countable ι
μ : ι → Measure α
s : Set α
⊢ ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧
        ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa only [← measure_eq_trim] using
    OuterMeasure.exists_measurable_superset_forall_eq_trim (fun i => (μ i).toOuterMeasure) s

Premises used: MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim, MeasureTheory.Measure.toOuterMeasure, MeasureTheory.measure_eq_trim
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ ν : Measure α
s : Set α
⊢ ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
          Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa only [Bool.forall_bool.trans and_comm] using
    exists_measurable_superset_forall_eq (fun b => cond b μ ν) s

Premises used: cond, Bool.forall_bool, and_comm, Iff.trans, MeasureTheory.exists_measurable_superset_forall_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
h ▸ exists_measurable_superset μ s

Premises used: Eq.rec, MeasureTheory.exists_measurable_superset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ (∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨fun ⟨_t, hst, _, ht⟩ => measure_mono_null hst ht, exists_measurable_superset_of_null⟩

Premises used: MeasureTheory.measure_mono_null, Iff.intro, _private.0.MeasureTheory.exists_measurable_superset_iff_measure_eq_zero.match_1, OfNat.ofNat, Eq, MeasureTheory.exists_measurable_superset_of_null, DFunLike.coe