awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
inst_2 : Countable ι
μ : F
s : ι → Set α
hs : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
t : Finset ι
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : { i : ι // i ∉ t }), s (↑i : ι)) : ℝ≥0∞)
    (∑' (i : { i : ι // i ∉ t }), (μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)) : ℝ≥0∞)

Tactic:
measure_iUnion_le _

Premises used: MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
inst_2 : Countable ι
μ : F
s : ι → Set α
hs : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
t : Finset ι
μ₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : { i : ι // i ∉ t }), s (↑i : ι)) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
    (∑' (b : { x : ι // x ∉ t }), (μ : (a : Set α) → ℝ≥0∞) (s (↑b : ι)) : ℝ≥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 _

Premises used: Filter.limsup, MeasureTheory.measure_iUnion_le, Filter.cofinite, Subtype.val, DFunLike.coe, Set.iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (limsup s atTop) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← Nat.cofinite_eq_atTop, measure_limsup_cofinite_eq_zero hs]

Premises used: MeasureTheory.measure_limsup_cofinite_eq_zero, Nat.cofinite_eq_atTop
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
inst_2 : Countable ι
μ : F
s : ι → Set α
h : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Set.Finite.{u_2} (α := ι) {i : ι | a ∈ s i}} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, Set.Finite.{u_2} (α := ι) {i : ι | x ∈ s i}

Tactic:
rw [ae_iff, ← measure_limsup_cofinite_eq_zero h]

Premises used: MeasureTheory.measure_limsup_cofinite_eq_zero, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
inst_2 : Countable ι
μ : F
s : ι → Set α
h : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
h₁ :
  ∀ (x : α),
    Membership.mem (γ := Set α) {a : α | ¬Set.Finite.{u_2} (α := ι) {i : ι | a ∈ s i}} x ↔ x ∈ limsup s cofinite
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Set.Finite.{u_2} (α := ι) {i : ι | a ∈ s i}} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)

Tactic:
congr 1 with x
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
inst_2 : Countable ι
μ : F
s : ι → Set α
h : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
x : α
⊢ Membership.mem (γ := Set α) {a : α | ¬Set.Finite.{u_2} (α := ι) {i : ι | a ∈ s i}} x ↔ x ∈ limsup s cofinite

Tactic:
simp [mem_limsup_iff_frequently_mem, Filter.Frequently]

Premises used: Filter.Frequently, Filter.mem_limsup_iff_frequently_mem
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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
p : ℕ → α → Prop
hp : Ne (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) {x : α | p i x}) ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ∃ᶠ (n : ℕ) in atTop, p n x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa only [limsup_eq_iInf_iSup_of_nat, frequently_atTop, ← bex_def, setOf_forall,
    setOf_exists] using measure_limsup_atTop_eq_zero hp

Premises used: Filter.frequently_atTop, bex_def, Set.setOf_exists, MeasureTheory.measure_limsup_atTop_eq_zero, Filter.limsup_eq_iInf_iSup_of_nat, Set.setOf_forall
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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)) ∞
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (n : ℕ) in atTop, x ∉ s n

Tactic:
measure_setOf_frequently_eq_zero hs

Premises used: MeasureTheory.measure_setOf_frequently_eq_zero, Set.Mem, Filter.Eventually, setOf, Set.Subset, Filter.Frequently
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
inst_2 : Countable ι
μ : F
inst_3 : Infinite ι
s : ι → Set α
h : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
rw :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (liminf s cofinite) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (liminf s cofinite) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero, ← measure_limsup_cofinite_eq_zero h]

Premises used: MeasureTheory.measure_limsup_cofinite_eq_zero, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
inst_2 : Countable ι
μ : F
inst_3 : Infinite ι
s : ι → Set α
h : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (liminf s cofinite) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)

Tactic:
measure_mono liminf_le_limsup

Premises used: Filter.liminf_le_limsup, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
Goal:
α : Type u_1
ι : Type u_2
F : Type u_3
inst : FunLike.{u_3 + 1, u_1 + 1, 1} F (Set α) ℝ≥0∞
inst_1 : OuterMeasureClass F α
inst_2 : Countable ι
μ : F
inst_3 : Infinite ι
s : ι → Set α
h : Ne (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (s i)) ∞
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (liminf s cofinite) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (limsup s cofinite) : ℝ≥0∞)

Tactic:
exact measure_mono liminf_le_limsup

Premises used: Filter.liminf_le_limsup, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (liminf s atTop) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← Nat.cofinite_eq_atTop, measure_liminf_cofinite_eq_zero h]

Premises used: MeasureTheory.measure_liminf_cofinite_eq_zero, Nat.cofinite_eq_atTop
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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
⊢ ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t

Tactic:
simp only [eventuallyEq_set, ← eventually_countable_forall] at h

