awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
ι : Type u_1
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
s : ι → Set α
h : ∀ (i : ι), m.IsCaratheodory (s i)
i : ι
⊢ m.IsCaratheodory (disjointed s i)

Tactic:
disjointedRec (fun _ j ht ↦ m.isCaratheodory_diff ht <| h j) (h i)

Premises used: disjointedRec, MeasureTheory.OuterMeasure.isCaratheodory_diff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range 0, (m : (a : Set α) → ℝ≥0∞) (t ∩ s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < 0), s i) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
rw : s n ∩ ⋃ (k : ℕ), ⋃ (_ : k < n), s k ⊆ ∅
⊢ 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∞)

Tactic:
rw [biUnion_lt_succ, Finset.sum_range_succ, Set.union_comm, isCaratheodory_sum h hd,
      m.measure_inter_union _ (h n), add_comm]

Premises used: Set.biUnion_lt_succ, Set.union_comm, add_comm, MeasureTheory.OuterMeasure.measure_inter_union, Finset.sum_range_succ
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
a : α
⊢ a ∈ s n ∩ ⋃ (k : ℕ), ⋃ (_ : k < n), s k → Membership.mem (γ := Set α) ∅ a

Tactic:
simpa using fun (h₁ : a ∈ s n) i (hi : i < n) h₂ => (hd (ne_of_gt hi)).le_bot ⟨h₁, h₂⟩

Premises used: Disjoint.le_bot, ne_of_gt, And.intro
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
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
⊢ m.IsCaratheodory (⋃ (i : ℕ), s i)

Tactic:
apply (isCaratheodory_iff_le' m).mpr

Premises used: Iff.mpr, MeasureTheory.OuterMeasure.isCaratheodory_iff_le'
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞) (⋃ (i : ℕ), t ∩ s i) : ℝ≥0∞)
    (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ s i) : ℝ≥0∞)

Tactic:
measure_iUnion_le (μ := m) fun i => t ∩ s i

Premises used: Inter.inter, MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞)
h₂ :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i))
    (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ s i))
⊢ 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:
convert! measure_iUnion_le (μ := m) fun i => t ∩ s i using 1

Premises used: Inter.inter, MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), t ∩ s i) : ℝ≥0∞)

Tactic:
simp [inter_iUnion]

Premises used: Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i))
    (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (t ∩ s i))

Tactic:
simp [ENNReal.tsum_eq_iSup_nat, isCaratheodory_sum m h hd]

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_sum, ENNReal.tsum_eq_iSup_nat
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞)

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]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞)
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∞)
⊢ 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:
grw [hp, ENNReal.iSup_add]

Premises used: ENNReal.iSup_add
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞)

Tactic:
iSup_le fun n => ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞)
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
⊢ 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:
refine iSup_le fun n => ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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 : ℕ
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∞)
⊢ 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:
rw [isCaratheodory_iUnion_lt _ (fun i _ => h i) t (n := n)]

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_iUnion_lt
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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 : ℕ
bc : ∀ (i : ℕ), ⋃ (_ : i < n), s i ⊆ s i
⊢ 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:
gcongr with i
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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 i : ℕ
⊢ ⋃ (_ : i < n), s i ⊆ s i

Tactic:
iUnion_subset fun _ => .rfl

Premises used: Set.iUnion_subset, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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 i : ℕ
⊢ ⋃ (_ : i < n), s i ⊆ s i

Tactic:
exact iUnion_subset fun _ => .rfl

Premises used: Set.iUnion_subset, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
rw : m.IsCaratheodory (⋃ (i : ℕ), disjointed s i)
⊢ m.IsCaratheodory (⋃ (i : ℕ), s i)

Tactic:
rw [← iUnion_disjointed]

Premises used: iUnion_disjointed
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ (i : ℕ), disjointed s i)

Tactic:
m.isCaratheodory_iUnion_of_disjoint (m.isCaratheodory_disjointed h)
    (disjoint_disjointed _)

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_disjointed, disjoint_disjointed, MeasureTheory.OuterMeasure.isCaratheodory_iUnion_of_disjoint
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ (i : ℕ), disjointed s i)

Tactic:
exact m.isCaratheodory_iUnion_of_disjoint (m.isCaratheodory_disjointed h)
    (disjoint_disjointed _)

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_disjointed, disjoint_disjointed, MeasureTheory.OuterMeasure.isCaratheodory_iUnion_of_disjoint
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞)

Tactic:
le_antisymm (measure_iUnion_le s) ?_

Premises used: le_antisymm, MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
refine :
  LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
refine le_antisymm (measure_iUnion_le s) ?_

