awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
Pu : P univ
⊢ inducedOuterMeasure (P := P) (fun (x : Set α) (x_1 : P x) ↦ 0) P0 ⋯ = 0
have h : ∀ (s : Set α),
  Eq (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) (fun (x : Set α) (x_1 : P x) ↦ 0) P0 sorry : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
Pu : P univ
s : Set α
⊢ Eq (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) (fun (x : Set α) (x_1 : P x) ↦ 0) P0 ⋯ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (_ : P t), ⨅ (_ : s ⊆ t), 0 : ℝ≥0∞)
  (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [inducedOuterMeasure_eq_iInf PU (fun _ _ => by simp) (fun _ _ => by simp)]
-- 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₂
f : α ≃ α
Pm : ∀ (s : Set α), P ((⇑f : (a : α) → α) ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m ((⇑f : (a : α) → α) ⁻¹' s) ⋯ = m s hs
A : Set α
⊢ Eq (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → α) ⁻¹' A) : ℝ≥0∞)
    ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : (⇑f : (a : α) → α) ⁻¹' A ⊆ t), m t ht)
  (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : A ⊆ t), m t ht)
Tactic: rw [inducedOuterMeasure_eq_iInf _ msU m_mono, inducedOuterMeasure_eq_iInf _ msU m_mono]
-- 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₂
f : α ≃ α
Pm : ∀ (s : Set α), P ((⇑f : (a : α) → α) ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m ((⇑f : (a : α) → α) ⁻¹' s) ⋯ = m s hs
A : Set α
⊢ Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : (⇑f : (a : α) → α) ⁻¹' A ⊆ t), m t ht)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : A ⊆ t), m t ht)
have symm : Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : A ⊆ t), m t ht)
  (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : (⇑f : (a : α) → α) ⁻¹' A ⊆ t), m t ht)
Tactic: symm
-- 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₂
f : α ≃ α
Pm : ∀ (s : Set α), P ((⇑f : (a : α) → α) ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m ((⇑f : (a : α) → α) ⁻¹' s) ⋯ = m s hs
A : Set α
⊢ Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : A ⊆ t), m t ht)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : (⇑f : (a : α) → α) ⁻¹' A ⊆ t), m t ht)
have refine : ∀ (s : Set α),
  Eq (α := ℝ≥0∞)
    (⨅ (ht : P ((⇑f : (a : α) → α) ⁻¹' s)),
      ⨅ (_ : Subset (α := Set α) ((⇑f : (a : α) → α) ⁻¹' A) ((⇑f : (a : α) → α) ⁻¹' s)),
        m ((⇑f : (a : α) → α) ⁻¹' s) ht)
    (⨅ (ht : P s), ⨅ (_ : A ⊆ s), m s ht)
Tactic: refine f.injective.preimage_surjective.iInf_congr (preimage f) fun s => ?_
-- 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₂
f : α ≃ α
Pm : ∀ (s : Set α), P ((⇑f : (a : α) → α) ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m ((⇑f : (a : α) → α) ⁻¹' s) ⋯ = m s hs
A s : Set α
⊢ Eq (α := ℝ≥0∞)
    (⨅ (ht : P ((⇑f : (a : α) → α) ⁻¹' s)),
      ⨅ (_ : Subset (α := Set α) ((⇑f : (a : α) → α) ⁻¹' A) ((⇑f : (a : α) → α) ⁻¹' s)),
        m ((⇑f : (a : α) → α) ⁻¹' s) ht)
    (⨅ (ht : P s), ⨅ (_ : A ⊆ s), m s ht)
have refine : ∀ (x : P s),
  Eq (α := ℝ≥0∞)
    (⨅ (_ : Subset (α := Set α) ((⇑f : (a : α) → α) ⁻¹' A) ((⇑f : (a : α) → α) ⁻¹' s)), m ((⇑f : (a : α) → α) ⁻¹' s) sorry)
    (⨅ (_ : A ⊆ s), m s x)
Tactic: refine iInf_congr_Prop (Pm s) ?_
-- 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₂
f : α ≃ α
Pm : ∀ (s : Set α), P ((⇑f : (a : α) → α) ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m ((⇑f : (a : α) → α) ⁻¹' s) ⋯ = m s hs
A s : Set α
hs : P s
⊢ Eq (α := ℝ≥0∞)
    (⨅ (_ : Subset (α := Set α) ((⇑f : (a : α) → α) ⁻¹' A) ((⇑f : (a : α) → α) ⁻¹' s)), m ((⇑f : (a : α) → α) ⁻¹' s) ⋯)
    (⨅ (_ : A ⊆ s), m s hs)
have refine : ∀ (x : A ⊆ s), m ((⇑f : (a : α) → α) ⁻¹' s) sorry = m s hs
Tactic: refine iInf_congr_Prop f.surjective.preimage_subset_preimage_iff ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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 α
hs : Ne (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ (t : Set α),
    P t ∧
      s ⊆ t ∧
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t ≤
          HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
have h : (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s <
  HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
Tactic: have h := ENNReal.lt_add_right hs 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)
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 α
hs : Ne (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
h :
  (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s <
    HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
| (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s <
    HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
have lhs : ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: lhs
-- 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 α
hs : Ne (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
h :
  (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s <
    HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
| ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht
Tactic: rw [inducedOuterMeasure_eq_iInf _ msU m_mono]
-- 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 α
hs : Ne (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
h :
  (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s <
    HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
| (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s <
    HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
have rw : ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht
Tactic: lhs
    rw [inducedOuterMeasure_eq_iInf _ msU m_mono]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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 α
hs : Ne (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
h :
  (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s <
    HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
⊢ ∃ (t : Set α),
    P t ∧
      s ⊆ t ∧
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t ≤
          HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
have h₁ : ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht <
  HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
Tactic: conv at h =>
    lhs
    rw [inducedOuterMeasure_eq_iInf _ msU m_mono]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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 α
hs : Ne (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
h :
  ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht <
    HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
⊢ ∃ (t : Set α),
    P t ∧
      s ⊆ t ∧
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t ≤
          HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
have h₁ : ∃ (i : Set α) (h : P i) (_ : s ⊆ i),
  m i sorry < HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
Tactic: simp only [iInf_lt_iff] at 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∞
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 α
hs : Ne (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
h :
  ∃ (i : Set α) (h : P i) (_ : s ⊆ i),
    m i ⋯ < HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
⊢ ∃ (t : Set α),
    P t ∧
      s ⊆ t ∧
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t ≤
          HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
have rcases : ∀ (t : Set α) (h1t : P t) (h2t : s ⊆ t)
  (h3t : m t sorry < HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε),
  ∃ (t : Set α),
    P t ∧
      s ⊆ t ∧
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t ≤
          HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
Tactic: rcases h with ⟨t, h1t, h2t, h3t⟩
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∞
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 α
⊢ MeasurableSet s ↔
    ∀ (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
have rw : (∀ (t : Set α),
    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) ↔
  ∀ (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
Tactic: rw [isCaratheodory_iff_le]
-- 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 α
⊢ (∀ (t : Set α),
      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) ↔
    ∀ (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
have mp : (∀ (t : Set α),
    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) →
  ∀ (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
Tactic: constructor
-- 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 α
mp :
  (∀ (t : Set α),
      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) →
    ∀ (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
⊢ (∀ (t : Set α),
      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) ↔
    ∀ (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
have mpr : (∀ (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) →
  ∀ (t : Set α),
    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
Tactic: constructor
-- 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 α
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 α
| ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
have rw : ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : u ⊆ t), m t ht
Tactic: rw [inducedOuterMeasure_eq_iInf _ msU m_mono]
-- 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 α
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 α
⊢ 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∞) ≤
    (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) u
have 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∞) ≤
  ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : u ⊆ t), m t ht
Tactic: conv_rhs => rw [inducedOuterMeasure_eq_iInf _ msU m_mono]
-- 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 α
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 α
⊢ 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
have 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
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 α
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
have 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
Tactic: refine le_iInf ?_