mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : 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
⊢ s.indicator f =ᵐ[μ] f

Tactic:
]

Goal state after:
α : 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
⊢ s.indicator f =ᵐ[μ] f
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : 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
⊢ s.indicator f =ᵐ[μ] 0

Tactic:
]

Goal state after:
α : 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
⊢ s.indicator f =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
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 = ∅
i : ℕ
hsi : s i = univ
⊢ μ (s i) < ∞

Tactic:
]

Goal state after:
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 = ∅
i : ℕ
hsi : s i = univ
⊢ μ (s i) < ∞
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ s.indicator f =ᵐ[μ] s.indicator g

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ s.indicator f =ᵐ[μ] s.indicator g
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ ν : Measure α
s✝ t : Set α
a : α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
i : ℕ
⊢ μ (spanningSets μ i ∩ s) < ∞

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ ν : Measure α
s✝ t : Set α
a : α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
i : ℕ
⊢ μ (spanningSets μ i ∩ s) < ∞
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
s : Set α
hxs : x ∈ s
hs : MeasurableSet s
q : (ℕ → Prop) → Prop
hq : s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
this : q fun x_1 ↦ x ∈ A x_1
⊢ (countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1) ⊆ ⋃ p, if q p then countablyGeneratedAtom α p else ∅

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
s : Set α
hxs : x ∈ s
hs : MeasurableSet s
q : (ℕ → Prop) → Prop
hq : s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
this : q fun x_1 ↦ x ∈ A x_1
⊢ (countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1) ⊆ ⋃ p, if q p then countablyGeneratedAtom α p else ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
s : Set α
hs : MeasurableSet s
q : (ℕ → Prop) → Prop
hq : s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
p : ℕ → Prop
hpq : q p
hpx : x ∈ countablyGeneratedAtom α p
this : p = fun x_1 ↦ x ∈ A x_1
⊢ q p

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
s : Set α
hs : MeasurableSet s
q : (ℕ → Prop) → Prop
hq : s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
p : ℕ → Prop
hpq : q p
hpx : x ∈ countablyGeneratedAtom α p
this : p = fun x_1 ↦ x ∈ A x_1
⊢ q p
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case intro.refine_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
n : ℕ
⊢ ∀ a ∈ Finset.univ, (μ a) (⋂ i, spanningSets (μ i) n) < ∞

Tactic:
]

Goal state after:
case intro.refine_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
n : ℕ
⊢ ∀ a ∈ Finset.univ, (μ a) (⋂ i, spanningSets (μ i) n) < ∞
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
⊢ MeasurableSet (countablyGeneratedAtom α fun x_1 ↦ x ∈ natGeneratingSequence α x_1)

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
⊢ MeasurableSet (countablyGeneratedAtom α fun x_1 ↦ x ∈ natGeneratingSequence α x_1)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ x = y

Tactic:
]

Goal state after:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ x = y
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ HasCountableSeparatingOn (↑s) MeasurableSet univ ↔ HasCountableSeparatingOn α MeasurableSet s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ HasCountableSeparatingOn (↑s) MeasurableSet univ ↔ HasCountableSeparatingOn α MeasurableSet s
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
h : CountablySeparated α
s : Set α
⊢ HasCountableSeparatingOn α MeasurableSet s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
h : CountablySeparated α
s : Set α
⊢ HasCountableSeparatingOn α MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case intro.refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
⊢ ⋂ i, ⋃ j, spanningSets (μ i) j = univ

pp: case intro.refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
⊢ ∀ (i : ι), Monotone (spanningSets (μ i))

Tactic:
]

Goal state after:
case intro.refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
⊢ ⋂ i, ⋃ j, spanningSets (μ i) j = univ

case intro.refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
⊢ ∀ (i : ι), Monotone (spanningSets (μ i))
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
b : Set (Set α)
inst✝ : SeparatesPoints α
hbc : b.Countable
hb : inst✝¹ = generateFrom b
⊢ ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
b : Set (Set α)
inst✝ : SeparatesPoints α
hbc : b.Countable
hb : inst✝¹ = generateFrom b
⊢ ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν✝ : Measure α
s t : Set α
a : α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ SigmaFinite (sum fun b ↦ bif b then μ else ν)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν✝ : Measure α
s t : Set α
a : α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ SigmaFinite (sum fun b ↦ bif b then μ else ν)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ ∀ (a : ℕ), Measurable fun x ↦ mapNatBool α x a

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ ∀ (a : ℕ), Measurable fun x ↦ mapNatBool α x a
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
⊢ x = y

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
⊢ x = y
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
⊢ x = y

