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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
⊢ ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
⊢ Injective f → ∃ x, MeasurableSet x ∧ ¬NullMeasurableSet (f '' x) μ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ μ (s ∆ t) = μ (s \ t) + μ (t \ s)

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ μ (s \ t ∪ t \ s) = μ (s \ t) + μ (t \ s)
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ a ≤ c

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ a ≤ c
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ c < b

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ c < b
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ b ≤ a

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ b ≤ a
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ∪ t =ᵐ[μ] s
⊢ μ (t \ s) = 0

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ∪ t =ᵐ[μ] s
⊢ μ (t \ s) = 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᵐ[μ] t
h₂ : μ t ≤ μ s
hsm : NullMeasurableSet s μ
ht : μ t ≠ ∞
⊢ μ (t \ s) = 0

Tactic:
replace h₂ : μ t = μ s := h₂.antisymm (measure_mono_ae h₁)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : NullMeasurableSet s μ
ht : μ t ≠ ∞
h₂ : μ t = μ s
⊢ μ (t \ s) = 0
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
b' : Xᵒᵈ
hb' : b' < toDual a
⊢ ∃ a_1 < toDual a, Ioo a_1 (toDual a) ⊆ ⇑ofDual ⁻¹' s

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
b' : Xᵒᵈ
hb' : b' < toDual a
⊢ ∃ a_1, a < a_1 ∧ Ioo a a_1 ⊆ s
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✝¹ : SFinite μ
inst✝ : SFinite ν
this : ∀ (b : Bool), SFinite (bif b then μ else ν)
⊢ SFinite (μ + ν)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
this : ∀ (b : Bool), SFinite (bif b then μ else ν)
⊢ SFinite (μ + ν)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
μ : Measure α
hs : Fact (μ s < ∞)
⊢ (μ.restrict s) univ < ∞

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
μ : Measure α
hs : Fact (μ s < ∞)
⊢ μ s < ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
T : ℕ → Set α := fun n ↦ toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
I : Finset ℕ
N : ℕ
hN : ∀ i ∈ I, t i ⊆ t N
⊢ ∑ n ∈ I, μ (Td n) ≤ ⨆ n, μ (t n)

Tactic:
calc
        (∑ n ∈ I, μ (Td n)) = μ (⋃ n ∈ I, Td n) :=
          (measure_biUnion_finset ((disjoint_disjointed T).set_pairwise I) fun n _ => hm n).symm
        _ ≤ μ (⋃ n ∈ I, T n) := measure_mono (iUnion₂_mono fun n _hn => disjointed_subset _ _)
        _ = μ (⋃ n ∈ I, t n) := measure_biUnion_toMeasurable I.countable_toSet _
        _ ≤ μ (t N) := measure_mono (iUnion₂_subset hN)
        _ ≤ ⨆ n, μ (t n) := le_iSup (μ ∘ t) N

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ∞
this : ∀ {s : Set α}, (sum fun n ↦ c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0
⊢ (sum fun n ↦ c n • sfiniteSeq μ n) univ < ∞

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ∞
this : ∀ {s : Set α}, (sum fun n ↦ c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0
⊢ ∑' (i : ℕ), ↑(c i) * (sfiniteSeq μ i) univ < ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
hμ : measureUnivNNReal μ ≤ 0
⊢ μ = 0

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
hμ : measureUnivNNReal μ ≤ 0
⊢ μ = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
hm : ∀ t ∈ C, MeasurableSet t
ht : ∀ t ∈ C, (μ.restrict t) s = 0
t : Set α
htc : t ∈ C
⊢ μ (s ∩ t) = 0

Tactic:
simpa using

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
hm : ∀ t ∈ C, MeasurableSet t
ht : ∀ t ∈ C, (μ.restrict t) s = 0
t : Set α
htc : t ∈ C
⊢ (μ.restrict t) s = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

Tactic:
simpa using

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ.restrict (s ∩ t) + μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i✝ : ι
hi : μ (s i✝) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
i : ι
ω : α
hω : Monotone fun x ↦ ω ∈ s x
⊢ ω ∈ s i ↔ ω ∈ t i

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i✝ : ι
hi : μ (s i✝) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
i : ι
ω : α
hω : Monotone fun x ↦ ω ∈ s x
⊢ ω ∈ s i → Monotone fun x ↦ ω ∈ s x
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s s' t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (s ∪ s')) t ≤ (μ.restrict s + μ.restrict s') t

Tactic:
simpa using

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s s' t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ s ∪ t ∩ s') ≤ μ (t ∩ s) + μ (t ∩ s')
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ μ.restrict (toMeasurable μ s) = μ.restrict s

Tactic:
simpa using

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ μ.restrict (toMeasurable μ s) = μ.restrict s
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
⊢ ∃ s, x ∈ s ∧ IsOpen[inst✝¹] s ∧ μ s < ∞

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
⊢ ∃ s, x ∈ s ∧ IsOpen[inst✝¹] s ∧ μ s < ∞
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
⊢ μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i) ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)

