awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
h :
  ∀ (t : Set α),
    P t →
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
          ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t
u : Set α
mpr :
  ∀ (i : Set α),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
        ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
      ⨅ (ht : P i), ⨅ (_ : u ⊆ i), m i ht
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : u ⊆ t), m t ht

Tactic:
refine le_iInf ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
h :
  ∀ (t : Set α),
    P t →
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
          ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t
u t : Set α
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    ⨅ (ht : P t), ⨅ (_ : u ⊆ t), m t ht

Tactic:
le_iInf ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
h :
  ∀ (t : Set α),
    P t →
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
          ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t
u t : Set α
mpr :
  ∀ (i : P t),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
        ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
      ⨅ (_ : u ⊆ t), m t i
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    ⨅ (ht : P t), ⨅ (_ : u ⊆ t), m t ht

Tactic:
refine le_iInf ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
h :
  ∀ (t : Set α),
    P t →
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
          ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t
u t : Set α
ht : P t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    ⨅ (_ : u ⊆ t), m t ht

Tactic:
le_iInf ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
h :
  ∀ (t : Set α),
    P t →
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
          ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t
u t : Set α
ht : P t
mpr :
  ∀ (i : u ⊆ t),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
        ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
      m t ht
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    ⨅ (_ : u ⊆ t), m t ht

Tactic:
refine le_iInf ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
h :
  ∀ (t : Set α),
    P t →
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
          ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t
u t : Set α
ht : P t
h2t : u ⊆ t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    m t ht

Tactic:
le_trans ?_ ((h t ht).trans_eq <| inducedOuterMeasure_eq' _ msU m_mono ht)

Premises used: LE.le.trans_eq, MeasureTheory.inducedOuterMeasure_eq', le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
h :
  ∀ (t : Set α),
    P t →
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
          ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t
u t : Set α
ht : P t
h2t : u ⊆ t
mpr :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    m t ht

Tactic:
refine le_trans ?_ ((h t ht).trans_eq <| inducedOuterMeasure_eq' _ msU m_mono ht)

Premises used: LE.le.trans_eq, MeasureTheory.inducedOuterMeasure_eq', le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
h :
  ∀ (t : Set α),
    P t →
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
          ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t
u t : Set α
ht : P t
h2t : u ⊆ t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
⊢ extend (P := MeasurableSet) m s₁ ≤ extend (P := MeasurableSet) m s₂

Tactic:
le_iInf ?_

Premises used: MeasureTheory.extend, le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
refine : ∀ (i : MeasurableSet s₂), extend (P := MeasurableSet) m s₁ ≤ m s₂ i
⊢ extend (P := MeasurableSet) m s₁ ≤ extend (P := MeasurableSet) m s₂

Tactic:
refine le_iInf ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
⊢ extend (P := MeasurableSet) m (s₁ ∪ s₂ \ s₁) =
    extend (P := MeasurableSet) m s₁ + extend (P := MeasurableSet) m (s₂ \ s₁)

Tactic:
have :=
    extend_union MeasurableSet.empty m0 MeasurableSet.iUnion mU disjoint_sdiff_self_right h₁
      (h₂.diff h₁)
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
this :
  extend (P := MeasurableSet) m (s₁ ∪ s₂ \ s₁) =
    extend (P := MeasurableSet) m s₁ + extend (P := MeasurableSet) m (s₂ \ s₁)
⊢ extend (P := MeasurableSet) m s₂ = extend (P := MeasurableSet) m s₁ + extend (P := MeasurableSet) m (s₂ \ s₁)

Tactic:
rw [union_diff_cancel hs] at this

Premises used: Set.union_diff_cancel
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
this : extend (P := MeasurableSet) m s₂ = extend (P := MeasurableSet) m s₁ + extend (P := MeasurableSet) m (s₂ \ s₁)
rw : extend (P := MeasurableSet) m s₁ ≤ extend (P := MeasurableSet) m s₂
⊢ extend (P := MeasurableSet) m s₁ ≤ m s₂ h₂

Tactic:
rw [← extend_eq m]

Premises used: MeasureTheory.extend_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
this : extend (P := MeasurableSet) m s₂ = extend (P := MeasurableSet) m s₁ + extend (P := MeasurableSet) m (s₂ \ s₁)
⊢ extend (P := MeasurableSet) m s₁ ≤ extend (P := MeasurableSet) m s₂

Tactic:
le_iff_exists_add.2 ⟨_, this⟩

Premises used: Iff.mpr, le_iff_exists_add, Exists.intro
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
this : extend (P := MeasurableSet) m s₂ = extend (P := MeasurableSet) m s₁ + extend (P := MeasurableSet) m (s₂ \ s₁)
⊢ extend (P := MeasurableSet) m s₁ ≤ extend (P := MeasurableSet) m s₂

Tactic:
exact le_iff_exists_add.2 ⟨_, this⟩

Premises used: Iff.mpr, le_iff_exists_add, Exists.intro
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
⊢ ∀ (s : ℕ → Set α), extend (P := MeasurableSet) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := MeasurableSet) m (s i)

Tactic:
extend_iUnion_le_tsum_nat' MeasurableSet.iUnion ?_

Premises used: MeasureTheory.extend_iUnion_le_tsum_nat', MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
refine : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
⊢ ∀ (s : ℕ → Set α), extend (P := MeasurableSet) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := MeasurableSet) m (s i)

Tactic:
refine extend_iUnion_le_tsum_nat' MeasurableSet.iUnion ?_