Premises used: Filter.eventuallyEq_set, eventually_countable_forall
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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

Tactic:
eventuallyEq_set.2 <| h.mono fun x hx ↦ ?_

Premises used: Iff.mpr, Filter.eventuallyEq_set, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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
refine : ∀ (x : α) (hx : ∀ (i : ℕ), x ∈ s i ↔ x ∈ t), x ∈ limsup s atTop ↔ x ∈ t
⊢ limsup s atTop =ᶠ[ae μ] t

Tactic:
refine eventuallyEq_set.2 <| h.mono fun x hx ↦ ?_

Premises used: Iff.mpr, Filter.eventuallyEq_set, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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
x : α
hx : ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
⊢ x ∈ limsup s atTop ↔ x ∈ t

Tactic:
simp [mem_limsup_iff_frequently_mem, hx]

Premises used: Filter.mem_limsup_iff_frequently_mem
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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

Tactic:
eventuallyEq_set.2 <| h.mono fun x hx ↦ ?_

Premises used: Iff.mpr, Filter.eventuallyEq_set, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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
refine : ∀ (x : α) (hx : ∀ (i : ℕ), x ∈ s i ↔ x ∈ t), x ∈ liminf s atTop ↔ x ∈ t
⊢ liminf s atTop =ᶠ[ae μ] t

Tactic:
refine eventuallyEq_set.2 <| h.mono fun x hx ↦ ?_

Premises used: Iff.mpr, Filter.eventuallyEq_set, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
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
x : α
hx : ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
⊢ x ∈ liminf s atTop ↔ x ∈ t

Tactic:
simp only [mem_liminf_iff_eventually_mem, hx, eventually_const]

Premises used: Filter.eventually_const, Filter.mem_liminf_iff_eventually_mem
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : Set α
⊢ m.IsCaratheodory 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:
forall_congr' fun _ => le_antisymm_iff.trans <| and_iff_right <| measure_le_inter_add_diff _ _ _

Premises used: MeasureTheory.OuterMeasure.IsCaratheodory, MeasureTheory.measure_le_inter_add_diff, and_iff_right, le_antisymm_iff, forall_congr', Iff.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
⊢ m.IsCaratheodory ∅

Tactic:
simp [IsCaratheodory, diff_empty]

Premises used: MeasureTheory.OuterMeasure.IsCaratheodory, Set.diff_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s₁ : Set α
⊢ m.IsCaratheodory s₁ → m.IsCaratheodory s₁ᶜ

Tactic:
simp [IsCaratheodory, diff_eq, add_comm]

Premises used: MeasureTheory.OuterMeasure.IsCaratheodory, Set.diff_eq, add_comm
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : Set α
h : m.IsCaratheodory sᶜ
⊢ m.IsCaratheodory s

Tactic:
simpa using isCaratheodory_compl m h

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_compl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
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∞)
⊢ (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∞)

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₁)]

Premises used: Set.union_diff_left, Inter.inter, Set.subset_union_left, SDiff.sdiff, Set.inter_eq_self_of_subset_right, Set.inter_diff_assoc, Union.union, Set.inter_assoc
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ 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:
simp [diff_eq, add_assoc]

Premises used: add_assoc, Set.diff_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
h : ∀ i ∈ t, m.IsCaratheodory (s i)
⊢ t.Finite

Tactic:
ht
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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 ι) (h : ∀ i ∈ (↑t : Set ι), m.IsCaratheodory (s i)), m.IsCaratheodory (⋃ i ∈ (↑t : Set ι), s i)
⊢ m.IsCaratheodory (⋃ i ∈ t, s i)

Tactic:
lift t to Finset ι using ht

Premises used: Finset
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
h : ∀ i ∈ (↑∅ : Set ι), m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ (↑∅ : Set ι), s i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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.insert i t) : Set ι), m.IsCaratheodory (s i_1)
insert : ∀ (h : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ t → m.IsCaratheodory (s i_1)), m.IsCaratheodory (s i ∪ ⋃ x ∈ t, s x)
⊢ m.IsCaratheodory (⋃ i_1 ∈ (↑(Insert.insert i t) : Set ι), s i_1)

Tactic:
simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢

Premises used: Finset.mem_insert, Set.iUnion_iUnion_eq_or_left, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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 : ι), i_1 = i ∨ i_1 ∈ t → m.IsCaratheodory (s i_1)
⊢ m.IsCaratheodory (s i ∪ ⋃ x ∈ t, s x)

Tactic:
m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_union, Or.inl, Or.inr, rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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 : ι), i_1 = i ∨ i_1 ∈ t → m.IsCaratheodory (s i_1)
⊢ m.IsCaratheodory (s i ∪ ⋃ x ∈ t, s x)

