awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
n : ℕ
hn_1 :
  Membership.mem (γ := Set ℕ)
    {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} n
hn : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' n) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (t'
          (↑(Subtype.mk (p := fun (a : ℕ) ↦
                Membership.mem (γ := Set ℕ)
                  {k : ℕ |
                    LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
                  a)
                n hn_1) :
            ℕ)) :
      ℝ≥0∞)
    (min
        ((μ : (a : Set α) → ℝ≥0∞)
          (t'
            (↑(Subtype.mk (p := fun (a : ℕ) ↦
                  Membership.mem (γ := Set ℕ)
                    {k : ℕ |
                      LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
                    a)
                  n hn_1) :
              ℕ)))
        ((ν : (a : Set α) → ℝ≥0∞)
          (t'
            (↑(Subtype.mk (p := fun (a : ℕ) ↦
                  Membership.mem (γ := Set ℕ)
                    {k : ℕ |
                      LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
                    a)
                  n hn_1) :
              ℕ))) :
      ℝ≥0∞)

Tactic:
simp [le_of_lt hn]

Premises used: le_of_lt
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
rw :
  Subset (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∩
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    ∅
⊢ Disjoint (α := Set ℕ)
    {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
    {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}

Tactic:
rw [Set.disjoint_iff]

Premises used: Set.disjoint_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
k : ℕ
hk₁ :
  Membership.mem (γ := Set ℕ)
    {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} k
hk₂ :
  Membership.mem (γ := Set ℕ)
    {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} k
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)

Tactic:
rw [mem_setOf_eq] at hk₁ hk₂

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
k : ℕ
hk₁ :
  Membership.mem (γ := Set ℕ)
    {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} k
hk₂ :
  Membership.mem (γ := Set ℕ)
    {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} k
hk₃ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)

Tactic:
rw [mem_setOf_eq] at hk₁ hk₂

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
k : ℕ
hk₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)
hk₂ : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)
⊢ Membership.mem (γ := Set ℕ) ∅ k

Tactic:
False.elim <| hk₂.not_ge hk₁

Premises used: False.elim, LT.lt.not_ge
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
k : ℕ
hk₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)
hk₂ : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)
⊢ Membership.mem (γ := Set ℕ) ∅ k

Tactic:
exact False.elim <| hk₂.not_ge hk₁

Premises used: False.elim, LT.lt.not_ge
-- 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 α
rw : m0 ≤ ⊤
⊢ m0 ≤ OuterMeasure.caratheodory ⊤

Tactic:
rw [OuterMeasure.top_caratheodory]

Premises used: MeasureTheory.OuterMeasure.top_caratheodory
-- 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 α
⊢ m0 ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- 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 α
⊢ m0 ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := Measure α) (OuterMeasure.toMeasure ⊤ ⋯) ⊤

Tactic:
toOuterMeasure_toMeasure (μ := ⊤)

Premises used: MeasureTheory.toOuterMeasure_toMeasure
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
x : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (toOuterMeasure ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ ⊤ + μ = ⊤

Tactic:
top_unique <| Measure.le_add_right le_rfl

Premises used: le_rfl, top_unique, MeasureTheory.Measure.le_add_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ + ⊤ = ⊤

Tactic:
top_unique <| Measure.le_add_left le_rfl

Premises used: le_rfl, top_unique, MeasureTheory.Measure.le_add_left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
_m0 : MeasurableSpace α
μ : Measure α
⊢ 0 ≤ μ

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ ≤ 0 ↔ μ = 0

Tactic:
μ.zero_le.ge_iff_eq'

Premises used: LE.le.ge_iff_eq', MeasureTheory.Measure.zero_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ μ = 0

Tactic:
⟨fun h => bot_unique fun s => (h ▸ measure_mono (subset_univ s) : μ s ≤ 0), fun h =>
    h.symm ▸ rfl⟩

Premises used: Set.subset_univ, Eq.rec, Iff.intro, MeasureTheory.measure_mono, bot_unique, Eq.symm, rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ μ ≠ 0

Tactic:
measure_univ_eq_zero.not

Premises used: Iff.not, MeasureTheory.Measure.measure_univ_eq_zero
-- 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 μ
⊢ NeZero (R := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
⟨measure_univ_ne_zero.2 <| NeZero.ne μ⟩

Premises used: Iff.mpr, NeZero.mk, MeasureTheory.Measure.measure_univ_ne_zero, NeZero.ne
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ↔ μ ≠ 0

Tactic:
pos_iff_ne_zero.trans measure_univ_ne_zero

Premises used: MeasureTheory.Measure.measure_univ_ne_zero, Iff.trans, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NeZero μ
h : IsEmpty α
⊢ False

Tactic:
simpa [eq_empty_of_isEmpty] using NeZero.ne (μ univ)

Premises used: Set.univ, Set.eq_empty_of_isEmpty, DFunLike.coe, NeZero.ne
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
E : Type u_8
inst : Zero E
μ : Measure α
f : α → E
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support f) : ℝ≥0∞) (0 : ℝ≥0∞) ↔ f =ᶠ[ae μ] 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
le_toMeasure_apply _ _ _

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

Tactic:
toMeasure_apply _ _ hs

Premises used: tsum, MeasureTheory.toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
apply : LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply le_antisymm ?_ (le_sum_apply _ _)

Premises used: MeasureTheory.Measure.le_sum_apply, le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
rcases :
  ∀ (t : Set α) (ts : t ⊆ s) (t_meas : MeasurableSet t) (ht : t =ᶠ[ae (sum f)] s),
    LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, t_meas, ht⟩

Premises used: MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
t : Set α
ts : t ⊆ s
t_meas : MeasurableSet t
ht : t =ᶠ[ae (sum f)] s
⊢ Eq (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
measure_congr ht.symm

Premises used: MeasureTheory.measure_congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
t : Set α
ts : t ⊆ s
t_meas : MeasurableSet t
ht : t =ᶠ[ae (sum f)] s
⊢ Eq (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
sum_apply _ t_meas

Premises used: MeasureTheory.Measure.sum_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
t : Set α
ts : t ⊆ s
t_meas : MeasurableSet t
ht : t =ᶠ[ae (sum f)] s
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) t) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s)

Tactic:
ENNReal.tsum_le_tsum fun i ↦ measure_mono ts

Premises used: ENNReal.tsum_le_tsum, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
t : Set α
ts : t ⊆ s
t_meas : MeasurableSet t
ht : t =ᶠ[ae (sum f)] s
⊢ LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
  sum f s = sum f t := measure_congr ht.symm
  _ = ∑' i, f i t := sum_apply _ t_meas
  _ ≤ ∑' i, f i s := ENNReal.tsum_le_tsum fun i ↦ measure_mono ts

Premises used: MeasureTheory.measure_congr, ENNReal.tsum_le_tsum, MeasureTheory.Measure.sum_apply, MeasureTheory.measure_mono, MeasureTheory.Measure.sum, DFunLike.coe, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Countable ι
f : ι → Measure α
s : Set α
apply : LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply le_antisymm ?_ (le_sum_apply _ _)

Premises used: MeasureTheory.Measure.le_sum_apply, le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Countable ι
f : ι → Measure α
s : Set α
rcases :
  ∀ (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∞)),
    LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rcases exists_measurable_superset_forall_eq f s with ⟨t, hst, htm, ht⟩

Premises used: MeasureTheory.exists_measurable_superset_forall_eq
-- 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∞)
⊢ LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
measure_mono hst

Premises used: MeasureTheory.measure_mono
-- 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∞) ((sum f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
sum_apply _ htm

Premises used: MeasureTheory.Measure.sum_apply