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
rw :
  ∀ (t : Set α),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
      ((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t
⊢ OuterMeasure.IsCaratheodory (OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯) s

Tactic:
rw [OuterMeasure.isCaratheodory_iff_le']

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_iff_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 α
rw :
  ⨅ (t_1 : ℕ → Set α),
    ⨅ (_ : ∀ (i : ℕ), t_1 i ∈ C), ⨅ (_ : t ⊆ ⋃ (i : ℕ), t_1 i), ∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (t_1 i)
| (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [OuterMeasure.ofFunction_eq_iInf_mem _ _ m_top]

Premises used: MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem
-- 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 α
conv_rhs :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ⨅ (t_1 : ℕ → Set α),
      ⨅ (_ : ∀ (i : ℕ), t_1 i ∈ C), ⨅ (_ : t ⊆ ⋃ (i : ℕ), t_1 i), ∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (t_1 i)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t

Tactic:
conv_rhs => rw [OuterMeasure.ofFunction_eq_iInf_mem _ _ m_top]

Premises used: MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem
-- 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 α
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ⨅ (t_1 : ℕ → Set α),
      ⨅ (_ : ∀ (i : ℕ), t_1 i ∈ C), ⨅ (_ : t ⊆ ⋃ (i : ℕ), t_1 i), ∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (t_1 i)

Tactic:
le_iInf fun f ↦ le_iInf fun hf ↦ le_iInf fun hf_subset ↦ ?_

Premises used: le_iInf
-- 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 α
refine :
  ∀ (f : ℕ → Set α) (hf : ∀ (i : ℕ), f i ∈ C) (hf_subset : t ⊆ ⋃ (i : ℕ), f i),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
      ∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ⨅ (t_1 : ℕ → Set α),
      ⨅ (_ : ∀ (i : ℕ), t_1 i ∈ C), ⨅ (_ : t ⊆ ⋃ (i : ℕ), t_1 i), ∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (t_1 i)

Tactic:
refine le_iInf fun f ↦ le_iInf fun hf ↦ le_iInf fun hf_subset ↦ ?_

Premises used: le_iInf
-- 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) ⋯ ⋯
i : ℕ
⊢ f i \ s = ⋃₀ (↑(A i) : Set (Set α))

Tactic:
simp [A, IsSetSemiring.sUnion_disjointOfDiff]

Premises used: MeasureTheory.IsSetSemiring.sUnion_disjointOfDiff
-- 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) ⋯ ⋯
⊢ ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))

Tactic:
have h_diff_eq_sUnion i : f i \ s = ⋃₀ A i := by simp [A, IsSetSemiring.sUnion_disjointOfDiff]
-- 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
⊢ ∀ (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∞)

Tactic:
have h_m_eq i : m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u :=
    eq_add_disjointOfDiff_of_subset hC (hC.inter_mem (f i) (hf i) s hs) (hf i) inter_subset_left
-- 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
simp_rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ∑' (i : ℕ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i ∩ s) : ℝ≥0∞)
        (∑ u ∈ A i, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)

Tactic:
simp_rw [h_m_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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (m : (a : Set α) → ℝ≥0∞) (f a ∩ s))
      (∑' (a : ℕ), ∑ u ∈ A a, (m : (a : Set α) → ℝ≥0∞) u)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ∑' (i : ℕ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i ∩ s) : ℝ≥0∞)
        (∑ u ∈ A i, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
rw [ENNReal.tsum_add]

Premises used: ENNReal.tsum_add
-- 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (m : (a : Set α) → ℝ≥0∞) (f a ∩ s))
      (∑' (a : ℕ), ∑ u ∈ A a, (m : (a : Set α) → ℝ≥0∞) u)

Tactic:
add_le_add ?_ ?_

Premises used: add_le_add
-- 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
refine_1 :
  LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (a : ℕ), (m : (a : Set α) → ℝ≥0∞) (f a ∩ s) : ℝ≥0∞)
refine_2 :
  LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
    (∑' (a : ℕ), ∑ u ∈ A a, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (m : (a : Set α) → ℝ≥0∞) (f a ∩ s))
      (∑' (a : ℕ), ∑ u ∈ A a, (m : (a : Set α) → ℝ≥0∞) u)

Tactic:
refine add_le_add ?_ ?_

Premises used: add_le_add
-- 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
⊢ LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (a : ℕ), (m : (a : Set α) → ℝ≥0∞) (f a ∩ s) : ℝ≥0∞)

Tactic:
iInf_le_of_le (fun i ↦ f i ∩ s) <| iInf_le_of_le ?_ le_rfl

Premises used: iInf, le_rfl, Inter.inter, iInf_le_of_le, ite
-- 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
refine_1 : t ∩ s ⊆ ⋃ (i : ℕ), (fun (i : ℕ) ↦ f i ∩ s) i
⊢ LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (a : ℕ), (m : (a : Set α) → ℝ≥0∞) (f a ∩ s) : ℝ≥0∞)

