awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Countable ι
f : ι → Measure α
s t : Set α
hst : s ⊆ t
htm : MeasurableSet t
ht : ∀ (i : ι), Eq (α := ℝ≥0∞) ((f i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) t) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s)

Tactic:
simp [ht]
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Countable ι
f : ι → Measure α
s t : Set α
hst : s ⊆ t
htm : MeasurableSet t
ht : ∀ (i : ι), Eq (α := ℝ≥0∞) ((f i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
sum : Eq (α := ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) t) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s)
⊢ LE.le (α := ℝ≥0∞) ((Measure.sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
  sum f s ≤ sum f t := measure_mono hst
  _ = ∑' i, f i t := sum_apply _ htm
  _ = ∑' i, f i s := by simp [ht]

Premises used: MeasureTheory.Measure.sum_apply, MeasureTheory.measure_mono, MeasureTheory.Measure.sum, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
μ : ι → Measure α
i : ι
s : Set α
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa only [sum_apply μ hs] using ENNReal.le_tsum i

Premises used: MeasureTheory.Measure.sum_apply, ENNReal.le_tsum
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Countable ι
μ : ι → Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [sum_apply_of_countable]

Premises used: MeasureTheory.Measure.sum_apply_of_countable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
μ : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
⊢ sum f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
simp +contextual [Measure.ext_iff, forall_comm (α := ι)]

Premises used: MeasureTheory.Measure.ext_iff, forall_comm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((sum fun (x : ι) ↦ 0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Measure α) (sum fun (x : ι) ↦ 0) 0

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((sum fun (x : ι) ↦ 0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [Measure.sum_apply _ hs]

Premises used: MeasureTheory.Measure.sum_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((sum fun (n : ι) ↦ sum (μ n) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((sum fun (p : ι × ι') ↦ μ p.1 p.2 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Measure α) (sum fun (n : ι) ↦ sum (μ n)) (sum fun (p : ι × ι') ↦ μ p.1 p.2)

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((sum fun (n : ι) ↦ sum (μ n) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (p : ι × ι') ↦ μ p.1 p.2 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [sum_apply _ hs, ENNReal.tsum_prod']

Premises used: MeasureTheory.Measure.sum_apply, ENNReal.tsum_prod'
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((sum fun (n : ι) ↦ sum (μ n) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((sum fun (m : ι') ↦ sum fun (n : ι) ↦ μ n m : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Measure α) (sum fun (n : ι) ↦ sum (μ n)) (sum fun (m : ι') ↦ sum fun (n : ι) ↦ μ n m)

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (∑' (i : ι) (i_1 : ι'), (μ i i_1 : (a : Set α) → ℝ≥0∞) s)
    (∑' (i : ι') (i_1 : ι), (μ i_1 i : (a : Set α) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞) (((sum fun (n : ι) ↦ sum (μ n) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (m : ι') ↦ sum fun (n : ι) ↦ μ n m : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [sum_apply _ hs]

Premises used: MeasureTheory.Measure.sum_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
h h₁ :
  Eq (α := ℝ≥0∞) (∑' (b : ι') (a : ι), (μ a b : (a : Set α) → ℝ≥0∞) s)
    (∑' (i : ι') (i_1 : ι), (μ i_1 i : (a : Set α) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι) (i_1 : ι'), (μ i i_1 : (a : Set α) → ℝ≥0∞) s)
    (∑' (i : ι') (i_1 : ι), (μ i_1 i : (a : Set α) → ℝ≥0∞) s)

Tactic:
rw [ENNReal.tsum_comm]

Premises used: ENNReal.tsum_comm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Countable ι
μ : ι → Measure α
p : α → Prop
⊢ (∀ᵐ (x : α) ∂sum μ, p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, p x

Tactic:
sum_apply_eq_zero

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.Measure.sum_apply_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
μ : ι → Measure α
p : α → Prop
h : MeasurableSet.{u_1} (α := α) {x : α | p x}
⊢ (∀ᵐ (x : α) ∂sum μ, p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, p x

Tactic:
sum_apply_eq_zero' h.compl

Premises used: MeasureTheory.Measure.sum_apply_eq_zero', Set.Mem, Filter.Eventually, setOf, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Fintype ι
μ : ι → Measure α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((∑ i : ι, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ sum μ = ∑ i : ι, μ i

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Fintype ι
μ : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((∑ i : ι, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [sum_apply, finsetSum_apply, hs, tsum_fintype]

Premises used: MeasureTheory.Measure.sum_apply, tsum_fintype, MeasureTheory.Measure.finsetSum_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Finset ι
μ : ι → Measure α
rw : Eq.{u_1 + 1} (α := Measure α) (∑ i : ↥s, μ (↑i : ι)) (∑ i ∈ s, μ i)
rw₁ rw₂ : Eq.{u_1 + 1} (α := Measure α) (∑ i ∈ s, μ i) (∑ i ∈ s, μ i)
⊢ Eq.{u_1 + 1} (α := Measure α) (sum fun (i : ↥s) ↦ μ (↑i : ι)) (∑ i ∈ s, μ i)

Tactic:
rw [sum_fintype, Finset.sum_coe_sort s μ]

Premises used: MeasureTheory.Measure.sum_fintype, Finset.sum_coe_sort
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Countable ι
μ : ι → Measure α
⊢ ae (sum μ) = ⨆ (i : ι), ae (μ i)

Tactic:
Filter.ext fun _ => ae_sum_iff.trans mem_iSup.symm

Premises used: MeasureTheory.Measure.ae_sum_iff, Filter.mem_iSup, Filter.ext, Iff.trans, Iff.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : Bool → Measure α
rw : ∑ i : Bool, f i = f true + f false
rw₁ rw₂ : f true + f false = f true + f false
⊢ sum f = f true + f false

Tactic:
rw [sum_fintype, Fintype.sum_bool]

Premises used: MeasureTheory.Measure.sum_fintype, Fintype.sum_bool
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ (sum fun (b : Bool) ↦ bif b then μ else ν) = μ + ν

Tactic:
sum_bool _

Premises used: MeasureTheory.Measure.sum_bool
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : IsEmpty ι
μ : ι → Measure α
rw : Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) (∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) univ) 0
rw₂ rw₃ : Eq (α := ℝ≥0∞) 0 0
⊢ sum μ = 0

Tactic:
rw [← measure_univ_eq_zero, sum_apply _ MeasurableSet.univ, tsum_empty]

Premises used: MeasureTheory.Measure.sum_apply, tsum_empty, MeasureTheory.Measure.measure_univ_eq_zero, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
h :
  ∀ (t : Set α) (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞)
      ((HAdd.hAdd (α := Measure α) (sum fun (i : (↑s : Type u_5)) ↦ μ (↑i : ι))
              (sum fun (i : (↑sᶜ : Type u_5)) ↦ μ (↑i : ι)) :
            (a : Set α) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      ((sum μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HAdd.hAdd (α := Measure α) (sum fun (i : (↑s : Type u_5)) ↦ μ (↑i : ι))
      (sum fun (i : (↑sᶜ : Type u_5)) ↦ μ (↑i : ι)) =
    sum μ

Tactic:
ext1 t ht
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
h :
  HAdd.hAdd (α := ℝ≥0∞) (∑' (i : (↑s : Type u_5)), (μ (↑i : ι) : (a : Set α) → ℝ≥0∞) t)
      (∑' (i : (↑sᶜ : Type u_5)), (μ (↑i : ι) : (a : Set α) → ℝ≥0∞) t) =
    ∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) t
⊢ Eq (α := ℝ≥0∞)
    ((HAdd.hAdd (α := Measure α) (sum fun (i : (↑s : Type u_5)) ↦ μ (↑i : ι))
            (sum fun (i : (↑sᶜ : Type u_5)) ↦ μ (↑i : ι)) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((sum μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [add_apply, sum_apply _ ht]

Premises used: MeasureTheory.Measure.sum_apply, MeasureTheory.Measure.add_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (i : (↑s : Type u_5)), (μ (↑i : ι) : (a : Set α) → ℝ≥0∞) t)
      (∑' (i : (↑sᶜ : Type u_5)), (μ (↑i : ι) : (a : Set α) → ℝ≥0∞) t) =
    ∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) t

Tactic:
ENNReal.summable.tsum_add_tsum_compl (f := fun i => μ i t) ENNReal.summable

Premises used: Summable.tsum_add_tsum_compl, ENNReal.summable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (i : (↑s : Type u_5)), (μ (↑i : ι) : (a : Set α) → ℝ≥0∞) t)
      (∑' (i : (↑sᶜ : Type u_5)), (μ (↑i : ι) : (a : Set α) → ℝ≥0∞) t) =
    ∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) t

Tactic:
exact ENNReal.summable.tsum_add_tsum_compl (f := fun i => μ i t) ENNReal.summable

Premises used: Summable.tsum_add_tsum_compl, ENNReal.summable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : ℕ → Measure α
h : ∀ (n : ℕ), μ n = ν n
⊢ sum μ = sum ν

Tactic:
congr_arg sum (funext h)

Premises used: congr_arg, funext, MeasureTheory.Measure.sum
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
μ ν : ι → Measure α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((sum μ + sum ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((sum fun (n : ι) ↦ μ n + ν n : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ sum μ + sum ν = sum fun (n : ι) ↦ μ n + ν n

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
μ ν : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((sum μ + sum ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (n : ι) ↦ μ n + ν n : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [add_apply, sum_apply _ hs,
    ENNReal.summable.tsum_add ENNReal.summable]

Premises used: MeasureTheory.Measure.sum_apply, ENNReal.summable, MeasureTheory.Measure.add_apply, Summable.tsum_add
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
e : ι' ≃ ι
m : ι → Measure α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((sum.{u_1, u_9} (ι := ι') (m ∘ (⇑e : (a : ι') → ι)) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((sum m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ sum.{u_1, u_9} (ι := ι') (m ∘ (⇑e : (a : ι') → ι)) = sum m

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
e : ι' ≃ ι
m : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((sum.{u_1, u_9} (ι := ι') (m ∘ (⇑e : (a : ι') → ι)) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((sum m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa [hs, sum_apply] using e.tsum_eq (fun n ↦ m n s)

Premises used: Equiv.tsum_eq, MeasureTheory.Measure.sum_apply, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
f : ι → ι'
hf : Injective f
m : ι → Measure α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((sum (Function.extend f m 0) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sum m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ sum (Function.extend f m 0) = sum m

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
f : ι → ι'
hf : Injective f
m : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((sum (Function.extend f m 0) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sum m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [*, Function.apply_extend (fun μ : Measure α ↦ μ s)]

Premises used: Function.apply_extend, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0_1 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
μ : Measure α
⊢ (fun (x : Set α) ↦ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)) ∅

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ s ∈ μ.cofinite ↔ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
rw :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜᶜ : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw₁ rw₂ :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ sᶜ ∈ μ.cofinite ↔ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [mem_cofinite, compl_compl]

Premises used: compl_compl, MeasureTheory.Measure.mem_cofinite
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
⊢ (∀ᶠ (x : α) in μ.cofinite, p x) ↔ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t s : Set α
hs : s ∈ μ.cofinite
⊢ ∃ t ∈ μ.cofinite, MeasurableSet t ∧ t ⊆ s

Tactic:
⟨(toMeasurable μ sᶜ)ᶜ, ?_, (measurableSet_toMeasurable _ _).compl, ?_⟩

Premises used: Compl.compl, MeasurableSet.compl, MeasureTheory.measurableSet_toMeasurable, And.intro, Exists.intro, MeasureTheory.toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t s : Set α
hs : s ∈ μ.cofinite
refine_1 : (toMeasurable μ sᶜ)ᶜ ∈ μ.cofinite
refine_2 : (toMeasurable μ sᶜ)ᶜ ⊆ s
⊢ ∃ t ∈ μ.cofinite, MeasurableSet t ∧ t ⊆ s

Tactic:
refine ⟨(toMeasurable μ sᶜ)ᶜ, ?_, (measurableSet_toMeasurable _ _).compl, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t s : Set α
hs : s ∈ μ.cofinite
refine_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ sᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (toMeasurable μ sᶜ)ᶜ ∈ μ.cofinite

Tactic:
rwa [compl_mem_cofinite, measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable, MeasureTheory.Measure.compl_mem_cofinite
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t s : Set α
hs : s ∈ μ.cofinite
refine_2 : sᶜ ⊆ toMeasurable μ sᶜ
⊢ (toMeasurable μ sᶜ)ᶜ ⊆ s

Tactic:
rw [compl_subset_comm]

Premises used: Set.compl_subset_comm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t s : Set α
hs : s ∈ μ.cofinite
⊢ sᶜ ⊆ toMeasurable μ sᶜ

Tactic:
apply subset_toMeasurable

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : s ∈ ae μ
⊢ s ∈ μ.cofinite

Tactic:
simp_all [mem_cofinite, mem_ae_iff]

Premises used: MeasureTheory.Measure.mem_cofinite, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
h : AEMeasurable f μ
⊢ NullMeasurable f μ

Tactic:
let ⟨_g, hgm, hg⟩ := h; hgm.nullMeasurable.congr hg.symm

Premises used: MeasureTheory.NullMeasurable.congr, Measurable.nullMeasurable, _private.0.AEMeasurable.nullMeasurable.match_1, MeasureTheory.NullMeasurable, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
s : Set β
hf : AEMeasurable f μ
hs : MeasurableSet s
⊢ NullMeasurableSet (f ⁻¹' s) μ

Tactic:
hf.nullMeasurable hs

Premises used: AEMeasurable.nullMeasurable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
rw : ∅ ∈ ae μ ↔ μ = 0
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ μ = 0
rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ μ = 0
rw₃ rw₄ : μ = 0 ↔ μ = 0
⊢ ae μ = ⊥ ↔ μ = 0

Tactic:
rw [← empty_mem_iff_bot, mem_ae_iff, compl_empty, measure_univ_eq_zero]

Premises used: Filter.empty_mem_iff_bot, Set.compl_empty, MeasureTheory.mem_ae_iff, MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ (ae μ).NeBot ↔ μ ≠ 0

Tactic:
neBot_iff.trans (not_congr ae_eq_bot)

Premises used: Filter.neBot_iff, MeasureTheory.ae_eq_bot, Iff.trans, not_congr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst_1 : NeZero μ
⊢ (ae μ).NeBot

Tactic:
ae_neBot.2 <| NeZero.ne μ

Premises used: Iff.mpr, MeasureTheory.ae_neBot, NeZero.ne
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
_m0 : MeasurableSpace α
⊢ ae (F := Measure α) 0 = ⊥

Tactic:
ae_eq_bot.2 rfl

Premises used: Iff.mpr, MeasureTheory.ae_eq_bot, rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, Iic i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
rw₁ : DirectedOn ((fun (x1 x2 : Set α) ↦ x1 ⊆ x2) on Iic) s
⊢ Eq (α := ℝ≥0∞) (⨆ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) (Iic x) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [← measure_biUnion_eq_iSup hsc]

Premises used: MeasureTheory.measure_biUnion_eq_iSup
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iic i) univ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, Iic i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ ∀ (x : α), ∃ (x_1 : α) (_ : x_1 ∈ s), x ≤ x_1

Tactic:
simp only [← bex_def] at hst

Premises used: bex_def
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Preorder α
s : Set α
hsc : s.Countable
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hst : ∀ (x : α), ∃ (x_1 : α) (_ : x_1 ∈ s), x ≤ x_1
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iic i) univ

Tactic:
iUnion₂_eq_univ_iff.2 hst

Premises used: Iff.mpr, Set.iUnion₂_eq_univ_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Preorder α
s : Set α
hsc : s.Countable
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hst : ∀ (x : α), ∃ (x_1 : α) (_ : x_1 ∈ s), x ≤ x_1
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iic i) univ

Tactic:
exact iUnion₂_eq_univ_iff.2 hst

Premises used: Iff.mpr, Set.iUnion₂_eq_univ_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ DirectedOn ((fun (x1 x2 : Set α) ↦ x1 ⊆ x2) on Iic) s

Tactic:
directedOn_iff_directed.2 (hdir.directed_val.mono_comp _ fun x y => Iic_subset_Iic.2)

Premises used: Iff.mpr, Set.Iic_subset_Iic, Directed.mono_comp, DirectedOn.directed_val, directedOn_iff_directed
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ DirectedOn ((fun (x1 x2 : Set α) ↦ x1 ⊆ x2) on Iic) s

Tactic:
exact directedOn_iff_directed.2 (hdir.directed_val.mono_comp _ fun x y => Iic_subset_Iic.2)

Premises used: Iff.mpr, Directed.mono_comp, directedOn_iff_directed