awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Trim
Goal:
α : Type u_3
β : Type u_4
m m0 : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace β
inst_1 : MeasurableEq β
hm : m ≤ m0
f g : α → β
hf : Measurable f
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ MeasurableSet.{u_3} (α := α) {a : α | ¬f a = g a}

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ ¬IsFiniteMeasure μ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [isFiniteMeasure_iff]

Premises used: MeasureTheory.isFiniteMeasure_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ IsFiniteMeasure (μ.restrict s) ↔ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [isFiniteMeasure_iff, lt_top_iff_ne_top]

Premises used: MeasureTheory.isFiniteMeasure_iff, lt_top_iff_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
μ : Measure α
hs : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa using hs.elim

Premises used: Fact.elim
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Set α
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono (subset_univ s)).trans_lt IsFiniteMeasure.measure_univ_lt_top

Premises used: Set.subset_univ, MeasureTheory.measure_mono, LE.le.trans_lt, MeasureTheory.IsFiniteMeasure.measure_univ_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s_1 t : Set α
μ : Measure α
s : Set α
h : IsFiniteMeasure μ
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Set α
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ne_of_lt (measure_lt_top μ s)

Premises used: MeasureTheory.measure_lt_top, ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
rw :
  (μ : (a : Set α) → ℝ≥0∞) univ ≤
    HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε)
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) tᶜ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) ε

Tactic:
rw [measure_compl ht (by finiteness), measure_compl hs (by finiteness), tsub_le_iff_right]

Premises used: MeasureTheory.measure_compl, tsub_le_iff_right
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
⊢ (μ : (a : Set α) → ℝ≥0∞) univ =
    HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
(tsub_add_cancel_of_le <| measure_mono s.subset_univ).symm

Premises used: Set.subset_univ, tsub_add_cancel_of_le, MeasureTheory.measure_mono, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
⊢ HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε =
    HAdd.hAdd (β := ℝ≥0∞)
        (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
        ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) +
      ε
rw₁ rw₂ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε =
    HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε)
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [add_right_comm, add_assoc]

Premises used: add_assoc, add_right_comm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
μ₁ :
  HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
μ₂ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε =
    HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε)
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) univ ≤
    HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε)
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
calc
    μ univ = μ univ - μ s + μ s := (tsub_add_cancel_of_le <| measure_mono s.subset_univ).symm
    _ ≤ μ univ - μ s + (μ t + ε) := by gcongr
    _ = _ := by rw [add_right_comm, add_assoc]

Premises used: Set.subset_univ, Set.univ, tsub_add_cancel_of_le, HAdd.hAdd, MeasureTheory.measure_mono, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ε ↔
    (μ : (a : Set α) → ℝ≥0∞) t ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε

Tactic:
⟨fun h => compl_compl s ▸ compl_compl t ▸ measure_compl_le_add_of_le_add hs.compl ht.compl h,
    measure_compl_le_add_of_le_add ht hs⟩

Premises used: compl_compl, MeasureTheory.measure_compl_le_add_of_le_add, Eq.rec, MeasurableSet.compl, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ.cofinite = ⊥ ↔ IsFiniteMeasure μ

Tactic:
simp [← empty_mem_iff_bot, μ.mem_cofinite, isFiniteMeasure_iff]

Premises used: MeasureTheory.isFiniteMeasure_iff, MeasureTheory.Measure.mem_cofinite, Filter.empty_mem_iff_bot
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
⊢ μ.cofinite = ⊥

Tactic:
cofinite_eq_bot_iff.2 ‹_›

Premises used: Iff.mpr, MeasureTheory.cofinite_eq_bot_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
⊢ LT.lt (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst : IsEmpty α
rw : IsFiniteMeasure.{u_1} (α := α) (m0 := m0) 0
⊢ IsFiniteMeasure μ

Tactic:
rw [eq_zero_of_isEmpty μ]

Premises used: MeasureTheory.Measure.eq_zero_of_isEmpty
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst : IsEmpty α
⊢ IsFiniteMeasure.{u_1} (α := α) (m0 := m0) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
⊢ measureUnivNNReal.{u_1} (α := α) (m0 := m0) 0 = 0

Tactic:
rfl

Premises used: ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, MeasureTheory.measureUnivNNReal, rfl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
rw :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [Measure.coe_add, Pi.add_apply, ENNReal.add_lt_top]

Premises used: MeasureTheory.Measure.coe_add, Pi.add_apply, ENNReal.add_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨measure_lt_top _ _, measure_lt_top _ _⟩

Premises used: MeasureTheory.measure_lt_top, And.intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨measure_lt_top _ _, measure_lt_top _ _⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
rw : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞
⊢ LT.lt (α := ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [smul_apply, smul_eq_mul, ← ENNReal.div_eq_inv_mul]

Premises used: MeasureTheory.Measure.smul_apply, smul_eq_mul, ENNReal.div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞

Tactic:
ENNReal.div_self_le_one.trans_lt ENNReal.one_lt_top

Premises used: ENNReal.div_self_le_one, ENNReal.one_lt_top, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞

Tactic:
exact ENNReal.div_self_le_one.trans_lt ENNReal.one_lt_top

Premises used: ENNReal.div_self_le_one, ENNReal.one_lt_top, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
R : Type u_5
inst : SMul R ℝ≥0
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0 ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : IsFiniteMeasure μ
r : R
rw : IsFiniteMeasure (HSMul.hSMul (β := ℝ≥0) r 1 • μ)
⊢ IsFiniteMeasure (r • μ)

Tactic:
rw [← smul_one_smul ℝ≥0 r μ]

Premises used: NNReal, smul_one_smul
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
R : Type u_5
inst : SMul R ℝ≥0
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0 ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : IsFiniteMeasure μ
r : R
⊢ IsFiniteMeasure (HSMul.hSMul (β := ℝ≥0) r 1 • μ)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure μ
h : ν ≤ μ
⊢ IsFiniteMeasure ν

Tactic:
{ measure_univ_lt_top := (h Set.univ).trans_lt (measure_lt_top _ _) }

Premises used: MeasureTheory.measure_lt_top, Set.univ, MeasureTheory.IsFiniteMeasure.mk, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
pos : ∀ (hf : AEMeasurable f μ), IsFiniteMeasure (m0 := mβ) (map f μ)
neg : ∀ (hf : ¬AEMeasurable f μ), IsFiniteMeasure (m0 := mβ) (map f μ)
⊢ IsFiniteMeasure (m0 := mβ) (map f μ)

Tactic:
by_cases hf : AEMeasurable f μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
pos : LT.lt (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure (m0 := mβ) (map f μ)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
pos : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' univ) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [map_apply_of_aemeasurable hf MeasurableSet.univ]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' univ) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_lt_top μ _

Premises used: MeasureTheory.measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' univ) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_lt_top μ _

Premises used: MeasureTheory.measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f μ
neg : IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) 0
⊢ IsFiniteMeasure (m0 := mβ) (map f μ)

Tactic:
rw [map_of_not_aemeasurable hf]

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f μ
⊢ IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) 0

