awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (goal)
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)
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∞)
refine₂ : ∀ (n : ℕ), (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₃ : ∀ (n : ℕ) (h' : Monotone s), (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₄ : ∀ (n : ℕ) (h' : Monotone s) (i : ℕ), s i ⊆ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₅ : ∀ (n : ℕ) (h' : Monotone s) (i : ℕ) ⦃x : α⦄ (hx : x ∈ s i), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₆ :
  ∀ (n : ℕ) (h' : Monotone s) (i : ℕ) ⦃x : α⦄ (hx : x ∈ s i) (this : ∃ (i : ℕ), x ∈ s i),
    x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₇ :
  ∀ (n : ℕ) (h' : Monotone s) (i : ℕ) ⦃x : α⦄ (hx : x ∈ s i) (this : ∃ (i : ℕ), x ∈ s i) (j : ℕ) (hj : x ∈ s j)
    (hlt : ∀ m < j, x ∉ s m), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₈ :
  ∀ (n : ℕ) (h' : Monotone s) ⦃x : α⦄ (this : ∃ (i : ℕ), x ∈ s i) (j : ℕ) (hj : x ∈ s j) (hlt : ∀ m < j, x ∉ s m),
    x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)
have inl : ∀ (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: classical
  refine measure_iUnion_of_tendsto_zero m atTop ?_
  refine tendsto_nhds_bot_mono' (ENNReal.tendsto_sum_nat_add _ h0) fun n => ?_
  refine (m.mono ?_).trans (measure_iUnion_le _)
  -- Current goal: `(⋃ k, s k) \ s n ⊆ ⋃ k, s (k + n + 1) \ s (k + n)`
  have h' : Monotone s := @monotone_nat_of_le_succ (Set α) _ _ h_mono
  simp only [diff_subset_iff, iUnion_subset_iff]
  intro i x hx
  have : ∃ i, x ∈ s i := by exists i
  rcases Nat.findX this with ⟨j, hj, hlt⟩
  clear hx i
  rcases le_or_gt j n with hjn | hnj
  · exact Or.inl (h' hjn hj)
  have : j - (n + 1) + n + 1 = j := by lia
  refine Or.inr (mem_iUnion.2 ⟨j - (n + 1), ?_, hlt _ ?_⟩)
  · rwa [this]
  · rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (goal)
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)
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∞)
refine₂ : ∀ (n : ℕ), (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₃ : ∀ (n : ℕ) (h' : Monotone s), (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₄ : ∀ (n : ℕ) (h' : Monotone s) (i : ℕ), s i ⊆ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₅ : ∀ (n : ℕ) (h' : Monotone s) (i : ℕ) ⦃x : α⦄ (hx : x ∈ s i), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₆ :
  ∀ (n : ℕ) (h' : Monotone s) (i : ℕ) ⦃x : α⦄ (hx : x ∈ s i) (this : ∃ (i : ℕ), x ∈ s i),
    x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₇ :
  ∀ (n : ℕ) (h' : Monotone s) (i : ℕ) ⦃x : α⦄ (hx : x ∈ s i) (this : ∃ (i : ℕ), x ∈ s i) (j : ℕ) (hj : x ∈ s j)
    (hlt : ∀ m < j, x ∉ s m), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₈ :
  ∀ (n : ℕ) (h' : Monotone s) ⦃x : α⦄ (this : ∃ (i : ℕ), x ∈ s i) (j : ℕ) (hj : x ∈ s j) (hlt : ∀ m < j, x ∉ s m),
    x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
inl :
  ∀ (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)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)
have inr : ∀ (n : ℕ) (h' : Monotone s) ⦃x : α⦄ (this : ∃ (i : ℕ), x ∈ s i) (j : ℕ) (hj : x ∈ s j) (hlt : ∀ m < j, x ∉ s m)
  (hnj : n < j), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
Tactic: classical
  refine measure_iUnion_of_tendsto_zero m atTop ?_
  refine tendsto_nhds_bot_mono' (ENNReal.tendsto_sum_nat_add _ h0) fun n => ?_
  refine (m.mono ?_).trans (measure_iUnion_le _)
  -- Current goal: `(⋃ k, s k) \ s n ⊆ ⋃ k, s (k + n + 1) \ s (k + n)`
  have h' : Monotone s := @monotone_nat_of_le_succ (Set α) _ _ h_mono
  simp only [diff_subset_iff, iUnion_subset_iff]
  intro i x hx
  have : ∃ i, x ∈ s i := by exists i
  rcases Nat.findX this with ⟨j, hj, hlt⟩
  clear hx i
  rcases le_or_gt j n with hjn | hnj
  · exact Or.inl (h' hjn hj)
  have : j - (n + 1) + n + 1 = j := by lia
  refine Or.inr (mem_iUnion.2 ⟨j - (n + 1), ?_, hlt _ ?_⟩)
  · rwa [this]
  · rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (goal)
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)
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∞)
refine₂ : ∀ (n : ℕ), (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₃ : ∀ (n : ℕ) (h' : Monotone s), (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₄ : ∀ (n : ℕ) (h' : Monotone s) (i : ℕ), s i ⊆ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₅ : ∀ (n : ℕ) (h' : Monotone s) (i : ℕ) ⦃x : α⦄ (hx : x ∈ s i), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₆ :
  ∀ (n : ℕ) (h' : Monotone s) (i : ℕ) ⦃x : α⦄ (hx : x ∈ s i) (this : ∃ (i : ℕ), x ∈ s i),
    x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₇ :
  ∀ (n : ℕ) (h' : Monotone s) (i : ℕ) ⦃x : α⦄ (hx : x ∈ s i) (this : ∃ (i : ℕ), x ∈ s i) (j : ℕ) (hj : x ∈ s j)
    (hlt : ∀ m < j, x ∉ s m), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₈ :
  ∀ (n : ℕ) (h' : Monotone s) ⦃x : α⦄ (this : ∃ (i : ℕ), x ∈ s i) (j : ℕ) (hj : x ∈ s j) (hlt : ∀ m < j, x ∉ s m),
    x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
inl :
  ∀ (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)
inr inr₁ :
  ∀ (n : ℕ) (h' : Monotone s) ⦃x : α⦄ (this : ∃ (i : ℕ), x ∈ s i) (j : ℕ) (hj : x ∈ s j) (hlt : ∀ m < j, x ∉ s m)
    (hnj : n < j), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)
have inr₂ : ∀ (n : ℕ) (h' : Monotone s) ⦃x : α⦄ (this : ∃ (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: classical
  refine measure_iUnion_of_tendsto_zero m atTop ?_
  refine tendsto_nhds_bot_mono' (ENNReal.tendsto_sum_nat_add _ h0) fun n => ?_
  refine (m.mono ?_).trans (measure_iUnion_le _)
  -- Current goal: `(⋃ k, s k) \ s n ⊆ ⋃ k, s (k + n + 1) \ s (k + n)`
  have h' : Monotone s := @monotone_nat_of_le_succ (Set α) _ _ h_mono
  simp only [diff_subset_iff, iUnion_subset_iff]
  intro i x hx
  have : ∃ i, x ∈ s i := by exists i
  rcases Nat.findX this with ⟨j, hj, hlt⟩
  clear hx i
  rcases le_or_gt j n with hjn | hnj
  · exact Or.inl (h' hjn hj)
  have : j - (n + 1) + n + 1 = j := by lia
  refine Or.inr (mem_iUnion.2 ⟨j - (n + 1), ?_, hlt _ ?_⟩)
  · rwa [this]
  · rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (goal)
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)
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∞)
refine₂ : ∀ (n : ℕ), (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₃ : ∀ (n : ℕ) (h' : Monotone s), (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₄ : ∀ (n : ℕ) (h' : Monotone s) (i : ℕ), s i ⊆ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₅ : ∀ (n : ℕ) (h' : Monotone s) (i : ℕ) ⦃x : α⦄ (hx : x ∈ s i), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₆ :
  ∀ (n : ℕ) (h' : Monotone s) (i : ℕ) ⦃x : α⦄ (hx : x ∈ s i) (this : ∃ (i : ℕ), x ∈ s i),
    x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₇ :
  ∀ (n : ℕ) (h' : Monotone s) (i : ℕ) ⦃x : α⦄ (hx : x ∈ s i) (this : ∃ (i : ℕ), x ∈ s i) (j : ℕ) (hj : x ∈ s j)
    (hlt : ∀ m < j, x ∉ s m), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine₈ :
  ∀ (n : ℕ) (h' : Monotone s) ⦃x : α⦄ (this : ∃ (i : ℕ), x ∈ s i) (j : ℕ) (hj : x ∈ s j) (hlt : ∀ m < j, x ∉ s m),
    x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
inl :
  ∀ (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)
inr inr₁ :
  ∀ (n : ℕ) (h' : Monotone s) ⦃x : α⦄ (this : ∃ (i : ℕ), x ∈ s i) (j : ℕ) (hj : x ∈ s j) (hlt : ∀ m < j, x ∉ s m)
    (hnj : n < j), x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
inr₂ :
  ∀ (n : ℕ) (h' : Monotone s) ⦃x : α⦄ (this : ∃ (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)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)
have inr₃ : ∀ (n : ℕ) (h' : Monotone s) ⦃x : α⦄ (this : ∃ (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 (j - (n + 1) + n + 1)
Tactic: classical
  refine measure_iUnion_of_tendsto_zero m atTop ?_
  refine tendsto_nhds_bot_mono' (ENNReal.tendsto_sum_nat_add _ h0) fun n => ?_
  refine (m.mono ?_).trans (measure_iUnion_le _)
  -- Current goal: `(⋃ k, s k) \ s n ⊆ ⋃ k, s (k + n + 1) \ s (k + n)`
  have h' : Monotone s := @monotone_nat_of_le_succ (Set α) _ _ h_mono
  simp only [diff_subset_iff, iUnion_subset_iff]
  intro i x hx
  have : ∃ i, x ∈ s i := by exists i
  rcases Nat.findX this with ⟨j, hj, hlt⟩
  clear hx i
  rcases le_or_gt j n with hjn | hnj
  · exact Or.inl (h' hjn hj)
  have : j - (n + 1) + n + 1 = j := by lia
  refine Or.inr (mem_iUnion.2 ⟨j - (n + 1), ?_, hlt _ ?_⟩)
  · rwa [this]
  · rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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∞)
have refine : ∀ (t : Finset ι),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
    (∑' (b : { x : ι // x ∉ t }), (μ : (a : Set α) → ℝ≥0∞) (s (↑b : ι)) : ℝ≥0∞)
Tactic: refine bot_unique <| ge_of_tendsto' (ENNReal.tendsto_tsum_compl_atTop_zero hs) fun t ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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 ι
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : { i : ι // i ∉ t }), s (↑i : ι)) : ℝ≥0∞)
have h : limsup s cofinite ⊆ ⋃ (i : { i : ι // i ∉ t }), s (↑i : ι)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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 ι
⊢ limsup s cofinite ⊆ ⋃ (i : { i : ι // i ∉ t }), s (↑i : ι)
have 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) : ι))
Tactic: rw [hasBasis_cofinite.limsup_eq_iInf_iSup, iUnion_subtype]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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 ι
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
    (∑' (b : { x : ι // x ∉ t }), (μ : (a : Set α) → ℝ≥0∞) (s (↑b : ι)) : ℝ≥0∞)
have μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : { i : ι // i ∉ t }), s (↑i : ι)) : ℝ≥0∞)
Tactic: calc
    μ (limsup s cofinite) ≤ μ (⋃ i : {i // i ∉ t}, s i) := by
      gcongr
      rw [hasBasis_cofinite.limsup_eq_iInf_iSup, iUnion_subtype]
      exact iInter₂_subset _ t.finite_toSet
    _ ≤ ∑' i : {i // i ∉ t}, μ (s i) := measure_iUnion_le _
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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 : Ne (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s atTop) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← Nat.cofinite_eq_atTop, measure_limsup_cofinite_eq_zero hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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 : Ne (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s atTop) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [← Nat.cofinite_eq_atTop, measure_limsup_cofinite_eq_zero hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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 α
h : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
⊢ ∀ᵐ (x : α) ∂μ, Set.Finite.{u_2} (α := ι) {i : ι | x ∈ s i}
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Set.Finite.{u_2} (α := ι) {i : ι | a ∈ s i}} : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
Tactic: rw [ae_iff, ← measure_limsup_cofinite_eq_zero h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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 α
h : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Set.Finite.{u_2} (α := ι) {i : ι | a ∈ s i}} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
have h₁ : ∀ (x : α), Membership.mem (γ := Set α) {a : α | ¬Set.Finite.{u_2} (α := ι) {i : ι | a ∈ s i}} x ↔ x ∈ limsup s cofinite
Tactic: congr 1 with x
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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
inst_3 : Infinite ι
s : ι → Set α
h : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (liminf s cofinite) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (liminf s cofinite) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero, ← measure_limsup_cofinite_eq_zero h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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 α
h : Ne (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (liminf s atTop) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (liminf s cofinite) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← Nat.cofinite_eq_atTop, measure_liminf_cofinite_eq_zero h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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 α
h : Ne (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (liminf s cofinite) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (liminf s atTop) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [← Nat.cofinite_eq_atTop, measure_liminf_cofinite_eq_zero h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (hypothesis)
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 α
t : Set α
h : ∀ (n : ℕ), s n =ᶠ[ae μ] t
⊢ limsup s atTop =ᶠ[ae μ] t
have h₁ : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
Tactic: simp only [eventuallyEq_set, ← eventually_countable_forall] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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 α
t : Set α
h : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
⊢ limsup s atTop =ᶠ[ae μ] t
have refine : ∀ (x : α) (hx : ∀ (i : ℕ), x ∈ s i ↔ x ∈ t), x ∈ limsup s atTop ↔ x ∈ t
Tactic: refine eventuallyEq_set.2 <| h.mono fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (hypothesis)
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 α
t : Set α
h : ∀ (n : ℕ), s n =ᶠ[ae μ] t
⊢ liminf s atTop =ᶠ[ae μ] t
have h₁ : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
Tactic: simp only [eventuallyEq_set, ← eventually_countable_forall] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (goal)
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 α
t : Set α
h : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
⊢ liminf s atTop =ᶠ[ae μ] t
have refine : ∀ (x : α) (hx : ∀ (i : ℕ), x ∈ s i ↔ x ∈ t), x ∈ liminf s atTop ↔ x ∈ t
Tactic: refine eventuallyEq_set.2 <| h.mono fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ (m : (a : Set α) → ℝ≥0∞) t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ (s₁ ∪ s₂)) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t \ (s₁ ∪ s₂)) : ℝ≥0∞)
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁ ∩ s₂) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) ((t ∩ s₁) \ s₂) : ℝ≥0∞) +
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t \ s₁ ∩ s₂) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) ((t \ s₁) \ s₂) : ℝ≥0∞) =
  HAdd.hAdd (β := ℝ≥0∞)
    (HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁ ∩ s₂) : ℝ≥0∞)
        ((m : (a : Set α) → ℝ≥0∞) ((t ∩ s₁) \ s₂) : ℝ≥0∞))
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ (s₂ \ s₁)) : ℝ≥0∞))
    ((m : (a : Set α) → ℝ≥0∞) (t \ (s₁ ∪ s₂)) : ℝ≥0∞)
Tactic: rw [h₁ t, h₂ (t ∩ s₁), h₂ (t \ s₁), h₁ (t ∩ (s₁ ∪ s₂)), inter_diff_assoc _ _ s₁,
    Set.inter_assoc _ _ s₁, inter_eq_self_of_subset_right Set.subset_union_left,
    union_diff_left, h₂ (t ∩ s₁)]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
h : ∀ i ∈ t, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ t, s i)
have lift : ∀ (t : Finset ι) (h : ∀ i ∈ (↑t : Set ι), m.IsCaratheodory (s i)), m.IsCaratheodory (⋃ i ∈ (↑t : Set ι), s i)
Tactic: lift t to Finset ι using ht
Cleared hypotheses: t, ht, h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
i : ι
t : Finset ι
hi : i ∉ t
IH : ∀ (h : ∀ i ∈ (↑t : Set ι), m.IsCaratheodory (s i)), m.IsCaratheodory (⋃ i ∈ (↑t : Set ι), s i)
h : ∀ i_1 ∈ (↑(insert i t) : Set ι), m.IsCaratheodory (s i_1)
⊢ m.IsCaratheodory (⋃ i_1 ∈ (↑(insert i t) : Set ι), s i_1)
have insert : ∀ (h : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ t → m.IsCaratheodory (s i_1)), m.IsCaratheodory (s i ∪ ⋃ x ∈ t, s x)
Tactic: simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Finset ι
h : ∀ i ∈ (↑t : Set ι), m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ (↑t : Set ι), s i)
have empty : ∀ (h : ∀ i ∈ (↑∅ : Set ι), m.IsCaratheodory (s i)), m.IsCaratheodory (⋃ i ∈ (↑∅ : Set ι), s i)
Tactic: induction t using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢
    exact m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Finset ι
h : ∀ i ∈ (↑t : Set ι), m.IsCaratheodory (s i)
empty : ∀ (h : ∀ i ∈ (↑∅ : Set ι), m.IsCaratheodory (s i)), m.IsCaratheodory (⋃ i ∈ (↑∅ : Set ι), s i)
⊢ m.IsCaratheodory (⋃ i ∈ (↑t : Set ι), s i)
have insert : ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
  (IH : ∀ (h : ∀ i ∈ (↑t : Set ι), m.IsCaratheodory (s i)), m.IsCaratheodory (⋃ i ∈ (↑t : Set ι), s i))
  (h : ∀ i_1 ∈ (↑(insert i t) : Set ι), m.IsCaratheodory (s i_1)),
  m.IsCaratheodory (⋃ i_1 ∈ (↑(insert i t) : Set ι), s i_1)
Tactic: induction t using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢
    exact m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
h : ∀ i ∈ t, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ t, s i)
have lift : ∀ (t : Finset ι) (ht : (↑t : Set ι).Finite) (h : ∀ i ∈ (↑t : Set ι), m.IsCaratheodory (s i)),
  m.IsCaratheodory (⋃ i ∈ (↑t : Set ι), s i)
Tactic: classical
  lift t to Finset ι using ht
  induction t using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢
    exact m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)
Cleared hypotheses: t, ht, h