mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case inr
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
x : α
hts : {x} ⊆ s
ht : {x}.Subsingleton
htl : {x} ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
·

Goal state after:
case inr
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
x : α
hts : {x} ⊆ s
ht : {x}.Subsingleton
htl : {x} ∈ l
⊢ ∃ a ∈ s, {a} ∈ l
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (ht.choose ∩ s) = μ (t ∩ s)

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ¬∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (A.choose ∩ s) = μ (t ∩ s)

Tactic:
·

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (ht.choose ∩ s) = μ (t ∩ s)
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case inl
α : Type u_1
l : Filter α
inst✝² : CountableInterFilter l
inst✝¹ : Nonempty α
p : Set α → Prop
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
inst✝ : HasCountableSeparatingOn α p ∅
hs : ∅ ∈ l
⊢ ∃ a, {a} ∈ l

pp: case inr
α : Type u_1
l : Filter α
inst✝² : CountableInterFilter l
inst✝¹ : Nonempty α
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hne : s.Nonempty
⊢ ∃ a, {a} ∈ l

Tactic:
·

Goal state after:
case inl
α : Type u_1
l : Filter α
inst✝² : CountableInterFilter l
inst✝¹ : Nonempty α
p : Set α → Prop
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
inst✝ : HasCountableSeparatingOn α p ∅
hs : ∅ ∈ l
⊢ ∃ a, {a} ∈ l
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
⊢ x ∈ iUnion t'

pp: case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t' n) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)

Tactic:
·

Goal state after:
case refine_1.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
⊢ x ∈ iUnion t'
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case inr
α : Type u_1
l : Filter α
inst✝² : CountableInterFilter l
inst✝¹ : Nonempty α
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hne : s.Nonempty
⊢ ∃ a, {a} ∈ l

Tactic:
·

Goal state after:
case inr
α : Type u_1
l : Filter α
inst✝² : CountableInterFilter l
inst✝¹ : Nonempty α
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hne : s.Nonempty
⊢ ∃ a, {a} ∈ l
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
A : t' ∩ s =ᵐ[μ] t ∩ s
⊢ NullMeasurableSet (t ∩ s) μ

Tactic:
obtain ⟨s', -, hs', s's⟩ : ∃ s' ⊇ s, MeasurableSet s' ∧ s' =ᵐ[μ] s :=
      hs.exists_measurable_superset_ae_eq

Goal state after:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
A : t' ∩ s =ᵐ[μ] t ∩ s
s' : Set α
hs' : MeasurableSet s'
s's : s' =ᵐ[μ] s
⊢ NullMeasurableSet (t ∩ s) μ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ¬∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (A.choose ∩ s) = μ (t ∩ s)

