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 : 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∞)
⊢ 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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : s ⊆ t
h : μ.restrict t = ν.restrict t
⊢ μ.restrict s = ν.restrict s
have rw : (μ.restrict t).restrict s = ν.restrict s
Tactic: rw [← restrict_restrict_of_subset hs, h, restrict_restrict_of_subset hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ μ.restrict s = ν.restrict s
have rw₁ : (ν.restrict t).restrict s = ν.restrict s
Tactic: rw [← restrict_restrict_of_subset hs, h, restrict_restrict_of_subset hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ μ.restrict s = ν.restrict s
have rw₂ : ν.restrict s = ν.restrict s
Tactic: rw [← restrict_restrict_of_subset hs, h, restrict_restrict_of_subset hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t
have refine : μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t → μ.restrict (s ∪ t) = ν.restrict (s ∪ t)
Tactic: refine ⟨fun h ↦ ⟨restrict_congr_mono subset_union_left h,
    restrict_congr_mono subset_union_right h⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
⊢ μ.restrict (s ∪ t) = ν.restrict (s ∪ t)
have h : ∀ (u : Set α) (hu : MeasurableSet u),
  Eq (α := ℝ≥0∞) ((μ.restrict (s ∪ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    ((ν.restrict (s ∪ t) : (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 α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (s ∪ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    ((ν.restrict (s ∪ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞)
Tactic: simp only [restrict_apply hu, inter_union_distrib_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞)
have 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∞)
Tactic: rcases exists_measurable_superset₂ μ ν (u ∩ s) with ⟨US, hsub, hm, hμ, hν⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      ((ν.restrict t : (a : Set α) → ℝ≥0∞) (u \ US) : ℝ≥0∞)
have 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∞)
Tactic: rw [hs, ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: rw [hs, ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞)
have μ₁ : 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: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞)
have μ₂ : 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: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ s ∪ u ∩ t) : ℝ≥0∞)
have μ₃ : 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: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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)
⊢ μ.restrict (⋃ i_1 ∈ insert i s, t i_1) = ν.restrict (⋃ i_1 ∈ insert i s, t i_1) ↔
    ∀ i_1 ∈ insert i s, μ.restrict (t i_1) = ν.restrict (t i_1)
have 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)
Tactic: simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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)
⊢ μ.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)
have insert : μ.restrict (t i) = ν.restrict (t i) ∧ μ.restrict (⋃ x ∈ s, t x) = ν.restrict (⋃ x ∈ s, t x) ↔
  μ.restrict (t i) = ν.restrict (t i) ∧ ∀ a ∈ s, μ.restrict (t a) = ν.restrict (t a)
Tactic: rw [restrict_union_congr, ← hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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) = ν.restrict (t i) ∧ μ.restrict (⋃ x ∈ s, t x) = ν.restrict (⋃ x ∈ s, t x) ↔
    μ.restrict (t i) = ν.restrict (t i) ∧ ∀ a ∈ s, μ.restrict (t a) = ν.restrict (t a)
⊢ μ.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)
have insert₁ : μ.restrict (t i) = ν.restrict (t i) ∧ μ.restrict (⋃ x ∈ s, t x) = ν.restrict (⋃ x ∈ s, t x) ↔
  μ.restrict (t i) = ν.restrict (t i) ∧ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i)
Tactic: rw [restrict_union_congr, ← hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Finset ι
t : ι → Set α
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
have empty : μ.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: induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs =>
    simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]
    rw [restrict_union_congr, ← hs]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Finset ι
t : ι → Set α
empty :
  μ.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)
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
have insert : ∀ (i : ι) (s : Finset ι),
  i ∉ s →
    ∀ (hs : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)),
      μ.restrict (⋃ i_1 ∈ insert i s, t i_1) = ν.restrict (⋃ i_1 ∈ insert i s, t i_1) ↔
        ∀ i_1 ∈ insert i s, μ.restrict (t i_1) = ν.restrict (t i_1)
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs =>
    simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]
    rw [restrict_union_congr, ← hs]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Finset ι
t : ι → Set α
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
have empty : μ.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: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs =>
    simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]
    rw [restrict_union_congr, ← hs]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Finset ι
t : ι → Set α
empty :
  μ.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)
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
have insert : ∀ (i : ι) (s : Finset ι),
  i ∉ s →
    ∀ (hs : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)),
      μ.restrict (⋃ i_1 ∈ insert i s, t i_1) = ν.restrict (⋃ i_1 ∈ insert i s, t i_1) ↔
        ∀ i_1 ∈ insert i s, μ.restrict (t i_1) = ν.restrict (t i_1)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs =>
    simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]
    rw [restrict_union_congr, ← hs]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
⊢ μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i) ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
have refine : ∀ (h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)), μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i)
Tactic: refine ⟨fun h i => restrict_congr_mono (subset_iUnion _ _) h, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
⊢ μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i)
have h₁ : ∀ (t : Set α) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((ν.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: ext1 t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((ν.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have D : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (t : Finset ι) ↦ ⋃ i ∈ t, s i
Tactic: have D : Directed (· ⊆ ·) fun t : Finset ι => ⋃ i ∈ t, s i :=
    Monotone.directed_le fun t₁ t₂ ht => biUnion_subset_biUnion_left ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
t : Set α
ht : MeasurableSet t
D : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (t : Finset ι) ↦ ⋃ i ∈ t, s i
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((ν.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (t : Finset ι), ⋃ i ∈ t, s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
  ((ν.restrict (⋃ (t : Finset ι), ⋃ i ∈ t, s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [iUnion_eq_iUnion_finset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Set ι
t : ι → Set α
hc : s.Countable
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
have haveI : ∀ (this : Encodable (↑s : Type u_6)),
  μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
Tactic: haveI := hc.toEncodable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S : Set (Set α)
hc : S.Countable
⊢ μ.restrict (⋃₀ S) = ν.restrict (⋃₀ S) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s
have rw : μ.restrict (⋃ i ∈ S, i) = ν.restrict (⋃ i ∈ S, i) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s
Tactic: rw [sUnion_eq_biUnion, restrict_biUnion_congr hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S : Set (Set α)
hc : S.Countable
rw : μ.restrict (⋃ i ∈ S, i) = ν.restrict (⋃ i ∈ S, i) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s
⊢ μ.restrict (⋃₀ S) = ν.restrict (⋃₀ S) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s
have rw₁ : (∀ i ∈ S, μ.restrict i = ν.restrict i) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s
Tactic: rw [sUnion_eq_biUnion, restrict_biUnion_congr hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
⊢ (sInf m).restrict t = sInf ((fun (μ : Measure α) ↦ μ.restrict t) '' m)
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf ((fun (μ : Measure α) ↦ μ.restrict t) '' m) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf ((fun (μ : Measure α) ↦ μ.restrict t) '' m) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht),
    Set.image_image, restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ←
    Set.image_image _ toOuterMeasure, ← OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _),
    OuterMeasure.restrict_apply]