Tactic:
exact m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_union, Or.inl, Or.inr, rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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)
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.insert i t) : Set ι), m.IsCaratheodory (s i_1)),
    m.IsCaratheodory (⋃ i_1 ∈ (↑(Insert.insert i t) : Set ι), s i_1)
⊢ m.IsCaratheodory (⋃ i ∈ (↑t : 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)

Premises used: Insert.insert, Finset.mem_insert, Set.iUnion_iUnion_eq_or_left, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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)
lift₁ : ∀ (t : Finset ι) (h : ∀ i ∈ (↑t : Set ι), m.IsCaratheodory (s i)), m.IsCaratheodory (⋃ i ∈ (↑t : Set ι), s i)
⊢ m.IsCaratheodory (⋃ i ∈ t, 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)

Premises used: Finset, Insert.insert, Finset.mem_insert, Set.iUnion_iUnion_eq_or_left, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
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∞)
rw₄ 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∞)
⊢ (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∞)

Tactic:
rw [h₁, Set.inter_assoc, Set.union_inter_cancel_left, inter_diff_assoc, union_diff_cancel_left h]

Premises used: Set.union_inter_cancel_left, Set.union_diff_cancel_left, Set.inter_diff_assoc, Set.inter_assoc
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ i < 0, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ (i : ℕ), ⋃ (_ : i < 0), s i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
n : ℕ
h : ∀ i < n + 1, m.IsCaratheodory (s i)
rw : m.IsCaratheodory ((⋃ (k : ℕ), ⋃ (_ : k < n), s k) ∪ s n)
⊢ m.IsCaratheodory (⋃ (i : ℕ), ⋃ (_ : i < n + 1), s i)

Tactic:
rw [biUnion_lt_succ]

Premises used: Set.biUnion_lt_succ
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
n : ℕ
h : ∀ i < n + 1, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory ((⋃ (k : ℕ), ⋃ (_ : k < n), s k) ∪ s n)

Tactic:
isCaratheodory_union m
            (isCaratheodory_iUnion_lt fun i hi => h i <| lt_of_lt_of_le hi <| Nat.le_succ _)
            (h n (le_refl (n + 1)))

Premises used: le_refl, MeasureTheory.OuterMeasure.isCaratheodory_union, Nat.le_succ, HAdd.hAdd, OfNat.ofNat, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
n : ℕ
h : ∀ i < n + 1, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory ((⋃ (k : ℕ), ⋃ (_ : k < n), s k) ∪ s n)

Tactic:
exact isCaratheodory_union m
            (isCaratheodory_iUnion_lt fun i hi => h i <| lt_of_lt_of_le hi <| Nat.le_succ _)
            (h n (le_refl (n + 1)))

Premises used: le_refl, MeasureTheory.OuterMeasure.isCaratheodory_union, Nat.le_succ, HAdd.hAdd, OfNat.ofNat, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
rw : m.IsCaratheodory (s₁ᶜ ∪ s₂ᶜ)
⊢ m.IsCaratheodory (s₁ ∩ s₂)

Tactic:
rw [← isCaratheodory_compl_iff, Set.compl_inter]

Premises used: Set.compl_inter, MeasureTheory.OuterMeasure.isCaratheodory_compl_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
⊢ m.IsCaratheodory (s₁ᶜ ∪ s₂ᶜ)

Tactic:
isCaratheodory_union _ (isCaratheodory_compl _ h₁) (isCaratheodory_compl _ h₂)

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_union, MeasureTheory.OuterMeasure.isCaratheodory_compl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
⊢ m.IsCaratheodory (s₁ᶜ ∪ s₂ᶜ)

Tactic:
exact isCaratheodory_union _ (isCaratheodory_compl _ h₁) (isCaratheodory_compl _ h₂)

Premises used: MeasureTheory.OuterMeasure.isCaratheodory_union, MeasureTheory.OuterMeasure.isCaratheodory_compl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory
Goal:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
⊢ m.IsCaratheodory (s₁ \ s₂)

Tactic:
m.isCaratheodory_inter h₁ (m.isCaratheodory_compl h₂)

Premises used: Set.Mem, Set.diff, MeasureTheory.OuterMeasure.isCaratheodory_inter, setOf, MeasureTheory.OuterMeasure.isCaratheodory_compl, Not
-- 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 (((partialSups s : OrderHom.{u_1, u} ι (Set α)) : (a : ι) → Set α) i)

Tactic:
simpa only [partialSups_apply, Finset.sup'_eq_sup, Finset.sup_set_eq_biUnion, ← Finset.mem_coe,
    Finset.coe_Iic] using .biUnion_of_finite (finite_Iic _) (fun j _ ↦ h j)

Premises used: partialSups_apply, Finset.coe_Iic, Finset.sup_set_eq_biUnion, Finset.sup'_eq_sup, Finset.mem_coe