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 α
ι : 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:
have B : Tendsto (fun k ↦ M + μ (S \ s k)) l (𝓝 M) := by simpa using tendsto_const_nhds.add h0
-- 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∞)
B : Tendsto (fun (k : ι) ↦ HAdd.hAdd (β := ℝ≥0∞) M ((μ : (a : Set α) → ℝ≥0∞) (S \ s k) : ℝ≥0∞)) l (𝓝 M)
⊢ (μ : (a : Set α) → ℝ≥0∞) S ≤ M

Tactic:
ge_of_tendsto' B A

Premises used: ge_of_tendsto'
-- 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∞)
B : Tendsto (fun (k : ι) ↦ HAdd.hAdd (β := ℝ≥0∞) M ((μ : (a : Set α) → ℝ≥0∞) (S \ s k) : ℝ≥0∞)) l (𝓝 M)
⊢ (μ : (a : Set α) → ℝ≥0∞) S ≤ M

Tactic:
exact ge_of_tendsto' B A

Premises used: ge_of_tendsto'
-- 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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
choose! :
  ∀ (u : (x : α) → Set α) (hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x)
    (hu₀ : ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u x) : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
choose! u hxu hu₀ using hs
-- 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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
u : (x : α) → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u x) : ℝ≥0∞) (0 : ℝ≥0∞)
choose :
  ∀ (t : Set α) (ht : t ⊆ s ∧ t.Countable ∧ s ⊆ ⋃ x ∈ t, u x),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
choose t ht using TopologicalSpace.countable_cover_nhdsWithin hxu

Premises used: TopologicalSpace.countable_cover_nhdsWithin
-- 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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
u : (x : α) → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u x) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ht : t ⊆ s ∧ t.Countable ∧ s ⊆ ⋃ x ∈ t, u x
⊢ t ⊆ s

Tactic:
rcases ht with ⟨ts, t_count, ht⟩
-- 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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
u : (x : α) → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u x) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ht : t ⊆ s ∧ t.Countable ∧ s ⊆ ⋃ x ∈ t, u x
ts : t ⊆ s
⊢ t.Countable

Tactic:
rcases ht with ⟨ts, t_count, ht⟩
-- 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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
u : (x : α) → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u x) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ht : t ⊆ s ∧ t.Countable ∧ s ⊆ ⋃ x ∈ t, u x
ts : t ⊆ s
t_count : t.Countable
⊢ s ⊆ ⋃ x ∈ t, u x

Tactic:
rcases ht with ⟨ts, t_count, ht⟩
-- 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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
u : (x : α) → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u x) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ ⋃ x ∈ t, u x
apply : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ x ∈ t, u x) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply measure_mono_null ht

Premises used: MeasureTheory.measure_mono_null
-- 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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
u : (x : α) → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u x) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ ⋃ x ∈ t, u x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ x ∈ t, u x) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(measure_biUnion_null_iff t_count).2 fun x hx => hu₀ x (ts hx)

Premises used: Iff.mpr, 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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
u : (x : α) → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u x) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ ⋃ x ∈ t, u x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ x ∈ t, u x) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact (measure_biUnion_null_iff t_count).2 fun x hx => hu₀ x (ts hx)

Premises used: Iff.mpr, 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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
contrapose! :
  ∀ (hs : ∀ (x : α) (_ : x ∈ s), ∃ t ∈ 𝓝[s] x, LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
contrapose! hs
-- 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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
hs : ∀ (x : α) (_ : x ∈ s), ∃ t ∈ 𝓝[s] x, LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (x : α) (_ : x ∈ s), ∃ t ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [nonpos_iff_eq_zero] at hs

Premises used: nonpos_iff_eq_zero
-- 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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
hs : ∀ (x : α) (_ : x ∈ s), ∃ t ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_null_of_locally_null s hs

Premises used: MeasureTheory.measure_null_of_locally_null
-- 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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
hs : ∀ (x : α) (_ : x ∈ s), ∃ t ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_null_of_locally_null s hs

Premises used: MeasureTheory.measure_null_of_locally_null
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
ι : Type u_3
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst : l.NeBot
h0 : Tendsto (β := ℝ≥0∞) (fun (k : ι) ↦ (m : (a : Set α) → ℝ≥0∞) ((⋃ (n : ι), s n) \ s k)) l (𝓝 0)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n) : ℝ≥0∞) (⨆ (n : ι), (m : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)

Tactic:
measure_iUnion_of_tendsto_zero m l h0

Premises used: MeasureTheory.measure_iUnion_of_tendsto_zero
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)

Tactic:
measure_iUnion_of_tendsto_zero m atTop ?_

