awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfAddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s : Set α
hs : MeasurableSet s
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    s
have basic : ∀ (u : Set α) (hu : u ∈ C),
  (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) sorry
        sorry).IsCaratheodory
    u
Tactic: induction hs with
  | basic u hu => exact isCaratheodory_inducedOuterMeasure_of_mem hC m hu
  | empty => exact OuterMeasure.isCaratheodory_empty _
  | compl t _ h => exact OuterMeasure.isCaratheodory_compl _ h
  | iUnion f _ h => exact OuterMeasure.isCaratheodory_iUnion _ h
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfAddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s : Set α
hs : MeasurableSet s
basic :
  ∀ (u : Set α) (hu : u ∈ C),
    (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
          ⋯).IsCaratheodory
      u
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    s
have empty : (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) sorry
      sorry).IsCaratheodory
  ∅
Tactic: induction hs with
  | basic u hu => exact isCaratheodory_inducedOuterMeasure_of_mem hC m hu
  | empty => exact OuterMeasure.isCaratheodory_empty _
  | compl t _ h => exact OuterMeasure.isCaratheodory_compl _ h
  | iUnion f _ h => exact OuterMeasure.isCaratheodory_iUnion _ h
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfAddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s : Set α
hs : MeasurableSet s
basic :
  ∀ (u : Set α) (hu : u ∈ C),
    (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
          ⋯).IsCaratheodory
      u
empty :
  (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    ∅
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    s
have compl : ∀ (t : Set α),
  MeasurableSpace.GenerateMeasurable C t →
    ∀
      (h :
        (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) sorry
              sorry).IsCaratheodory
          t),
      (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) sorry
            sorry).IsCaratheodory
        tᶜ
Tactic: induction hs with
  | basic u hu => exact isCaratheodory_inducedOuterMeasure_of_mem hC m hu
  | empty => exact OuterMeasure.isCaratheodory_empty _
  | compl t _ h => exact OuterMeasure.isCaratheodory_compl _ h
  | iUnion f _ h => exact OuterMeasure.isCaratheodory_iUnion _ h
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfAddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s : Set α
hs : MeasurableSet s
basic :
  ∀ (u : Set α) (hu : u ∈ C),
    (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
          ⋯).IsCaratheodory
      u
empty :
  (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    ∅
compl :
  ∀ (t : Set α),
    MeasurableSpace.GenerateMeasurable C t →
      ∀
        (h :
          (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
                ⋯).IsCaratheodory
            t),
        (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
              ⋯).IsCaratheodory
          tᶜ
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    s
have iUnion : ∀ (f : ℕ → Set α),
  (∀ (n : ℕ), MeasurableSpace.GenerateMeasurable C (f n)) →
    ∀
      (h :
        ∀ (n : ℕ),
          (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) sorry
                sorry).IsCaratheodory
            (f n)),
      (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) sorry
            sorry).IsCaratheodory
        (⋃ (i : ℕ), f i)
Tactic: induction hs with
  | basic u hu => exact isCaratheodory_inducedOuterMeasure_of_mem hC m hu
  | empty => exact OuterMeasure.isCaratheodory_empty _
  | compl t _ h => exact OuterMeasure.isCaratheodory_compl _ h
  | iUnion f _ h => exact OuterMeasure.isCaratheodory_iUnion _ h
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfAddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_sigma_subadd : m.IsSigmaSubadditive (C := C)
this : MeasurableSpace α :=
  (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
      ⋯).caratheodory
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯ ⋯).trim ≤
    inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯ ⋯
