awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ t \ s ⊆ (⋃ (i : ℕ), f i) \ s

Tactic:
diff_subset_diff_left hf

Premises used: Set.diff_subset_diff_left
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ t \ s ⊆ (⋃ (i : ℕ), f i) \ s

Tactic:
exact diff_subset_diff_left hf

Premises used: Set.diff_subset_diff_left
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
refine_3 :
  LE.le (α := ℝ≥0∞) (∑' (a : ℕ), (m ((fun (i : ℕ) ↦ f i ∩ s) a) + m ((fun (i : ℕ) ↦ f i \ s) a))) (∑' (i : ℕ), m (f i))
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), m ((fun (i : ℕ) ↦ f i ∩ s) i)) (∑' (i : ℕ), m ((fun (i : ℕ) ↦ f i \ s) i)) ≤
    ∑' (i : ℕ), m (f i)

Tactic:
rw [← ENNReal.tsum_add]

Premises used: ENNReal.tsum_add
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ LE.le (α := ℝ≥0∞) (∑' (a : ℕ), (m ((fun (i : ℕ) ↦ f i ∩ s) a) + m ((fun (i : ℕ) ↦ f i \ s) a))) (∑' (i : ℕ), m (f i))

Tactic:
ENNReal.tsum_le_tsum fun i => hs _

Premises used: ENNReal.tsum_le_tsum
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ LE.le (α := ℝ≥0∞) (∑' (a : ℕ), (m ((fun (i : ℕ) ↦ f i ∩ s) a) + m ((fun (i : ℕ) ↦ f i \ s) a))) (∑' (i : ℕ), m (f i))

Tactic:
exact ENNReal.tsum_le_tsum fun i => hs _

Premises used: ENNReal.tsum_le_tsum
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
hs₁ :
  ∀ (t : Set α),
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤
      ⨆ (_ : t.Nonempty), m t
⊢ MeasurableSet s

Tactic:
apply ofFunction_caratheodory

Premises used: MeasureTheory.OuterMeasure.ofFunction_caratheodory
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
hs₁ :
  HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (∅ ∩ s).Nonempty), m (∅ ∩ s)) (⨆ (_ : (∅ \ s).Nonempty), m (∅ \ s)) ≤
    ⨆ (_ : Set.Nonempty.{u_1} (α := α) ∅), m ∅
hs₂ :
  ∀ (h : t.Nonempty),
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤
      ⨆ (_ : t.Nonempty), m t
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤
    ⨆ (_ : t.Nonempty), m t

Tactic:
rcases t.eq_empty_or_nonempty with rfl | h

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (∅ ∩ s).Nonempty), m (∅ ∩ s)) (⨆ (_ : (∅ \ s).Nonempty), m (∅ \ s)) ≤
    ⨆ (_ : Set.Nonempty.{u_1} (α := α) ∅), m ∅

Tactic:
simp [Set.not_nonempty_empty]

Premises used: Set.not_nonempty_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤ m t

Tactic:
le_trans _ (hs t)

Premises used: le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
h₁ : ⨆ (_ : t.Nonempty), m t = m t
hs₁ :
  HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤
    m (t ∩ s) + m (t \ s)
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤
    ⨆ (_ : t.Nonempty), m t

Tactic:
convert! le_trans _ (hs t)

Premises used: le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), m t = m t

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤
    m (t ∩ s) + m (t \ s)

Tactic:
add_le_add iSup_const_le iSup_const_le

Premises used: add_le_add, iSup_const_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤
    m (t ∩ s) + m (t \ s)

Tactic:
exact add_le_add iSup_const_le iSup_const_le

Premises used: add_le_add, iSup_const_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := MeasurableSpace α) (OuterMeasure.caratheodory 0) ⊤

Tactic:
top_unique fun _ _ _ => (add_zero _).symm

Premises used: top_unique, add_zero, OfNat.ofNat, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
s : Set α
h : MeasurableSet s
t : Set α
ht : t = ∅
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t

Tactic:
simp [ht]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
s : Set α
h : MeasurableSet s
t : Set α
ht : t.Nonempty
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t

Tactic:
simp only [ht, top_apply, le_top]

Premises used: le_top, MeasureTheory.OuterMeasure.top_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
hs₁ :
  Membership.mem (γ := Set (Set α))
    ((fun (m : MeasurableSpace α) ↦ ({t : Set α | MeasurableSet t} : Set (Set α))) m₁.caratheodory) s
hs₂ :
  Membership.mem (γ := Set (Set α))
    ((fun (m : MeasurableSpace α) ↦ ({t : Set α | MeasurableSet t} : Set (Set α))) m₂.caratheodory) s
