awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
lift :
  ∀ (t : Finset ι) (ht : (↑t : Set ι).Finite) (h : ∀ i ∈ (↑t : Set ι), m.IsCaratheodory (s i)),
    m.IsCaratheodory (⋃ i ∈ (↑t : Set ι), 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: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h : s₁ ∩ s₂ ⊆ ∅
h₁ : m.IsCaratheodory s₁
t : Set α
⊢ (m : (a : Set α) → ℝ≥0∞) (t ∩ (s₁ ∪ s₂)) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ (s₁ ∪ s₂) ∩ s₁) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) ((t ∩ (s₁ ∪ s₂)) \ s₁) : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
Tactic: rw [h₁, Set.inter_assoc, Set.union_inter_cancel_left, inter_diff_assoc, union_diff_cancel_left h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h : s₁ ∩ s₂ ⊆ ∅
h₁ : m.IsCaratheodory s₁
t : Set α
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ (s₁ ∪ s₂) ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) ((t ∩ (s₁ ∪ s₂)) \ s₁) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
⊢ (m : (a : Set α) → ℝ≥0∞) (t ∩ (s₁ ∪ s₂)) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ((s₁ ∪ s₂) ∩ s₁)) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) ((t ∩ (s₁ ∪ s₂)) \ s₁) : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
Tactic: rw [h₁, Set.inter_assoc, Set.union_inter_cancel_left, inter_diff_assoc, union_diff_cancel_left h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h : s₁ ∩ s₂ ⊆ ∅
h₁ : m.IsCaratheodory s₁
t : Set α
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ (s₁ ∪ s₂) ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) ((t ∩ (s₁ ∪ s₂)) \ s₁) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ((s₁ ∪ s₂) ∩ s₁)) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) ((t ∩ (s₁ ∪ s₂)) \ s₁) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
⊢ (m : (a : Set α) → ℝ≥0∞) (t ∩ (s₁ ∪ s₂)) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
have rw₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) ((t ∩ (s₁ ∪ s₂)) \ s₁) : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
Tactic: rw [h₁, Set.inter_assoc, Set.union_inter_cancel_left, inter_diff_assoc, union_diff_cancel_left h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h : s₁ ∩ s₂ ⊆ ∅
h₁ : m.IsCaratheodory s₁
t : Set α
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ (s₁ ∪ s₂) ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) ((t ∩ (s₁ ∪ s₂)) \ s₁) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ((s₁ ∪ s₂) ∩ s₁)) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) ((t ∩ (s₁ ∪ s₂)) \ s₁) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) ((t ∩ (s₁ ∪ s₂)) \ s₁) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
⊢ (m : (a : Set α) → ℝ≥0∞) (t ∩ (s₁ ∪ s₂)) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
have rw₃ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (t ∩ ((s₁ ∪ s₂) \ s₁)) : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
Tactic: rw [h₁, Set.inter_assoc, Set.union_inter_cancel_left, inter_diff_assoc, union_diff_cancel_left h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h : s₁ ∩ s₂ ⊆ ∅
h₁ : m.IsCaratheodory s₁
t : Set α
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ (s₁ ∪ s₂) ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) ((t ∩ (s₁ ∪ s₂)) \ s₁) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ((s₁ ∪ s₂) ∩ s₁)) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) ((t ∩ (s₁ ∪ s₂)) \ s₁) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) ((t ∩ (s₁ ∪ s₂)) \ s₁) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
rw₃ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ ((s₁ ∪ s₂) \ s₁)) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
⊢ (m : (a : Set α) → ℝ≥0∞) (t ∩ (s₁ ∪ s₂)) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
have rw₄ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₁) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (t ∩ s₂) : ℝ≥0∞)
Tactic: rw [h₁, Set.inter_assoc, Set.union_inter_cancel_left, inter_diff_assoc, union_diff_cancel_left h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
n : ℕ
h : ∀ i < n + 1, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ (i : ℕ), ⋃ (_ : i < n + 1), s i)
have rw : m.IsCaratheodory ((⋃ (k : ℕ), ⋃ (_ : k < n), s k) ∪ s n)
Tactic: rw [biUnion_lt_succ]
-- 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₂
⊢ m.IsCaratheodory (s₁ ∩ s₂)
have rw : m.IsCaratheodory (s₁ᶜ ∪ s₂ᶜ)
Tactic: rw [← isCaratheodory_compl_iff, Set.compl_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n.succ, (m : (a : Set α) → ℝ≥0∞) (t ∩ s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n.succ), s i) : ℝ≥0∞)
have rw : s n ∩ ⋃ (k : ℕ), ⋃ (_ : k < n), s k ⊆ ∅
Tactic: rw [biUnion_lt_succ, Finset.sum_range_succ, Set.union_comm, isCaratheodory_sum h hd,
      m.measure_inter_union _ (h n), add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ m.IsCaratheodory (⋃ (i : ℕ), s i)
have apply : ∀ (t : Set α),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t \ ⋃ (i : ℕ), s i) : ℝ≥0∞) ≤
    (m : (a : Set α) → ℝ≥0∞) t