Tactic:
MeasureTheory.isFiniteMeasureZero

Premises used: MeasureTheory.isFiniteMeasureZero
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f μ
⊢ IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) 0

Tactic:
exact MeasureTheory.isFiniteMeasureZero

Premises used: MeasureTheory.isFiniteMeasureZero
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
inst : IsFiniteMeasure (m0 := mβ) (map f μ)
rw : LT.lt (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← Set.preimage_univ (f := f), ← map_apply_of_aemeasurable hf .univ]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable, Set.preimage_univ, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
inst : IsFiniteMeasure (m0 := mβ) (map f μ)
⊢ LT.lt (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
IsFiniteMeasure.measure_univ_lt_top

Premises used: MeasureTheory.IsFiniteMeasure.measure_univ_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
inst : IsFiniteMeasure (m0 := mβ) (map f μ)
⊢ LT.lt (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact IsFiniteMeasure.measure_univ_lt_top

Premises used: MeasureTheory.IsFiniteMeasure.measure_univ_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ IsFiniteMeasure (m0 := mβ) (map f μ) ↔ IsFiniteMeasure μ

Tactic:
⟨fun _ ↦ isFiniteMeasure_of_map hf, fun _ ↦ isFiniteMeasure_map μ f⟩

Premises used: MeasureTheory.Measure.isFiniteMeasure_of_map, MeasureTheory.Measure.isFiniteMeasure_map, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
rw : measureUnivNNReal μ = 0 ↔ (↑(measureUnivNNReal μ) : ℝ≥0∞) = 0
⊢ measureUnivNNReal μ = 0 ↔ μ = 0

Tactic:
rw [← MeasureTheory.Measure.measure_univ_eq_zero, ← coe_measureUnivNNReal]

Premises used: MeasureTheory.coe_measureUnivNNReal, MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : measureUnivNNReal μ = 0 ↔ measureUnivNNReal μ = 0
⊢ measureUnivNNReal μ = 0 ↔ (↑(measureUnivNNReal μ) : ℝ≥0∞) = 0

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
contrapose! : ∀ (hμ : measureUnivNNReal μ ≤ 0), μ = 0
⊢ 0 < measureUnivNNReal μ

Tactic:
contrapose! hμ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
hμ : measureUnivNNReal μ ≤ 0
⊢ μ = 0

Tactic:
simpa [measureUnivNNReal_eq_zero, Nat.le_zero] using hμ

Premises used: Nat.le_zero, MeasureTheory.measureUnivNNReal_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : IsFiniteMeasure μ
A2 : μ + ν₁ ≤ μ + ν₂
⊢ ν₁ ≤ ν₂

Tactic:
fun S => ENNReal.le_of_add_le_add_left (MeasureTheory.measure_ne_top μ S) (A2 S)

Premises used: ENNReal.le_of_add_le_add_left, MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ μ = ν

Tactic:
le_antisymm hμν (le_intro fun s hs _ ↦ ?_)

Premises used: le_antisymm, MeasureTheory.Measure.le_intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
refine :
  ∀ (s : Set α) (hs : MeasurableSet s),
    s.Nonempty → LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν

Tactic:
refine le_antisymm hμν (le_intro fun s hs _ ↦ ?_)

Premises used: le_antisymm, MeasureTheory.Measure.le_intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h : s.Nonempty
by_contra! : ∀ (h_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)), False
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
by_contra! h_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h : s.Nonempty
h_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Disjoint s sᶜ

Tactic:
have h_disj : Disjoint s sᶜ := disjoint_compl_right_iff_subset.mpr subset_rfl