awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
rw : μ.restrict (s ∪ sᶜ) = μ
rw₁ : μ.restrict univ = μ
rw₂ rw₃ : μ = μ
⊢ μ.restrict s + μ.restrict sᶜ = μ

Tactic:
rw [← restrict_union (@disjoint_compl_right (Set α) _ _) hs.compl, union_compl_self,
    restrict_univ]

Premises used: MeasureTheory.Measure.restrict_union, Set.union_compl_self, MeasurableSet.compl, disjoint_compl_right, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
rw : μ.restrict s + μ.restrict sᶜ = μ
rw₁ rw₂ : μ = μ
⊢ μ.restrict sᶜ + μ.restrict s = μ

Tactic:
rw [add_comm, restrict_add_restrict_compl hs]

Premises used: MeasureTheory.Measure.restrict_add_restrict_compl, add_comm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s s' t : Set α
ht : MeasurableSet t
⊢ LE.le (α := ℝ≥0∞) ((μ.restrict (s ∪ s') : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict s + μ.restrict s' : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simpa [ht, inter_union_distrib_left] using measure_union_le (t ∩ s) (t ∩ s')

Premises used: Inter.inter, Set.inter_union_distrib_left, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
t : Set α
ht : MeasurableSet t
simp :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t ∩ s i) : ℝ≥0∞)
    (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (t ∩ s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (∑' (i : ι), (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [restrict_apply, ht, inter_iUnion]

Premises used: MeasureTheory.Measure.restrict_apply, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t ∩ s i) : ℝ≥0∞)
    (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (t ∩ s i) : ℝ≥0∞)

Tactic:
measure_iUnion₀ (hd.mono fun i j h => h.mono inter_subset_right inter_subset_right)
      fun i => ht.nullMeasurableSet.inter (hm i)

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measure_iUnion₀, MeasureTheory.NullMeasurableSet.inter, Set.inter_subset_right, MeasureTheory.AEDisjoint.mono, Pairwise.mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t ∩ s i) : ℝ≥0∞)
    (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (t ∩ s i) : ℝ≥0∞)

Tactic:
exact
    measure_iUnion₀ (hd.mono fun i j h => h.mono inter_subset_right inter_subset_right)
      fun i => ht.nullMeasurableSet.inter (hm i)

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measure_iUnion₀, MeasureTheory.NullMeasurableSet.inter, Set.inter_subset_right, MeasureTheory.AEDisjoint.mono, Pairwise.mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (∑' (i : ι), (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
restrict_iUnion_apply_ae hd.aedisjoint (fun i => (hm i).nullMeasurableSet) ht

Premises used: MeasurableSet.nullMeasurableSet, Pairwise.aedisjoint, MeasureTheory.Measure.restrict_iUnion_apply_ae
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
t : Set α
ht : MeasurableSet t
simp :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t ∩ s i) : ℝ≥0∞)
    (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (t ∩ s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (⨆ (i : ι), (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [restrict_apply ht, inter_iUnion]

Premises used: MeasureTheory.Measure.restrict_apply, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
t : Set α
ht : MeasurableSet t
rw : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (i : ι) ↦ t ∩ s i
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t ∩ s i) : ℝ≥0∞)
    (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (t ∩ s i) : ℝ≥0∞)

Tactic:
rw [Directed.measure_iUnion]

Premises used: Directed.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
t : Set α
ht : MeasurableSet t
⊢ Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (i : ι) ↦ t ∩ s i

Tactic:
hd.mono_comp _ fun s₁ s₂ => inter_subset_inter_right _

Premises used: Set.inter_subset_inter_right, Directed.mono_comp
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
t : Set α
ht : MeasurableSet t
⊢ Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (i : ι) ↦ t ∩ s i

Tactic:
exacts [hd.mono_comp _ fun s₁ s₂ => inter_subset_inter_right _]

Premises used: Set.inter_subset_inter_right, Directed.mono_comp
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (((restrict (map f μ) s : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    (((map f (μ.restrict (f ⁻¹' s)) : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp [*, hf ht]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hst : s ⊆ t
h₁ :
  ∀ (u : Set α) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞) ((μ.restrict (t ∩ toMeasurable μ s) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ μ.restrict (t ∩ toMeasurable μ s) = μ.restrict s

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

Tactic:
rw [restrict_apply hu, restrict_apply hu, inter_comm t, inter_comm, inter_assoc,
    measure_toMeasurable_inter (ht.inter hu) h]

Premises used: MeasureTheory.Measure.measure_toMeasurable_inter, MeasureTheory.Measure.restrict_apply, Set.inter_comm, Set.inter_assoc, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hst : s ⊆ t
u : Set α
hu : MeasurableSet u
h₁ : s ∩ (t ∩ u) = u ∩ s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (t ∩ u)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hst : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ s ∩ (t ∩ u) = u ∩ s

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.restrict (toMeasurable μ s) = μ.restrict s

Tactic:
simpa using restrict_inter_toMeasurable h MeasurableSet.univ (subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.Measure.restrict_inter_toMeasurable, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
_m0 : MeasurableSpace α
s : Set α
μ : Measure α
hs : ∀ᵐ (x : α) ∂μ, x ∈ s
⊢ μ.restrict s = μ

Tactic:
calc
    μ.restrict s = μ.restrict univ := restrict_congr_set (eventuallyEq_univ.mpr hs)
    _ = μ := restrict_univ

Premises used: Iff.mpr, Trans.trans, MeasureTheory.Measure.restrict_congr_set, Filter.eventuallyEq_univ, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : μ.restrict s = ν.restrict s
t : Set α
hts : t ⊆ s
ht : MeasurableSet t
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥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∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [← inter_eq_self_of_subset_left hts, ← restrict_apply ht, H, restrict_apply ht]

Premises used: MeasureTheory.Measure.restrict_apply, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : ∀ t ⊆ s, MeasurableSet t → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : MeasurableSet t
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (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∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [restrict_apply ht, restrict_apply ht, H _ inter_subset_right (ht.inter hs)]

Premises used: MeasureTheory.Measure.restrict_apply, Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : s ⊆ t
h : μ.restrict t = ν.restrict t
rw : (μ.restrict t).restrict s = ν.restrict s
rw₁ : (ν.restrict t).restrict s = ν.restrict s
rw₂ rw₃ : ν.restrict s = ν.restrict s
⊢ μ.restrict s = ν.restrict s

Tactic:
rw [← restrict_restrict_of_subset hs, h, restrict_restrict_of_subset hs]

Premises used: MeasureTheory.Measure.restrict_restrict_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t

Tactic:
⟨fun h ↦ ⟨restrict_congr_mono subset_union_left h,
    restrict_congr_mono subset_union_right h⟩, ?_⟩

Premises used: Set.subset_union_right, MeasureTheory.Measure.restrict_congr_mono, Set.subset_union_left, And.intro, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
refine : μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t → μ.restrict (s ∪ t) = ν.restrict (s ∪ t)
⊢ μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t

Tactic:
refine ⟨fun h ↦ ⟨restrict_congr_mono subset_union_left h,
    restrict_congr_mono subset_union_right h⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
h :
  ∀ (u : Set α) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞) ((μ.restrict (s ∪ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((ν.restrict (s ∪ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ μ.restrict (s ∪ t) = ν.restrict (s ∪ t)

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

Tactic:
simp only [restrict_apply hu, inter_union_distrib_left]

Premises used: MeasureTheory.Measure.restrict_apply, Set.inter_union_distrib_left
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
h :
  ∀ (US : Set α) (hsub : u ∩ s ⊆ US) (hm : MeasurableSet US)
    (hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞))
    (hν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞)

Tactic:
rcases exists_measurable_superset₂ μ ν (u ∩ s) with ⟨US, hsub, hm, hμ, hν⟩

Premises used: MeasureTheory.exists_measurable_superset₂, Inter.inter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (US ∪ u ∩ t) : ℝ≥0∞)

Tactic:
measure_union_congr_of_subset hsub hμ.le Subset.rfl le_rfl

Premises used: le_rfl, Eq.le, Set.Subset.rfl, MeasureTheory.measure_union_congr_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (US ∪ u ∩ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((u ∩ t) \ US) : ℝ≥0∞)

Tactic:
(measure_add_diff hm.nullMeasurableSet _).symm

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measure_add_diff, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((u ∩ t) \ US) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((μ.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞)

Tactic:
simp only [restrict_apply, hu, hu.diff hm, hμ, ← inter_comm t, inter_diff_assoc]

Premises used: MeasurableSet.diff, MeasureTheory.Measure.restrict_apply, Set.inter_comm, Set.inter_diff_assoc
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((μ.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((ν.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞)
rw₁ rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((ν.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((ν.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((μ.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((ν.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞)

Tactic:
rw [hs, ht]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((ν.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) ((u ∩ t) \ US) : ℝ≥0∞)

Tactic:
simp only [restrict_apply, hu, hu.diff hm, hν, ← inter_comm t, inter_diff_assoc]

Premises used: MeasurableSet.diff, MeasureTheory.Measure.restrict_apply, Set.inter_comm, Set.inter_diff_assoc
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) ((u ∩ t) \ US) : ℝ≥0∞) =
    (ν : (a : Set α) → ℝ≥0∞) (US ∪ u ∩ t)

Tactic:
measure_add_diff hm.nullMeasurableSet _

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measure_add_diff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (US ∪ u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞)

Tactic:
.symm <| measure_union_congr_of_subset hsub hν.le Subset.rfl le_rfl

Premises used: le_rfl, Eq.le, Set.Subset.rfl, MeasureTheory.measure_union_congr_of_subset, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
μ₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((u ∩ t) \ US) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((μ.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞)
μ₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((μ.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((ν.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞)
μ₃ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((ν.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) US : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) ((u ∩ t) \ US) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞)

Tactic:
calc
    μ (u ∩ s ∪ u ∩ t) = μ (US ∪ u ∩ t) :=
      measure_union_congr_of_subset hsub hμ.le Subset.rfl le_rfl
    _ = μ US + μ ((u ∩ t) \ US) := (measure_add_diff hm.nullMeasurableSet _).symm
    _ = restrict μ s u + restrict μ t (u \ US) := by
      simp only [restrict_apply, hu, hu.diff hm, hμ, ← inter_comm t, inter_diff_assoc]
    _ = restrict ν s u + restrict ν t (u \ US) := by rw [hs, ht]
    _ = ν US + ν ((u ∩ t) \ US) := by
      simp only [restrict_apply, hu, hu.diff hm, hν, ← inter_comm t, inter_diff_assoc]
    _ = ν (US ∪ u ∩ t) := measure_add_diff hm.nullMeasurableSet _
    _ = ν (u ∩ s ∪ u ∩ t) := .symm <| measure_union_congr_of_subset hsub hν.le Subset.rfl le_rfl

Premises used: le_rfl, MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.restrict, MeasureTheory.measure_add_diff, Eq.le, Inter.inter, SDiff.sdiff, Set.Subset.rfl, MeasureTheory.measure_union_congr_of_subset, Union.union, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
t : ι → Set α
⊢ μ.restrict (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), t i) =
      ν.restrict (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), t i) ↔
    ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → μ.restrict (t i) = ν.restrict (t i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
t : ι → Set α
i : ι
s : Finset ι
h : i ∉ s
hs : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
insert :
  μ.restrict (t i ∪ ⋃ x ∈ s, t x) = ν.restrict (t i ∪ ⋃ x ∈ s, t x) ↔
    μ.restrict (t i) = ν.restrict (t i) ∧ ∀ a ∈ s, μ.restrict (t a) = ν.restrict (t a)
⊢ μ.restrict (⋃ i_1 ∈ Insert.insert i s, t i_1) = ν.restrict (⋃ i_1 ∈ Insert.insert i s, t i_1) ↔
    ∀ i_1 ∈ Insert.insert i s, μ.restrict (t i_1) = ν.restrict (t i_1)

Tactic:
simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]

Premises used: Finset.mem_insert, forall_eq_or_imp, Set.iUnion_iUnion_eq_or_left