Tactic: apply (isCaratheodory_iff_le' m).mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
    (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
  ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), t ∩ s i) : ℝ≥0∞)
Tactic: convert! measure_iUnion_le (μ := m) fun i => t ∩ s i using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
h₁ :
  Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), t ∩ s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
    (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i))
  (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ s i))
Tactic: convert! measure_iUnion_le (μ := m) fun i => t ∩ s i using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (hypothesis)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t \ ⋃ (i : ℕ), s i) : ℝ≥0∞) ≤
    (m : (a : Set α) → ℝ≥0∞) t
have hp : LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
  (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
Tactic: have hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i < n, s i) := by
    convert! measure_iUnion_le (μ := m) fun i => t ∩ s i using 1
    · simp [inter_iUnion]
    · simp [ENNReal.tsum_eq_iSup_nat, isCaratheodory_sum m h hd]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp :
  LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
    (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t \ ⋃ (i : ℕ), s i) : ℝ≥0∞) ≤
    (m : (a : Set α) → ℝ≥0∞) t
have grw : LE.le (α := ℝ≥0∞)
  (⨆ (i : ℕ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i_1 : ℕ), ⋃ (_ : i_1 < i), s i_1) : ℝ≥0∞)
        ((m : (a : Set α) → ℝ≥0∞) (t \ ⋃ (i : ℕ), s i) : ℝ≥0∞) :
    ℝ≥0∞)
  ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: grw [hp, ENNReal.iSup_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp :
  LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
    (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (i : ℕ),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i_1 : ℕ), ⋃ (_ : i_1 < i), s i_1) : ℝ≥0∞)
          ((m : (a : Set α) → ℝ≥0∞) (t \ ⋃ (i : ℕ), s i) : ℝ≥0∞) :
      ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have refine : ∀ (n : ℕ),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t \ ⋃ (i : ℕ), s i) : ℝ≥0∞) ≤
    (m : (a : Set α) → ℝ≥0∞) t
