awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
this : μ (s i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
rcases :
  ∀ (t : ℕ → Set α) (ht : ⨅ (_ : s i ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)),
    ∃ (f : ℕ → Set α), s i ⊆ ⋃ (i : ℕ), f i ∧ ∑' (i : ℕ), m (f i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ ∃ (f : ℕ → Set α), s i ⊆ ⋃ (i : ℕ), f i ∧ ∑' (i : ℕ), m (f i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
rcases iInf_lt_iff.mp this with ⟨t, ht⟩

Premises used: iInf_lt_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
this : μ (s i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
t : ℕ → Set α
ht : ⨅ (_ : s i ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
exists : s i ⊆ ⋃ (i : ℕ), t i ∧ ∑' (i : ℕ), m (t i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ ∃ (f : ℕ → Set α), s i ⊆ ⋃ (i : ℕ), f i ∧ ∑' (i : ℕ), m (f i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
exists t
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
this : μ (s i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
t : ℕ → Set α
ht : ⨅ (_ : s i ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
contrapose! :
  ∀ (ht : ∀ (_ : s i ⊆ ⋃ (i : ℕ), t i), μ (s i) + (↑(ε' i) : ℝ≥0∞) ≤ ∑' (i : ℕ), m (t i)),
    μ (s i) + (↑(ε' i) : ℝ≥0∞) ≤ ⨅ (_ : s i ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)
⊢ s i ⊆ ⋃ (i : ℕ), t i ∧ ∑' (i : ℕ), m (t i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
contrapose! ht
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
this : μ (s i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
t : ℕ → Set α
ht : ∀ (_ : s i ⊆ ⋃ (i : ℕ), t i), μ (s i) + (↑(ε' i) : ℝ≥0∞) ≤ ∑' (i : ℕ), m (t i)
⊢ μ (s i) + (↑(ε' i) : ℝ≥0∞) ≤ ⨅ (_ : s i ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)

Tactic:
le_iInf ht

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
i : ℕ
this : μ (s i) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
t : ℕ → Set α
ht : ∀ (_ : s i ⊆ ⋃ (i : ℕ), t i), μ (s i) + (↑(ε' i) : ℝ≥0∞) ≤ ∑' (i : ℕ), m (t i)
⊢ μ (s i) + (↑(ε' i) : ℝ≥0∞) ≤ ⨅ (_ : s i ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)

Tactic:
exact le_iInf ht

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
choose :
  ∀ (f : (i : ℕ) → ℕ → Set α)
    (hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)),
    μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ), (μ (s a) + (↑(ε' a) : ℝ≥0∞))
⊢ μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ), (μ (s a) + (↑(ε' a) : ℝ≥0∞))

Tactic:
choose f hf using
          show ∀ i, ∃ f : ℕ → Set α, (s i ⊆ ⋃ i, f i) ∧ (∑' i, m (f i)) < μ (s i) + ε' i by
            intro i
            have : μ (s i) < μ (s i) + ε' i :=
              ENNReal.lt_add_right (ne_top_of_le_ne_top hb.ne <| ENNReal.le_tsum _)
                (by simpa using (hε' i).ne')
            rcases iInf_lt_iff.mp this with ⟨t, ht⟩
            exists t
            contrapose! ht
            exact le_iInf ht
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ), (μ (s a) + (↑(ε' a) : ℝ≥0∞))

Tactic:
le_trans ?_ (ENNReal.tsum_le_tsum fun i => le_of_lt (hf i).2)

Premises used: ENNReal.tsum_le_tsum, le_of_lt, And.right, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
refine : μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ) (i : ℕ), m (f a i)
⊢ μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ), (μ (s a) + (↑(ε' a) : ℝ≥0∞))

Tactic:
refine le_trans ?_ (ENNReal.tsum_le_tsum fun i => le_of_lt (hf i).2)

Premises used: ENNReal.tsum_le_tsum, le_of_lt, And.right, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
rw :
  μ (⋃ (i : ℕ), s i) ≤
    ∑' (c : ℕ), m (f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) c).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) c).2)
⊢ μ (⋃ (i : ℕ), s i) ≤ ∑' (a : ℕ) (i : ℕ), m (f a i)

Tactic:
rw [← ENNReal.tsum_prod, ← Nat.pairEquiv.symm.tsum_eq]

Premises used: Equiv.tsum_eq, ENNReal.tsum_prod, Nat.pairEquiv, Equiv.symm
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ μ (⋃ (i : ℕ), s i) ≤
    ∑' (c : ℕ), m (f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) c).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) c).2)

Tactic:
iInf_le_of_le _ (iInf_le _ ?_)

Premises used: iInf_le_of_le, iInf_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
refine :
  Subset.{u_1} (α := Set α) (⋃ (i : ℕ), s i)
    (⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2)
⊢ μ (⋃ (i : ℕ), s i) ≤
    ∑' (c : ℕ), m (f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) c).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) c).2)

Tactic:
refine iInf_le_of_le _ (iInf_le _ ?_)

Premises used: iInf_le_of_le, iInf_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h_1 : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
h :
  ∀ (i : ℕ),
    s i ⊆ ⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2
⊢ Subset.{u_1} (α := Set α) (⋃ (i : ℕ), s i)
    (⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2)

Tactic:
apply iUnion_subset

Premises used: Set.iUnion_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h_1 : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
i : ℕ
h :
  Subset.{u_1} (α := Set α) (⋃ (i_1 : ℕ), f i i_1)
    (⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2)
⊢ s i ⊆ ⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2

Tactic:
apply Subset.trans (hf i).1

Premises used: Set.Subset.trans, And.left
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h_1 : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
i : ℕ
h :
  ∀ (i_1 : ℕ),
    f i i_1 ⊆ ⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2
⊢ Subset.{u_1} (α := Set α) (⋃ (i_1 : ℕ), f i i_1)
    (⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2)

Tactic:
apply iUnion_subset

Premises used: Set.iUnion_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h_1 : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
i : ℕ
h : ∀ (i_1 : ℕ), f i i_1 ⊆ ⋃ (i : ℕ), f (Nat.unpair i).1 (Nat.unpair i).2
⊢ ∀ (i_1 : ℕ),
    f i i_1 ⊆ ⋃ (i : ℕ), f ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).1 ((Nat.pairEquiv.symm : (a : ℕ) → ℕ × ℕ) i).2

Tactic:
simp only [Nat.pairEquiv_symm_apply]

Premises used: Nat.pairEquiv_symm_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : (s : Set α) → ℝ≥0∞ := fun (s : Set α) ↦ ⨅ (f : ℕ → Set α), ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
h : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), μ (s i)) ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
f : (i : ℕ) → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ (i_1 : ℕ), f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + (↑(ε' i) : ℝ≥0∞)
i j : ℕ
⊢ f i j ⊆ ⋃ (i : ℕ), ⋃ (j : ℕ), f i j

Tactic:
apply subset_iUnion₂ i

Premises used: Set.subset_iUnion₂
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
⊢ Eq (α := ℝ≥0∞) ((OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n) : ℝ≥0∞)

Tactic:
rfl

Premises used: iInf, rfl, ite
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
a :
  LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
    (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
a₁ :
  LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
⊢ Eq (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
    (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
h_1 : ∀ (i : ℕ), P (t i)
h : s ⊆ ⋃ (i : ℕ), t i
⊢ s ⊆ iUnion t

Tactic:
h
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
h_1 : ∀ (i : ℕ), P (t i)
h : s ⊆ ⋃ (i : ℕ), t i
⊢ s ⊆ iUnion t

Tactic:
exact h
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
    (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))

Tactic:
exact le_iInf fun t ↦ le_iInf fun _ ↦ le_iInf fun h ↦ iInf₂_le _ (by exact h)

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
a :
  ∀ (i : ℕ → Set α) (i_1 : s ⊆ iUnion i),
    LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
      (∑' (n : ℕ), m (i n))
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n))

Tactic:
simp_rw [le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ ∀ (i : ℕ → Set α) (i_1 : s ⊆ iUnion i),
    LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
      (∑' (n : ℕ), m (i n))

Tactic:
fun t ht_subset ↦ iInf_le_of_le t ?_

Premises used: iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
a :
  ∀ (t : ℕ → Set α) (ht_subset : s ⊆ iUnion t),
    LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
      (∑' (n : ℕ), m (t n))
⊢ ∀ (i : ℕ → Set α) (i_1 : s ⊆ iUnion i),
    LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
      (∑' (n : ℕ), m (i n))

Tactic:
refine fun t ht_subset ↦ iInf_le_of_le t ?_

Premises used: iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
pos :
  ∀ (ht : ∀ (i : ℕ), P (t i)),
    LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
      (∑' (n : ℕ), m (t n))
neg :
  ∀ (ht : ¬∀ (i : ℕ), P (t i)),
    LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
      (∑' (n : ℕ), m (t n))
⊢ LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)) (∑' (n : ℕ), m (t n))

Tactic:
by_cases ht : ∀ i, P (t i)
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ∀ (i : ℕ), P (t i)
⊢ LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)) (∑' (n : ℕ), m (t n))

Tactic:
iInf_le_of_le ht (iInf_le_of_le ht_subset le_rfl)

Premises used: le_rfl, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ∀ (i : ℕ), P (t i)
⊢ LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)) (∑' (n : ℕ), m (t n))

Tactic:
exact iInf_le_of_le ht (iInf_le_of_le ht_subset le_rfl)

Premises used: iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ¬∀ (i : ℕ), P (t i)
neg : Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (t i)) ∞
⊢ LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)) (∑' (n : ℕ), m (t n))

Tactic:
simp only [ht, not_false_eq_true, iInf_neg, top_le_iff]

Premises used: top_le_iff, iInf_neg, not_false_eq_true
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ¬∀ (i : ℕ), P (t i)
⊢ ∃ (i : ℕ), ¬P (t i)

Tactic:
push Not at ht

Premises used: Not
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ∃ (i : ℕ), ¬P (t i)
neg : ∀ (i : ℕ) (hti_notMem : ¬P (t i)), Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (t i)) ∞
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (t i)) ∞

Tactic:
obtain ⟨i, hti_notMem⟩ := ht
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
i : ℕ
hti_notMem : ¬P (t i)
⊢ m (t i) = ∞

Tactic:
have hfi_top : m (t i) = ∞ := m_top _ hti_notMem
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
i : ℕ
hti_notMem : ¬P (t i)
hfi_top : m (t i) = ∞
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (t i)) ∞

Tactic:
ENNReal.tsum_eq_top_of_eq_top ⟨i, hfi_top⟩

Premises used: ENNReal.tsum_eq_top_of_eq_top, Exists.intro
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
i : ℕ
hti_notMem : ¬P (t i)
hfi_top : m (t i) = ∞
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (t i)) ∞

Tactic:
exact ENNReal.tsum_eq_top_of_eq_top ⟨i, hfi_top⟩

Premises used: ENNReal.tsum_eq_top_of_eq_top, Exists.intro
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun (i : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ Set α) i s fun (x : ℕ) ↦ ∅
⊢ Ne (α := ℕ) 0 0 → m (f 0) = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun (i : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ Set α) i s fun (x : ℕ) ↦ ∅
i : ℕ
⊢ i + 1 ≠ 0 → m (f (i + 1)) = 0

Tactic:
simp [f, m_empty]
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t
m_subadd : ∀ (s : ℕ → Set α), m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), m (s i)
⊢ (OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s = m s

Tactic:
le_antisymm (ofFunction_le s) <|
    le_iInf fun f => le_iInf fun hf => le_trans (m_mono hf) (m_subadd f)

Premises used: le_iInf, le_antisymm, MeasureTheory.OuterMeasure.ofFunction_le, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : OuterMeasure α
⊢ μ ≤ OuterMeasure.ofFunction m m_empty ↔ ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s ≤ m s

Tactic:
⟨fun H s => le_trans (H s) (ofFunction_le s), fun H _ =>
    le_iInf fun f =>
      le_iInf fun hs =>
        le_trans (μ.mono hs) <| le_trans (measure_iUnion_le f) <| ENNReal.tsum_le_tsum fun _ => H _⟩

Premises used: ENNReal.tsum_le_tsum, MeasureTheory.OuterMeasure.mono, le_iInf, Iff.intro, MeasureTheory.OuterMeasure.ofFunction_le, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
⊢ IsGreatest {μ : OuterMeasure α | ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s ≤ m s} (OuterMeasure.ofFunction m m_empty)

Tactic:
⟨fun _ => ofFunction_le _, fun _ => le_ofFunction.2⟩

Premises used: Iff.mpr, IsGreatest, And.intro, MeasureTheory.OuterMeasure.ofFunction_le, MeasureTheory.OuterMeasure.le_ofFunction
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
⊢ OuterMeasure.ofFunction m m_empty = sSup {μ : OuterMeasure α | ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s ≤ m s}

Tactic:
(@isGreatest_ofFunction α m m_empty).isLUB.sSup_eq.symm

Premises used: IsLUB.sSup_eq, IsGreatest.isLUB, MeasureTheory.OuterMeasure.isGreatest_ofFunction, Eq.symm
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
⊢ (OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
le_antisymm (measure_union_le _ _) (le_iInf₂ fun f hf ↦ ?_)

Premises used: le_iInf₂, le_antisymm, MeasureTheory.measure_union_le