awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤
    ⨆ (_ : t.Nonempty), m t
have hs₁ : HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (∅ ∩ s).Nonempty), m (∅ ∩ s)) (⨆ (_ : (∅ \ s).Nonempty), m (∅ \ s)) ≤
  ⨆ (_ : Set.Nonempty.{u_1} (α := α) ∅), m ∅
Tactic: rcases t.eq_empty_or_nonempty with rfl | h
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
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 ∅
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤
    ⨆ (_ : t.Nonempty), m t
have hs₂ : ∀ (h : t.Nonempty),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
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)) ≤
    ⨆ (_ : t.Nonempty), m t
have h₁ : ⨆ (_ : t.Nonempty), m t = m t
Tactic: convert! le_trans _ (hs t)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
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
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤
    ⨆ (_ : t.Nonempty), m t
have hs₁ : HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤
  m (t ∩ s) + m (t \ s)
Tactic: convert! le_trans _ (hs t)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ 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∞)
have 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∞)
Tactic: rw [(isCaratheodory_iff m).mp h t]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u_1
a : α
s : Set α
h : MeasurableSet s
t : Set α
⊢ (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∞)
have 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∞)
Tactic: by_cases ht : a ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
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∞)
⊢ (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∞)
have 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∞)
Tactic: by_cases ht : a ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
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∞)
have 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∞)
Tactic: by_cases hs : a ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
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∞)
⊢ (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∞)
have 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∞)
Tactic: by_cases hs : a ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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
⊢ c • extend (P := P) m = extend (P := P) fun (s : α) (h : P s) ↦ c • m s h
have h : ∀ (s : α), (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
Tactic: ext s
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 : α
⊢ (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
have pos : ∀ (h : P 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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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
⊢ (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
have neg : ∀ (h : ¬P 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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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
⊢ c • extend (P := P) m = extend (P := P) fun (s : α) (h : P s) ↦ c • m s h
have h : ∀ (s : α), (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
Tactic: classical
  ext s; by_cases h : P s <;> simp [extend, ENNReal.smul_top, *]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
⊢ c • extend (P := P) m = extend (P := P) fun (s : α) (h : P s) ↦ c • m s h
have h : ∀ (s : α), (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
Tactic: ext s
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
s : α
⊢ (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
have pos : ∀ (h : P 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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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
⊢ (c • extend (P := P) m) s = extend (P := P) (fun (s : α) (h : P s) ↦ c • m s h) s
have neg : ∀ (h : ¬P 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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : P s
⊢ m s h ≤ extend (P := P) m s
have simp : ∀ (i : P s), m s h ≤ m s i
Tactic: simp only [extend, le_iInf_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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) ⋯
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (f i) ⋯) (∑' (i : ℕ), extend (P := P) m (f i))
have e_f : ∀ (i : ℕ), m (f i) sorry = extend (P := P) m (f i)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 : ℕ
⊢ m (f i) ⋯ = extend (P := P) m (f i)
have e_f : m (f i) sorry = m (f i) sorry
Tactic: rw [extend_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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) ⋯
⊢ m (f i) ⋯ = extend (P := P) m (f i)
have e_f₁ : P (f i)
Tactic: rw [extend_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 α
⊢ extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)
have pos : ∀ (h : ∀ (i : ℕ), P (s i)), extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)
Tactic: by_cases! h : ∀ i, P (s i)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
⊢ extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)
have neg : ∀ (h : ∃ (i : ℕ), ¬P (s i)), extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)
Tactic: by_cases! h : ∀ i, P (s i)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
⊢ extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)
have pos : m (⋃ (i : ℕ), s i) sorry ≤ ∑' (i : ℕ), m (s i) sorry
Tactic: rw [extend_eq _ (PU h), congr_arg tsum _]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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) ⋯
⊢ extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)
have rw : ℕ → ℝ≥0∞
Tactic: rw [extend_eq _ (PU h), congr_arg tsum _]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞
⊢ extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)
have rw₁ : Eq (α := ℕ → ℝ≥0∞) (fun (i : ℕ) ↦ extend (P := P) m (s i)) fun (i : ℕ) ↦ m (s i) sorry
Tactic: rw [extend_eq _ (PU h), congr_arg tsum _]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (i : ℕ) ↦ extend (P := P) m (s i)) fun (i : ℕ) ↦ m (s i) ⋯
have h₁ : ∀ (i : ℕ), extend (P := P) m (s i) = m (s i) sorry
Tactic: funext i
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
⊢ extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)
have neg : ∀ (i : ℕ) (hi : ¬P (s i)), extend (P := P) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := P) m (s i)
Tactic: obtain ⟨i, hi⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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₂
have refine : ∀ (i : P s₂), extend (P := P) m s₁ ≤ m s₂ i
Tactic: refine le_iInf ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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₂
⊢ extend (P := P) m s₁ ≤ m s₂ h₂
have rw : m s₁ h₁ ≤ m s₂ h₂
Tactic: rw [extend_eq m h₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
⊢ extend (P := P) m (⋃ (i : β), f i) = ∑' (i : β), extend (P := P) m (f i)
have intro : ∀ (val : Encodable β), extend (P := P) m (⋃ (i : β), f i) = ∑' (i : β), extend (P := P) m (f i)
Tactic: cases nonempty_encodable β
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val : Encodable β
⊢ extend (P := P) m (⋃ (i : β), f i) = ∑' (i : β), extend (P := P) m (f i)
have intro : extend (P := P) m (⋃ (i : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b) =
  ∑' (i : ℕ), extend (P := P) m (⋃ b ∈ Encodable.decode₂ β i, f b)
Tactic: rw [← Encodable.iUnion_decode₂, ← tsum_iUnion_decode₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val : Encodable β
intro :
  extend (P := P) m (⋃ (i : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b) =
    ∑' (i : ℕ), extend (P := P) m (⋃ b ∈ Encodable.decode₂ β i, f b)
⊢ extend (P := P) m (⋃ (i : β), f i) = ∑' (i : β), extend (P := P) m (f i)
have intro₁ : extend (P := P) m ∅ = 0
Tactic: rw [← Encodable.iUnion_decode₂, ← tsum_iUnion_decode₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
hd : Disjoint s₁ s₂
h₁ : P s₁
h₂ : P s₂
⊢ extend (P := P) m (s₁ ∪ s₂) = extend (P := P) m s₁ + extend (P := P) m s₂
have rw : ∑ b : Bool, extend (P := P) m (bif b then s₁ else s₂) = extend (P := P) m s₁ + extend (P := P) m s₂
Tactic: rw [union_eq_iUnion,
    extend_iUnion P0 m0 PU mU (pairwise_disjoint_on_bool.2 hd) (Bool.forall_bool.2 ⟨h₂, h₁⟩),
    tsum_fintype]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 α
⊢ Eq (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)
have a : LE.le (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 α
a :
  LE.le (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)
have a₁ : LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)
  ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 α
⊢ LE.le (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)
have a : ∀ (i : Set α) (i_1 : P i) (i_2 : s ⊆ i), (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s ≤ m i i_1
Tactic: simp only [le_iInf_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 t : Set α
ht : P t
hs : s ⊆ t
⊢ (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s ≤ m t ht
have a : (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t ≤ m t ht
Tactic: grw [hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 α
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)
    ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have a : ∀ (i : ℕ → Set α),
  LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht)
    (⨅ (_ : s ⊆ ⋃ (i_1 : ℕ), i i_1), ∑' (i_1 : ℕ), extend (P := P) m (i i_1))
Tactic: refine le_iInf ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 α
f : ℕ → Set α
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht)
    (⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), extend (P := P) m (f i))
have a : ∀ (i : s ⊆ ⋃ (i : ℕ), f i),
  LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht) (∑' (i : ℕ), extend (P := P) m (f i))
Tactic: refine le_iInf ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht) (∑' (i : ℕ), extend (P := P) m (f i))
have a : ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ extend (P := P) m (⋃ (i : ℕ), f i)
Tactic: refine le_trans ?_ (extend_iUnion_le_tsum_nat' _ msU _)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
⊢ ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ extend (P := P) m (⋃ (i : ℕ), f i)
have a : ∀ (i : P (⋃ (i : ℕ), f i)), ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ m (⋃ (i : ℕ), f i) i
Tactic: refine le_iInf ?_