awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ 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.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : Measure Ω
hμ : IsFiniteMeasure μ
⊢ Eq (α := (a : Set Ω) → ℝ≥0) (⇑(Subtype.mk (p := fun (μ : Measure Ω) ↦ IsFiniteMeasure μ) μ hμ) : (a : Set Ω) → ℝ≥0)
    fun (s : Set Ω) ↦ ENNReal.toNNReal ((μ : (a : Set Ω) → ℝ≥0∞) s)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : Measure Ω
h : IsFiniteMeasure μ
⊢ (↑(Subtype.mk (p := fun (μ : Measure Ω) ↦ IsFiniteMeasure μ) μ h) : Measure Ω) = μ

Tactic:
rfl

Premises used: MeasureTheory.FiniteMeasure.toMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
⊢ (↑μ : Measure Ω).real s = (↑((μ : (a : Set Ω) → ℝ≥0) s) : ℝ)

Tactic:
rfl

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

Tactic:
ENNReal.coe_toNNReal (measure_lt_top (↑ν) s).ne

Premises used: ENNReal.coe_toNNReal
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : FiniteMeasure Ω
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.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.coe_zero
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)

Tactic:
ENNReal.toNNReal_mono (measure_ne_top _ s₂) ((μ : Measure Ω).mono h)

Premises used: MeasureTheory.OuterMeasure.mono, MeasureTheory.measure_ne_top, ENNReal.toNNReal_mono, MeasureTheory.Measure.toOuterMeasure, MeasureTheory.FiniteMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
⊢ ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)

Tactic:
have := measure_union_le (μ := (μ : Measure Ω)) s₁ s₂
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
this :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞) ≠
    ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
this :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)
apply :
  (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
        (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)).toNNReal =
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (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:
apply (ENNReal.toNNReal_mono (by finiteness) this).trans_eq

Premises used: LE.le.trans_eq, ENNReal.toNNReal_mono
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
this :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
this :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
this :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)
rw :
  ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁) +
      ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂) =
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
rw₁ rw₂ :
  ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁) +
      ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂) =
    HAdd.hAdd (α := ℝ≥0) ((fun (s : Set Ω) ↦ ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)) s₁)
      ((fun (s : Set Ω) ↦ ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)) s₂)
⊢ (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
        (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)).toNNReal =
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)

Tactic:
rw [ENNReal.toNNReal_add (by finiteness) (by finiteness), coeFn_def]

Premises used: ENNReal.toNNReal_add, MeasureTheory.FiniteMeasure.coeFn_def
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s t : Set Ω
μ : FiniteMeasure Ω
h : s ⊆ t
ht : Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) t : ℝ≥0) (0 : ℝ≥0)
⊢ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) (0 : ℝ≥0)

Tactic:
eq_bot_mono (apply_mono μ h) ht

Premises used: MeasureTheory.FiniteMeasure.apply_mono, eq_bot_mono
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s t : Set Ω
μ : FiniteMeasure Ω
h : s ⊆ t
hs : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) t : ℝ≥0)

Tactic:
hs.trans_le <| μ.apply_mono h

Premises used: MeasureTheory.FiniteMeasure.apply_mono, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
inst_1 : Preorder ι
inst_2 : IsCountablyGenerated.{u_2} (α := ι) atTop
μ : FiniteMeasure Ω
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]
    using tendsto_measure_iUnion_accumulate (μ := μ.toMeasure) (ι := ι)

Premises used: MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure, MeasureTheory.tendsto_measure_iUnion_accumulate
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
⊢ (μ : (a : Set Ω) → ℝ≥0) s ≤ μ.mass

Tactic:
simpa using apply_mono μ (subset_univ s)

Premises used: Set.subset_univ, MeasureTheory.FiniteMeasure.apply_mono
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ (↑μ.mass : ℝ≥0∞) = ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ

Tactic:
ennreal_coeFn_eq_coeFn_toMeasure μ Set.univ

Premises used: MeasureTheory.FiniteMeasure.mass, Set.univ, MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
⊢ Eq.{u_1 + 1} (α := (a : Set Ω) → ℝ≥0) (⇑0 : (a : Set Ω) → ℝ≥0) 0

Tactic:
rfl

Premises used: ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
⊢ mass.{u_1} (Ω := Ω) 0 = 0

Tactic:
rfl

Premises used: MeasureTheory.FiniteMeasure.mass, ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
hμ : μ = 0
⊢ μ.mass = 0

Tactic:
simp only [hμ, zero_mass]