Tactic: refine iSup_le fun n => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp :
  LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
    (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
n : ℕ
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t \ ⋃ (i : ℕ), s i) : ℝ≥0∞) ≤
    (m : (a : Set α) → ℝ≥0∞) t
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (t \ ⋃ (i : ℕ), s i) : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (t \ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
Tactic: rw [isCaratheodory_iUnion_lt _ (fun i _ => h i) t (n := n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp :
  LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
    (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
n : ℕ
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t \ ⋃ (i : ℕ), s i) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (t \ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
have bc : ∀ (i : ℕ), ⋃ (_ : i < n), s i ⊆ s i
Tactic: gcongr with i
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ (i : ℕ), s i)
have rw : m.IsCaratheodory (⋃ (i : ℕ), disjointed s i)
Tactic: rw [← iUnion_disjointed]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
Tactic: refine le_antisymm (measure_iUnion_le s) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) (⨆ (i : ℕ), ∑ a ∈ Finset.range i, (m : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
  ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
Tactic: rw [ENNReal.tsum_eq_iSup_nat]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ LE.le (α := ℝ≥0∞) (⨆ (i : ℕ), ∑ a ∈ Finset.range i, (m : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
have refine : ∀ (n : ℕ),
  LE.le (α := ℝ≥0∞) (∑ a ∈ Finset.range n, (m : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
Tactic: refine iSup_le fun n => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (hypothesis)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
⊢ LE.le (α := ℝ≥0∞) (∑ a ∈ Finset.range n, (m : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
have this : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, (m : (a : Set α) → ℝ≥0∞) (univ ∩ s i) : ℝ≥0∞)
  ((m : (a : Set α) → ℝ≥0∞) (univ ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
Tactic: have := @isCaratheodory_sum _ m _ h hd univ n
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (hypothesis)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, (m : (a : Set α) → ℝ≥0∞) (univ ∩ s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (univ ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ a ∈ Finset.range n, (m : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
have this₁ : Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, (m : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞)
  ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
Tactic: simp only [inter_comm, inter_univ, univ_inter] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this :
  Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, (m : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ a ∈ Finset.range n, (m : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
have simp : LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
  ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
⊢ MeasurableSpace α
have apply : ∀ (s₁ s₂ : Set α), m.caratheodoryDynkin.Has s₁ → m.caratheodoryDynkin.Has s₂ → m.caratheodoryDynkin.Has (s₁ ∩ s₂)
Tactic: apply MeasurableSpace.DynkinSystem.toMeasurableSpace (caratheodoryDynkin m)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ MeasurableSet s
have apply : ∀ (t : Set α),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    (OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) t
Tactic: apply (isCaratheodory_iff_le _).mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ ∀ (t : Set α),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        ((OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
      (OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) t
have refine : ∀ (t : Set α) (f : ℕ → Set α) (hf : t ⊆ ⋃ (i : ℕ), f i),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (f i)
Tactic: refine fun t => le_iInf fun f => le_iInf fun hf => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (f i)
have refine_1 : t ∩ s ⊆ ⋃ (i : ℕ), (fun (i : ℕ) ↦ f i ∩ s) i
Tactic: refine
    le_trans
      (add_le_add ((iInf_le_of_le fun i => f i ∩ s) <| iInf_le _ ?_)
        ((iInf_le_of_le fun i => f i \ s) <| iInf_le _ ?_))
      ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
refine_1 : t ∩ s ⊆ ⋃ (i : ℕ), (fun (i : ℕ) ↦ f i ∩ s) i
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (f i)
have refine_2 : t \ s ⊆ ⋃ (i : ℕ), (fun (i : ℕ) ↦ f i \ s) i
Tactic: refine
    le_trans
      (add_le_add ((iInf_le_of_le fun i => f i ∩ s) <| iInf_le _ ?_)
        ((iInf_le_of_le fun i => f i \ s) <| iInf_le _ ?_))
      ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
refine_1 : t ∩ s ⊆ ⋃ (i : ℕ), (fun (i : ℕ) ↦ f i ∩ s) i
refine_2 : t \ s ⊆ ⋃ (i : ℕ), (fun (i : ℕ) ↦ f i \ s) i
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((OuterMeasure.ofFunction m h₀ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (f i)
have refine_3 : HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), m ((fun (i : ℕ) ↦ f i ∩ s) i)) (∑' (i : ℕ), m ((fun (i : ℕ) ↦ f i \ s) i)) ≤
  ∑' (i : ℕ), m (f i)
Tactic: refine
    le_trans
      (add_le_add ((iInf_le_of_le fun i => f i ∩ s) <| iInf_le _ ?_)
        ((iInf_le_of_le fun i => f i \ s) <| iInf_le _ ?_))
      ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ t ∩ s ⊆ ⋃ (i : ℕ), (fun (i : ℕ) ↦ f i ∩ s) i
have refine_1 : t ∩ s ⊆ (⋃ (i : ℕ), f i) ∩ s
Tactic: rw [← iUnion_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ t \ s ⊆ ⋃ (i : ℕ), (fun (i : ℕ) ↦ f i \ s) i
have refine_2 : t \ s ⊆ (⋃ (i : ℕ), f i) \ s
Tactic: rw [← iUnion_diff]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ (i : ℕ), f i
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), m ((fun (i : ℕ) ↦ f i ∩ s) i)) (∑' (i : ℕ), m ((fun (i : ℕ) ↦ f i \ s) i)) ≤
    ∑' (i : ℕ), m (f i)
have refine_3 : LE.le (α := ℝ≥0∞) (∑' (a : ℕ), (m ((fun (i : ℕ) ↦ f i ∩ s) a) + m ((fun (i : ℕ) ↦ f i \ s) a))) (∑' (i : ℕ), m (f i))
Tactic: rw [← ENNReal.tsum_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Caratheodory (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ MeasurableSet s
have hs₁ : ∀ (t : Set α),
  HAdd.hAdd (α := ℝ≥0∞) (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) (⨆ (_ : (t \ s).Nonempty), m (t \ s)) ≤
    ⨆ (_ : t.Nonempty), m t
Tactic: apply ofFunction_caratheodory