awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((μ.restrict s).toOuterMeasure : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((μ.toOuterMeasure : (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∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
rw [← toOuterMeasure_apply,
    Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs,
    OuterMeasure.restrict_apply s t _, toOuterMeasure_apply]

Premises used: MeasureTheory.Measure.toOuterMeasure_apply, MeasureTheory.Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict, MeasureTheory.OuterMeasure.restrict_apply
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
obtain :
  ∀ (t : ℕ → Set α) (ht1 : ∀ (n : ℕ), t n ∈ C) (ht2 : Eq.{u_2 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
obtain ⟨t, ht1, ht2⟩ := hC
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
t : ℕ → Set α
ht1 : ∀ (n : ℕ), t n ∈ C
ht2 : Eq.{u_2 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
rw : s = s ∩ ⋃ (i : ℕ), t i
rw₁ : s = s ∩ univ
rw₂ rw₃ : s = s
⊢ s = ⋃ (n : ℕ), s ∩ t n

Tactic:
rw [← inter_iUnion, ht2, inter_univ]

Premises used: Set.inter_univ, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
t : ℕ → Set α
ht1 : ∀ (n : ℕ), t n ∈ C
ht2 : Eq.{u_2 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
rw : ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [show s = ⋃ n, s ∩ t n by rw [← inter_iUnion, ht2, inter_univ], measure_iUnion_null_iff]

Premises used: MeasureTheory.measure_iUnion_null_iff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
t : ℕ → Set α
ht1 : ∀ (n : ℕ), t n ∈ C
ht2 : Eq.{u_2 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
⊢ ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
fun i => ht (t i) (ht1 i)
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
t : ℕ → Set α
ht1 : ∀ (n : ℕ), t n ∈ C
ht2 : Eq.{u_2 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
⊢ ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact fun i => ht (t i) (ht1 i)
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
hm : C ⊆ MeasurableSet
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← forall_measure_inter_isCountablySpanning_eq_zero hC]

Premises used: MeasureTheory.Measure.forall_measure_inter_isCountablySpanning_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
hm : C ⊆ MeasurableSet
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
fun t htc => ?_
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
hm : C ⊆ MeasurableSet
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
refine : ∀ (t : Set α) (htc : t ∈ C), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine fun t htc => ?_
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
hm : C ⊆ MeasurableSet
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
htc : t ∈ C
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [← μ.restrict_apply' (hm htc)] using ht t htc

Premises used: MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
rw :
  Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ toMeasurable μ 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∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
rw [← restrict_congr_set hs.toMeasurable_ae_eq,
    restrict_apply' (measurableSet_toMeasurable _ _),
    measure_congr ((ae_eq_refl t).inter hs.toMeasurable_ae_eq)]

Premises used: MeasureTheory.measure_congr, MeasureTheory.Measure.restrict_congr_set, Filter.EventuallyEq.inter, MeasureTheory.ae_eq_refl, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ.restrict s ≤ μ

Tactic:
Measure.le_iff.2 fun t ht => calc
    μ.restrict s t = μ (t ∩ s) := restrict_apply ht
    _ ≤ μ t := measure_mono inter_subset_left

Premises used: Iff.mpr, Trans.trans, MeasureTheory.Measure.restrict_apply, Set.inter_subset_left, MeasureTheory.Measure.le_iff, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ.restrict s ≪ μ

Tactic:
Measure.absolutelyContinuous_of_le Measure.restrict_le_self

Premises used: MeasureTheory.Measure.restrict_le_self, MeasureTheory.Measure.absolutelyContinuous_of_le
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
rw :
  Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) (toMeasurable (μ.restrict t) s) : ℝ≥0∞)
    ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ.restrict t) s ∩ t) : ℝ≥0∞)
    ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← restrict_apply (measurableSet_toMeasurable _ _), measure_toMeasurable]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.measure_toMeasurable, MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
restrict_eq_self μ Subset.rfl

Premises used: Set.Subset.rfl, MeasureTheory.Measure.restrict_eq_self
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [restrict_apply MeasurableSet.univ, Set.univ_inter]

Premises used: MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
calc
    μ (t ∩ s) = μ.restrict s (t ∩ s) := (restrict_eq_self μ inter_subset_right).symm
    _ ≤ μ.restrict s t := measure_mono inter_subset_left

Premises used: Trans.trans, Set.inter_subset_left, MeasureTheory.measure_mono, Eq.symm, MeasureTheory.Measure.restrict_eq_self, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
Measure.le_iff'.1 restrict_le_self _

Premises used: MeasureTheory.Measure.le_iff', MeasureTheory.Measure.restrict_le_self, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
((measure_mono (subset_univ _)).trans_eq <| restrict_apply_univ _).antisymm
    ((restrict_apply_self μ s).symm.trans_le <| measure_mono h)

Premises used: LE.le.trans_eq, MeasureTheory.Measure.restrict_apply_self, Set.subset_univ, LE.le.antisymm, MeasureTheory.Measure.restrict_apply_univ, Eq.trans_le, MeasureTheory.measure_mono, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
_m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
⊢ (μ + ν).restrict s = μ.restrict s + ν.restrict s

Tactic:
(restrictₗ s).map_add μ ν

Premises used: LinearMap.map_add, MeasureTheory.Measure.restrict, MeasureTheory.Measure.restrictₗ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
_m0 : MeasurableSpace α
s : Set α
⊢ Eq (α := Measure α) (restrict 0 s) 0

Tactic:
(restrictₗ s).map_zero

Premises used: LinearMap.map_zero, MeasureTheory.Measure.restrict, MeasureTheory.Measure.restrictₗ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
_m0 : MeasurableSpace α
R : Type u_7
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
μ : Measure α
s : Set α
⊢ (c • μ).restrict s = c • μ.restrict s

Tactic:
simpa only [smul_one_smul] using (restrictₗ s).map_smul (c • 1) μ

Premises used: smul_one_smul, LinearMap.map_smul, HSMul.hSMul, OfNat.ofNat, MeasureTheory.Measure.restrictₗ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s (μ.restrict t)
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) (((μ.restrict t).restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    ((μ.restrict (s ∩ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
simp only [Set.inter_assoc, restrict_apply hu,
      restrict_apply₀ (hu.nullMeasurableSet.inter hs)]

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.restrict_apply, MeasureTheory.NullMeasurableSet.inter, MeasureTheory.Measure.restrict_apply₀, Set.inter_assoc
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ (μ.restrict t).restrict s = μ.restrict (s ∩ t)

Tactic:
restrict_restrict₀ hs.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.restrict_restrict₀
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
h₁ :
  ∀ (u : Set α) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞) (((μ.restrict t).restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ (μ.restrict t).restrict s = μ.restrict s

Tactic:
ext1 u hu
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
h₁ : u ∩ s ⊆ t
⊢ Eq (α := ℝ≥0∞) (((μ.restrict t).restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
rw [restrict_apply hu, restrict_apply hu, restrict_eq_self]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.restrict_eq_self
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ u ∩ s ⊆ t

Tactic:
inter_subset_right.trans h

Premises used: HasSubset.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ u ∩ s ⊆ t

Tactic:
exact inter_subset_right.trans h

Premises used: HasSubset.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) (((μ.restrict t).restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    ((μ.restrict (s ∩ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
simp only [restrict_apply hu, restrict_apply₀' ht, inter_assoc]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.restrict_apply₀', Set.inter_assoc
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
⊢ (μ.restrict t).restrict s = μ.restrict (s ∩ t)

Tactic:
restrict_restrict₀' ht.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.restrict_restrict₀'
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
rw : μ.restrict (s ∩ t) = (μ.restrict s).restrict t
rw₁ : μ.restrict (s ∩ t) = μ.restrict (t ∩ s)
rw₂ rw₃ : μ.restrict (t ∩ s) = μ.restrict (t ∩ s)
⊢ (μ.restrict t).restrict s = (μ.restrict s).restrict t

Tactic:
rw [restrict_restrict hs, restrict_restrict' hs, inter_comm]

Premises used: MeasureTheory.Measure.restrict_restrict', MeasureTheory.Measure.restrict_restrict, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [restrict_apply ht]

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
nonpos_iff_eq_zero.1 (h ▸ le_restrict_apply _ _)

Premises used: Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [restrict_apply' hs]

Premises used: MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.restrict s = 0 ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← measure_univ_eq_zero, restrict_apply_univ]

Premises used: MeasureTheory.Measure.restrict_apply_univ, MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
δ : Type u_4
γ : Type u_5
ι : Type u_6
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst_2 : NeZero (R := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ NeZero (μ.restrict s)

Tactic:
⟨mt restrict_eq_zero.mp <| NeZero.ne _⟩

Premises used: NeZero.mk, MeasureTheory.Measure.restrict_eq_zero, mt, Iff.mp, NeZero.ne
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.restrict s = 0

Tactic:
restrict_eq_zero.2 h

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
⊢ μ.restrict ∅ = 0

Tactic:
restrict_zero_set measure_empty

Premises used: MeasureTheory.measure_empty, MeasureTheory.Measure.restrict_zero_set
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.restrict univ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
h :
  ∀ (u : Set α) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞) ((μ.restrict (s ∩ t) + μ.restrict (s \ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s

Tactic:
ext1 u hu
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
u : Set α
hu : MeasurableSet u
h :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∩ tᶜ) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (u ∩ s)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (s ∩ t) + μ.restrict (s \ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
simp only [add_apply, restrict_apply hu, ← inter_assoc, diff_eq]

Premises used: MeasureTheory.Measure.restrict_apply, Set.diff_eq, MeasureTheory.Measure.add_apply, Set.inter_assoc
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
u : Set α
hu : MeasurableSet u
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∩ tᶜ) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (u ∩ s)

Tactic:
measure_inter_add_diff₀ (u ∩ s) ht

Premises used: MeasureTheory.measure_inter_add_diff₀, Set.Mem, setOf, Set.inter, Inter.inter, Not
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
u : Set α
hu : MeasurableSet u
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∩ tᶜ) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (u ∩ s)

Tactic:
exact measure_inter_add_diff₀ (u ∩ s) ht

Premises used: MeasureTheory.measure_inter_add_diff₀, Inter.inter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s

Tactic:
restrict_inter_add_diff₀ s ht.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.restrict_inter_add_diff₀
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
rw : μ.restrict ((s ∪ t) ∩ t) + μ.restrict ((s ∪ t) \ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
rw₁ : μ.restrict t + μ.restrict ((s ∪ t) \ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
rw₂ : μ.restrict t + μ.restrict (s \ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
rw₃ : μ.restrict t + μ.restrict (s \ t) + μ.restrict (s ∩ t) = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.restrict t
rw₄ : μ.restrict (s ∩ t) + (μ.restrict t + μ.restrict (s \ t)) = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.restrict t
rw₅ : μ.restrict (s ∩ t) + μ.restrict t + μ.restrict (s \ t) = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.restrict t
rw₆ rw₇ :
  μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.restrict t = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.restrict t
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

Tactic:
rw [← restrict_inter_add_diff₀ (s ∪ t) ht, union_inter_cancel_right, union_diff_right, ←
    restrict_inter_add_diff₀ s ht, add_comm, ← add_assoc, add_right_comm]

Premises used: add_assoc, MeasureTheory.Measure.restrict_inter_add_diff₀, add_right_comm, add_comm, Set.union_diff_right, Union.union, Set.union_inter_cancel_right
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

Tactic:
restrict_union_add_inter₀ s ht.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.restrict_union_add_inter₀
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

Tactic:
simpa only [union_comm, inter_comm, add_comm] using restrict_union_add_inter t hs

Premises used: MeasureTheory.Measure.restrict_union_add_inter, Set.union_comm, add_comm, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

Tactic:
simp [← restrict_union_add_inter₀ s ht, restrict_zero_set h]

Premises used: MeasureTheory.Measure.restrict_union_add_inter₀, MeasureTheory.Measure.restrict_zero_set
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
ht : MeasurableSet t
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

Tactic:
restrict_union₀ h.aedisjoint ht.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.restrict_union₀, Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
hs : MeasurableSet s
rw : μ.restrict (t ∪ s) = μ.restrict s + μ.restrict t
rw₁ : μ.restrict t + μ.restrict s = μ.restrict s + μ.restrict t
rw₂ rw₃ : μ.restrict s + μ.restrict t = μ.restrict s + μ.restrict t
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

Tactic:
rw [union_comm, restrict_union h.symm hs, add_comm]

Premises used: MeasureTheory.Measure.restrict_union, Set.union_comm, add_comm, Disjoint.symm