Tactic:
apply separating_of_generateFrom (range (natGeneratingSequence _))

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
⊢ ∀ s ∈ range (natGeneratingSequence α), x ∈ s ↔ y ∈ s
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ decide (x ∈ natGeneratingSequence α n) = decide (y ∈ natGeneratingSequence α n)

pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ Decidable (x ∈ natGeneratingSequence α n)

pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ Decidable (y ∈ natGeneratingSequence α n)

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ decide (x ∈ natGeneratingSequence α n) = decide (y ∈ natGeneratingSequence α n)

α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ Decidable (x ∈ natGeneratingSequence α n)

α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : CountablyGenerated α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ Decidable (y ∈ natGeneratingSequence α n)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case measurable_invFun
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯) '' natGeneratingSequence α n)

Tactic:
]

Goal state after:
case measurable_invFun
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯) '' natGeneratingSequence α n)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case measurable_invFun
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ ⇑(Equiv.ofInjective (mapNatBool α) ⋯) ⁻¹' Subtype.val ⁻¹' {y | y n = true} = natGeneratingSequence α n

Tactic:
]

Goal state after:
case measurable_invFun
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ ⇑(Equiv.ofInjective (mapNatBool α) ⋯) ⁻¹' Subtype.val ⁻¹' {y | y n = true} = natGeneratingSequence α n
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet (f ⁻¹' {f x})

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet (f ⁻¹' {f x})
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s \ t n ∪ s ∩ t n)

Tactic:
]

Goal state after:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s \ t n ∪ s ∩ t n)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s \ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s \ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
h : SigmaFinite (Measure.map f μ)
⊢ univ = univ

Tactic:
]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
n : ℕ
⊢ μ (f ⁻¹' f '' spanningSets μ n ∪ f ⁻¹' (range f)ᶜ) < ∞

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
n : ℕ
⊢ μ (f ⁻¹' f '' spanningSets μ n ∪ f ⁻¹' (range f)ᶜ) < ∞
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.compl.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ⋃₀ (memPartition t n \ ↑S) ⊔ ⋃₀ ↑S = ⊤

Tactic:
]

Goal state after:
case refine_1.compl.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ⋃₀ (memPartition t n \ ↑S) ⊔ ⋃₀ ↑S = ⊤
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.compl.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ⋃₀ memPartition t n = ⋃₀ memPartition t n

Tactic:
]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ univ = univ

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ ν : Measure α
s✝ t✝ : Set α
a : α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : IsLocallyFiniteMeasure μ
s : α → Set α
hsx : ∀ (x : α), s x ∈ 𝓝 x
hsμ : ∀ (x : α), μ (s x) < ∞
t : Set α
htc : t.Countable
htU : ⋃ x ∈ t, s x = univ
⊢ ⋃ a ∈ t, s a = univ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ ν : Measure α
s✝ t✝ : Set α
a : α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : IsLocallyFiniteMeasure μ
s : α → Set α
hsx : ∀ (x : α), s x ∈ 𝓝 x
hsμ : ∀ (x : α), μ (s x) < ∞
t : Set α
htc : t.Countable
htU : ⋃ x ∈ t, s x = univ
⊢ ⋃ a ∈ t, s a = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
hS_eq : s = ⋃₀ ↑S
⊢ MeasurableSet (⋃ i ∈ ↑S, i)

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
hS_eq : s = ⋃₀ ↑S
⊢ MeasurableSet (⋃ i ∈ ↑S, i)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
i : ι
⊢ (μ i) {x | f x ≠ mk f ⋯ x} = 0

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
i : ι
⊢ (μ i) {x | f x ≠ mk f ⋯ x} = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
⊢ MeasurableSet (⋃ u ∈ memPartition t n, u ∩ t n)

Tactic:
]

Goal state after:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
⊢ MeasurableSet (⋃ u ∈ memPartition t n, u ∩ t n)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ v ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}

Tactic:
]

Goal state after:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ v ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
⊢ Measurable ((⋂ i, s i).domRestrict (const α default))

Tactic:
]

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
⊢ Measurable ((⋂ i, s i).domRestrict (const α default))
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
i : ι
hi : i ∈ F
C : Finset ι
x : α
hx : (∀ i ∈ C, x ∈ s i) ∧ ∀ i ∈ F \ C, x ∈ (s i)ᶜ
hxs : x ∈ s i
⊢ i ∈ C

Tactic:
]

Goal state after:
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
i : ι
hi : i ∈ F
C : Finset ι
x : α
hx : (∀ i ∈ C, x ∈ s i) ∧ ∀ i ∈ F \ C, x ∈ (s i)ᶜ
hxs : x ∈ s i
⊢ i ∈ C
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.zero
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u = univ
⊢ MeasurableSet univ

Tactic:
]

Goal state after:
case refine_1.zero
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u = univ
⊢ MeasurableSet univ