awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ (i : ℕ), f i
A : ℕ → Finset (Set α) := fun (i : ℕ) ↦ hC.disjointOfDiff (C := C) (s := f i) (t := f i ∩ s) ⋯ ⋯
h_m_eq :
  ∀ (i : ℕ),
    (m : (a : Set α) → ℝ≥0∞) (f i) =
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i ∩ s) : ℝ≥0∞)
        (∑ u ∈ A i, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
i : ℕ
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ (↑(A i) : Set (Set α)), i_1
⊢ LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞)
        (⋃ i_1 ∈ A i, id i_1) :
      ℝ≥0∞)
    (∑ i ∈ A i, ((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (id i) :
      ℝ≥0∞)

Tactic:
obtain h6 := MeasureTheory.measure_biUnion_finset_le
      (μ := OuterMeasure.ofFunction m addContent_empty) (A i) id

Premises used: id, MeasureTheory.measure_biUnion_finset_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ (i : ℕ), f i
A : ℕ → Finset (Set α) := fun (i : ℕ) ↦ hC.disjointOfDiff (C := C) (s := f i) (t := f i ∩ s) ⋯ ⋯
h_m_eq :
  ∀ (i : ℕ),
    (m : (a : Set α) → ℝ≥0∞) (f i) =
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i ∩ s) : ℝ≥0∞)
        (∑ u ∈ A i, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
i : ℕ
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ (↑(A i) : Set (Set α)), i_1
h6 :
  LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞)
        (⋃ i_1 ∈ A i, id i_1) :
      ℝ≥0∞)
    (∑ i ∈ A i, ((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (id i) :
      ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ i_1 ∈ A i, i_1) :
      ℝ≥0∞)
    (∑ x ∈ A i, ((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
simp only [id_eq] at h6

Premises used: id_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ (i : ℕ), f i
A : ℕ → Finset (Set α) := fun (i : ℕ) ↦ hC.disjointOfDiff (C := C) (s := f i) (t := f i ∩ s) ⋯ ⋯
h_m_eq :
  ∀ (i : ℕ),
    (m : (a : Set α) → ℝ≥0∞) (f i) =
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i ∩ s) : ℝ≥0∞)
        (∑ u ∈ A i, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
i : ℕ
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ (↑(A i) : Set (Set α)), i_1
h6 :
  LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ i_1 ∈ A i, i_1) :
      ℝ≥0∞)
    (∑ x ∈ A i, ((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞)
        (⋃ i_1 ∈ (↑(A i) : Set (Set α)), i_1) :
      ℝ≥0∞)
    (∑ u ∈ hC.disjointOfDiff (C := C) (s := f i) (t := f i ∩ s) ⋯ ⋯, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
le_trans h6 <| Finset.sum_le_sum <| fun b _ ↦ OuterMeasure.ofFunction_le b

Premises used: MeasureTheory.OuterMeasure.ofFunction_le, Finset.sum_le_sum, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ (i : ℕ), f i
A : ℕ → Finset (Set α) := fun (i : ℕ) ↦ hC.disjointOfDiff (C := C) (s := f i) (t := f i ∩ s) ⋯ ⋯
h_m_eq :
  ∀ (i : ℕ),
    (m : (a : Set α) → ℝ≥0∞) (f i) =
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i ∩ s) : ℝ≥0∞)
        (∑ u ∈ A i, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
i : ℕ
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ (↑(A i) : Set (Set α)), i_1
h6 :
  LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ i_1 ∈ A i, i_1) :
      ℝ≥0∞)
    (∑ x ∈ A i, ((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞)
        (⋃ i_1 ∈ (↑(A i) : Set (Set α)), i_1) :
      ℝ≥0∞)
    (∑ u ∈ hC.disjointOfDiff (C := C) (s := f i) (t := f i ∩ s) ⋯ ⋯, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
exact le_trans h6 <| Finset.sum_le_sum <| fun b _ ↦ OuterMeasure.ofFunction_le b

Premises used: MeasureTheory.OuterMeasure.ofFunction_le, Finset.sum_le_sum, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s : Set α
hs : s ∈ C
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    s

Tactic:
isCaratheodory_ofFunction_of_mem hC (m.extend hC) (fun _ ↦ m.extend_eq_top hC) hs

Premises used: MeasureTheory.AddContent.isCaratheodory_ofFunction_of_mem, iInf, MeasureTheory.extend, MeasureTheory.inducedOuterMeasure, MeasureTheory.AddContent.extend, MeasureTheory.AddContent.extend_eq_top, ite
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s u : Set α
hu : u ∈ C
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    u

Tactic:
isCaratheodory_inducedOuterMeasure_of_mem hC m hu

Premises used: MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure_of_mem
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s u : Set α
hu : u ∈ C
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    u

Tactic:
exact isCaratheodory_inducedOuterMeasure_of_mem hC m hu

Premises used: MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure_of_mem
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s : Set α
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    ∅

Tactic:
OuterMeasure.isCaratheodory_empty _

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s : Set α
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    ∅

Tactic:
exact OuterMeasure.isCaratheodory_empty _

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s t : Set α
h_1 : 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ᶜ

Tactic:
OuterMeasure.isCaratheodory_compl _ h

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_compl
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s t : Set α
h_1 : 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ᶜ

Tactic:
exact OuterMeasure.isCaratheodory_compl _ h

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_compl
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s : Set α
f : ℕ → Set α
h_1 : ∀ (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) ⋯
          ⋯).IsCaratheodory
      (f n)
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    (⋃ (i : ℕ), f i)

Tactic:
OuterMeasure.isCaratheodory_iUnion _ h

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s : Set α
f : ℕ → Set α
h_1 : ∀ (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) ⋯
          ⋯).IsCaratheodory
      (f n)
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    (⋃ (i : ℕ), f i)

