awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
calc :
  LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑ q ∈ Q.parts, ∑' (i : ℕ), f ((↑q : Set X) ⊓ (↑(s' i) : Set X)))
calc₁ :
  Eq (α := ℝ≥0∞) (∑' (i : ℕ), ∑ q ∈ Q.parts, f ((↑q : Set X) ⊓ (↑(s' i) : Set X)))
    (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))
⊢ LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))

Tactic:
calc ∑ q ∈ Q.parts, f q
      _ ≤ ∑ q ∈ Q.parts, ∑' i, f (q ⊓ s' i) := by
          apply Finset.sum_le_sum fun q hq => ?_
          have hq_eq : q.val = ⋃ i, q.val ∩ s i := by
            rw [← Set.inter_iUnion]; exact (Set.inter_eq_left.mpr (Q.le hq)).symm
          let t (i : ℕ) : Subtype MeasurableSet := ⟨q.val ∩ s i, q.2.inter (hs i)⟩
          have ht_disj : Pairwise (Disjoint on (Subtype.val ∘ t)) :=
            fun i j hij => (hs' hij).mono Set.inter_subset_right Set.inter_subset_right
          calc f q
            _ = f (⋃ i, q.val ∩ s i) := congrArg f hq_eq
            _ = f (⋃ i, (t i).val) := rfl
            _ ≤ ∑' i, f (t i) := hf t ht_disj
            _ = ∑' i, f (q ⊓ s' i) := rfl
      _ = ∑' i, ∑ q ∈ Q.parts, f (q ⊓ s' i) :=
          (Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)).symm
      _ = ∑' i, ∑ p ∈ (P i).parts, f p := by
          congr 1; funext i
          exact (Q.sum_restrict _ (fun p => f p) hf').symm

Premises used: ENNReal.summable, Finpartition.parts, Eq.symm, Summable.tsum_finsetSum
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
⊢ LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))

Tactic:
have splitting : ∑ q ∈ Q.parts, f q ≤ ∑' i, ∑ p ∈ (P i).parts, f p := by
    calc ∑ q ∈ Q.parts, f q
      _ ≤ ∑ q ∈ Q.parts, ∑' i, f (q ⊓ s' i) := by
          apply Finset.sum_le_sum fun q hq => ?_
          have hq_eq : q.val = ⋃ i, q.val ∩ s i := by
            rw [← Set.inter_iUnion]; exact (Set.inter_eq_left.mpr (Q.le hq)).symm
          let t (i : ℕ) : Subtype MeasurableSet := ⟨q.val ∩ s i, q.2.inter (hs i)⟩
          have ht_disj : Pairwise (Disjoint on (Subtype.val ∘ t)) :=
            fun i j hij => (hs' hij).mono Set.inter_subset_right Set.inter_subset_right
          calc f q
            _ = f (⋃ i, q.val ∩ s i) := congrArg f hq_eq
            _ = f (⋃ i, (t i).val) := rfl
            _ ≤ ∑' i, f (t i) := hf t ht_disj
            _ = ∑' i, f (q ⊓ s' i) := rfl
      _ = ∑' i, ∑ q ∈ Q.parts, f (q ⊓ s' i) :=
          (Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)).symm
      _ = ∑' i, ∑ p ∈ (P i).parts, f p := by
          congr 1; funext i
          exact (Q.sum_restrict _ (fun p => f p) hf').symm
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
splitting : LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))
obtain :
  ∀ (n : ℕ) (hn : b < ∑ a ∈ Finset.range n, ∑ p ∈ (P a).parts, f (↑p : Set X)),
    ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)
⊢ ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)

Tactic:
obtain ⟨n, hn⟩ := lt_iSup_iff.mp <| ENNReal.tsum_eq_iSup_nat ▸ lt_of_lt_of_le hQ splitting

Premises used: Iff.mp, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
splitting : LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))
n : ℕ
hn : b < ∑ a ∈ Finset.range n, ∑ p ∈ (P a).parts, f (↑p : Set X)
⊢ ∀ (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X) ≤ preVariationFun f (s i)

Tactic:
have bound (i : ℕ) : ∑ p ∈ (P i).parts, f p ≤ preVariationFun f (s i) := sum_le f (hs i) (P i)
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
splitting : LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))
n : ℕ
hn : b < ∑ a ∈ Finset.range n, ∑ p ∈ (P a).parts, f (↑p : Set X)
bound : ∀ (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X) ≤ preVariationFun f (s i)
⊢ ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)

Tactic:
⟨Finset.range n, lt_of_lt_of_le hn (Finset.sum_le_sum fun i _ => bound i)⟩

Premises used: Finset.range, Exists.intro, Finset.sum_le_sum, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
splitting : LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))
n : ℕ
hn : b < ∑ a ∈ Finset.range n, ∑ p ∈ (P a).parts, f (↑p : Set X)
bound : ∀ (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X) ≤ preVariationFun f (s i)
⊢ ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)

