awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (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 t : Set α
h : t =ᶠ[ae μ] ∅
⊢ ∅ = s ∩ ∅
have h₁ : Eq.{u_1 + 1} (α := α → Prop) ∅ ∅
Tactic: rw [inter_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (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
M : Type u_4
inst_2 : One M
f : α → M
s : Set α
⊢ s.mulIndicator f =ᶠ[ae μ] 1 ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ Function.mulSupport f) : ℝ≥0∞) (0 : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | a ∈ s ∧ ¬f a = 1} : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ Function.mulSupport f) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp [EventuallyEq, eventually_iff, ae, compl_setOf]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (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 t : Set α
H : s ≤ᶠ[ae μ] t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s \ t) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
Tactic: rw [union_diff_self, Set.union_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (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 t : Set α
H : s ≤ᶠ[ae μ] t
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s \ t) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
Tactic: rw [union_diff_self, Set.union_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (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 t : Set α
H : s ≤ᶠ[ae μ] t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) t
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) t
Tactic: rw [ae_le_set.1 H, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.AE (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 t : Set α
H : s ≤ᶠ[ae μ] t
rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) t
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [ae_le_set.1 H, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
μ : F
inst_2 : Countable ι
s : ι → Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
    (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have refine : ∀ (t : ℕ → Set α),
  (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) ((μ : (a : Set α) → ℝ≥0∞) (⨆ (i : ℕ), t i))
    (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i))
Tactic: refine rel_iSup_tsum μ measure_empty (· ≤ ·) (fun t ↦ ?_) _
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
μ : 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∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), t i) : ℝ≥0∞)
Tactic: rw [iUnion_disjointed]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
μ : F
inst_2 : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (disjointed t i)) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i))
have h : ∀ (i : ℕ), disjointed t i ⊆ t i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
μ : F
inst_2 : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) ((μ : (a : Set α) → ℝ≥0∞) (⨆ (i : ℕ), t i))
    (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i))
have μ₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), t i) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), disjointed t i) : ℝ≥0∞)
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 ..
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
μ : 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∞) ((μ : (a : Set α) → ℝ≥0∞) (⨆ (i : ℕ), t i)) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i))
have μ₂ : LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (disjointed 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 ..
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (hypothesis)
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 α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞)
    (∑' (i : (↑I : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)) : ℝ≥0∞)
have this : Countable.{u_2 + 1} (↑I : Type u_2)
Tactic: have := hI.to_subtype
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
this : Countable.{u_2 + 1} (↑I : Type u_2)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞)
    (∑' (i : (↑I : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)) : ℝ≥0∞)
have 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∞)
Tactic: rw [biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 t : Set α
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 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∞)
have bc : s ∩ t ⊆ t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
μ : 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∞)
have 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∞)
Tactic: refine ⟨fun h i hi ↦ measure_mono_null (subset_biUnion_of_mem hi) h, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (0 : ℝ≥0∞)
have x : Countable.{u_2 + 1} (↑I : Type u_2)
Tactic: have _ := hI.to_subtype
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 (Set α)
hS : S.Countable
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ S) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ S, i) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [sUnion_eq_biUnion, measure_biUnion_null_iff hS]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 (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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ S) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : (∀ i ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [sUnion_eq_biUnion, measure_biUnion_null_iff hS]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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
ι : Sort u_4
inst_2 : Countable ι
s : ι → Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ range s) : ℝ≥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]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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
ι : 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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: rw [← sUnion_range, measure_sUnion_null_iff (countable_range s), forall_mem_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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
ι : 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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₂ : (∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 : s.Countable
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, {i}) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← measure_biUnion_null_iff hs, biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 : s.Countable
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, {i}) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← measure_biUnion_null_iff hs, biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
ι : 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∞)
have refine : LE.le (α := ℝ≥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 _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
ι : 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)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n) : ℝ≥0∞)
    (⨆ (n : ι), (μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)
have 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∞)
Tactic: set S := ⋃ n, s n
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
ι : 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 : ι
⊢ 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∞)
have bc : S ∩ s k ⊆ s k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
ι : 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 : ι
⊢ 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∞)
have bc : (μ : (a : Set α) → ℝ≥0∞) (s k) ≤ M
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
ι : 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 : Set α) → ℝ≥0∞) S ≤ M
have A : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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 α
ι : 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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) S ≤ M
have B : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: choose! u hxu hu₀ using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have choose : ∀ (t : Set α) (ht : t ⊆ s ∧ t.Countable ∧ s ⊆ ⋃ x ∈ t, u x),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: choose t ht using TopologicalSpace.countable_cover_nhdsWithin hxu
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have ts : t ⊆ s
Tactic: rcases ht with ⟨ts, t_count, ht⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have t_count : t.Countable
Tactic: rcases ht with ⟨ts, t_count, ht⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have ht₁ : s ⊆ ⋃ x ∈ t, u x
Tactic: rcases ht with ⟨ts, t_count, ht⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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
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∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have apply : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ x ∈ t, u x) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply measure_mono_null ht
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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
inst_2 : TopologicalSpace α
inst_3 : SecondCountableTopology α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have 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∞)
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Basic (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
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have hs₁ : ∀ (x : α) (_ : x ∈ s), ∃ t ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [nonpos_iff_eq_zero] at hs
Cleared hypotheses: hs