Tactic:
·

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ¬∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (A.choose ∩ s) = μ (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
⊢ NullMeasurableSet t (μ.restrict s)

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
⊢ NullMeasurableSet t (μ.restrict s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∈ t
⊢ x ∈ iUnion t'

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∉ t
⊢ x ∈ iUnion t'

Tactic:
·

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∈ t
⊢ x ∈ iUnion t'
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∉ t
⊢ x ∈ iUnion t'

Tactic:
·

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∉ t
⊢ x ∈ iUnion t'
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ s ⊆ ⋃ y ∈ s, measurableAtom y

pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ ⋃ y ∈ s, measurableAtom y ⊆ s

Tactic:
·

Goal state after:
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ s ⊆ ⋃ y ∈ s, measurableAtom y
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ ⋃ y ∈ s, measurableAtom y ⊆ s

Tactic:
·

Goal state after:
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ ⋃ y ∈ s, measurableAtom y ⊆ s
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
p : ℕ → Prop
⊢ MeasurableSet (countablyGeneratedAtom α p)

Tactic:
refine MeasurableSet.iInter fun n ↦ ?_
  exact MeasurableSet.ite' (fun _ ↦ measurableSet_natGeneratingSequence n)
    (fun _ ↦ (measurableSet_natGeneratingSequence n).compl)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t' n) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)

Tactic:
·

Goal state after:
case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t' n) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ volume (Subtype.val '' univ) = volume u

pp: δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ Injective Subtype.val

pp: δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ ∀ (s : Set { x // x ∈ u }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume

Tactic:
·

Goal state after:
δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ volume (Subtype.val '' univ) = volume u
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ Injective Subtype.val

pp: δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ ∀ (s : Set { x // x ∈ u }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume

Tactic:
·

Goal state after:
δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ Injective Subtype.val
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ ∀ (s : Set { x // x ∈ u }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume

Tactic:
·

Goal state after:
δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ ∀ (s : Set { x // x ∈ u }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ t ∈ range (natGeneratingSequence α), MeasurableSet t → ∃ q, t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∃ q, ∅ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

pp: case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (t : Set α),
    MeasurableSet t →
      (∃ q, t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
        ∃ q, tᶜ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

pp: case refine_4
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n : ℕ), ∃ q, s n = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
        ∃ q, ⋃ i, s i = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ t ∈ range (natGeneratingSequence α), MeasurableSet t → ∃ q, t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
hx : x ∈ natGeneratingSequence α n
⊢ ∃ i, i n ∧ x ∈ countablyGeneratedAtom α i

pp: case refine_1.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
⊢ (∃ i, i n ∧ x ∈ countablyGeneratedAtom α i) → x ∈ natGeneratingSequence α n

Tactic:
·

Goal state after:
case refine_1.refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
hx : x ∈ natGeneratingSequence α n
⊢ ∃ i, i n ∧ x ∈ countablyGeneratedAtom α i
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
hx : x ∈ natGeneratingSequence α n
⊢ ∃ i, i n ∧ x ∈ countablyGeneratedAtom α i

Tactic:
exact ⟨(x ∈ natGeneratingSequence α ·), by simp [countablyGeneratedAtom]; grind⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
hμ : ∀ (a : α), μ {a} < ∞
h✝ : IsEmpty α
⊢ SigmaFinite μ

pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
hμ : ∀ (a : α), μ {a} < ∞
h✝ : Nonempty α
⊢ SigmaFinite μ

Tactic:
·

Goal state after:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
hμ : ∀ (a : α), μ {a} < ∞
h✝ : IsEmpty α
⊢ SigmaFinite μ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
⊢ (∃ i, i n ∧ x ∈ countablyGeneratedAtom α i) → x ∈ natGeneratingSequence α n

Tactic:
·

Goal state after:
case refine_1.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
⊢ (∃ i, i n ∧ x ∈ countablyGeneratedAtom α i) → x ∈ natGeneratingSequence α n
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
hμ : ∀ (a : α), μ {a} < ∞
h✝ : Nonempty α
⊢ SigmaFinite μ

Tactic:
·

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
hμ : ∀ (a : α), μ {a} < ∞
h✝ : Nonempty α
⊢ SigmaFinite μ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∃ q, ∅ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

pp: case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (t : Set α),
    MeasurableSet t →
      (∃ q, t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
        ∃ q, tᶜ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

pp: case refine_4
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n : ℕ), ∃ q, s n = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
        ∃ q, ⋃ i, s i = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∃ q, ∅ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (t : Set α),
    MeasurableSet t →
      (∃ q, t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
        ∃ q, tᶜ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

pp: case refine_4
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n : ℕ), ∃ q, s n = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
        ∃ q, ⋃ i, s i = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (t : Set α),
    MeasurableSet t →
      (∃ q, t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
        ∃ q, tᶜ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case pos
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : univ = ∅
⊢ μ univ < ∞

pp: case neg
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
⊢ μ univ < ∞

Tactic:
·

Goal state after:
case pos
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : univ = ∅
⊢ μ univ < ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ min (μ (t' 0)) (ν (t' 0)) + min (μ (t' 1)) (ν (t' 1)) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)

pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∀ (x : ℕ), (if x = 1 then 0 else if x = 0 then 0 else min (μ (t' x)) (ν (t' x))) = 0

Tactic:
·

Goal state after:
case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ min (μ (t' 0)) (ν (t' 0)) + min (μ (t' 1)) (ν (t' 1)) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_3.refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
h : ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i
⊢ ∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i

pp: case refine_3.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
⊢ (∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i) → ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i

Tactic:
·

Goal state after:
case refine_3.refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
h : ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i
⊢ ∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_3.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
⊢ (∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i) → ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i

Tactic:
·

Goal state after:
case refine_3.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
⊢ (∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i) → ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
·

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
hxs : x ∈ s
⊢ s.indicator f x = f x

pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
hxs : x ∉ s
⊢ s.indicator f x = f x

Tactic:
·

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
hxs : x ∈ s
⊢ s.indicator f x = f x