awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∃ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  ∀ (i : ι) (hi : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)

Tactic:
rcases htop with ⟨i, hi⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
hi ▸ h_le i

Premises used: Eq.rec
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)

Tactic:
measure_mono <| subset_iUnion _ _

Premises used: Set.subset_iUnion, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)

Tactic:
calc
      μ (⋃ i, t i) ≤ ∞ := le_top
      _ ≤ μ (s i) := hi ▸ h_le i
      _ ≤ μ (⋃ i, s i) := measure_mono <| subset_iUnion _ _

Premises used: Set.subset_iUnion, le_top, MeasureTheory.measure_mono, DFunLike.coe, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
⊢ ∀ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b) =ᶠ[ae μ] M (t b)

Tactic:
fun b => ae_eq_of_subset_of_measure_ge inter_subset_left ?_ ?_ ?_

Premises used: Set.inter_subset_left, MeasureTheory.ae_eq_of_subset_of_measure_ge
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
refine_1 :
  ∀ (b : ι),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (M (t b)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (M (t b) ∩ M (⋃ (b : ι), s b)) : ℝ≥0∞)
refine_2 : ∀ (b : ι), NullMeasurableSet (M (t b) ∩ M (⋃ (b : ι), s b)) μ
refine_3 : ∀ (b : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (M (t b)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b) =ᶠ[ae μ] M (t b)

Tactic:
refine fun b => ae_eq_of_subset_of_measure_ge inter_subset_left ?_ ?_ ?_

Premises used: Set.inter_subset_left, MeasureTheory.ae_eq_of_subset_of_measure_ge
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
b : ι
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (M (t b)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞)

Tactic:
measure_toMeasurable _

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
b : ι
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s b) : ℝ≥0∞)

Tactic:
h_le b
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
b : ι
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s b) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (M (t b) ∩ M (⋃ (b : ι), s b)) : ℝ≥0∞)

Tactic:
measure_mono <|
            subset_inter ((hsub b).trans <| subset_toMeasurable _ _)
              ((subset_iUnion _ _).trans <| subset_toMeasurable _ _)

Premises used: HasSubset.Subset.trans, MeasureTheory.subset_toMeasurable, Set.subset_iUnion, Set.subset_inter, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
b : ι
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (M (t b)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (M (t b) ∩ M (⋃ (b : ι), s b)) : ℝ≥0∞)

Tactic:
calc
        μ (M (t b)) = μ (t b) := measure_toMeasurable _
        _ ≤ μ (s b) := h_le b
        _ ≤ μ (M (t b) ∩ M (⋃ b, s b)) :=
          measure_mono <|
            subset_inter ((hsub b).trans <| subset_toMeasurable _ _)
              ((subset_iUnion _ _).trans <| subset_toMeasurable _ _)

Premises used: HasSubset.Subset.trans, MeasureTheory.subset_toMeasurable, Inter.inter, Set.subset_iUnion, MeasureTheory.measure_toMeasurable, Set.subset_inter, MeasureTheory.measure_mono, DFunLike.coe, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
b : ι
⊢ NullMeasurableSet (M (t b) ∩ M (⋃ (b : ι), s b)) μ

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
b : ι
refine_3 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (M (t b)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
b : ι
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
htop b
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
b : ι
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact htop b
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
⊢ ∀ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b) =ᶠ[ae μ] M (t b)

Tactic:
have H : ∀ b, (M (t b) ∩ M (⋃ b, s b) : Set α) =ᵐ[μ] M (t b) := by
    refine fun b => ae_eq_of_subset_of_measure_ge inter_subset_left ?_ ?_ ?_
    · calc
        μ (M (t b)) = μ (t b) := measure_toMeasurable _
        _ ≤ μ (s b) := h_le b
        _ ≤ μ (M (t b) ∩ M (⋃ b, s b)) :=
          measure_mono <|
            subset_inter ((hsub b).trans <| subset_toMeasurable _ _)
              ((subset_iUnion _ _).trans <| subset_toMeasurable _ _)
    · measurability
    · rw [measure_toMeasurable]
      exact htop b
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
H : ∀ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b) =ᶠ[ae μ] M (t b)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : ι), t b) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : ι), M (t b)) : ℝ≥0∞)

