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 (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u : Set α
f : ℕ → Set α
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f i ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⋃ (i : ℕ), f i) ∩ t) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) ((⋃ (i : ℕ), f i) ∩ t) : ℝ≥0∞)
have h : ∀
  (ihf :
    ∀ (i : ℕ),
      Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
        ((ν.restrict t : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    ((ν.restrict t : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
Tactic: simp only [← restrict_apply (hfm _), ← restrict_apply (MeasurableSet.iUnion hfm)] at ihf ⊢
Cleared hypotheses: ihf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (∅ ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (∅ ∩ t) : ℝ≥0∞)
Tactic: induction u, hu using induction_on_inter h_gen h_inter with
  | empty => simp only [Set.empty_inter, measure_empty]
  | basic u hu => exact ST_eq _ ht _ hu
  | compl u hu ihu =>
    have := T_eq t ht
    rw [Set.inter_comm] at ihu ⊢
    rwa [← measure_inter_add_diff t hu, ← measure_inter_add_diff t hu, ← ihu,
      ENNReal.add_right_inj] at this
    exact ne_top_of_le_ne_top (htop t ht) (measure_mono Set.inter_subset_left)
  | iUnion f hfd hfm ihf =>
    simp only [← restrict_apply (hfm _), ← restrict_apply (MeasurableSet.iUnion hfm)] at ihf ⊢
    simp only [measure_iUnion hfd hfm, ihf]
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u : Set α
hu : MeasurableSet u
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (∅ ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (∅ ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
have h₁ : ∀ (u : Set α) (hu : u ∈ S),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
Tactic: induction u, hu using induction_on_inter h_gen h_inter with
  | empty => simp only [Set.empty_inter, measure_empty]
  | basic u hu => exact ST_eq _ ht _ hu
  | compl u hu ihu =>
    have := T_eq t ht
    rw [Set.inter_comm] at ihu ⊢
    rwa [← measure_inter_add_diff t hu, ← measure_inter_add_diff t hu, ← ihu,
      ENNReal.add_right_inj] at this
    exact ne_top_of_le_ne_top (htop t ht) (measure_mono Set.inter_subset_left)
  | iUnion f hfd hfm ihf =>
    simp only [← restrict_apply (hfm _), ← restrict_apply (MeasurableSet.iUnion hfm)] at ihf ⊢
    simp only [measure_iUnion hfd hfm, ihf]
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u : Set α
hu : MeasurableSet u
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (∅ ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (∅ ∩ t) : ℝ≥0∞)
h₁ :
  ∀ (u : Set α) (hu : u ∈ S),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
have h₂ : ∀ (u : Set α) (hu : MeasurableSet u)
  (ihu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (uᶜ ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (uᶜ ∩ t) : ℝ≥0∞)
Tactic: induction u, hu using induction_on_inter h_gen h_inter with
  | empty => simp only [Set.empty_inter, measure_empty]
  | basic u hu => exact ST_eq _ ht _ hu
  | compl u hu ihu =>
    have := T_eq t ht
    rw [Set.inter_comm] at ihu ⊢
    rwa [← measure_inter_add_diff t hu, ← measure_inter_add_diff t hu, ← ihu,
      ENNReal.add_right_inj] at this
    exact ne_top_of_le_ne_top (htop t ht) (measure_mono Set.inter_subset_left)
  | iUnion f hfd hfm ihf =>
    simp only [← restrict_apply (hfm _), ← restrict_apply (MeasurableSet.iUnion hfm)] at ihf ⊢
    simp only [measure_iUnion hfd hfm, ihf]
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u : Set α
hu : MeasurableSet u
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (∅ ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (∅ ∩ t) : ℝ≥0∞)
h₁ :
  ∀ (u : Set α) (hu : u ∈ S),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
h₂ :
  ∀ (u : Set α) (hu : MeasurableSet u)
    (ihu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (uᶜ ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (uᶜ ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
have h₃ : ∀ (f : ℕ → Set α) (hfd : Pairwise (Disjoint on f)) (hfm : ∀ (i : ℕ), MeasurableSet (f i))
  (ihf :
    ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f i ∩ t) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⋃ (i : ℕ), f i) ∩ t) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) ((⋃ (i : ℕ), f i) ∩ t) : ℝ≥0∞)
Tactic: induction u, hu using induction_on_inter h_gen h_inter with
  | empty => simp only [Set.empty_inter, measure_empty]
  | basic u hu => exact ST_eq _ ht _ hu
  | compl u hu ihu =>
    have := T_eq t ht
    rw [Set.inter_comm] at ihu ⊢
    rwa [← measure_inter_add_diff t hu, ← measure_inter_add_diff t hu, ← ihu,
      ENNReal.add_right_inj] at this
    exact ne_top_of_le_ne_top (htop t ht) (measure_mono Set.inter_subset_left)
  | iUnion f hfd hfm ihf =>
    simp only [← restrict_apply (hfm _), ← restrict_apply (MeasurableSet.iUnion hfm)] at ihf ⊢
    simp only [measure_iUnion hfd hfm, ihf]
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_eq : ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν
have refine : ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: refine ext_of_generateFrom_of_cover h_gen hc h_inter hU htop ?_ fun t ht => h_eq t (h_sub ht)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_eq : ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have inl : ∀ (H : s ∩ t = ∅), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rcases (s ∩ t).eq_empty_or_nonempty with H | H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_eq : ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
inl :
  ∀ (H : s ∩ t = ∅), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have inr : ∀ (H : (s ∩ t).Nonempty),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rcases (s ∩ t).eq_empty_or_nonempty with H | H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : Eq.{u_2 + 1} (α := Set α) (⋃ (i : ℕ), B i) univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_eq : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν
have refine_1 : range B ⊆ C
Tactic: refine ext_of_generateFrom_of_cover_subset hA hC ?_ (countable_range B) h1B ?_ h_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : Eq.{u_2 + 1} (α := Set α) (⋃ (i : ℕ), B i) univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_eq : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
refine_1 : range B ⊆ C
⊢ μ = ν
have refine_2 : ∀ s ∈ range B, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ext_of_generateFrom_of_cover_subset hA hC ?_ (countable_range B) h1B ?_ h_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst : Countable ι
μ : ι → Measure α
s : Set α
⊢ (sum μ).restrict s = sum fun (i : ι) ↦ (μ i).restrict s
have h : ∀ (t : Set α) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞) (((sum μ).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((sum fun (i : ι) ↦ (μ i).restrict s : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: ext t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst : Countable ι
μ : ι → Measure α
s t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (((sum μ).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((sum fun (i : ι) ↦ (μ i).restrict s : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((sum μ).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
  (∑' (i : ι), ((μ i).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp_rw [sum_apply _ ht, restrict_apply ht, sum_apply_of_countable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst : Countable ι
μ : ι → Measure α
s t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) (((sum μ).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (∑' (i : ι), ((μ i).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((sum μ).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((sum fun (i : ι) ↦ (μ i).restrict s : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: simp_rw [sum_apply _ ht, restrict_apply ht, sum_apply_of_countable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s : Set α
⊢ μ.restrict s ≪ ν.restrict s
have refine : ∀ (t : Set α) (ht : MeasurableSet t) (htν : Eq (α := ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine Measure.AbsolutelyContinuous.mk (fun t ht htν ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s t : Set α
ht : MeasurableSet t
htν : Eq (α := ℝ≥0∞) ((ν.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : ∀ (htν : 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] at htν ⊢
Cleared hypotheses: htν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
T : Set ι
hT : Countable.{u_6 + 1} (↑T : Type u_6)
hd : T.Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ.restrict (⋃ i ∈ T, s i) = sum fun (i : (↑T : Type u_6)) ↦ μ.restrict (s (↑i : ι))
have rw : μ.restrict (⋃ (x : (↑T : Type u_6)), s (↑x : ι)) = sum fun (i : (↑T : Type u_6)) ↦ μ.restrict (s (↑i : ι))
Tactic: rw [Set.biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))
have this : Countable.{u_6 + 1} (↑t : Type u_6)
Tactic: haveI := ht.to_subtype
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable.{u_6 + 1} (↑t : Type u_6)
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))
have rw : ae (μ.restrict (⋃ (x : (↑t : Type u_6)), s (↑x : ι))) = ⨆ i ∈ t, ae (μ.restrict (s i))
Tactic: rw [biUnion_eq_iUnion, ae_restrict_iUnion_eq, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable.{u_6 + 1} (↑t : Type u_6)
rw : ae (μ.restrict (⋃ (x : (↑t : Type u_6)), s (↑x : ι))) = ⨆ i ∈ t, ae (μ.restrict (s i))
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))
have rw₁ : Eq.{u_2 + 1} (α := Filter α) (⨆ (i : (↑t : Type u_6)), ae (μ.restrict (s (↑i : ι)))) (⨆ i ∈ t, ae (μ.restrict (s i)))
Tactic: rw [biUnion_eq_iUnion, ae_restrict_iUnion_eq, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable.{u_6 + 1} (↑t : Type u_6)
rw : ae (μ.restrict (⋃ (x : (↑t : Type u_6)), s (↑x : ι))) = ⨆ i ∈ t, ae (μ.restrict (s i))
rw₁ :
  Eq.{u_2 + 1} (α := Filter α) (⨆ (i : (↑t : Type u_6)), ae (μ.restrict (s (↑i : ι)))) (⨆ i ∈ t, ae (μ.restrict (s i)))
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))
have rw₂ : Eq.{u_2 + 1} (α := Filter α) (⨆ (i : (↑t : Type u_6)), ae (μ.restrict (s (↑i : ι))))
  (⨆ (i : (↑t : Type u_6)), ae (μ.restrict (s (↑i : ι))))
Tactic: rw [biUnion_eq_iUnion, ae_restrict_iUnion_eq, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x
have simp_rw : {x : α | p x} ∈ ae (μ.restrict (⋃ i ∈ t, s i)) ↔ ∀ i ∈ t, {x : α | p x} ∈ ae (μ.restrict (s i))
Tactic: simp_rw [Filter.Eventually, ae_restrict_biUnion_eq s ht, mem_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
p : α → Prop
simp_rw : {x : α | p x} ∈ ae (μ.restrict (⋃ i ∈ t, s i)) ↔ ∀ i ∈ t, {x : α | p x} ∈ ae (μ.restrict (s i))
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x
have simp_rw₁ : Membership.mem (γ := Filter α) (⨆ i ∈ t, ae (μ.restrict (s i))) {x : α | p x} ↔
  ∀ i ∈ t, {x : α | p x} ∈ ae (μ.restrict (s i))
Tactic: simp_rw [Filter.Eventually, ae_restrict_biUnion_eq s ht, mem_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Finset ι
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x
have simp_rw : {x : α | p x} ∈ ae (μ.restrict (⋃ i ∈ t, s i)) ↔ ∀ i ∈ t, {x : α | p x} ∈ ae (μ.restrict (s i))
Tactic: simp_rw [Filter.Eventually, ae_restrict_biUnion_finset_eq s, mem_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Finset ι
p : α → Prop
simp_rw : {x : α | p x} ∈ ae (μ.restrict (⋃ i ∈ t, s i)) ↔ ∀ i ∈ t, {x : α | p x} ∈ ae (μ.restrict (s i))
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x
have simp_rw₁ : Membership.mem (γ := Filter α) (⨆ i ∈ t, ae (μ.restrict (s i))) {x : α | p x} ↔
  ∀ i ∈ t, {x : α | p x} ∈ ae (μ.restrict (s i))
Tactic: simp_rw [Filter.Eventually, ae_restrict_biUnion_finset_eq s, mem_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
f g : α → δ
⊢ f =ᶠ[ae (μ.restrict (⋃ (i : ι), s i))] g ↔ ∀ (i : ι), f =ᶠ[ae (μ.restrict (s i))] g
have simp_rw : (∀ᵐ (x : α) ∂μ.restrict (⋃ (i : ι), s i), f x = g x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x
Tactic: simp_rw [EventuallyEq, ae_restrict_iUnion_eq, eventually_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
f g : α → δ
simp_rw : (∀ᵐ (x : α) ∂μ.restrict (⋃ (i : ι), s i), f x = g x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x
⊢ f =ᶠ[ae (μ.restrict (⋃ (i : ι), s i))] g ↔ ∀ (i : ι), f =ᶠ[ae (μ.restrict (s i))] g
have simp_rw₁ : (∀ᶠ (x : α) in ⨆ (i : ι), ae (μ.restrict (s i)), f x = g x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x
Tactic: simp_rw [EventuallyEq, ae_restrict_iUnion_eq, eventually_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
f g : α → δ
⊢ f =ᶠ[ae (μ.restrict (⋃ i ∈ t, s i))] g ↔ ∀ i ∈ t, f =ᶠ[ae (μ.restrict (s i))] g
have simp_rw : f =ᶠ[⨆ i ∈ t, ae (μ.restrict (s i))] g ↔ ∀ i ∈ t, f =ᶠ[ae (μ.restrict (s i))] g
Tactic: simp_rw [ae_restrict_biUnion_eq s ht, EventuallyEq, eventually_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
f g : α → δ
simp_rw : f =ᶠ[⨆ i ∈ t, ae (μ.restrict (s i))] g ↔ ∀ i ∈ t, f =ᶠ[ae (μ.restrict (s i))] g
⊢ f =ᶠ[ae (μ.restrict (⋃ i ∈ t, s i))] g ↔ ∀ i ∈ t, f =ᶠ[ae (μ.restrict (s i))] g
have simp_rw₁ : (∀ᶠ (x : α) in ⨆ i ∈ t, ae (μ.restrict (s i)), f x = g x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x
Tactic: simp_rw [ae_restrict_biUnion_eq s ht, EventuallyEq, eventually_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : LinearOrder α
a b : α
P : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict (Ι a b), P x) ↔
    (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x
have rw : (∀ᶠ (x : α) in ae (μ.restrict (Ioc a b)) ⊔ ae (μ.restrict (Ioc b a)), P x) ↔
  (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x
Tactic: rw [ae_restrict_uIoc_eq, eventually_sup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : LinearOrder α
a b : α
P : α → Prop
rw :
  (∀ᶠ (x : α) in ae (μ.restrict (Ioc a b)) ⊔ ae (μ.restrict (Ioc b a)), P x) ↔
    (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x
⊢ (∀ᵐ (x : α) ∂μ.restrict (Ι a b), P x) ↔
    (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x
have rw₁ : ((∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x) ↔
  (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x
Tactic: rw [ae_restrict_uIoc_eq, eventually_sup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x : α | p x} (μ.restrict s)
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x
have simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [ae_iff, ← compl_setOf, Measure.restrict_apply₀ hp.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x : α | p x} (μ.restrict s)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) =
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [iff_iff_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x : α | p x} (μ.restrict s)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) =
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have e_a : ∀ (x : α), x ∈ {x : α | p x}ᶜ ∩ s ↔ Membership.mem (γ := Set α) {x : α | x ∈ s → p x}ᶜ x
Tactic: congr with x