⊢ (m₁ + m₂ : (a : Set α) → ℝ≥0∞) t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m₁ + m₂ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((m₁ + m₂ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
simp [hs₁ t, hs₂ t, add_left_comm, add_assoc]

Premises used: add_left_comm, add_assoc
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ (sum m : (a : Set α) → ℝ≥0∞) t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((sum m : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((sum m : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
simp [fun i => MeasurableSpace.measurableSet_iInf.1 h i t, ENNReal.tsum_add]

Premises used: MeasurableSpace.measurableSet_iInf, ENNReal.tsum_add, Iff.mp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
rw :
  a *
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        ((m : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) a ((m : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) +
      HMul.hMul (β := ℝ≥0∞) a ((m : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) a ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) a ((m : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) +
      HMul.hMul (β := ℝ≥0∞) a ((m : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
rw [(isCaratheodory_iff m).mp h t]

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a *
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        ((m : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) a ((m : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) +
      HMul.hMul (β := ℝ≥0∞) a ((m : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
a : α
s : Set α
h : MeasurableSet s
t : Set α
pos :
  ∀ (ht : a ∈ t),
    (dirac a : (a : Set α) → ℝ≥0∞) t =
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((dirac a : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        ((dirac a : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
neg :
  ∀ (ht : a ∉ t),
    (dirac a : (a : Set α) → ℝ≥0∞) t =
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((dirac a : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        ((dirac a : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
⊢ (dirac a : (a : Set α) → ℝ≥0∞) t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((dirac a : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((dirac a : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
by_cases ht : a ∈ t
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
a : α
s : Set α
h : MeasurableSet s
t : Set α
ht : a ∉ t
⊢ (dirac a : (a : Set α) → ℝ≥0∞) t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((dirac a : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((dirac a : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
simp [ht]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
a : α
s : Set α
h : MeasurableSet s
t : Set α
ht : a ∈ t
pos :
  ∀ (hs : a ∈ s),
    (dirac a : (a : Set α) → ℝ≥0∞) t =
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((dirac a : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        ((dirac a : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
neg :
  ∀ (hs : a ∉ s),
    (dirac a : (a : Set α) → ℝ≥0∞) t =
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((dirac a : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        ((dirac a : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
⊢ (dirac a : (a : Set α) → ℝ≥0∞) t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((dirac a : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((dirac a : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
by_cases hs : a ∈ s
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
a : α
s : Set α
h : MeasurableSet s
t : Set α
ht : a ∈ t
hs : a ∈ s
⊢ (dirac a : (a : Set α) → ℝ≥0∞) t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((dirac a : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((dirac a : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
a : α
s : Set α
h : MeasurableSet s
t : Set α
ht : a ∈ t
hs : a ∉ s
⊢ (dirac a : (a : Set α) → ℝ≥0∞) t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((dirac a : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((dirac a : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Defs
Goal:
α : Type u_1
m : OuterMeasure α
⊢ m.measureOf = (⇑m : (a : Set α) → ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : P s
⊢ extend (P := P) m s = m s h

Tactic:
simp [extend, h]

Premises used: MeasureTheory.extend
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : ¬P s
⊢ extend (P := P) m s = ∞

Tactic:
simp [extend, h]

Premises used: MeasureTheory.extend
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
h : ∀ (s : α), (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
⊢ c • extend (P := P) m = extend (P := P) fun (s : α) (h : P s) ↦ c • m s h

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
pos : ∀ (h : P s), (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
neg : ∀ (h : ¬P s), (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
⊢ (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s

Tactic:
by_cases h : P s
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : P s
⊢ (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s

Tactic:
simp [extend, ENNReal.smul_top, *]

Premises used: MeasureTheory.extend, ENNReal.smul_top
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : ¬P s
⊢ (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s

Tactic:
simp [extend, ENNReal.smul_top, *]

Premises used: MeasureTheory.extend, ENNReal.smul_top
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
h h₁ : ∀ (s : α), (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
⊢ c • extend (P := P) m = extend (P := P) fun (s : α) (h : P s) ↦ c • m s h

Tactic:
classical
  ext s; by_cases h : P s <;> simp [extend, ENNReal.smul_top, *]

Premises used: MeasureTheory.extend, ENNReal.smul_top
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
h : ∀ (s : α), (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
⊢ c • extend (P := P) m = extend (P := P) fun (s : α) (h : P s) ↦ c • m s h

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
s : α
pos : ∀ (h : P s), (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
neg : ∀ (h : ¬P s), (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
⊢ (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s

Tactic:
by_cases h : P s
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
s : α
h : P s
⊢ (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s

Tactic:
simp [extend, *]

Premises used: MeasureTheory.extend
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
s : α
h : ¬P s
⊢ (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s

Tactic:
simp [extend, *]

Premises used: MeasureTheory.extend
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : P s
simp : ∀ (i : P s), m s h ≤ m s i
⊢ m s h ≤ extend (P := P) m s

Tactic:
simp only [extend, le_iInf_iff]

Premises used: MeasureTheory.extend, le_iInf_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h i : P s
⊢ m s h ≤ m s h

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
β : Type u_3
Pb : β → Prop
mb : (s : β) → Pb s → ℝ≥0∞
sa : α
sb : β
hP : P sa ↔ Pb sb
hm : ∀ (ha : P sa) (hb : Pb sb), m sa ha = mb sb hb
⊢ extend (P := P) m sa = extend (P := Pb) mb sb

Tactic:
iInf_congr_Prop hP fun _h => hm _ _

Premises used: Iff.mpr, MeasureTheory.extend, iInf_congr_Prop
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_3
P : α → Prop
⊢ Eq.{u_3 + 1} (α := (s : α) → ℝ≥0∞) (extend (P := P) fun (x : α) (x_1 : P x) ↦ ∞) ⊤

Tactic:
funext fun _ => iInf_eq_top.mpr fun _ => rfl

Premises used: Iff.mpr, iInf_eq_top, funext, rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
f : ℕ → Set α
hm : ∀ (i : ℕ), P (f i)
mU : m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
e_f : ∀ (i : ℕ), m (f i) ⋯ = extend (P := P) m (f i)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (f i) ⋯) (∑' (i : ℕ), extend (P := P) m (f i))

Tactic:
congr with i
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
f : ℕ → Set α
hm : ∀ (i : ℕ), P (f i)
mU : m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
i : ℕ
e_f : m (f i) ⋯ = m (f i) ⋯
e_f₁ : P (f i)
e_f₂ : m (f i) ⋯ = m (f i) ⋯
e_f₃ : P (f i)
⊢ m (f i) ⋯ = extend (P := P) m (f i)

Tactic:
rw [extend_eq]

Premises used: MeasureTheory.extend_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
⊢ extend (P := P) m ∅ = 0

Tactic:
(extend_eq _ P0).trans m0

Premises used: MeasureTheory.extend_eq, Eq.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥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) ⋯
s : ℕ → Set α
pos : ∀ (h : ∀ (i : ℕ), P (s i)), extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)
neg : ∀ (h : ∃ (i : ℕ), ¬P (s i)), extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)
⊢ extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)

Tactic:
by_cases! h : ∀ i, P (s i)
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥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) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
pos : m (⋃ (i : ℕ), s i) ⋯ ≤ ∑' (i : ℕ), m (s i) ⋯
rw : ℕ → ℝ≥0∞
rw₁ : Eq (α := ℕ → ℝ≥0∞) (fun (i : ℕ) ↦ extend (P := P) m (s i)) fun (i : ℕ) ↦ m (s i) ⋯
⊢ extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)

Tactic:
rw [extend_eq _ (PU h), congr_arg tsum _]

Premises used: congr_arg, tsum, MeasureTheory.extend_eq, SummationFilter.unconditional
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥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) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
⊢ m (⋃ (i : ℕ), s i) ⋯ ≤ ∑' (i : ℕ), m (s i) ⋯

Tactic:
apply msU h
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥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) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
h₁ : ∀ (i : ℕ), extend (P := P) m (s i) = m (s i) ⋯
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (i : ℕ) ↦ extend (P := P) m (s i)) fun (i : ℕ) ↦ m (s i) ⋯

Tactic:
funext i
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥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) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
i : ℕ
⊢ extend (P := P) m (s i) = m (s i) ⋯

Tactic:
apply extend_eq _ (h i)

Premises used: MeasureTheory.extend_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥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) ⋯
s : ℕ → Set α
h : ∃ (i : ℕ), ¬P (s i)
neg : ∀ (i : ℕ) (hi : ¬P (s i)), extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)
⊢ extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)

Tactic:
obtain ⟨i, hi⟩ := h
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥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) ⋯
s : ℕ → Set α
i : ℕ
hi : ¬P (s i)
⊢ extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)

Tactic:
le_trans (le_iInf fun h => hi.elim h) (ENNReal.le_tsum i)

Premises used: le_iInf, ENNReal.le_tsum, Not.elim, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥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) ⋯
s : ℕ → Set α
i : ℕ
hi : ¬P (s i)
⊢ extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)

Tactic:
exact le_trans (le_iInf fun h => hi.elim h) (ENNReal.le_tsum i)

Premises used: le_iInf, Not.elim, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
⊢ extend (P := P) m s₁ ≤ extend (P := P) m s₂

Tactic:
le_iInf ?_

Premises used: MeasureTheory.extend, le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
refine : ∀ (i : P s₂), extend (P := P) m s₁ ≤ m s₂ i
⊢ extend (P := P) m s₁ ≤ extend (P := P) m s₂

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∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
h₂ : P s₂
rw : m s₁ h₁ ≤ m s₂ h₂
⊢ extend (P := P) m s₁ ≤ m s₂ h₂

Tactic:
rw [extend_eq m h₁]

Premises used: MeasureTheory.extend_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
h₂ : P s₂
⊢ m s₁ h₁ ≤ m s₂ h₂

Tactic:
m_mono h₁ h₂ hs
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
h₂ : P s₂
⊢ m s₁ h₁ ≤ m s₂ h₂

Tactic:
exact m_mono h₁ h₂ hs