Premises used: MeasureTheory.measure_iUnion_of_tendsto_zero, Filter.atTop
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
refine : Tendsto (β := ℝ≥0∞) (fun (k : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) ((⋃ (n : ℕ), s n) \ s k)) atTop (𝓝 0)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)

Tactic:
refine measure_iUnion_of_tendsto_zero m atTop ?_

Premises used: MeasureTheory.measure_iUnion_of_tendsto_zero, Filter.atTop
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (k : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) ((⋃ (n : ℕ), s n) \ s k)) atTop (𝓝 0)

Tactic:
tendsto_nhds_bot_mono' (ENNReal.tendsto_sum_nat_add _ h0) fun n => ?_

Premises used: tendsto_nhds_bot_mono', ENNReal.tendsto_sum_nat_add
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
refine :
  ∀ (n : ℕ),
    LE.le (α := (fun (a : ℕ) ↦ ℝ≥0∞) n) ((m : (a : Set α) → ℝ≥0∞) ((⋃ (n : ℕ), s n) \ s n) : ℝ≥0∞)
      (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + n + 1) \ s (k + n)) : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (k : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) ((⋃ (n : ℕ), s n) \ s k)) atTop (𝓝 0)

Tactic:
refine tendsto_nhds_bot_mono' (ENNReal.tendsto_sum_nat_add _ h0) fun n => ?_

Premises used: tendsto_nhds_bot_mono', ENNReal.tendsto_sum_nat_add
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
⊢ LE.le (α := (fun (a : ℕ) ↦ ℝ≥0∞) n) ((m : (a : Set α) → ℝ≥0∞) ((⋃ (n : ℕ), s n) \ s n) : ℝ≥0∞)
    (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + n + 1) \ s (k + n)) : ℝ≥0∞)

Tactic:
(m.mono ?_).trans (measure_iUnion_le _)

Premises used: MeasureTheory.OuterMeasure.mono, MeasureTheory.measure_iUnion_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
refine : (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
⊢ LE.le (α := (fun (a : ℕ) ↦ ℝ≥0∞) n) ((m : (a : Set α) → ℝ≥0∞) ((⋃ (n : ℕ), s n) \ s n) : ℝ≥0∞)
    (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + n + 1) \ s (k + n)) : ℝ≥0∞)

Tactic:
refine (m.mono ?_).trans (measure_iUnion_le _)

Premises used: MeasureTheory.OuterMeasure.mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
⊢ Monotone s

Tactic:
have h' : Monotone s := @monotone_nat_of_le_succ (Set α) _ _ h_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
simp : ∀ (i : ℕ), s i ⊆ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
⊢ (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)

Tactic:
simp only [diff_subset_iff, iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff, Set.diff_subset_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx exists exists₁ : x ∈ s i
⊢ ∃ (i : ℕ), x ∈ s i

Tactic:
exists i
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
⊢ ∃ (i : ℕ), x ∈ s i

Tactic:
have : ∃ i, x ∈ s i := by exists i
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
this : ∃ (i : ℕ), x ∈ s i
rcases : ∀ (j : ℕ) (hj : x ∈ s j) (hlt : ∀ m < j, x ∉ s m), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)

Tactic:
rcases Nat.findX this with ⟨j, hj, hlt⟩

Premises used: Nat.findX
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
x : α
this : ∃ (i : ℕ), x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
inl : ∀ (hjn : j ≤ n), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
inr : ∀ (hnj : n < j), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)

Tactic:
rcases le_or_gt j n with hjn | hnj

Premises used: le_or_gt
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
x : α
this : ∃ (i : ℕ), x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hjn : j ≤ n
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)

Tactic:
Or.inl (h' hjn hj)

Premises used: Set.union, Set.Mem, setOf, Or.inl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
x : α
this : ∃ (i : ℕ), x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hjn : j ≤ n
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)

Tactic:
exact Or.inl (h' hjn hj)

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
x : α
this : ∃ (i : ℕ), x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
⊢ j - (n + 1) + n + 1 = j

Tactic:
lia
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
x : α
this : ∃ (i : ℕ), x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
⊢ j - (n + 1) + n + 1 = j

Tactic:
have : j - (n + 1) + n + 1 = j := by lia
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
x : α
this_1 : ∃ (i : ℕ), x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)

Tactic:
Or.inr (mem_iUnion.2 ⟨j - (n + 1), ?_, hlt _ ?_⟩)

Premises used: Iff.mpr, Set.union, Set.Mem, setOf, HSub.hSub, Set.mem_iUnion, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, Or.inr
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
x : α
this_1 : ∃ (i : ℕ), x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
inr : x ∈ s (j - (n + 1) + n + 1)
inr₁ : j - (n + 1) + n < j
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)