Premises used: le_antisymm, MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
rw :
  LE.le (α := ℝ≥0∞) (⨆ (i : ℕ), ∑ a ∈ Finset.range i, (m : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)

Tactic:
rw [ENNReal.tsum_eq_iSup_nat]

Premises used: ENNReal.tsum_eq_iSup_nat
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞)

Tactic:
iSup_le fun n => ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
refine :
  ∀ (n : ℕ),
    LE.le (α := ℝ≥0∞) (∑ a ∈ Finset.range n, (m : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (⨆ (i : ℕ), ∑ a ∈ Finset.range i, (m : (a : Set α) → ℝ≥0∞) (s a) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)

Tactic:
refine iSup_le fun n => ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
⊢ 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
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞)
⊢ 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

Premises used: Set.inter_univ, Set.univ_inter, Set.inter_comm
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞)
simp :
  LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), 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∞)

Tactic:
simp only [this]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)

Tactic:
m.mono (iUnion₂_subset fun i _ => subset_iUnion _ i)

Premises used: Set.iUnion₂_subset, MeasureTheory.OuterMeasure.mono, Set.subset_iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), ⋃ (_ : i < n), s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)

Tactic:
exact m.mono (iUnion₂_subset fun i _ => subset_iUnion _ i)

Premises used: Set.iUnion₂_subset, MeasureTheory.OuterMeasure.mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
f : ℕ → Set α
h : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), m.IsCaratheodory (f i)
hn : Set α
⊢ (m : (a : Set α) → ℝ≥0∞) hn =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (hn ∩ ⋃ (i : ℕ), f i) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (hn \ ⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
apply isCaratheodory_iUnion m hf

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
apply :
  ∀ (s₁ s₂ : Set α), m.caratheodoryDynkin.Has s₁ → m.caratheodoryDynkin.Has s₂ → m.caratheodoryDynkin.Has (s₁ ∩ s₂)
⊢ MeasurableSpace α

Tactic:
apply MeasurableSpace.DynkinSystem.toMeasurableSpace (caratheodoryDynkin m)

Premises used: MeasurableSpace.DynkinSystem.toMeasurableSpace, MeasureTheory.OuterMeasure.caratheodoryDynkin
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s s₁_1 s₂_1 s₁ s₂ : Set α
⊢ m.caratheodoryDynkin.Has s₁ → m.caratheodoryDynkin.Has s₂ → m.caratheodoryDynkin.Has (s₁ ∩ s₂)

Tactic:
apply isCaratheodory_inter

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : Set α
⊢ MeasurableSet s ↔
    ∀ (t : Set α),
      (m : (a : Set α) → ℝ≥0∞) t =
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
          ((m : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
Iff.rfl

Premises used: MeasurableSet, Iff.rfl, MeasureTheory.OuterMeasure.IsCaratheodory
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : Set α
⊢ MeasurableSet s ↔
    ∀ (t : Set α),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
          ((m : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
        (m : (a : Set α) → ℝ≥0∞) t

Tactic:
isCaratheodory_iff_le' m

Premises used: MeasurableSet, MeasureTheory.OuterMeasure.isCaratheodory_iff_le', MeasureTheory.OuterMeasure.IsCaratheodory
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (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∞)

Tactic:
f_iUnion m h hd

Premises used: MeasureTheory.OuterMeasure.f_iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
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
⊢ MeasurableSet s

Tactic:
apply (isCaratheodory_iff_le _).mpr

Premises used: Iff.mpr, MeasureTheory.OuterMeasure.isCaratheodory_iff_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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

Tactic:
fun t => le_iInf fun f => le_iInf fun hf => ?_

Premises used: iInf, le_iInf, ite
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
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)
⊢ ∀ (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:
refine fun t => le_iInf fun f => le_iInf fun hf => ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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)

Tactic:
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 _ ?_))
      ?_

Premises used: add_le_add, Inter.inter, SDiff.sdiff, iInf_le_of_le, iInf_le, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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
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)
⊢ 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
    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 _ ?_))
      ?_
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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 : ℕ), f i) ∩ s
⊢ t ∩ s ⊆ ⋃ (i : ℕ), (fun (i : ℕ) ↦ f i ∩ s) i

Tactic:
rw [← iUnion_inter]

Premises used: Set.iUnion_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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 : ℕ), f i) ∩ s

Tactic:
inter_subset_inter_left _ hf

Premises used: Set.inter_subset_inter_left
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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 : ℕ), f i) ∩ s

Tactic:
exact inter_subset_inter_left _ hf

Premises used: Set.inter_subset_inter_left
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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_2 : t \ s ⊆ (⋃ (i : ℕ), f i) \ s
⊢ t \ s ⊆ ⋃ (i : ℕ), (fun (i : ℕ) ↦ f i \ s) i

Tactic:
rw [← iUnion_diff]

Premises used: Set.iUnion_diff