Premises used: MeasureTheory.FiniteMeasure.zero_mass
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
refine : ∀ (μ_mass : μ.mass = 0), μ = 0
⊢ μ.mass = 0 ↔ μ = 0

Tactic:
refine ⟨fun μ_mass => ?_, fun hμ => by simp only [hμ, zero_mass]⟩
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
a : (↑μ : Measure Ω) = (↑0 : Measure Ω)
⊢ μ = 0

Tactic:
apply toMeasure_injective

Premises used: MeasureTheory.FiniteMeasure.toMeasure_injective
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
a : Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (↑μ : Measure Ω) = (↑0 : Measure Ω)

Tactic:
apply Measure.measure_univ_eq_zero.mp

Premises used: Iff.mp, MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
a : (↑μ.mass : ℝ≥0∞) = 0
a₁ a₂ a₃ a₄ : μ.mass = 0
⊢ Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rwa [← ennreal_mass, ENNReal.coe_eq_zero]

Premises used: ENNReal.coe_eq_zero, MeasureTheory.FiniteMeasure.ennreal_mass
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ μ.mass ≠ 0 ↔ μ ≠ 0

Tactic:
not_iff_not.mpr <| FiniteMeasure.mass_zero_iff μ

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

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
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.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
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.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
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.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
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.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
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.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure, congr_arg
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
⊢ Eq.{u_1 + 1} (α := Measure Ω) (↑0 : Measure Ω) 0

Tactic:
rfl

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

Tactic:
rfl

Premises used: MeasureTheory.FiniteMeasure.toMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
R : Type u_2
inst_1 : SMul R ℝ≥0
inst_2 : SMul R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
inst_4 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
μ : FiniteMeasure Ω
⊢ (↑(c • μ) : Measure Ω) = c • (↑μ : Measure Ω)

Tactic:
rfl

Premises used: MeasureTheory.FiniteMeasure.toMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (x : Set Ω),
    (μ + ν : (a : Set Ω) → ℝ≥0) x =
      HAdd.hAdd (α := (a : Set Ω) → ℝ≥0) (β := (a : Set Ω) → ℝ≥0) (⇑μ : (a : Set Ω) → ℝ≥0) (⇑ν : (a : Set Ω) → ℝ≥0) x
⊢ (⇑(μ + ν) : (a : Set Ω) → ℝ≥0) = HAdd.hAdd (α := (a : Set Ω) → ℝ≥0) (⇑μ : (a : Set Ω) → ℝ≥0) (⇑ν : (a : Set Ω) → ℝ≥0)

Tactic:
funext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
x : Set Ω
h :
  ((↑(μ + ν) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) x =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) x : ℝ≥0∞)
      (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) x : ℝ≥0∞)
⊢ (μ + ν : (a : Set Ω) → ℝ≥0) x =
    HAdd.hAdd (α := (a : Set Ω) → ℝ≥0) (β := (a : Set Ω) → ℝ≥0) (⇑μ : (a : Set Ω) → ℝ≥0) (⇑ν : (a : Set Ω) → ℝ≥0) x

Tactic:
simp only [Pi.add_apply, ← ENNReal.coe_inj, ennreal_coeFn_eq_coeFn_toMeasure,
    ENNReal.coe_add]

Premises used: ENNReal.coe_inj, ENNReal.coe_add, MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure, Pi.add_apply
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
x : Set Ω
⊢ ((↑(μ + ν) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) x =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) x : ℝ≥0∞)
      (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
R : Type u_2
inst_1 : SMul R ℝ≥0
inst_2 : SMul R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
inst_4 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_5 : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
h : ∀ (x : Set Ω), (c • μ : (a : Set Ω) → ℝ≥0) x = HSMul.hSMul (β := (a : Set Ω) → ℝ≥0) c (⇑μ : (a : Set Ω) → ℝ≥0) x
⊢ (⇑(c • μ) : (a : Set Ω) → ℝ≥0) = HSMul.hSMul (β := (a : Set Ω) → ℝ≥0) c (⇑μ : (a : Set Ω) → ℝ≥0)

Tactic:
funext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
R : Type u_2
inst_1 : SMul R ℝ≥0
inst_2 : SMul R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
inst_4 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_5 : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
x : Set Ω
⊢ (c • μ : (a : Set Ω) → ℝ≥0) x = HSMul.hSMul (β := (a : Set Ω) → ℝ≥0) c (⇑μ : (a : Set Ω) → ℝ≥0) x

Tactic:
simp [← ENNReal.coe_inj, ENNReal.coe_smul]

Premises used: ENNReal.coe_inj, ENNReal.coe_smul
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
s : Finset ι
ν : ι → FiniteMeasure Ω
⊢ Eq.{u_1 + 1} (α := Measure Ω) (↑(∑ i ∈ s, ν i) : Measure Ω) (∑ i ∈ s, (↑(ν i) : Measure Ω))

Tactic:
map_sum toMeasureAddMonoidHom _ _

Premises used: map_sum, MeasureTheory.FiniteMeasure.toMeasure, MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
R : Type u_2
inst_1 : SMul R ℝ≥0
inst_2 : SMul R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
inst_4 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_5 : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
s : Set Ω
rw :
  HSMul.hSMul (β := (a : Set Ω) → ℝ≥0) c (⇑μ : (a : Set Ω) → ℝ≥0) s =
    HSMul.hSMul (β := ℝ≥0) c ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
rw₁ rw₂ :
  HSMul.hSMul (β := ℝ≥0) c ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) =
    HSMul.hSMul (β := ℝ≥0) c ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