have apply : ∀ (s : Set α) (hs : s ∈ C),
  LE.le (α := ℝ≥0∞)
    (((inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) sorry
              sorry).trim :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply le_inducedOuterMeasure.mpr fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfAddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s_1 : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_sigma_subadd : m.IsSigmaSubadditive (C := C)
this : MeasurableSpace α :=
  (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
      ⋯).caratheodory
s : Set α
hs : s ∈ C
hs_meas : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞)
    (((inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
              ⋯).trim :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞)
  ((inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) sorry sorry :
        (a : Set α) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [OuterMeasure.trim_eq _ hs_meas, m.inducedOuterMeasure_eq hC m_sigma_subadd hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfAddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s_1 : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_sigma_subadd : m.IsSigmaSubadditive (C := C)
this : MeasurableSpace α :=
  (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
      ⋯).caratheodory
s : Set α
hs : s ∈ C
hs_meas : MeasurableSet s
rw :
  LE.le (α := ℝ≥0∞)
    ((inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯ ⋯ :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (((inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
              ⋯).trim :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [OuterMeasure.trim_eq _ hs_meas, m.inducedOuterMeasure_eq hC m_sigma_subadd hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfAddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
mα : MeasurableSpace α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
hC_gen : mα = MeasurableSpace.generateFrom C
m_sigma_subadd : m.IsSigmaSubadditive (C := C)
hs : s ∈ C
⊢ Eq (α := ℝ≥0∞) ((m.measure (C := C) hC ⋯ m_sigma_subadd : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((m.measureCaratheodory (C := C) hC m_sigma_subadd : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [measure, trim_measurableSet_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfAddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
mα : MeasurableSpace α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
hC_gen : mα = MeasurableSpace.generateFrom C
m_sigma_subadd : m.IsSigmaSubadditive (C := C)
hs : s ∈ C
rw :
  Eq (α := ℝ≥0∞) ((m.measureCaratheodory (C := C) hC m_sigma_subadd : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m.measure (C := C) hC ⋯ m_sigma_subadd : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have hs₁ : MeasurableSet s
Tactic: rw [measure, trim_measurableSet_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfAddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
mα : MeasurableSpace α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
hC_gen : mα = MeasurableSpace.generateFrom C
m_sigma_subadd : m.IsSigmaSubadditive (C := C)
hs : s ∈ C
⊢ MeasurableSet s
have hs₁ : MeasurableSet s
Tactic: rw [hC_gen]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
⊢ μ ∅ = 0
have rw : μ ∅ ≤ 0
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
⊢ μ (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), μ (s i) + (↑ε : ℝ≥0∞)
have rcases : ∀ (ε' : ℕ → ℝ≥0) (hε' : ∀ (i : ℕ), 0 < ε' i) (hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)),
  μ (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), μ (s i) + (↑ε : ℝ≥0∞)
Tactic: rcases ENNReal.exists_pos_sum_of_countable (ENNReal.coe_pos.2 hε).ne' ℕ with ⟨ε', hε', hl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
⊢ μ (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), μ (s i) + (↑ε : ℝ≥0∞)
have grw : μ (⋃ (i : ℕ), s i) ≤ HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) (∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞))
Tactic: grw [← hl]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
⊢ μ (⋃ (i : ℕ), s i) ≤ HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) (∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞))
have rw : μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ), (μ (s a) + (↑(ε' a) : ℝ≥0∞))
Tactic: rw [← ENNReal.tsum_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (hypothesis)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
⊢ ∃ (f : ℕ → Set α), s i ⊆ ⋃ (i : ℕ), f i ∧ ∑' (i : ℕ), m (f i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
have this : μ (s i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
Tactic: have : μ (s i) < μ (s i) + ε' i :=
              ENNReal.lt_add_right (ne_top_of_le_ne_top hb.ne <| ENNReal.le_tsum _)
                (by simpa using (hε' i).ne')
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
this : μ (s i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ ∃ (f : ℕ → Set α), s i ⊆ ⋃ (i : ℕ), f i ∧ ∑' (i : ℕ), m (f i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
have rcases : ∀ (t : ℕ → Set α) (ht : ⨅ (_ : s i ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)),
  ∃ (f : ℕ → Set α), s i ⊆ ⋃ (i : ℕ), f i ∧ ∑' (i : ℕ), m (f i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
Tactic: rcases iInf_lt_iff.mp this with ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
this : μ (s i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
t : ℕ → Set α
ht : ⨅ (_ : s i ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ ∃ (f : ℕ → Set α), s i ⊆ ⋃ (i : ℕ), f i ∧ ∑' (i : ℕ), m (f i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
have exists : s i ⊆ ⋃ (i : ℕ), t i ∧ ∑' (i : ℕ), m (t i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
Tactic: exists t
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
this : μ (s i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
t : ℕ → Set α
ht : ⨅ (_ : s i ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ s i ⊆ ⋃ (i : ℕ), t i ∧ ∑' (i : ℕ), m (t i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
have contrapose! : ∀ (ht : ∀ (_ : s i ⊆ ⋃ (i : ℕ), t i), μ (s i) + (↑(ε' i) : ℝ≥0∞) ≤ ∑' (i : ℕ), m (t i)),
  μ (s i) + (↑(ε' i) : ℝ≥0∞) ≤ ⨅ (_ : s i ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)
Tactic: contrapose! ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
⊢ μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ), (μ (s a) + (↑(ε' a) : ℝ≥0∞))
have choose : ∀ (f : (i : ℕ) → ℕ → Set α)
  (hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)),
  μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ), (μ (s a) + (↑(ε' a) : ℝ≥0∞))
Tactic: choose f hf using
          show ∀ i, ∃ f : ℕ → Set α, (s i ⊆ ⋃ i, f i) ∧ (∑' i, m (f i)) < μ (s i) + ε' i by
            intro i
            have : μ (s i) < μ (s i) + ε' i :=
              ENNReal.lt_add_right (ne_top_of_le_ne_top hb.ne <| ENNReal.le_tsum _)
                (by simpa using (hε' i).ne')
            rcases iInf_lt_iff.mp this with ⟨t, ht⟩
            exists t
            contrapose! ht
            exact le_iInf ht
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ), (μ (s a) + (↑(ε' a) : ℝ≥0∞))
have refine : μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ) (i : ℕ), m (f a i)
Tactic: refine le_trans ?_ (ENNReal.tsum_le_tsum fun i => le_of_lt (hf i).2)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ) (i : ℕ), m (f a i)
have rw : μ (⋃ (i : ℕ), s i) ≤
  ∑' (c : ℕ), m (f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) c).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) c).2)
Tactic: rw [← ENNReal.tsum_prod, ← Nat.pairEquiv.symm.tsum_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ μ (⋃ (i : ℕ), s i) ≤
    ∑' (c : ℕ), m (f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) c).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) c).2)
have refine : Subset.{u_1} (α := Set α) (⋃ (i : ℕ), s i)
  (⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2)
Tactic: refine iInf_le_of_le _ (iInf_le _ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ Subset.{u_1} (α := Set α) (⋃ (i : ℕ), s i)
    (⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2)
have h : ∀ (i : ℕ), s i ⊆ ⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2
Tactic: apply iUnion_subset
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
i : ℕ
⊢ s i ⊆ ⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2
have h : Subset.{u_1} (α := Set α) (⋃ (i_1 : ℕ), f i i_1)
  (⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2)
Tactic: apply Subset.trans (hf i).1
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
i : ℕ
⊢ Subset.{u_1} (α := Set α) (⋃ (i_1 : ℕ), f i i_1)
    (⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2)
have h : ∀ (i_1 : ℕ),
  f i i_1 ⊆ ⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2
Tactic: apply iUnion_subset
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
i : ℕ
⊢ ∀ (i_1 : ℕ),
    f i i_1 ⊆ ⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2
have h : ∀ (i_1 : ℕ), f i i_1 ⊆ ⋃ (i : ℕ), f (Nat.unpair i).1 (Nat.unpair i).2
Tactic: simp only [Nat.pairEquiv_symm_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ Eq (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
    (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
have a : LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
  (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
a :
  LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
    (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
⊢ Eq (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
    (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
have a₁ : LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
  (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
have a : ∀ (i : ℕ → Set α) (i_1 : s ⊆ iUnion i),
  LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
    (∑' (n : ℕ), m (i n))
Tactic: simp_rw [le_iInf_iff]