awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ.restrict t) s ∩ t) : ℝ≥0∞)
    ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) (toMeasurable (μ.restrict t) s) : ℝ≥0∞)
  ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← restrict_apply (measurableSet_toMeasurable _ _), measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ.restrict t) s ∩ t) : ℝ≥0∞)
    ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← restrict_apply (measurableSet_toMeasurable _ _), measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [restrict_apply MeasurableSet.univ, Set.univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [restrict_apply MeasurableSet.univ, Set.univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
⊢ (μ.restrict t).restrict s = μ.restrict s
have h₁ : ∀ (u : Set α) (hu : MeasurableSet u),
  Eq (α := ℝ≥0∞) (((μ.restrict t).restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
Tactic: ext1 u hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) (((μ.restrict t).restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
have h₁ : u ∩ s ⊆ t
Tactic: rw [restrict_apply hu, restrict_apply hu, restrict_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ (μ.restrict t).restrict s = (μ.restrict s).restrict t
have rw : μ.restrict (s ∩ t) = (μ.restrict s).restrict t
Tactic: rw [restrict_restrict hs, restrict_restrict' hs, inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
rw : μ.restrict (s ∩ t) = (μ.restrict s).restrict t
⊢ (μ.restrict t).restrict s = (μ.restrict s).restrict t
have rw₁ : μ.restrict (s ∩ t) = μ.restrict (t ∩ s)
Tactic: rw [restrict_restrict hs, restrict_restrict' hs, inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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)
⊢ (μ.restrict t).restrict s = (μ.restrict s).restrict t
have rw₂ : μ.restrict (t ∩ s) = μ.restrict (t ∩ s)
Tactic: rw [restrict_restrict hs, restrict_restrict' hs, inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [restrict_apply ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [restrict_apply' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ.restrict s = 0 ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← measure_univ_eq_zero, restrict_apply_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ μ.restrict s = 0 ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← measure_univ_eq_zero, restrict_apply_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s
have 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∞)
Tactic: ext1 u hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
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∞)
have h : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∩ t) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∩ tᶜ) : ℝ≥0∞) =
  (μ : (a : Set α) → ℝ≥0∞) (u ∩ s)
Tactic: simp only [add_apply, restrict_apply hu, ← inter_assoc, diff_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
have rw : μ.restrict ((s ∪ t) ∩ t) + μ.restrict ((s ∪ t) \ 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
have rw₁ : μ.restrict t + μ.restrict ((s ∪ t) \ 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
have rw₂ : μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
have rw₃ : μ.restrict t + μ.restrict (s \ t) + μ.restrict (s ∩ t) = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
have rw₄ : μ.restrict (s ∩ t) + (μ.restrict t + μ.restrict (s \ t)) = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
have rw₅ : μ.restrict (s ∩ t) + μ.restrict t + μ.restrict (s \ t) = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
have rw₆ : μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.restrict t = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
hs : MeasurableSet s
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
have rw : μ.restrict (t ∪ s) = μ.restrict s + μ.restrict t
Tactic: rw [union_comm, restrict_union h.symm hs, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
have rw₁ : μ.restrict t + μ.restrict s = μ.restrict s + μ.restrict t
Tactic: rw [union_comm, restrict_union h.symm hs, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
have rw₂ : μ.restrict s + μ.restrict t = μ.restrict s + μ.restrict t
Tactic: rw [union_comm, restrict_union h.symm hs, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ μ.restrict s + μ.restrict sᶜ = μ
have rw : μ.restrict (s ∪ sᶜ) = μ
Tactic: rw [← restrict_union (@disjoint_compl_right (Set α) _ _) hs.compl, union_compl_self,
    restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
rw : μ.restrict (s ∪ sᶜ) = μ
⊢ μ.restrict s + μ.restrict sᶜ = μ
have rw₁ : μ.restrict univ = μ
Tactic: rw [← restrict_union (@disjoint_compl_right (Set α) _ _) hs.compl, union_compl_self,
    restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
rw : μ.restrict (s ∪ sᶜ) = μ
rw₁ : μ.restrict univ = μ
⊢ μ.restrict s + μ.restrict sᶜ = μ
have rw₂ : μ = μ
Tactic: rw [← restrict_union (@disjoint_compl_right (Set α) _ _) hs.compl, union_compl_self,
    restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ μ.restrict sᶜ + μ.restrict s = μ
have rw : μ.restrict s + μ.restrict sᶜ = μ
Tactic: rw [add_comm, restrict_add_restrict_compl hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
rw : μ.restrict s + μ.restrict sᶜ = μ
⊢ μ.restrict sᶜ + μ.restrict s = μ
have rw₁ : μ = μ
Tactic: rw [add_comm, restrict_add_restrict_compl hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞) ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (∑' (i : ι), (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t ∩ s i) : ℝ≥0∞)
  (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (t ∩ s i) : ℝ≥0∞)
Tactic: simp only [restrict_apply, ht, inter_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (⨆ (i : ι), (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t ∩ s i) : ℝ≥0∞)
  (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (t ∩ s i) : ℝ≥0∞)
Tactic: simp only [restrict_apply ht, inter_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t ∩ s i) : ℝ≥0∞)
    (⨆ (i : ι), (μ : (a : Set α) → ℝ≥0∞) (t ∩ s i) : ℝ≥0∞)
have rw : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (i : ι) ↦ t ∩ s i
Tactic: rw [Directed.measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ μ.restrict (t ∩ toMeasurable μ s) = μ.restrict s
have h₁ : ∀ (u : Set α) (hu : MeasurableSet u),
  Eq (α := ℝ≥0∞) ((μ.restrict (t ∩ toMeasurable μ s) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
Tactic: ext u hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (t ∩ toMeasurable μ s) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (t ∩ u)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
Tactic: rw [restrict_apply hu, restrict_apply hu, inter_comm t, inter_comm, inter_assoc,
    measure_toMeasurable_inter (ht.inter hu) h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (t ∩ u)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
have h₁ : s ∩ (t ∩ u) = u ∩ s
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← inter_eq_self_of_subset_left hts, ← restrict_apply ht, H, restrict_apply ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← inter_eq_self_of_subset_left hts, ← restrict_apply ht, H, restrict_apply ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← inter_eq_self_of_subset_left hts, ← restrict_apply ht, H, restrict_apply ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← inter_eq_self_of_subset_left hts, ← restrict_apply ht, H, restrict_apply ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [restrict_apply ht, restrict_apply ht, H _ inter_subset_right (ht.inter hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [restrict_apply ht, restrict_apply ht, H _ inter_subset_right (ht.inter hs)]