awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
rw :
  HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [← measure_inter_add_diff (s ∪ t) ht, Set.union_inter_cancel_right, union_diff_right, ←
    measure_inter_add_diff s ht]

Premises used: MeasureTheory.measure_inter_add_diff, Set.union_diff_right, Union.union, Set.union_inter_cancel_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
ac_rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₃ rw₄ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [union_comm, inter_comm, measure_union_add_inter t hs, add_comm]

Premises used: MeasureTheory.measure_union_add_inter, Set.union_comm, add_comm, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
simpa only [symmDiff_def, sup_eq_union]
    using measure_union₀ (ht.diff hs) disjoint_sdiff_sdiff.aedisjoint

Premises used: symmDiff_def, Set.sup_eq_union, Disjoint.aedisjoint, MeasureTheory.NullMeasurableSet.diff, MeasureTheory.measure_union₀, disjoint_sdiff_sdiff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∆ u) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t ∆ u) : ℝ≥0∞)

Tactic:
le_trans (μ.mono <| symmDiff_triangle s t u) (measure_union_le (s ∆ t) (t ∆ u))

Premises used: MeasureTheory.OuterMeasure.mono, symmDiff_triangle, MeasureTheory.Measure.toOuterMeasure, symmDiff, MeasureTheory.measure_union_le, le_trans
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_mono_top subset_union_right (measure_diff_eq_top ht hs)

Premises used: Set.subset_union_right, MeasureTheory.measure_mono_top, MeasureTheory.measure_diff_eq_top
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) univ

Tactic:
measure_add_measure_compl₀ h.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measure_add_measure_compl₀
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
haveI :
  ∀ (this : Encodable (↑s : Type u_2)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞)
      (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f (↑p : β)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞)
    (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f (↑p : β)) : ℝ≥0∞)

Tactic:
haveI := hs.toEncodable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
this : Encodable (↑s : Type u_2)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : (↑s : Type u_2)), f (↑x : β)) : ℝ≥0∞)
    (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f (↑p : β)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞)
    (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f (↑p : β)) : ℝ≥0∞)

Tactic:
rw [biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
this : Encodable (↑s : Type u_2)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : (↑s : Type u_2)), f (↑x : β)) : ℝ≥0∞)
    (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f (↑p : β)) : ℝ≥0∞)

Tactic:
measure_iUnion₀ (hd.on_injective Subtype.coe_injective fun x => x.2) fun x => h x x.2

Premises used: MeasureTheory.measure_iUnion₀, Subtype.coe_injective, Set.Pairwise.on_injective, Subtype.val, Subtype.property
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
this : Encodable (↑s : Type u_2)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : (↑s : Type u_2)), f (↑x : β)) : ℝ≥0∞)
    (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f (↑p : β)) : ℝ≥0∞)

Tactic:
exact measure_iUnion₀ (hd.on_injective Subtype.coe_injective fun x => x.2) fun x => h x x.2

Premises used: MeasureTheory.measure_iUnion₀, Subtype.coe_injective, Set.Pairwise.on_injective, Subtype.val, Subtype.property
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.PairwiseDisjoint f
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞)
    (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f (↑p : β)) : ℝ≥0∞)

Tactic:
measure_biUnion₀ hs hd.aedisjoint fun b hb => (h b hb).nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, Set.PairwiseDisjoint.aedisjoint, MeasureTheory.measure_biUnion₀
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hs : S.Countable
hd : S.Pairwise (AEDisjoint μ)
h : ∀ s ∈ S, NullMeasurableSet s μ
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ S, i) : ℝ≥0∞)
    (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∑' (p : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑p : Set α))
    (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ S) : ℝ≥0∞)
    (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)

Tactic:
rw [sUnion_eq_biUnion, measure_biUnion₀ hs hd h]