Tactic:
exact ⟨Finset.range n, lt_of_lt_of_le hn (Finset.sum_le_sum fun i _ => bound i)⟩
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
x : Set X
h : ¬MeasurableSet x
⊢ preVariationFun f x = 0

Tactic:
simp [preVariationFun, h]

Premises used: MeasureTheory.preVariationFun
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : Set X
⊢ (↑(ennrealPreVariation f hf hf') : Set X → ℝ≥0∞) s = preVariationFun f s

Tactic:
rfl

Premises used: dite, MeasureTheory.preVariationFun, rfl
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (0 ∅) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
h : ∀ (i : Set X), MeasurableSet i → (↑(ennrealPreVariation 0 ⋯ ⋯) : Set X → ℝ≥0∞) i = (↑0 : Set X → ℝ≥0∞) i
⊢ Eq.{u_1 + 1} (α := VectorMeasure X ℝ≥0∞) (ennrealPreVariation 0 ⋯ ⋯) 0

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
i : Set X
h : MeasurableSet i
⊢ (↑(ennrealPreVariation 0 ⋯ ⋯) : Set X → ℝ≥0∞) i = (↑0 : Set X → ℝ≥0∞) i

Tactic:
simp [ennrealPreVariation_apply]

Premises used: MeasureTheory.ennrealPreVariation_apply
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : Set X
⊢ Eq (α := ℝ≥0∞) ((preVariation f hf hf' : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((ennrealPreVariation f hf hf').ennrealToMeasure : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
h :
  ∀ (s : Set X),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((preVariation 0 ⋯ ⋯ : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
        (((0 : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Measure X) (preVariation 0 ⋯ ⋯) 0

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
s : Set X
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((preVariation 0 ⋯ ⋯ : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [preVariation_apply]

Premises used: MeasureTheory.preVariation_apply
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ IsProbabilityMeasure (↑μ : Measure Ω)

Tactic:
μ.prop

Premises used: Subtype.prop, MeasureTheory.ProbabilityMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : Measure Ω
hμ : IsProbabilityMeasure μ
⊢ (↑(Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) μ hμ) : Measure Ω) = μ

Tactic:
rfl

Premises used: MeasureTheory.ProbabilityMeasure.toMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
⊢ (↑ν : Measure Ω) = (↑ν : Measure Ω)

Tactic:
rfl

Premises used: MeasureTheory.ProbabilityMeasure.toMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := ProbabilityMeasure Ω) toMeasure

Tactic:
Subtype.coe_injective

Premises used: MeasureTheory.ProbabilityMeasure, Subtype.coe_injective, MeasureTheory.ProbabilityMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h :
  Eq.{max (u_1 + 1) 1} (α := (a : Set Ω) → ℝ≥0)
    ((fun (μ : ProbabilityMeasure Ω) (s : Set Ω) ↦ ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)) μ)
    ((fun (μ : ProbabilityMeasure Ω) (s : Set Ω) ↦ ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)) ν)
s : Set Ω
h_1 : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa [ENNReal.toNNReal_eq_toNNReal_iff, measure_ne_top] using congr_fun h s

Premises used: ENNReal.toNNReal_eq_toNNReal_iff, MeasureTheory.measure_ne_top, congr_fun
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ Eq (α := (a : Set Ω) → ℝ≥0) (⇑μ : (a : Set Ω) → ℝ≥0) fun (s : Set Ω) ↦
    ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : Measure Ω
hμ : IsProbabilityMeasure μ
⊢ Eq (α := (a : Set Ω) → ℝ≥0)
    (⇑(Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) μ hμ) : (a : Set Ω) → ℝ≥0) fun (s : Set Ω) ↦
    ENNReal.toNNReal ((μ : (a : Set Ω) → ℝ≥0∞) s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : Measure Ω
hμ : IsProbabilityMeasure μ
s : Set Ω
⊢ (Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) μ hμ : (a : Set Ω) → ℝ≥0) s =
    ENNReal.toNNReal ((μ : (a : Set Ω) → ℝ≥0∞) s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
⊢ Eq (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) univ : ℝ≥0) (1 : ℝ≥0)

Tactic:
congr_arg ENNReal.toNNReal ν.prop.measure_univ

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, ENNReal.toNNReal, congr_arg, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
⊢ Eq (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) ∅ : ℝ≥0) (0 : ℝ≥0)

Tactic:
simp [coeFn_def]

Premises used: MeasureTheory.ProbabilityMeasure.coeFn_def
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
⊢ Ne (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) univ : ℝ≥0) (0 : ℝ≥0)

Tactic:
simp only [coeFn_univ, Ne, one_ne_zero, not_false_iff]

Premises used: Ne, MeasureTheory.ProbabilityMeasure.coeFn_univ, not_false_iff, one_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
⊢ (↑ν : Measure Ω).real s = (↑((ν : (a : Set Ω) → ℝ≥0) s) : ℝ)

Tactic:
simp [coeFn_def, Measure.real, ENNReal.toReal]

Premises used: MeasureTheory.Measure.real, MeasureTheory.ProbabilityMeasure.coeFn_def, ENNReal.toReal
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
⊢ ((↑ν : Measure Ω).real s).toNNReal = (ν : (a : Set Ω) → ℝ≥0) s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ Eq (α := (a : Set Ω) → ℝ≥0) (⇑μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) (⇑μ : (a : Set Ω) → ℝ≥0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
⊢ Eq (α := ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
⊢ (↑ν.toFiniteMeasure : Measure Ω) = (↑ν : Measure Ω)

Tactic:
rfl

Premises used: MeasureTheory.ProbabilityMeasure, MeasureTheory.ProbabilityMeasure.toMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
⊢ Eq (α := (a : Set Ω) → ℝ≥0) (⇑ν.toFiniteMeasure : (a : Set Ω) → ℝ≥0) (⇑ν : (a : Set Ω) → ℝ≥0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
⊢ Eq (α := ℝ≥0) ((ν.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) s : ℝ≥0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
rw : (↑((ν.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = ((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
rw₁ :
  Eq (α := ℝ≥0∞) (((↑ν.toFiniteMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (↑((ν : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = ((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s

Tactic:
rw [← coeFn_comp_toFiniteMeasure_eq_coeFn, FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure,
    toMeasure_comp_toFiniteMeasure_eq_toMeasure]

Premises used: MeasureTheory.ProbabilityMeasure.toMeasure_comp_toFiniteMeasure_eq_toMeasure, MeasureTheory.ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn, MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
h : Eq (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) s : ℝ≥0) (0 : ℝ≥0)
rw : (↑((ν : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = 0
rw₁ : (↑0 : ℝ≥0∞) = 0
rw₂ rw₃ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero]

Premises used: MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.coe_zero
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
rw :
  LE.le (α := ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
⊢ LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)

Tactic:
rw [← coeFn_comp_toFiniteMeasure_eq_coeFn]

Premises used: MeasureTheory.ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ LE.le (α := ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)

Tactic:
FiniteMeasure.apply_mono _ h

Premises used: MeasureTheory.FiniteMeasure.apply_mono
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ LE.le (α := ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)

Tactic:
exact FiniteMeasure.apply_mono _ h

Premises used: MeasureTheory.FiniteMeasure.apply_mono
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
rw :
  (μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0)
      ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
⊢ (μ : (a : Set Ω) → ℝ≥0) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)

Tactic:
rw [← coeFn_comp_toFiniteMeasure_eq_coeFn]

Premises used: MeasureTheory.ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
⊢ (μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0)
      ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)

Tactic:
FiniteMeasure.apply_union_le _

Premises used: MeasureTheory.FiniteMeasure.apply_union_le
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
⊢ (μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0)
      ((μ.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)

Tactic:
exact FiniteMeasure.apply_union_le _

Premises used: MeasureTheory.FiniteMeasure.apply_union_le
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
inst_1 : Preorder ι
inst_2 : IsCountablyGenerated.{u_2} (α := ι) atTop
μ : ProbabilityMeasure Ω
f : ι → Set Ω
⊢ Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0) (⋃ (i : ι), f i)) : Filter ℝ≥0)

Tactic:
simpa [← ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.tendsto_coe]
    using tendsto_measure_iUnion_accumulate (μ := μ.toMeasure)

Premises used: MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.tendsto_coe, MeasureTheory.tendsto_measure_iUnion_accumulate
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
⊢ LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) (1 : ℝ≥0)

Tactic:
simpa using apply_mono μ (subset_univ s)

Premises used: Set.subset_univ, MeasureTheory.ProbabilityMeasure.apply_mono
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ Nonempty Ω

Tactic:
nonempty_of_isProbabilityMeasure μ

Premises used: MeasureTheory.nonempty_of_isProbabilityMeasure, MeasureTheory.ProbabilityMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h :
  ∀ (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
a : (↑μ : Measure Ω) = (↑ν : Measure Ω)
⊢ μ = ν

Tactic:
apply toMeasure_injective

Premises used: MeasureTheory.ProbabilityMeasure.toMeasure_injective
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h a :
  ∀ (s : Set Ω) (s_mble : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (↑μ : Measure Ω) = (↑ν : Measure Ω)

Tactic:
ext1 s s_mble
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h :
  ∀ (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
s : Set Ω
s_mble : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
h s s_mble
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h :
  ∀ (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
s : Set Ω
s_mble : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact h s s_mble
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
h₁ :
  ∀ (s : Set Ω) (s_mble : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν

Tactic:
ext1 s s_mble
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
s : Set Ω
s_mble : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa [ennreal_coeFn_eq_coeFn_toMeasure] using congr_arg ((↑) : ℝ≥0 → ℝ≥0∞) (h s s_mble)

Premises used: ENNReal.ofNNReal, MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, congr_arg
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ μ.toFiniteMeasure.mass = 1

Tactic:
μ.coeFn_univ

Premises used: MeasureTheory.FiniteMeasure.mass, MeasureTheory.ProbabilityMeasure.coeFn_univ