mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case intro.m0
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m ∅ = 0

Tactic:
·

Goal state after:
case intro.m0
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m ∅ = 0
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: case e'_4
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), m t = m t

pp: case inr.convert_2
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ m (t ∩ s) + m (t \ s)

Tactic:
·

Goal state after:
case e'_4
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), m t = m t
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∉ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

pp: case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Tactic:
·

Goal state after:
case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∉ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
⊢ ⋂ b ∈ T, f b = ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b

pp: case refine_2
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
⊢ ∀ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b ∈ g b

Tactic:
·

Goal state after:
case refine_1
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
⊢ ⋂ b ∈ T, f b = ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1.mp
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
⊢ a ∈ ⋂ b ∈ T, f b → a ∈ ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b

Tactic:
·

Goal state after:
case refine_1.mp
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
⊢ a ∈ ⋂ b ∈ T, f b → a ∈ ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (inducedOuterMeasure m P0 m0) s ≤ ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht

pp: case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ (inducedOuterMeasure m P0 m0) s

Tactic:
·

Goal state after:
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (inducedOuterMeasure m P0 m0) s ≤ ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
⊢ a ∈ ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b → a ∈ ⋂ b ∈ T, f b

Tactic:
·

Goal state after:
case refine_1.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
⊢ a ∈ ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b → a ∈ ⋂ b ∈ T, f b
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
⊢ ∀ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b ∈ g b

Tactic:
·

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
⊢ ∀ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b ∈ g b
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ (inducedOuterMeasure m P0 m0) s

Tactic:
·

Goal state after:
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ (inducedOuterMeasure m P0 m0) s
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
b : β
h_b : ∃ (x : b ∈ s), ⟨b, ⋯⟩ ∈ T
⊢ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b ∈ g b

Tactic:
obtain ⟨h_b_w, h_b_h⟩ := h_b

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : ⟨b, ⋯⟩ ∈ T
⊢ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b ∈ g b
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} → s ∈ π i ∨ s ∈ {univ}

pp: case refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

Tactic:
·

Goal state after:
case refine_1
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} → s ∈ π i ∨ s ∈ {univ}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

pp: case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

Tactic:
·

Goal state after:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

Tactic:
simp only [ht_eq_i, Finset.mem_singleton, iInter_iInter_eq_left]

Goal state after:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ f i ∈ π i ∨ f i ∈ {univ}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

Tactic:
·

Goal state after:
case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

Tactic:
·

Goal state after:
case refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inl
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

pp: case refine_2.inr
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

Tactic:
·

Goal state after:
case refine_2.inl
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inl.refine_1
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ ↑{i} ⊆ {i}

pp: case refine_2.inl.refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x ∈ {i}
⊢ (fun x ↦ s) x ∈ π x

pp: case refine_2.inl.refine_3
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s = ⋂ x ∈ {i}, (fun x ↦ s) x

Tactic:
·

Goal state after:
case refine_2.inl.refine_1
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ ↑{i} ⊆ {i}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inl.refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x ∈ {i}
⊢ (fun x ↦ s) x ∈ π x

pp: case refine_2.inl.refine_3
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s = ⋂ x ∈ {i}, (fun x ↦ s) x

Tactic:
·

Goal state after:
case refine_2.inl.refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x ∈ {i}
⊢ (fun x ↦ s) x ∈ π x
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inl.refine_3
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s = ⋂ x ∈ {i}, (fun x ↦ s) x

Tactic:
·

Goal state after:
case refine_2.inl.refine_3
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s = ⋂ x ∈ {i}, (fun x ↦ s) x
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inr
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

Tactic:
·

Goal state after:
case refine_2.inr
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ ∀ t ∈ piiUnionInter (fun k ↦ {s k}) S, MeasurableSet t

pp: case refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ {t | ∃ k ∈ S, s k = t} ⊆ piiUnionInter (fun k ↦ {s k}) S

Tactic:
·

Goal state after:
case refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ ∀ t ∈ piiUnionInter (fun k ↦ {s k}) S, MeasurableSet t
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ {t | ∃ k ∈ S, s k = t} ⊆ piiUnionInter (fun k ↦ {s k}) S

Tactic:
·

Goal state after:
case refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ {t | ∃ k ∈ S, s k = t} ⊆ piiUnionInter (fun k ↦ {s k}) S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m ∈ ↑{k}
⊢ m ∈ S

pp: case refine_2.refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
i : ι
x✝ : i ∈ {k}
⊢ s i ∈ (fun k ↦ {s k}) i

pp: case refine_2.refine_3
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k = ⋂ x ∈ {k}, s x

Tactic:
·

Goal state after:
case refine_2.refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m ∈ ↑{k}
⊢ m ∈ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
i : ι
x✝ : i ∈ {k}
⊢ s i ∈ (fun k ↦ {s k}) i

pp: case refine_2.refine_3
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k = ⋂ x ∈ {k}, s x

Tactic:
·

Goal state after:
case refine_2.refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
i : ι
x✝ : i ∈ {k}
⊢ s i ∈ (fun k ↦ {s k}) i
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.refine_3
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k = ⋂ x ∈ {k}, s x

Tactic:
·

Goal state after:
case refine_2.refine_3
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k = ⋂ x ∈ {k}, s x
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
⊢ f1 n ∩ f2 n ∈ π n

pp: case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∉ p2
⊢ f1 n ∩ univ ∈ π n

pp: case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∈ p2
⊢ univ ∩ f2 n ∈ π n

pp: case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∉ p2
⊢ univ ∩ univ ∈ π n

Tactic:
·

Goal state after:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
⊢ f1 n ∩ f2 n ∈ π n
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
⊢ (fun i ↦ ⋃ (_ : i ∈ s), f i) = fun i ↦ ⋃ (_ : i ∈ hs.toFinset), f i

pp: case convert_2
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
⊢ ∑ i ∈ hs.toFinset, μ (f i) < ∞

Tactic:
·

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
⊢ (fun i ↦ ⋃ (_ : i ∈ s), f i) = fun i ↦ ⋃ (_ : i ∈ hs.toFinset), f i
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∉ p2
⊢ f1 n ∩ univ ∈ π n

pp: case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∈ p2
⊢ univ ∩ f2 n ∈ π n

pp: case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∉ p2
⊢ univ ∩ univ ∈ π n

Tactic:
·

Goal state after:
case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∉ p2
⊢ f1 n ∩ univ ∈ π n
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case convert_2
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
⊢ ∑ i ∈ hs.toFinset, μ (f i) < ∞

Tactic:
·

Goal state after:
case convert_2
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
⊢ ∑ i ∈ hs.toFinset, μ (f i) < ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ∞
⊢ μ s < ∞

pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ∞
⊢ μ t < ∞

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ∞
⊢ μ s < ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ∞
⊢ μ t < ∞

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ∞
⊢ μ t < ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ∞
⊢ μ t < ∞

Tactic:
exact (measure_mono Set.subset_union_right).trans_lt h

Goal state after: