awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s ⊆ t
hs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
hs.trans_le <| measure_mono h

Premises used: LT.lt.trans_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s ⊆ t
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
eq_top_mono (measure_mono h) hs

Premises used: eq_top_mono, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s ⊆ t
ht : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono h).trans_lt ht

Premises used: MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
h : s ⊆ t
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
hs.bot_lt.trans_le (measure_mono h)

Premises used: LT.lt.trans_le, MeasureTheory.measure_mono, Ne.bot_lt
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
inst_2 : Countable ι
s : ι → Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
    (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rel_iSup_tsum μ measure_empty (· ≤ ·) (fun t ↦ ?_) _

Premises used: MeasureTheory.measure_empty, LE.le, rel_iSup_tsum, DFunLike.coe, Set.iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
inst_2 : Countable ι
s : ι → Set α
refine :
  ∀ (t : ℕ → Set α),
    (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) ((μ : (a : Set α) → ℝ≥0∞) (⨆ (i : ℕ), t i))
      (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i))
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
    (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
refine rel_iSup_tsum μ measure_empty (· ≤ ·) (fun t ↦ ?_) _

Premises used: MeasureTheory.measure_empty, LE.le, rel_iSup_tsum, DFunLike.coe
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
inst_2 : Countable ι
s : ι → Set α
t : ℕ → Set α
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), t i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), t i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), disjointed t i) : ℝ≥0∞)

Tactic:
rw [iUnion_disjointed]

Premises used: iUnion_disjointed
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
inst_2 : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), disjointed t i) : ℝ≥0∞)
    (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (disjointed t i) : ℝ≥0∞)

Tactic:
OuterMeasureClass.measure_iUnion_nat_le _ _ (disjoint_disjointed _)

Premises used: disjoint_disjointed, MeasureTheory.OuterMeasureClass.measure_iUnion_nat_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
inst_2 : Countable ι
s : ι → Set α
t : ℕ → Set α
h : ∀ (i : ℕ), disjointed t i ⊆ t i
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (disjointed t i)) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i))

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
inst_2 : Countable ι
s : ι → Set α
t : ℕ → Set α
i : ℕ
⊢ disjointed t i ⊆ t i

Tactic:
disjointed_subset ..

Premises used: disjointed_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
inst_2 : Countable ι
s : ι → Set α
t : ℕ → Set α
i : ℕ
⊢ disjointed t i ⊆ t i

Tactic:
exact disjointed_subset ..

Premises used: disjointed_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
inst_2 : Countable ι
s : ι → Set α
t : ℕ → Set α
μ₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), t i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), disjointed t i) : ℝ≥0∞)
μ₂ :
  LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (disjointed t i)) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i))
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⨆ (i : ℕ), t i)) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i))

Tactic:
calc
    μ (⋃ i, t i) = μ (⋃ i, disjointed t i) := by rw [iUnion_disjointed]
    _ ≤ ∑' i, μ (disjointed t i) :=
      OuterMeasureClass.measure_iUnion_nat_le _ _ (disjoint_disjointed _)
    _ ≤ ∑' i, μ (t i) := by gcongr; exact disjointed_subset ..

Premises used: disjointed, disjoint_disjointed, MeasureTheory.OuterMeasureClass.measure_iUnion_nat_le, DFunLike.coe, Set.iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
⊢ Countable.{u_2 + 1} (↑I : Type u_2)

Tactic:
have := hI.to_subtype
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
this : Countable.{u_2 + 1} (↑I : Type u_2)
rw :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : (↑I : Type u_2)), s (↑x : ι)) : ℝ≥0∞)
    (∑' (i : (↑I : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞)
    (∑' (i : (↑I : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)) : ℝ≥0∞)

Tactic:
rw [biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
this : Countable.{u_2 + 1} (↑I : Type u_2)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : (↑I : Type u_2)), s (↑x : ι)) : ℝ≥0∞)
    (∑' (i : (↑I : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)) : ℝ≥0∞)

Tactic:
apply measure_iUnion_le

Premises used: MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
I : Finset ι
s : ι → Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
(measure_biUnion_le μ I.countable_toSet s).trans_eq <| I.tsum_subtype (μ <| s ·)

Premises used: MeasureTheory.measure_biUnion_le, LE.le.trans_eq, Finset.countable_toSet, DFunLike.coe, Finset.tsum_subtype
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
inst_2 : Fintype ι
μ : F
s : ι → Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (∑ i : ι, (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simpa using measure_biUnion_finset_le Finset.univ s

Premises used: Finset.univ, MeasureTheory.measure_biUnion_finset_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simpa [union_eq_iUnion] using measure_iUnion_fintype_le μ (cond · s t)

Premises used: cond, MeasureTheory.measure_iUnion_fintype_le, Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s : Set α
⊢ (μ : (a : Set α) → ℝ≥0∞) univ ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞)

Tactic:
s.union_compl_self ▸ measure_union_le s sᶜ

Premises used: Compl.compl, Eq.rec, Set.union_compl_self, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)

Tactic:
simpa using measure_union_le (s ∩ t) (s \ t)

Premises used: Inter.inter, SDiff.sdiff, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
bc : s ∩ t ⊆ t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s ∩ t ⊆ t

Tactic:
apply inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s \ t)

Tactic:
simp [ht]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
I : Set ι
hI : I.Countable
s : ι → Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ i ∈ I, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨fun h i hi ↦ measure_mono_null (subset_biUnion_of_mem hi) h, fun h ↦ ?_⟩

Premises used: Set.subset_biUnion_of_mem, MeasureTheory.measure_mono_null, Iff.intro
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
I : Set ι
hI : I.Countable
s : ι → Set α
refine :
  ∀ (h : ∀ i ∈ I, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ i ∈ I, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine ⟨fun h i hi ↦ measure_mono_null (subset_biUnion_of_mem hi) h, fun h ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
I : Set ι
hI : I.Countable
s : ι → Set α
h : ∀ i ∈ I, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Countable.{u_2 + 1} (↑I : Type u_2)

Tactic:
have _ := hI.to_subtype
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
I : Set ι
hI : I.Countable
s : ι → Set α
h : ∀ i ∈ I, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 : Countable.{u_2 + 1} (↑I : Type u_2)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [h] using measure_iUnion_le (μ := μ) fun x : I ↦ s x

Premises used: MeasureTheory.measure_iUnion_le, Subtype.val
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
S : Set (Set α)
hS : S.Countable
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ S, i) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ rw₂ :
  (∀ i ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ S) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [sUnion_eq_biUnion, measure_biUnion_null_iff hS]

Premises used: Set.sUnion_eq_biUnion, MeasureTheory.measure_biUnion_null_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
ι : Sort u_4
inst_2 : Countable ι
s : ι → Set α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ range s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ :
  (∀ s_1 ∈ range s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₂ rw₃ :
  (∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← sUnion_range, measure_sUnion_null_iff (countable_range s), forall_mem_range]

Premises used: Set.sUnion_range, Set.forall_mem_range, Set.countable_range, MeasureTheory.measure_sUnion_null_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [union_eq_iUnion, and_comm]

Premises used: and_comm, Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s t : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
μ : F
s : Set α
hs : s.Countable
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, {i}) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← measure_biUnion_null_iff hs, biUnion_of_singleton]

Premises used: Set.biUnion_of_singleton, MeasureTheory.measure_biUnion_null_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst_2 : l.NeBot
h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) ((⋃ (n : ι), s n) \ s k)) l (𝓝 0)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n) : ℝ≥0∞) (⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)

Tactic:
le_antisymm ?_ <| iSup_le fun n ↦ measure_mono <| subset_iUnion _ _

Premises used: Set.subset_iUnion, le_antisymm, MeasureTheory.measure_mono, iSup_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst_2 : l.NeBot
h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) ((⋃ (n : ι), s n) \ s k)) l (𝓝 0)
refine :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n) : ℝ≥0∞)
    (⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n) : ℝ≥0∞) (⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)

Tactic:
refine le_antisymm ?_ <| iSup_le fun n ↦ measure_mono <| subset_iUnion _ _

Premises used: Set.subset_iUnion, le_antisymm, MeasureTheory.measure_mono, iSup_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst_2 : l.NeBot
h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) ((⋃ (n : ι), s n) \ s k)) l (𝓝 0)
set :
  let S : Set α := ⋃ (n : ι), s n;
  ∀ (h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (S \ s k)) l (𝓝 0)),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n) : ℝ≥0∞)
    (⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)

Tactic:
set S := ⋃ n, s n
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst_2 : l.NeBot
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (S \ s k)) l (𝓝 0)
set :
  let M : ℝ≥0∞ := ⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n);
  (μ : (a : Set α) → ℝ≥0∞) S ≤ M
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)

Tactic:
set M := ⨆ n, μ (s n)
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst_2 : l.NeBot
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n)
k : ι
bc : S ∩ s k ⊆ s k
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S ∩ s k) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (S \ s k) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (S \ s k) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst_2 : l.NeBot
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n)
k : ι
⊢ S ∩ s k ⊆ s k

Tactic:
apply inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst_2 : l.NeBot
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n)
k : ι
bc : (μ : (a : Set α) → ℝ≥0∞) (s k) ≤ M
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s k) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (S \ s k) : ℝ≥0∞) ≤
    HAdd.hAdd (β := ℝ≥0∞) M ((μ : (a : Set α) → ℝ≥0∞) (S \ s k) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst_2 : l.NeBot
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n)
k : ι
⊢ (μ : (a : Set α) → ℝ≥0∞) (s k) ≤ M

Tactic:
le_iSup (μ ∘ s) k

Premises used: Function.comp, le_iSup, DFunLike.coe
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst_2 : l.NeBot
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n)
k : ι
⊢ (μ : (a : Set α) → ℝ≥0∞) (s k) ≤ M

Tactic:
exact le_iSup (μ ∘ s) k

Premises used: Function.comp, le_iSup, DFunLike.coe
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst_2 : l.NeBot
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n)
⊢ ∀ (k : ι), (μ : (a : Set α) → ℝ≥0∞) S ≤ HAdd.hAdd (β := ℝ≥0∞) M ((μ : (a : Set α) → ℝ≥0∞) (S \ s k) : ℝ≥0∞)

Tactic:
have A : ∀ k, μ S ≤ M + μ (S \ s k) := fun k ↦ calc
    μ S ≤ μ (S ∩ s k) + μ (S \ s k) := measure_le_inter_add_diff _ _ _
    _ ≤ μ (s k) + μ (S \ s k) := by gcongr; apply inter_subset_right
    _ ≤ M + μ (S \ s k) := by gcongr; exact le_iSup (μ ∘ s) k
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst_2 : l.NeBot
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n)
A : ∀ (k : ι), (μ : (a : Set α) → ℝ≥0∞) S ≤ HAdd.hAdd (β := ℝ≥0∞) M ((μ : (a : Set α) → ℝ≥0∞) (S \ s k) : ℝ≥0∞)
⊢ Tendsto (fun (k : ι) ↦ HAdd.hAdd (β := ℝ≥0∞) M ((μ : (a : Set α) → ℝ≥0∞) (S \ s k) : ℝ≥0∞)) l (𝓝 M)

Tactic:
simpa using tendsto_const_nhds.add h0

Premises used: tendsto_const_nhds, Filter.Tendsto.add