Tactic:
measure_mono (iUnion_mono fun b => subset_toMeasurable _ _)

Premises used: MeasureTheory.subset_toMeasurable, MeasureTheory.measure_mono, Set.iUnion_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
H : ∀ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b) =ᶠ[ae μ] M (t b)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : ι), M (t b)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b)) : ℝ≥0∞)

Tactic:
measure_congr (Filter.EventuallyEq.countable_iUnion H).symm

Premises used: MeasureTheory.measure_congr, Filter.EventuallyEq.countable_iUnion, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
H : ∀ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b) =ᶠ[ae μ] M (t b)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (M (⋃ (b : ι), s b)) : ℝ≥0∞)

Tactic:
measure_mono (iUnion_subset fun b => inter_subset_right)

Premises used: Set.iUnion_subset, MeasureTheory.measure_mono, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
H : ∀ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b) =ᶠ[ae μ] M (t b)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (M (⋃ (b : ι), s b)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : ι), s b) : ℝ≥0∞)

Tactic:
measure_toMeasurable _

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
H : ∀ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b) =ᶠ[ae μ] M (t b)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)

Tactic:
calc
    μ (⋃ b, t b) ≤ μ (⋃ b, M (t b)) := measure_mono (iUnion_mono fun b => subset_toMeasurable _ _)
    _ = μ (⋃ b, M (t b) ∩ M (⋃ b, s b)) :=
      measure_congr (Filter.EventuallyEq.countable_iUnion H).symm
    _ ≤ μ (M (⋃ b, s b)) := measure_mono (iUnion_subset fun b => inter_subset_right)
    _ = μ (⋃ b, s b) := measure_toMeasurable _

Premises used: MeasureTheory.measure_congr, Set.iUnion_subset, MeasureTheory.subset_toMeasurable, Filter.EventuallyEq.countable_iUnion, Inter.inter, MeasureTheory.measure_toMeasurable, MeasureTheory.measure_mono, Set.iUnion_mono, DFunLike.coe, Set.iUnion, Filter.EventuallyEq.symm, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞)
ht : t₁ ⊆ t₂
htμ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₁ : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : Bool), bif b then s₁ else t₁) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : Bool), bif b then s₂ else t₂) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ t₁) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₂ ∪ t₂) : ℝ≥0∞)

Tactic:
rw [union_eq_iUnion, union_eq_iUnion]

Premises used: Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞)
ht : t₁ ⊆ t₂
htμ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₁ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : Bool), bif b then s₁ else t₁) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : Bool), bif b then s₂ else t₂) : ℝ≥0∞)

Tactic:
measure_iUnion_congr_of_subset (Bool.forall_bool.2 ⟨ht, hs⟩) (Bool.forall_bool.2 ⟨htμ, hsμ⟩)

Premises used: Iff.mpr, Bool.forall_bool, And.intro, MeasureTheory.measure_iUnion_congr_of_subset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞)
ht : t₁ ⊆ t₂
htμ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₁ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : Bool), bif b then s₁ else t₁) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : Bool), bif b then s₂ else t₂) : ℝ≥0∞)

Tactic:
exact measure_iUnion_congr_of_subset (Bool.forall_bool.2 ⟨ht, hs⟩) (Bool.forall_bool.2 ⟨htμ, hsμ⟩)

Premises used: Iff.mpr, Bool.forall_bool, And.intro, MeasureTheory.measure_iUnion_congr_of_subset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s : ι → Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), toMeasurable μ (s i)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)

Tactic:
Eq.symm <| measure_iUnion_congr_of_subset (fun _i => subset_toMeasurable _ _) fun _i ↦
    (measure_toMeasurable _).le