Tactic:
refine Or.inr (mem_iUnion.2 ⟨j - (n + 1), ?_, hlt _ ?_⟩)
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
x : α
this_1 : ∃ (i : ℕ), x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
inr inr₁ inr₂ inr₃ : x ∈ s j
⊢ x ∈ s (j - (n + 1) + n + 1)

Tactic:
rwa [this]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : Ne (α := ℝ≥0∞) (∑' (k : ℕ), (m : (a : Set α) → ℝ≥0∞) (s (k + 1) \ s k)) ∞
n : ℕ
h' : Monotone s
x : α
this_1 : ∃ (i : ℕ), x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
inr : (j - (n + 1) + n).succ ≤ j
inr₁ : j - (n + 1) + n + 1 ≤ j
inr₂ inr₃ : j ≤ j
⊢ j - (n + 1) + n < j

Tactic:
rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, this]

Premises used: Nat.succ_eq_add_one, Nat.succ_le_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
⊢ Injective (β := (s : Set α) → ℝ≥0∞) fun (μ : OuterMeasure α) (s : Set α) ↦ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
μ₁ μ₂ : OuterMeasure α
h : ∀ (s : Set α), Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ₁ = μ₂

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.MeasureTheory.OuterMeasure.Basic
Goal:
α : Type u_1
μ₁ μ₂ : OuterMeasure α
h : ∀ (s : Set α), s.Nonempty → Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
s : Set α
he : s = ∅
⊢ Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [he]
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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 : Countable ι
μ : F
s : ι → Set α
hs : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
bot_unique <| ge_of_tendsto' (ENNReal.tendsto_tsum_compl_atTop_zero hs) fun t ↦ ?_

Premises used: ENNReal.tendsto_tsum_compl_atTop_zero, ge_of_tendsto', bot_unique
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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 : Countable ι
μ : F
s : ι → Set α
hs : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
refine :
  ∀ (t : Finset ι),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
      (∑' (b : { x : ι // x ∉ t }), (μ : (a : Set α) → ℝ≥0∞) (s (↑b : ι)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine bot_unique <| ge_of_tendsto' (ENNReal.tendsto_tsum_compl_atTop_zero hs) fun t ↦ ?_

Premises used: ENNReal.tendsto_tsum_compl_atTop_zero, ge_of_tendsto', bot_unique
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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 : Countable ι
μ : F
s : ι → Set α
hs : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
t : Finset ι
h : limsup s cofinite ⊆ ⋃ (i : { i : ι // i ∉ t }), s (↑i : ι)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : { i : ι // i ∉ t }), s (↑i : ι)) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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 : Countable ι
μ : F
s : ι → Set α
hs : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
t : Finset ι
h :
  Subset.{u_1} (α := Set α) (⨅ (i : Set ι), ⨅ (_ : i.Finite), ⨆ a ∈ iᶜ, s a)
    (⋃ (x : ι), ⋃ (hx : x ∉ t), s (↑(Subtype.mk (p := fun (x : ι) ↦ x ∉ t) x hx) : ι))
⊢ limsup s cofinite ⊆ ⋃ (i : { i : ι // i ∉ t }), s (↑i : ι)

Tactic:
rw [hasBasis_cofinite.limsup_eq_iInf_iSup, iUnion_subtype]

Premises used: Filter.hasBasis_cofinite, Set.iUnion_subtype, Filter.HasBasis.limsup_eq_iInf_iSup
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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 : Countable ι
μ : F
s : ι → Set α
hs : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
t : Finset ι
⊢ Subset.{u_1} (α := Set α) (⨅ (i : Set ι), ⨅ (_ : i.Finite), ⨆ a ∈ iᶜ, s a)
    (⋃ (x : ι), ⋃ (hx : x ∉ t), s (↑(Subtype.mk (p := fun (x : ι) ↦ x ∉ t) x hx) : ι))

Tactic:
iInter₂_subset _ t.finite_toSet

Premises used: Set.Mem, Set.iInter, Set.iInter₂_subset, setOf, Finset.finite_toSet, Set.iUnion, Not
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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 : Countable ι
μ : F
s : ι → Set α
hs : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
t : Finset ι
⊢ Subset.{u_1} (α := Set α) (⨅ (i : Set ι), ⨅ (_ : i.Finite), ⨆ a ∈ iᶜ, s a)
    (⋃ (x : ι), ⋃ (hx : x ∉ t), s (↑(Subtype.mk (p := fun (x : ι) ↦ x ∉ t) x hx) : ι))

Tactic:
exact iInter₂_subset _ t.finite_toSet

Premises used: Set.iInter₂_subset, Finset.finite_toSet