⊢ (c • μ : (a : Set Ω) → ℝ≥0) s = HSMul.hSMul (β := ℝ≥0) c ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)

Tactic:
rw [coeFn_smul, Pi.smul_apply]

Premises used: MeasureTheory.FiniteMeasure.coeFn_smul, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
⊢ (↑(μ.restrict A) : Measure Ω) = (↑μ : Measure Ω).restrict A

Tactic:
rfl

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.FiniteMeasure.toMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
A s : Set Ω
s_mble : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((↑(μ.restrict A) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)

Tactic:
Measure.restrict_apply s_mble

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
A s : Set Ω
s_mble : MeasurableSet s
apply :
  Eq (α := ℝ≥0∞) (((↑(μ.restrict A) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0) ((μ.restrict A : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) (s ∩ A) : ℝ≥0)

Tactic:
apply congr_arg ENNReal.toNNReal

Premises used: ENNReal.toNNReal, congr_arg
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
A s : Set Ω
s_mble : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((↑(μ.restrict A) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)

Tactic:
exact Measure.restrict_apply s_mble

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
⊢ (μ.restrict A).mass = (μ : (a : Set Ω) → ℝ≥0) A

Tactic:
simp only [mass, restrict_apply μ A MeasurableSet.univ, univ_inter]

Premises used: MeasureTheory.FiniteMeasure.mass, Set.univ_inter, MeasureTheory.FiniteMeasure.restrict_apply, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
h :
  ∀ (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((↑(μ.restrict univ) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.restrict univ = μ

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((↑(μ.restrict univ) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s t : Set Ω
h : Disjoint s t
ht : MeasurableSet t
h₁ :
  ∀ (u : Set Ω) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞) (((↑(μ.restrict (s ∪ t)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) u : ℝ≥0∞)
      (((↑(μ.restrict s + μ.restrict t) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) u : ℝ≥0∞)
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

Tactic:
ext u hu
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s t : Set Ω
h : Disjoint s t
ht : MeasurableSet t
u : Set Ω
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) (((↑(μ.restrict (s ∪ t)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) u : ℝ≥0∞)
    (((↑(μ.restrict s + μ.restrict t) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
simp [Measure.restrict_union h ht]

Premises used: MeasureTheory.Measure.restrict_union
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
h :
  ∀ (t : Set Ω) (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞) (((↑(μ.restrict (⋃ i ∈ T, s i)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      ((((↑(∑ i ∈ T, μ.restrict (s i)) : Measure Ω) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ μ.restrict (⋃ i ∈ T, s i) = ∑ i ∈ T, μ.restrict (s i)

Tactic:
ext t ht
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) (((↑μ : Measure Ω).restrict (⋃ i ∈ T, s i) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
    (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((↑(μ.restrict (⋃ i ∈ T, s i)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
    ((((↑(∑ i ∈ T, μ.restrict (s i)) : Measure Ω) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [restrict_measure_eq, toMeasure_sum, Measure.coe_finsetSum, Finset.sum_apply]

Premises used: MeasureTheory.Measure.coe_finsetSum, Finset.sum_apply, MeasureTheory.FiniteMeasure.restrict_measure_eq, MeasureTheory.FiniteMeasure.toMeasure_sum
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞)
    (((Measure.sum fun (i : ↥T) ↦ (↑μ : Measure Ω).restrict (s (↑i : ι)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
    (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((↑μ : Measure Ω).restrict (⋃ i ∈ T, s i) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
    (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [Measure.restrict_biUnion_finset hd hm]

Premises used: MeasureTheory.Measure.restrict_biUnion_finset