Premises used: Set.sUnion_eq_biUnion, MeasureTheory.measure_biUnion₀
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hs : S.Countable
hd : S.Pairwise Disjoint
h : ∀ s ∈ S, MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ S, i) : ℝ≥0∞)
    (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∑' (p : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑p : Set α))
    (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ S) : ℝ≥0∞)
    (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)

Tactic:
rw [sUnion_eq_biUnion, measure_biUnion hs hd h]

Premises used: MeasureTheory.measure_biUnion, Set.sUnion_eq_biUnion
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞)
    (∑' (b : ↥s), (μ : (a : Set α) → ℝ≥0∞) (f (↑b : ι)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞) (∑ p ∈ s, (μ : (a : Set α) → ℝ≥0∞) (f p) : ℝ≥0∞)

Tactic:
rw [← Finset.sum_attach, Finset.attach_eq_univ, ← tsum_fintype (L := .unconditional s)]

Premises used: Finset.attach_eq_univ, Finset.sum_attach, tsum_fintype
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞)
    (∑' (b : ↥s), (μ : (a : Set α) → ℝ≥0∞) (f (↑b : ι)) : ℝ≥0∞)

Tactic:
measure_biUnion₀ s.countable_toSet hd hm

Premises used: Finset.countable_toSet, MeasureTheory.measure_biUnion₀
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞)
    (∑' (b : ↥s), (μ : (a : Set α) → ℝ≥0∞) (f (↑b : ι)) : ℝ≥0∞)

Tactic:
exact measure_biUnion₀ s.countable_toSet hd hm

Premises used: Finset.countable_toSet, MeasureTheory.measure_biUnion₀
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ s, MeasurableSet (f b)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞) (∑ p ∈ s, (μ : (a : Set α) → ℝ≥0∞) (f p) : ℝ≥0∞)

Tactic:
measure_biUnion_finset₀ hd.aedisjoint fun b hb => (hm b hb).nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, Set.PairwiseDisjoint.aedisjoint, MeasureTheory.measure_biUnion_finset₀
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_8
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
rw :
  ∀ (i : Finset ι),
    LE.le (α := ℝ≥0∞) (∑ a ∈ i, (μ : (a : Set α) → ℝ≥0∞) (As a) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞)

Tactic:
rw [ENNReal.tsum_eq_iSup_sum, iSup_le_iff]

Premises used: ENNReal.tsum_eq_iSup_sum, iSup_le_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_8
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
simp :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, As b) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ a ∈ s, (μ : (a : Set α) → ℝ≥0∞) (As a) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞)

Tactic:
simp only [← measure_biUnion_finset₀ (fun _i _hi _j _hj hij => As_disj hij) fun i _ => As_mble i]

Premises used: MeasureTheory.measure_biUnion_finset₀
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_8
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
h : ∀ (i : ι), ⋃ (_ : i ∈ s), As i ⊆ As i
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, As b) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_8
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
i : ι
⊢ ⋃ (_ : i ∈ s), As i ⊆ As i

Tactic:
iUnion_subset fun _ ↦ Subset.rfl

Premises used: Set.iUnion_subset, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_8
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
i : ι
⊢ ⋃ (_ : i ∈ s), As i ⊆ As i

Tactic:
exact iUnion_subset fun _ ↦ Subset.rfl

Premises used: Set.iUnion_subset, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_8
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞)

Tactic:
tsum_meas_le_meas_iUnion_of_disjoint₀ μ (fun i ↦ (As_mble i).nullMeasurableSet)
    (fun _ _ h ↦ Disjoint.aedisjoint (As_disj h))

Premises used: MeasurableSet.nullMeasurableSet, Disjoint.aedisjoint, MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
hs : s.Countable
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
rw :
  Eq (α := ℝ≥0∞) (∑' (b : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {(↑b : β)}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ s, f ⁻¹' {y}) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∑' (b : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {(↑b : β)}))
    (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {(↑p : β)}))
