awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ∩ s ⊆ t'
ht' : MeasurableSet t'
hμt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
htt'₁ : t ⊆ sᶜ ∪ t'
ht'₁ : MeasurableSet t'
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
rw [inter_subset] at htt'

Premises used: Set.inter_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)

Tactic:
(measure_mono htt').trans ?_

Premises used: MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
refine_1 :
  LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (sᶜ ∪ t') :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)

Tactic:
refine (measure_mono htt').trans ?_

Premises used: MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
refine_1 : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (sᶜ ∪ t') :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)

Tactic:
rw [trim_eq _ (hs.compl.union ht'), restrict_apply, union_inter_distrib_right, compl_inter_self,
      Set.empty_union]

Premises used: Set.empty_union, MeasurableSet.compl, MeasurableSet.union, MeasureTheory.OuterMeasure.trim_eq, MeasureTheory.OuterMeasure.restrict_apply, Set.compl_inter_self, Set.union_inter_distrib_right
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)

Tactic:
measure_mono inter_subset_left

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)

Tactic:
exact measure_mono inter_subset_left

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
refine_2 :
  LE.le (α := ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine_2₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine_2₂ refine_2₃ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.trim : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [restrict_apply, trim_eq _ (ht.inter hs), restrict_apply]

Premises used: MeasureTheory.OuterMeasure.trim_eq, MeasureTheory.OuterMeasure.restrict_apply, MeasurableSet.inter
-- 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)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
⊢ Eq (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
le_antisymm (OuterMeasure.ofFunction_le s) ?_

Premises used: le_antisymm, MeasureTheory.OuterMeasure.ofFunction_le
-- 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)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
refine :
  LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine le_antisymm (OuterMeasure.ofFunction_le s) ?_

Premises used: le_antisymm, MeasureTheory.OuterMeasure.ofFunction_le
-- 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)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
rw :
  LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : ℕ → Set α),
        ⨅ (_ : ∀ (i : ℕ), t i ∈ C), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (t i) :
      ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑m : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥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_sigma_subadd : m.IsSigmaSubadditive (C := C)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : ℕ → Set α),
        ⨅ (_ : ∀ (i : ℕ), t i ∈ C), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (t i) :
      ℝ≥0∞)

Tactic:
le_iInf fun f ↦ le_iInf fun hf ↦ le_iInf fun hs_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_sigma_subadd : m.IsSigmaSubadditive (C := C)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
refine :
  ∀ (f : ℕ → Set α) (hf : ∀ (i : ℕ), f i ∈ C) (hs_subset : s ⊆ ⋃ (i : ℕ), f i),
    LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : ℕ → Set α),
        ⨅ (_ : ∀ (i : ℕ), t i ∈ C), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (t i) :
      ℝ≥0∞)

Tactic:
refine le_iInf fun f ↦ le_iInf fun hf ↦ le_iInf fun hs_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_sigma_subadd : m.IsSigmaSubadditive (C := C)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ (i : ℕ), f i
rw rw₁ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ ⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
rw [inter_eq_self_of_subset_left hs_subset]

Premises used: Set.inter_eq_self_of_subset_left
-- 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)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ (i : ℕ), f i
rw rw₁ :
  Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ f i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ ⋃ (i : ℕ), f i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ f i) : ℝ≥0∞)

Tactic:
rw [inter_iUnion]

Premises used: Set.inter_iUnion
-- 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)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ (i : ℕ), f i
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ f i) : ℝ≥0∞)
    (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s ∩ f i) : ℝ≥0∞)

Tactic:
m_sigma_subadd (fun i ↦ hC.inter_mem _ hs _ (hf i)) ?_

Premises used: MeasureTheory.IsSetSemiring.inter_mem
-- 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)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ (i : ℕ), f i
refine : ⋃ (i : ℕ), s ∩ f i ∈ C
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ f i) : ℝ≥0∞)
    (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s ∩ f i) : ℝ≥0∞)

Tactic:
refine m_sigma_subadd (fun i ↦ hC.inter_mem _ hs _ (hf i)) ?_

Premises used: MeasureTheory.IsSetSemiring.inter_mem
-- 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)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ (i : ℕ), f i
rwa : s ∩ ⋃ (i : ℕ), f i ∈ C
rwa₁ rwa₂ rwa₃ rwa₄ : s ∈ C
⊢ ⋃ (i : ℕ), s ∩ f i ∈ C

Tactic:
rwa [← inter_iUnion, inter_eq_self_of_subset_left hs_subset]

Premises used: Set.inter_iUnion, Set.inter_eq_self_of_subset_left
-- 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)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ (i : ℕ), f i
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s ∩ f i)) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i))

Tactic:
ENNReal.summable.tsum_le_tsum (fun i ↦ ?_) ENNReal.summable

Premises used: ENNReal.summable, Summable.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_sigma_subadd : m.IsSigmaSubadditive (C := C)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ (i : ℕ), f i
refine :
  ∀ (i : ℕ), LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ f i) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s ∩ f i)) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i))

Tactic:
refine ENNReal.summable.tsum_le_tsum (fun i ↦ ?_) ENNReal.summable

Premises used: ENNReal.summable, Summable.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_sigma_subadd : m.IsSigmaSubadditive (C := C)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ (i : ℕ), f i
i : ℕ
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ f i) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
addContent_mono hC (hC.inter_mem _ hs _ (hf i)) (hf i) Set.inter_subset_right