Tactic:
refine iInf_le_of_le (fun i ↦ f i ∩ s) <| iInf_le_of_le ?_ le_rfl

Premises used: le_rfl, Inter.inter, iInf_le_of_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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
refine_1 : t ∩ s ⊆ (⋃ (i : ℕ), f i) ∩ s
⊢ t ∩ s ⊆ ⋃ (i : ℕ), (fun (i : ℕ) ↦ f i ∩ s) i

Tactic:
rw [← iUnion_inter]

Premises used: Set.iUnion_inter
-- 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
⊢ t ∩ s ⊆ (⋃ (i : ℕ), f i) ∩ s

Tactic:
Set.inter_subset_inter_left _ hf_subset

Premises used: Set.inter_subset_inter_left
-- 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
⊢ t ∩ s ⊆ (⋃ (i : ℕ), f i) ∩ s

Tactic:
exact Set.inter_subset_inter_left _ hf_subset

Premises used: Set.inter_subset_inter_left
-- 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
refine_2 :
  OuterMeasure.measureOf (α := α) (OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯) (⋃ (i : ℕ), f i \ s) ≤
    ∑' (a : ℕ), ∑ u ∈ A a, (m : (a : Set α) → ℝ≥0∞) u
⊢ LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
    (∑' (a : ℕ), ∑ u ∈ A a, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
apply le_trans <| (OuterMeasure.ofFunction m addContent_empty).mono
      <| (iUnion_diff s f) ▸ diff_subset_diff_left hf_subset

Premises used: MeasureTheory.OuterMeasure.mono, DFunLike.coe, MeasureTheory.addContent_empty, MeasureTheory.OuterMeasure.ofFunction, 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
refine_2 :
  LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞)
        (⋃ (i : ℕ), f i \ s) :
      ℝ≥0∞)
    (∑' (a : ℕ), ∑ u ∈ hC.disjointOfDiff (C := C) (s := f a) (t := f a ∩ s) ⋯ ⋯, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ OuterMeasure.measureOf (α := α) (OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯) (⋃ (i : ℕ), f i \ s) ≤
    ∑' (a : ℕ), ∑ u ∈ A a, (m : (a : Set α) → ℝ≥0∞) u

Tactic:
simp only [OuterMeasure.measureOf_eq_coe, A]

Premises used: MeasureTheory.OuterMeasure.measureOf_eq_coe
-- 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
refine_2 :
  LE.le (α := ℝ≥0∞)
    (∑' (i : ℕ),
      ((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i \ s))
    (∑' (a : ℕ), ∑ u ∈ hC.disjointOfDiff (C := C) (s := f a) (t := f a ∩ s) ⋯ ⋯, (m : (a : Set α) → ℝ≥0∞) u)
⊢ LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞)
        (⋃ (i : ℕ), f i \ s) :
      ℝ≥0∞)
    (∑' (a : ℕ), ∑ u ∈ hC.disjointOfDiff (C := C) (s := f a) (t := f a ∩ s) ⋯ ⋯, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
apply le_trans <| measure_iUnion_le (μ := OuterMeasure.ofFunction m addContent_empty)
      (fun i ↦ f i \ s)

Premises used: SDiff.sdiff, MeasureTheory.measure_iUnion_le, 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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∞)
refine_2 :
  ∀ (a : ℕ),
    LE.le (α := ℝ≥0∞)
      (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f a \ s) : ℝ≥0∞)
      (∑ u ∈ hC.disjointOfDiff (C := C) (s := f a) (t := f a ∩ s) ⋯ ⋯, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (∑' (i : ℕ),
      ((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i \ s))
    (∑' (a : ℕ), ∑ u ∈ hC.disjointOfDiff (C := C) (s := f a) (t := f a ∩ s) ⋯ ⋯, (m : (a : Set α) → ℝ≥0∞) u)

Tactic:
apply ENNReal.tsum_le_tsum

Premises used: ENNReal.tsum_le_tsum
-- 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_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ (↑(A i) : Set (Set α))
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 : ℕ
⊢ ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ (↑(A i) : Set (Set α)), i_1

Tactic:
simp_rw [sUnion_eq_biUnion] at h_diff_eq_sUnion

Premises used: Set.sUnion_eq_biUnion
-- 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
refine_2 :
  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∞)
⊢ LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i \ s) : ℝ≥0∞)
    (∑ u ∈ hC.disjointOfDiff (C := C) (s := f i) (t := f i ∩ s) ⋯ ⋯, (m : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
rw [h_diff_eq_sUnion]