Premises used: Eq.le, MeasureTheory.subset_toMeasurable, MeasureTheory.measure_toMeasurable, Eq.symm, MeasureTheory.measure_iUnion_congr_of_subset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
I : Set β
hc : I.Countable
s : β → Set α
haveI :
  ∀ (this : Encodable (↑I : Type u_2)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ I, toMeasurable μ (s b)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ I, s b) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ I, toMeasurable μ (s b)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ I, s b) : ℝ≥0∞)

Tactic:
haveI := hc.toEncodable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
I : Set β
hc : I.Countable
s : β → Set α
this : Encodable (↑I : Type u_2)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ I, toMeasurable μ (s b)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ I, s b) : ℝ≥0∞)

Tactic:
simp only [biUnion_eq_iUnion, measure_iUnion_toMeasurable]

Premises used: Set.biUnion_eq_iUnion, MeasureTheory.measure_iUnion_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)

Tactic:
Eq.symm <|
    measure_union_congr_of_subset (subset_toMeasurable _ _) (measure_toMeasurable _).le Subset.rfl
      le_rfl

Premises used: le_rfl, Eq.le, MeasureTheory.subset_toMeasurable, MeasureTheory.measure_toMeasurable, Set.Subset.rfl, MeasureTheory.measure_union_congr_of_subset, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ toMeasurable μ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)

Tactic:
Eq.symm <|
    measure_union_congr_of_subset Subset.rfl le_rfl (subset_toMeasurable _ _)
      (measure_toMeasurable _).le

Premises used: le_rfl, Eq.le, MeasureTheory.subset_toMeasurable, MeasureTheory.measure_toMeasurable, Set.Subset.rfl, MeasureTheory.measure_union_congr_of_subset, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : (↑s : Set ι).Pairwise (AEDisjoint μ on t)
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, t b) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [← measure_biUnion_finset₀ H h]

Premises used: MeasureTheory.measure_biUnion_finset₀
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : (↑s : Set ι).Pairwise (AEDisjoint μ on t)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, t b) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
measure_mono (subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : (↑s : Set ι).Pairwise (AEDisjoint μ on t)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, t b) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
exact measure_mono (subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : Pairwise (AEDisjoint μ on s)
rw :
  LE.le (α := ℝ≥0∞) (⨆ (s_1 : Finset ι), ∑ a ∈ s_1, (μ : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [ENNReal.tsum_eq_iSup_sum]

Premises used: ENNReal.tsum_eq_iSup_sum
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : Pairwise (AEDisjoint μ on s)
⊢ LE.le (α := ℝ≥0∞) (⨆ (s_1 : Finset ι), ∑ a ∈ s_1, (μ : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
iSup_le fun s =>
    sum_measure_le_measure_univ (fun i _hi => hs i) fun i _hi j _hj hij => H hij

Premises used: MeasureTheory.sum_measure_le_measure_univ, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : Pairwise (AEDisjoint μ on s)
⊢ LE.le (α := ℝ≥0∞) (⨆ (s_1 : Finset ι), ∑ a ∈ s_1, (μ : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
exact iSup_le fun s =>
    sum_measure_le_measure_univ (fun i _hi => hs i) fun i _hi j _hj hij => H hij

Premises used: MeasureTheory.sum_measure_le_measure_univ, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
contrapose! :
  ∀ (H : ∀ (i j : ι) (_ : i ≠ j), s i ∩ s j = ∅),
    LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∃ (i : ι) (j : ι), i ≠ j ∧ (s i ∩ s j).Nonempty

Tactic:
contrapose! H
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : ∀ (i j : ι) (_ : i ≠ j), s i ∩ s j = ∅
apply : Pairwise (AEDisjoint μ on s)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
apply tsum_measure_le_measure_univ hs

Premises used: MeasureTheory.tsum_measure_le_measure_univ