⊢ Eq (α := ℝ≥0∞) (∑' (b : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {(↑b : β)}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [← Set.biUnion_preimage_singleton, measure_biUnion hs (pairwiseDisjoint_fiber f s) hf]

Premises used: Set.biUnion_preimage_singleton, MeasureTheory.measure_biUnion, Set.pairwiseDisjoint_fiber
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : α → β
hs : s.Countable
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ s, f ⁻¹' {y}) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {x}) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ rw₂ :
  (∀ i ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {i}) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {x}) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {x}) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← biUnion_preimage_singleton, measure_biUnion_null_iff hs]

Premises used: Set.biUnion_preimage_singleton, MeasureTheory.measure_biUnion_null_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
⊢ Eq (α := ℝ≥0∞) (∑ b ∈ s, (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {b}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' (↑s : Set β)) : ℝ≥0∞)

Tactic:
simp only [← measure_biUnion_finset (pairwiseDisjoint_fiber f s) hf,
    Finset.set_biUnion_preimage_singleton]

Premises used: SetLike.coe, MeasureTheory.measure_biUnion_finset, Set.pairwiseDisjoint_fiber, Finset.set_biUnion_preimage_singleton
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst : MeasurableSingletonClass α
trans : Eq (α := ℝ≥0∞) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) {x}) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' {x}))
trans₁ :
  Eq (α := ℝ≥0∞) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' {x}) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)

Tactic:
trans ∑ x ∈ s, μ (id ⁻¹' {x})
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst : MeasurableSingletonClass α
⊢ Eq (α := ℝ≥0∞) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) {x}) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' {x}))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst : MeasurableSingletonClass α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' (↑s : Set α)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
hf : ∀ y ∈ s, MeasurableSet (α := α) (id ⁻¹' {y})
⊢ Eq (α := ℝ≥0∞) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' {x}) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)

Tactic:
rw [sum_measure_preimage_singleton]

Premises used: MeasureTheory.sum_measure_preimage_singleton
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst : MeasurableSingletonClass α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' (↑s : Set α)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst : MeasurableSingletonClass α
⊢ ∀ y ∈ s, MeasurableSet (α := α) (id ⁻¹' {y})

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∩ s₂) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ \ s₂) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞)

Tactic:
measure_congr <| diff_ae_eq_self.2 h

Premises used: Iff.mpr, MeasureTheory.measure_congr, MeasureTheory.diff_ae_eq_self
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t \ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∪ t)

Tactic:
rw [← measure_union₀' hs disjoint_sdiff_right.aedisjoint, union_diff_self]

Premises used: MeasureTheory.measure_union₀', Disjoint.aedisjoint, Set.disjoint_sdiff_right, Set.union_diff_self
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
hm : NullMeasurableSet t μ
h_fin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∪ t)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∪ t)

Tactic:
rw [add_comm, measure_add_diff hm, union_comm]

Premises used: MeasureTheory.measure_add_diff, Set.union_comm, add_comm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₂ ⊆ s₁
h₂ : NullMeasurableSet s₂ μ
h_fin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)
rw₁ rw₂ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s₁ \ s₂) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)

Tactic:
rw [measure_diff' _ h₂ h_fin, union_eq_self_of_subset_right h]

Premises used: Set.union_eq_self_of_subset_right, MeasureTheory.measure_diff'
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
bc : s₁ ∩ s₂ ⊆ s₂
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∩ s₂) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s₁ \ s₂) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ \ s₂) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ s₁ ∩ s₂ ⊆ s₂

Tactic:
apply inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ s₁ \ s₂ ⊆ s₁ ∆ s₂

Tactic:
simp [symmDiff_def]

Premises used: symmDiff_def
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
suffices :
  ∀ (u v : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∆ v) : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
suffices h : ∀ u v, μ (u ∆ v) ≠ ∞ → μ u = ∞ → μ v = ∞
    from ⟨h s t hμst, h t s (symmDiff_comm s t ▸ hμst)⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Set α
hμuv : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∆ v) : ℝ≥0∞) (∞ : ℝ≥0∞)
hμu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
by_contra! : ∀ (hμv : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)), False
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
by_contra! hμv