Premises used: MeasureTheory.addContent_mono, MeasureTheory.IsSetSemiring.inter_mem, Set.inter_subset_right
-- 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)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ (i : ℕ), f i
i : ℕ
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ f i) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
exact addContent_mono hC (hC.inter_mem _ hs _ (hf i)) (hf i) Set.inter_subset_right

Premises used: MeasureTheory.addContent_mono, MeasureTheory.IsSetSemiring.inter_mem, Set.inter_subset_right
-- 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)
m_top : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ (i : ℕ), f i
calc : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ ⋃ (i : ℕ), f i) : ℝ≥0∞)
calc₁ :
  Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ ⋃ (i : ℕ), f i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ f i) : ℝ≥0∞)
calc₂ :
  LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ f i) : ℝ≥0∞)
    (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s ∩ f i) : ℝ≥0∞)
calc₃ : LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s ∩ f i)) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i))
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
calc m s = m (s ∩ ⋃ i, f i) := by rw [inter_eq_self_of_subset_left hs_subset]
    _ = m (⋃ i, s ∩ f i) := by rw [inter_iUnion]
    _ ≤ ∑' i, m (s ∩ f i) := by
      refine m_sigma_subadd (fun i ↦ hC.inter_mem _ hs _ (hf i)) ?_
      rwa [← inter_iUnion, inter_eq_self_of_subset_left hs_subset]
    _ ≤ ∑' i, m (f i) := by
      refine ENNReal.summable.tsum_le_tsum (fun i ↦ ?_) ENNReal.summable
      exact addContent_mono hC (hC.inter_mem _ hs _ (hf i)) (hf i) Set.inter_subset_right

Premises used: Inter.inter, DFunLike.coe, Set.iUnion
-- 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)
hs : s ∈ C
this :
  Eq (α := ℝ≥0∞)
    ((inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯ ⋯ :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Eq (α := ℝ≥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∞)),
    Eq (α := ℝ≥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∞)
⊢ Eq (α := ℝ≥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∞)

Tactic:
rwa [m.extend_eq hC hs] at this

Premises used: MeasureTheory.AddContent.extend_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)
hs : s ∈ C
suffices :
  Eq (α := ℝ≥0∞)
    ((inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯ ⋯ :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥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∞)

Tactic:
suffices inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s = m.extend hC s by
    rwa [m.extend_eq hC hs] at this
-- 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)
hs : s ∈ C
⊢ Eq (α := ℝ≥0∞)
    ((inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯ ⋯ :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
Eq.trans ?_ ((m.extend hC).ofFunction_eq hC ?_ ?_ hs)

Premises used: MeasureTheory.AddContent.ofFunction_eq, MeasureTheory.AddContent.extend, Eq.trans
-- 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)
hs : s ∈ C
refine_1 :
  Eq (α := ℝ≥0∞)
    ((inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯ ⋯ :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑(AddContent.extend (C := C) hC m) : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
refine_2 : (AddContent.extend (C := C) hC m).IsSigmaSubadditive (C := C)
refine_3 : ∀ s ∉ C, Eq (α := ℝ≥0∞) ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯ ⋯ :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine Eq.trans ?_ ((m.extend hC).ofFunction_eq hC ?_ ?_ hs)

Premises used: MeasureTheory.AddContent.ofFunction_eq, MeasureTheory.AddContent.extend, Eq.trans
-- 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)
hs : s ∈ C
⊢ Eq (α := ℝ≥0∞)
    ((inducedOuterMeasure (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ⋯ ⋯ :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((OuterMeasure.ofFunction (⇑(AddContent.extend (C := C) hC m) : (a : Set α) → ℝ≥0∞) ⋯ : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
congr
-- 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)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ (i : ℕ), f i ∈ C
refine_2 :
  LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
rw [m.extend_eq hC hf_mem]

Premises used: MeasureTheory.AddContent.extend_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)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ (i : ℕ), f i ∈ C
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
(m_sigma_subadd hf hf_mem).trans_eq ?_

Premises used: LE.le.trans_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)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ (i : ℕ), f i ∈ C
refine_2 :
  Eq (α := ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i))
    (∑' (i : ℕ), (AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) (f i))
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
refine (m_sigma_subadd hf hf_mem).trans_eq ?_

Premises used: LE.le.trans_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)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ (i : ℕ), f i ∈ C
refine_2 :
  ∀ (i : ℕ),
    Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
      ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i))
    (∑' (i : ℕ), (AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) (f i))

Tactic:
congr with i
-- 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)
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ (i : ℕ), f i ∈ C
i : ℕ
refine_2 refine_2₁ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
rw [m.extend_eq hC (hf i)]

Premises used: MeasureTheory.AddContent.extend_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)
hs : s ∈ C
⊢ ∀ s ∉ C, Eq (α := ℝ≥0∞) ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
fun _ ↦ m.extend_eq_top _

Premises used: MeasureTheory.AddContent.extend_eq_top
-- 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)
hs : s ∈ C
⊢ ∀ s ∉ C, Eq (α := ℝ≥0∞) ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact fun _ ↦ m.extend_eq_top _

Premises used: MeasureTheory.AddContent.extend_eq_top