Tactic:
exact OuterMeasure.isCaratheodory_iUnion _ h

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
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ᶜ
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) ⋯
                  ⋯).IsCaratheodory
              (f n)),
        (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
              ⋯).IsCaratheodory
          (⋃ (i : ℕ), f i)
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    s

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

Premises used: Compl.compl, MeasureTheory.OuterMeasure.isCaratheodory_empty, Set.iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
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
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) ⋯
                ⋯).trim :
            (a : Set α) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (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) ⋯ ⋯

Tactic:
apply le_inducedOuterMeasure.mpr fun s hs ↦ ?_

Premises used: Iff.mpr, MeasureTheory.le_inducedOuterMeasure
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
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
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    s

Tactic:
isCaratheodory_inducedOuterMeasure_of_mem hC m hs

Premises used: MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure_of_mem
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
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
⊢ (inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯
        ⋯).IsCaratheodory
    s

Tactic:
exact isCaratheodory_inducedOuterMeasure_of_mem hC m hs

Premises used: MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure_of_mem
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
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∞)
rw₁ rw₂ : LE.le (α := ℝ≥0∞) ((m : (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∞)

Tactic:
rw [OuterMeasure.trim_eq _ hs_meas, m.inducedOuterMeasure_eq hC m_sigma_subadd hs]

Premises used: MeasureTheory.AddContent.inducedOuterMeasure_eq, MeasureTheory.OuterMeasure.trim_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive (C := C)
⊢ Eq (α := ℝ≥0∞) ((m.measureCaratheodory (C := C) hC m_sigma_subadd : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯ ⋯ :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_sigma_subadd : m.IsSigmaSubadditive (C := C)
hs : s ∈ C
⊢ Eq (α := ℝ≥0∞) ((m.measureCaratheodory (C := C) hC m_sigma_subadd : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
m.inducedOuterMeasure_eq hC m_sigma_subadd hs

Premises used: MeasureTheory.AddContent.inducedOuterMeasure_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
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∞)
hs₁ : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((m.measure (C := C) hC ⋯ m_sigma_subadd : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [measure, trim_measurableSet_eq]

Premises used: MeasureTheory.trim_measurableSet_eq, MeasureTheory.AddContent.measure
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
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.measureCaratheodory (C := C) hC m_sigma_subadd : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
m.measureCaratheodory_eq hC m_sigma_subadd hs

Premises used: MeasureTheory.AddContent.measureCaratheodory_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
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.measureCaratheodory (C := C) hC m_sigma_subadd : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact m.measureCaratheodory_eq hC m_sigma_subadd hs

Premises used: MeasureTheory.AddContent.measureCaratheodory_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
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
hs₁ : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rw [hC_gen]
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent
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

Tactic:
apply MeasurableSpace.measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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)
rw : μ ∅ ≤ 0
⊢ μ ∅ = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), m ((fun (x : ℕ) ↦ (∅ : Set α)) i)) 0

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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

Tactic:
exact (iInf_le_of_le fun _ => ∅) <| iInf_le_of_le (empty_subset _) <| by simpa

Premises used: Set.empty_subset, EmptyCollection.emptyCollection, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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∞)
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞ → μ (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), μ (s i) + (↑ε : ℝ≥0∞)

Tactic:
(hb : (∑' i, μ (s i)) < ∞)
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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)) ∞
rcases :
  ∀ (ε' : ℕ → ℝ≥0) (hε' : ∀ (i : ℕ), 0 < ε' i) (hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)),
    μ (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), μ (s i) + (↑ε : ℝ≥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⟩

Premises used: Iff.mpr, LT.lt.ne', ENNReal.coe_pos, ENNReal.exists_pos_sum_of_countable, Nat
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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∞)
grw : μ (⋃ (i : ℕ), s i) ≤ HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) (∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞))
⊢ μ (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), μ (s i) + (↑ε : ℝ≥0∞)

Tactic:
grw [← hl]
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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∞)
rw : μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ), (μ (s a) + (↑(ε' a) : ℝ≥0∞))
⊢ μ (⋃ (i : ℕ), s i) ≤ HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) (∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞))

Tactic:
rw [← ENNReal.tsum_add]

Premises used: ENNReal.tsum_add
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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 : ℕ
⊢ (↑(ε' i) : ℝ≥0∞) ≠ 0

Tactic:
simpa using (hε' i).ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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) < μ (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')