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₂
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 α
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)
⊢ 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:
refine f.injective.preimage_surjective.iInf_congr (preimage f) fun s => ?_

Premises used: Function.Injective.preimage_surjective, Set.preimage, Function.Surjective.iInf_congr, Equiv.injective, DFunLike.coe
-- 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₂
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)

Tactic:
iInf_congr_Prop (Pm s) ?_

Premises used: iInf_congr_Prop
-- 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₂
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 α
refine :
  ∀ (x : P s),
    Eq (α := ℝ≥0∞)
      (⨅ (_ : Subset (α := Set α) ((⇑f : (a : α) → α) ⁻¹' A) ((⇑f : (a : α) → α) ⁻¹' s)),
        m ((⇑f : (a : α) → α) ⁻¹' s) ⋯)
      (⨅ (_ : A ⊆ s), m s x)
⊢ 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 iInf_congr_Prop (Pm s) ?_

Premises used: iInf_congr_Prop
-- 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₂
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)

Tactic:
iInf_congr_Prop f.surjective.preimage_subset_preimage_iff ?_

Premises used: Function.Surjective.preimage_subset_preimage_iff, iInf_congr_Prop, Equiv.surjective
-- 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₂
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
refine : ∀ (x : A ⊆ s), m ((⇑f : (a : α) → α) ⁻¹' s) ⋯ = m s hs
⊢ Eq (α := ℝ≥0∞)
    (⨅ (_ : Subset (α := Set α) ((⇑f : (a : α) → α) ⁻¹' A) ((⇑f : (a : α) → α) ⁻¹' s)), m ((⇑f : (a : α) → α) ⁻¹' s) ⋯)
    (⨅ (_ : A ⊆ s), m s hs)

Tactic:
refine iInf_congr_Prop f.surjective.preimage_subset_preimage_iff ?_

Premises used: Function.Surjective.preimage_subset_preimage_iff, iInf_congr_Prop, Equiv.surjective
-- 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₂
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
h : A ⊆ s
⊢ m ((⇑f : (a : α) → α) ⁻¹' s) ⋯ = m s hs

Tactic:
mm s hs
-- 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₂
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
h : A ⊆ s
⊢ m ((⇑f : (a : α) → α) ⁻¹' s) ⋯ = m s hs

Tactic:
exact mm s hs
-- 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 α
hs : Ne (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 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∞) ε

Tactic:
have h := ENNReal.lt_add_right hs hε
-- 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 α
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∞) ε
lhs : ((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∞) ε

Tactic:
lhs
-- 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 α
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∞) ε
rw : ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht
| ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [inducedOuterMeasure_eq_iInf _ msU m_mono]

Premises used: MeasureTheory.inducedOuterMeasure_eq_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 α
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∞) ε
rw : ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht
| (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:
lhs
    rw [inducedOuterMeasure_eq_iInf _ msU m_mono]

Premises used: MeasureTheory.inducedOuterMeasure_eq_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 α
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 α), ⨅ (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]

Premises used: MeasureTheory.inducedOuterMeasure_eq_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 α
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∞) ε
⊢ ∃ (i : Set α) (h : P i) (_ : s ⊆ i),
    m i ⋯ < HAdd.hAdd (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε

Tactic:
simp only [iInf_lt_iff] at h

Premises used: iInf_lt_iff
-- 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 α
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∞) ε
rcases :
  ∀ (t : Set α) (h1t : P t) (h2t : s ⊆ t)
    (h3t : m t ⋯ < 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∞) ε
⊢ ∃ (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⟩
-- 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 α
hs : Ne (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
h1t : P t
h2t : s ⊆ t
h3t : m t ⋯ < 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:
⟨t, h1t, h2t, le_trans (le_of_eq <| inducedOuterMeasure_eq' _ msU m_mono h1t) (le_of_lt h3t)⟩

Premises used: MeasureTheory.inducedOuterMeasure_eq', le_of_lt, And.intro, Exists.intro, le_of_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 α
hs : Ne (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
h1t : P t
h2t : s ⊆ t
h3t : m t ⋯ < 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:
exact
    ⟨t, h1t, h2t, le_trans (le_of_eq <| inducedOuterMeasure_eq' _ msU m_mono h1t) (le_of_lt h3t)⟩
-- 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 α
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
⊢ 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

Tactic:
rw [isCaratheodory_iff_le]

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_iff_le
-- 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 α
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
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
⊢ (∀ (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
-- 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 α),
    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 α
_ht : 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:
h t
-- 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 α),
    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 α
_ht : 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:
exact h t
-- 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 α
rw : ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : u ⊆ t), m t ht
| ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
rw [inducedOuterMeasure_eq_iInf _ msU m_mono]

Premises used: MeasureTheory.inducedOuterMeasure_eq_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 : Set α
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
⊢ 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

Tactic:
conv_rhs => rw [inducedOuterMeasure_eq_iInf _ msU m_mono]

Premises used: MeasureTheory.inducedOuterMeasure_eq_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 : 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

Tactic:
le_iInf ?_

Premises used: le_iInf