Tactic:
refine ⟨fun h i => restrict_congr_mono (subset_iUnion _ _) h, fun h => ?_⟩
  ext1 t ht
  have D : Directed (· ⊆ ·) fun t : Finset ι => ⋃ i ∈ t, s i :=
    Monotone.directed_le fun t₁ t₂ ht => biUnion_subset_biUnion_left ht
  rw [iUnion_eq_iUnion_finset]
  simp only [restrict_iUnion_apply_eq_iSup D ht, restrict_biUnion_finset_congr.2 fun i _ => h i]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
⊢ (∀ a ∈ s, ∃ t ∈ 𝓝[s] a, μ t = 0) → μ s = 0

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
⊢ (∀ a ∈ s, ∃ t ∈ 𝓝[s] a, tᶜ ∈ ae μ) → sᶜ ∈ ae μ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i, s i)) t ≤ (sum fun i ↦ μ.restrict (s i)) t

Tactic:
simpa using

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
t : Set α
ht : MeasurableSet t
⊢ μ (⋃ i, t ∩ s i) ≤ ∑' (i : ι), μ (t ∩ s i)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
T : Set ι
hT : Countable ↑T
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i ∈ T, s i)) t ≤ (sum fun i ↦ μ.restrict (s ↑i)) t

Tactic:
simpa using

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
T : Set ι
hT : Countable ↑T
t : Set α
ht : MeasurableSet t
⊢ μ (⋃ i ∈ T, t ∩ s i) ≤ ∑' (i : ↑T), μ (t ∩ s ↑i)
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case h
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : (range S).Nonempty
hSc : (range S).Countable
hS : (∀ s ∈ range S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ range S, x ∈ s ↔ y ∈ s) → x = y
⊢ (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Tactic:
simpa using

Goal state after:
case h
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : (range S).Nonempty
hSc : (range S).Countable
hS : (∀ s ∈ range S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ range S, x ∈ s ↔ y ∈ s) → x = y
⊢ (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
h : (μ.restrict s) {a | ¬p a} = 0
⊢ μ {a | ¬(a ∈ s → p a)} = 0

Tactic:
simpa using

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
h : (μ.restrict s) {a | ¬p a} = 0
⊢ μ (s ∩ {a | ¬p a}) = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f / g =ᵐ[μ] 1
x : α
hx : (f / g) x = 1 x
⊢ f x = g x

Tactic:
rwa [Pi.div_apply, Pi.one_apply, div_eq_one] at hx

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

Goal state before:
pp: α : 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
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t') = (x ∈ t)
y : α
hy : y ∈ s → (y ∈ t') = (y ∈ t)
⊢ (y ∈ t' ∩ s) = (y ∈ t ∩ s)

Tactic:
simpa using

Goal state after:
α : 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
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t') = (x ∈ t)
y : α
hy : y ∈ s → (y ∈ t') = (y ∈ t)
⊢ y ∈ s → (y ∈ t' ↔ y ∈ t)
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) μ
A : NullMeasurableSet (t \ s) (μ.restrict s)
B : NullMeasurableSet (t ∩ s) (μ.restrict s)
⊢ NullMeasurableSet t (μ.restrict s)

Tactic:
simpa using

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

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

Tactic:
apply Subset.antisymm

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

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: case h₁
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ x ∈ ⋃ y ∈ s, measurableAtom y

Tactic:
simpa using

Goal state after:
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ ∃ i ∈ s, x ∈ measurableAtom i
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case hC
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
t' : Set ↑s
ht' : t' ∈ {t | ∃ s_1, MeasurableSet s_1 ∧ Subtype.val ⁻¹' s_1 = t}
ht✝ : MeasurableSet t'
⊢ NullMeasurableSet (Subtype.val '' t') μ

Tactic:
obtain ⟨s', hs', rfl⟩ := ht'
    rw [Subtype.image_preimage_coe]
    exact hs.inter (hs'.nullMeasurableSet)

Goal state after:
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 : α
p : ℕ → Prop
hpn : p n
hpx : x ∈ if p n then natGeneratingSequence α n else (natGeneratingSequence α n)ᶜ
⊢ x ∈ natGeneratingSequence α n

Tactic:
simpa using

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 : α
p : ℕ → Prop
hpn : p n
hpx : x ∈ if p n then natGeneratingSequence α n else (natGeneratingSequence α n)ᶜ
⊢ x ∈ natGeneratingSequence α n
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
hμ : ∀ (a : α), μ {a} < ∞
h✝ : Nonempty α
f : ℕ → α
hf : Surjective f
⊢ ∀ (i : ℕ), μ {f i} < ∞

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
hμ : ∀ (a : α), μ {a} < ∞
h✝ : Nonempty α
f : ℕ → α
hf : Surjective f
⊢ ∀ (i : ℕ), μ {f i} < ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : 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 = ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
⊢ ∀ (i : ℕ), s i = ∅

Tactic:
simpa using

Goal state after:
α : 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 = ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
⊢ ∀ (i : ℕ), 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
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
⊢ s.indicator f x = s.indicator g x

Tactic:
by_cases hxs : x ∈ s
    · simp [hxs, hx hxs]
    · simp [hxs]

Goal state after:
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
h : s.indicator f =ᵐ[μ] s.indicator g
x : α
hx : s.indicator f x = s.indicator g x
hxs : x ∈ s
⊢ f x = g x

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : s.indicator f =ᵐ[μ] s.indicator g
x : α
hx : s.indicator f x = s.indicator g x
hxs : x ∈ s
⊢ f x = g x
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : Nonempty β
inst✝ : SeparatesPoints β
f : α → β
hf : Measurable f
⊢ ∃ c, f = fun x ↦ c

Tactic:
by
  have h (a₁ : α) (a₂ : α) : f a₁ = f a₂ := by
    by_contra! h
    obtain ⟨s, hs, hx, hy⟩ := exists_measurableSet_of_ne h
    obtain h' | h' := MeasurableSpace.measurableSet_bot_iff.mp (hf hs)
    · absurd hx
      simp [← mem_preimage, h']
    · absurd hy
      simp [← mem_preimage, h']
  obtain h' | h' := isEmpty_or_nonempty α
  · use (Classical.ofNonempty : β), funext (by simp)
  · use f (Classical.ofNonempty : α), funext (fun x ↦ h _ _)

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

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
x : α
hx : x ∈ s
⊢ g x ∈ t

Tactic:
simpa using

Goal state after:
case pos
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
x : α
hx : x ∈ s
⊢ h₀.some ∈ t
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
x : α
hx : x ∉ s
⊢ g x ∈ t

Tactic:
simp only [g, hx, piecewise_eq_of_notMem, not_false_iff]

Goal state after:
case neg
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
x : α
hx : x ∉ s
⊢ mk f H x ∈ t
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ ν : Measure α
f : α → δ
h : μ ≤ ν
hf : AEMeasurable f ν
s : Set δ
hs : MeasurableSet s
⊢ (map f μ) s ≤ (map f ν) s

Tactic:
simpa using

Goal state after:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ ν : Measure α
f : α → δ
h : μ ≤ ν
hf : AEMeasurable f ν
s : Set δ
hs : MeasurableSet s
⊢ μ (f ⁻¹' s) ≤ ν (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NeZero μ
h : IsEmpty α
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NeZero μ
h : IsEmpty α
⊢ False
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
μ : ι → Measure α
i : ι
s : Set α
hs : MeasurableSet s
⊢ (μ i) s ≤ (sum μ) s

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
μ : ι → Measure α
i : ι
s : Set α
hs : MeasurableSet s
⊢ (μ i) s ≤ ∑' (i : ι), (μ i) s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
e : ι' ≃ ι
m : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum (m ∘ ⇑e)) s = (sum m) s

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
e : ι' ≃ ι
m : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ ∑' (i : ι'), (m (e i)) s = ∑' (i : ι), (m i) s
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
h : NullMeasurable f μ
inst✝ : MeasurableSpace.CountablyGenerated ↑∅
hft : ∀ᵐ (x : α) ∂μ, f x ∈ ∅
⊢ μ = 0

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
h : NullMeasurable f μ
inst✝ : MeasurableSpace.CountablyGenerated ↑∅
hft : ∀ᵐ (x : α) ∂μ, f x ∈ ∅
⊢ μ = 0