awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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_1 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∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
have := T_eq t ht
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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_1 u : Set α
hu : MeasurableSet u
ihu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
h :
  ∀ (ihu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞))
    (this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ uᶜ) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ uᶜ) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (uᶜ ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (uᶜ ∩ t) : ℝ≥0∞)

Tactic:
rw [Set.inter_comm] at ihu ⊢

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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_1 u : Set α
hu : MeasurableSet u
ihu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
h :
  ∀
    (this :
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (t \ u) : ℝ≥0∞) =
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
          ((ν : (a : Set α) → ℝ≥0∞) (t \ u) : ℝ≥0∞)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ uᶜ) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ uᶜ) : ℝ≥0∞)

Tactic:
rwa [← measure_inter_add_diff t hu, ← measure_inter_add_diff t hu, ← ihu,
      ENNReal.add_right_inj] at this

Premises used: ENNReal.add_right_inj, MeasureTheory.measure_inter_add_diff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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_1 u : Set α
hu : MeasurableSet u
ihu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
this :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t \ u) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (t \ u) : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ne_top_of_le_ne_top (htop t ht) (measure_mono Set.inter_subset_left)

Premises used: Set.inter_subset_left, ne_top_of_le_ne_top, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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_1 u : Set α
hu : MeasurableSet u
ihu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
this :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t \ u) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (t \ u) : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ne_top_of_le_ne_top (htop t ht) (measure_mono Set.inter_subset_left)

Premises used: Set.inter_subset_left, ne_top_of_le_ne_top, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⋃ (i : ℕ), f i) ∩ t) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) ((⋃ (i : ℕ), f i) ∩ t) : ℝ≥0∞)

Tactic:
simp only [← restrict_apply (hfm _), ← restrict_apply (MeasurableSet.iUnion hfm)] at ihf ⊢

Premises used: MeasureTheory.Measure.restrict_apply, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞) ((μ.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 [measure_iUnion hfd hfm, ihf]

Premises used: MeasureTheory.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
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∞)
⊢ 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]

Premises used: Compl.compl, ENNReal.add_right_inj, Set.empty_inter, Set.inter_subset_left, MeasureTheory.measure_empty, Set.inter_comm, MeasureTheory.measure_inter_add_diff, ne_top_of_le_ne_top, MeasureTheory.measure_mono, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
⊢ μ = ν

Tactic:
ext_of_generateFrom_of_cover h_gen hc h_inter hU htop ?_ fun t ht => h_eq t (h_sub ht)

Premises used: MeasureTheory.Measure.ext_of_generateFrom_of_cover
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
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)

Premises used: MeasureTheory.Measure.ext_of_generateFrom_of_cover
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
inr :
  ∀ (H : (s ∩ t).Nonempty),
    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∞)

Tactic:
rcases (s ∩ t).eq_empty_or_nonempty with H | H

Premises used: Inter.inter, Set.eq_empty_or_nonempty
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
H : s ∩ t = ∅
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)

Tactic:
simp only [H, measure_empty]

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
H : (s ∩ t).Nonempty
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)

Tactic:
h_eq _ (h_inter _ hs _ (h_sub ht) H)
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
H : (s ∩ t).Nonempty
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)

Tactic:
exact h_eq _ (h_inter _ hs _ (h_sub ht) H)
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
⊢ μ = ν

Tactic:
ext_of_generateFrom_of_cover_subset hA hC ?_ (countable_range B) h1B ?_ h_eq

Premises used: Set.countable_range, MeasureTheory.Measure.ext_of_generateFrom_of_cover_subset
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
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

Premises used: Set.countable_range, MeasureTheory.Measure.ext_of_generateFrom_of_cover_subset
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
i : ℕ
⊢ B i ∈ C

Tactic:
apply h2B
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
i : ℕ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply hμB
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : ι → Measure α
s : Set α
hs : MeasurableSet 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∞)

Tactic:
simp only [sum_apply, restrict_apply, ht, ht.inter hs]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.sum_apply, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst : Countable ι
μ : ι → Measure α
s : Set α
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∞)
⊢ (sum μ).restrict s = sum fun (i : ι) ↦ (μ i).restrict s

Tactic:
ext t ht
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
h₁ :
  Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((sum μ).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((sum fun (i : ι) ↦ (μ i).restrict s : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp_rw [sum_apply _ ht, restrict_apply ht, sum_apply_of_countable]

Premises used: MeasureTheory.Measure.sum_apply_of_countable, MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.sum_apply
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s : Set α
⊢ μ.restrict s ≪ ν.restrict s

Tactic:
Measure.AbsolutelyContinuous.mk (fun t ht htν ↦ ?_)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s : Set α
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∞)
⊢ μ.restrict s ≪ ν.restrict s

Tactic:
refine Measure.AbsolutelyContinuous.mk (fun t ht htν ↦ ?_)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
rw :
  ∀ (htν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [restrict_apply ht] at htν ⊢

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

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

Tactic:
exact h htν
-- 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∞) ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((sum fun (i : ι) ↦ μ.restrict (s i) : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [sum_apply _ ht, restrict_iUnion_apply_ae hd hm ht]

Premises used: MeasureTheory.Measure.sum_apply, 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 : Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ.restrict (⋃ (i : ι), s i) = sum fun (i : ι) ↦ μ.restrict (s i)

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

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.restrict_iUnion_ae, Pairwise.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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)
rw : μ.restrict (⋃ (x : (↑T : Type u_6)), s (↑x : ι)) = sum fun (i : (↑T : Type u_6)) ↦ μ.restrict (s (↑i : ι))
⊢ μ.restrict (⋃ i ∈ T, s i) = sum fun (i : (↑T : Type u_6)) ↦ μ.restrict (s (↑i : ι))

Tactic:
rw [Set.biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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 (⋃ (x : (↑T : Type u_6)), s (↑x : ι)) = sum fun (i : (↑T : Type u_6)) ↦ μ.restrict (s (↑i : ι))

Tactic:
restrict_iUnion (fun i j hij ↦ hd i.coe_prop j.coe_prop (Subtype.coe_ne_coe.mpr hij)) (hm ·)

Premises used: Iff.mpr, Subtype.coe_prop, MeasureTheory.Measure.restrict_iUnion, Subtype.val, Subtype.coe_ne_coe
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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 (⋃ (x : (↑T : Type u_6)), s (↑x : ι)) = sum fun (i : (↑T : Type u_6)) ↦ μ.restrict (s (↑i : ι))

Tactic:
exact restrict_iUnion (fun i j hij ↦ hd i.coe_prop j.coe_prop (Subtype.coe_ne_coe.mpr hij)) (hm ·)
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
T : Finset ι
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ.restrict (⋃ i ∈ T, s i) = sum fun (i : ↥T) ↦ μ.restrict (s (↑i : ι))

Tactic:
restrict_biUnion (T := (T : Set ι)) Finite.to_countable hd hm

Premises used: MeasureTheory.Measure.restrict_biUnion, Finite.to_countable
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
t : Set α
ht : MeasurableSet t
⊢ LE.le (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((sum fun (i : ι) ↦ μ.restrict (s i) : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simpa [ht, inter_iUnion] using measure_iUnion_le (t ∩ s ·)

Premises used: Inter.inter, MeasureTheory.measure_iUnion_le, Set.inter_iUnion