Premises used: MeasureTheory.extend_iUnion_le_tsum_nat', MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
simp : m (⋃ (i : ℕ), disjointed f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
⊢ m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯

Tactic:
simp +singlePass only [iUnion_disjointed.symm]

Premises used: iUnion_disjointed, Eq.symm
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
rw : LE.le (α := ℝ≥0∞) (∑' (i : ℕ), m (disjointed f i) ⋯) (∑' (i : ℕ), m (f i) ⋯)
⊢ m (⋃ (i : ℕ), disjointed f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯

Tactic:
rw [mU (MeasurableSet.disjointed h) (disjoint_disjointed _)]

Premises used: MeasurableSet.disjointed, disjoint_disjointed
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), m (disjointed f i) ⋯) (∑' (i : ℕ), m (f i) ⋯)

Tactic:
ENNReal.tsum_le_tsum fun i => ?_

Premises used: ENNReal.tsum_le_tsum
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
refine : ∀ (i : ℕ), m (disjointed f i) ⋯ ≤ m (f i) ⋯
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), m (disjointed f i) ⋯) (∑' (i : ℕ), m (f i) ⋯)

Tactic:
refine ENNReal.tsum_le_tsum fun i => ?_

Premises used: ENNReal.tsum_le_tsum
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
i : ℕ
rw : extend (P := MeasurableSet) m (disjointed f i) ≤ extend (P := MeasurableSet) m (f i)
⊢ m (disjointed f i) ⋯ ≤ m (f i) ⋯

Tactic:
rw [← extend_eq m, ← extend_eq m]

Premises used: MeasureTheory.extend_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
i : ℕ
⊢ extend (P := MeasurableSet) m (disjointed f i) ≤ extend (P := MeasurableSet) m (f i)

Tactic:
extend_mono m0 mU (MeasurableSet.disjointed h _) (disjointed_le f _)

Premises used: MeasureTheory.extend_mono, disjointed_le, MeasurableSet.disjointed
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
i : ℕ
⊢ extend (P := MeasurableSet) m (disjointed f i) ≤ extend (P := MeasurableSet) m (f i)

Tactic:
exact extend_mono m0 mU (MeasurableSet.disjointed h _) (disjointed_le f _)

Premises used: MeasureTheory.extend_mono, disjointed_le, MeasurableSet.disjointed
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s : Set α
hs : MeasurableSet s
⊢ (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) s = extend (P := MeasurableSet) m s

Tactic:
ofFunction_eq s (fun _t => extend_mono m0 mU hs) (extend_iUnion_le_tsum_nat m0 mU)

Premises used: MeasureTheory.extend_iUnion_le_tsum_nat, MeasureTheory.extend_mono, MeasureTheory.OuterMeasure.ofFunction_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s : Set α
hs : MeasurableSet s
⊢ (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) s = m s hs

Tactic:
(inducedOuterMeasure_eq_extend m0 mU hs).trans <| extend_eq _ _

Premises used: MeasureTheory.inducedOuterMeasure_eq_extend, MeasureTheory.extend_eq, Eq.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m₁ m₂ : OuterMeasure α
⊢ m₁ ≤ m₂.trim ↔
    ∀ (s : Set α),
      MeasurableSet s → LE.le (α := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
le_inducedOuterMeasure

Premises used: MeasureTheory.le_inducedOuterMeasure
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
⊢ m ≤ m.trim

Tactic:
le_trim_iff.2 fun _ _ ↦ le_rfl

Premises used: Iff.mpr, le_rfl, MeasureTheory.OuterMeasure.le_trim_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
h : Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
nonpos_iff_eq_zero.1 <| (le_trim m s).trans_eq h

Premises used: LE.le.trans_eq, MeasureTheory.OuterMeasure.le_trim, Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
inducedOuterMeasure_eq' MeasurableSet.iUnion (fun f _hf => measure_iUnion_le f)
    (fun _ _ _ _ h => measure_mono h) hs

Premises used: MeasureTheory.inducedOuterMeasure_eq', MeasureTheory.measure_mono, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m₁ m₂ : OuterMeasure α
H :
  ∀ {s : Set α},
    MeasurableSet s → Eq (α := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ m₁.trim = m₂.trim

Tactic:
simp +contextual only [trim, H]

Premises used: MeasureTheory.OuterMeasure.trim
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Monotone.{u_1, u_1} (α := OuterMeasure α) trim

Tactic:
fun _m₁ _m₂ H _s =>
  iInf₂_mono fun _f _hs => ENNReal.tsum_le_tsum fun _b => iInf_mono fun _hf => H _

Premises used: iInf, ENNReal.tsum_le_tsum, Monotone, iInf_mono, iInf₂_mono, ite
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
simp :
  ∀ (s : Set α),
    MeasurableSet s → LE.le (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ m.trim ≤ m.trim

Tactic:
simp only [le_trim_iff]

Premises used: MeasureTheory.OuterMeasure.le_trim_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
s : Set α
hs : MeasurableSet s
rw rw₁ : LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [trim_eq _ (h s hs)]

Premises used: MeasureTheory.OuterMeasure.trim_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m₁ m₂ : OuterMeasure α
s : Set α
hs : MeasurableSet s
rw rw₁ :
  LE.le (α := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ↔
    LE.le (α := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((m₁.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ↔
    LE.le (α := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [trim_eq _ hs]

Premises used: MeasureTheory.OuterMeasure.trim_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m₁ m₂ : OuterMeasure α
⊢ m₁.trim = m₂.trim ↔
    ∀ (s : Set α),
      MeasurableSet s → Eq (α := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [le_antisymm_iff, trim_le_trim_iff, forall_and]

Premises used: MeasureTheory.OuterMeasure.trim_le_trim_iff, le_antisymm_iff, forall_and