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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ s) = μ (t ∩ s)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
⊢ μ Set.univ < ∞

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
⊢ μ Set.univ < ∞
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
]

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
⊢ SigmaFinite (μ.trim ⋯)
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ IsFiniteMeasure (μ.trim ⋯) ↔ IsFiniteMeasure μ

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ IsFiniteMeasure (μ.trim ⋯) ↔ IsFiniteMeasure μ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ μ (⋃ i, toMeasurable μ (t ∩ disjointed w i) ∩ u) ≤ ∑' (n : ℕ), μ (toMeasurable μ (t ∩ disjointed w n) ∩ u)

Tactic:
]

Goal state after:
α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ μ (⋃ i, toMeasurable μ (t ∩ disjointed w i) ∩ u) ≤ ∑' (n : ℕ), μ (toMeasurable μ (t ∩ disjointed w n) ∩ u)
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (μ.trim ⋯)
h_univ : μ Set.univ < ∞
⊢ μ Set.univ < ∞

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (μ.trim ⋯)
h_univ : μ Set.univ < ∞
⊢ μ Set.univ < ∞
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
h_univ : μ Set.univ < ∞
⊢ μ Set.univ < ∞

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
h_univ : μ Set.univ < ∞
⊢ μ Set.univ < ∞
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
hsν : ν s = 0
⊢ μ s = 0

Tactic:
]

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
hsν : ν s = 0
⊢ μ s = 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁✝ μ₂✝ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
x✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
⊢ ∑' (i : ℕ), μ₁ (s i) + ∑' (i : ℕ), μ₂ (s i) = ∑' (a : ℕ), μ₁ (s a) + ∑' (a : ℕ), μ₂ (s a)

Tactic:
]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableEq β
hm : m ≤ m0
f g : α → β
hf : Measurable f
hg : Measurable g
hfg : f =ᵐ[μ] g
⊢ μ {a | ¬f a = g a} = 0

pp: α : Type u_3
β : Type u_4
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableEq β
hm : m ≤ m0
f g : α → β
hf : Measurable f
hg : Measurable g
hfg : f =ᵐ[μ] g
⊢ MeasurableSet {a | ¬f a = g a}

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableEq β
hm : m ≤ m0
f g : α → β
hf : Measurable f
hg : Measurable g
hfg : f =ᵐ[μ] g
⊢ μ {a | ¬f a = g a} = 0

α : Type u_3
β : Type u_4
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableEq β
hm : m ≤ m0
f g : α → β
hf : Measurable f
hg : Measurable g
hfg : f =ᵐ[μ] g
⊢ MeasurableSet {a | ¬f a = g a}
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁✝ μ₂✝ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
x✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
⊢ μ₁.toOuterMeasure + μ₂.toOuterMeasure ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁✝ μ₂✝ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
x✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
⊢ (μ₁.toOuterMeasure + μ₂.toOuterMeasure).trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure

Tactic:
rw [OuterMeasure.trim_add, μ₁.trimmed, μ₂.trimmed]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
x✝ : MeasurableSpace α
c : R
μ : Measure α
⊢ c • μ.toOuterMeasure ≤ c • μ.toOuterMeasure

Tactic:
]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
I : Finset ι
μ : ι → Measure α
s : Set α
⊢ ∑ c ∈ I, (μ c) s = ∑ i ∈ I, (μ i) s

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : univ ≠ univ
hu : u = univ
hv : v = univ
⊢ Disjoint u v

Tactic:
]

Goal state after:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : univ ≠ univ
hu : u = univ
hv : v = univ
⊢ Disjoint u v
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hu : u ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
hv : v ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
huv : u ≠ v
⊢ Disjoint u v

Tactic:
]

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hu : u ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
hv : v ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
huv : u ≠ v
⊢ Disjoint u v
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s t : Set α
ht : MeasurableSet t
htν : ν (t ∩ s) = 0
⊢ μ (t ∩ s) = 0

Tactic:
]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s t : Set α
ht : MeasurableSet t
htν : ν (t ∩ s) = 0
⊢ μ (t ∩ s) = 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
R : Type u_6
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, p x
c : R
⊢ 0 = 0

Tactic:
]

Goal state after:
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
hd : T.Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ.restrict (⋃ x, s ↑x) = sum fun i ↦ μ.restrict (s ↑i)

Tactic:
]

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
T : Set ι
hT : Countable ↑T
hd : T.Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ.restrict (⋃ x, s ↑x) = sum fun i ↦ μ.restrict (s ↑i)
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
⊢ ⋃₀ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} = univ

Tactic:
]

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
⊢ ⋃₀ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} = univ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable ↑t
⊢ ⨆ i, ae (μ.restrict (s ↑i)) = ⨆ i, ae (μ.restrict (s ↑i))

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
⊢ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}.Finite

Tactic:
]

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
⊢ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}.Finite
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (ν + μ) t ≠ ∞
h' : s ⊆ t
h'' : (ν + μ) s = (ν + μ) t
⊢ ν s = ν t

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (ν + μ) t ≠ ∞
h' : s ⊆ t
h'' : (ν + μ) s = (ν + μ) t
⊢ ν s = ν t
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ Finite ↑{s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}

Tactic:
]

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ Finite ↑{s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
u : Set α
x✝ : u ∈ memPartition f n
⊢ ({a | a = u ∩ f n} ∪ {a | a = u \ f n}).Finite

Tactic:
]

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
u : Set α
x✝ : u ∈ memPartition f n
⊢ ({a | a = u ∩ f n} ∪ {a | a = u \ f n}).Finite
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ (μ + ν) t ≠ ∞

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ (μ + ν) t ≠ ∞
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) ∈
    {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}

Tactic:
]

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) ∈
    {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (ν + μ) t ≠ ∞
⊢ ν (toMeasurable (ν + μ) t ∩ s) = ν (t ∩ s)

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (ν + μ) t ≠ ∞
⊢ ν (toMeasurable (ν + μ) t ∩ s) = ν (t ∩ s)
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
⊢ a ∈ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n

Tactic:
]

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
⊢ a ∈ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case e_f
α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ μ (disjointed w n ∩ (t ∩ u)) = μ (disjointed w n ∩ (t ∩ u))

pp: case e_f
α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ MeasurableSet (disjointed w n)

Tactic:
]

Goal state after:
case e_f
α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ MeasurableSet (disjointed w n)
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ (s ∩ memPartitionSet f n a).Nonempty

Tactic:
]

Goal state after:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ (s ∩ memPartitionSet f n a).Nonempty
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder α
a b : α
P : α → Prop
⊢ ((∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x) ↔
    (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
⊢ (μ ({x | p x}ᶜ ∩ s) = 0) = (μ {x | x ∈ s → p x}ᶜ = 0)

Tactic:
]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
⊢ (μ ({x | p x}ᶜ ∩ s) = 0) = (μ {x | x ∈ s → p x}ᶜ = 0)
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : Set ↑t → Set α
hpV : ∀ s ∈ S, p (V s)
hV : ∀ s ∈ S, Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s
U : Set ↑t
hU : U ∈ S
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' V U ↔ ⟨y, hy⟩ ∈ Subtype.val ⁻¹' V U

Tactic:
]

Goal state after:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : Set ↑t → Set α
hpV : ∀ s ∈ S, p (V s)
hV : ∀ s ∈ S, Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s
U : Set ↑t
hU : U ∈ S
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' V U ↔ ⟨y, hy⟩ ∈ Subtype.val ⁻¹' V U
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ (μ ({x | p x}ᶜ ∩ s) = 0) = (μ {x | x ∈ s → p x}ᶜ = 0)

Tactic:
]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ (μ ({x | p x}ᶜ ∩ s) = 0) = (μ {x | x ∈ s → p x}ᶜ = 0)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∑' (n : ℕ), (μ.restrict (t ∩ u)) (disjointed w n) = ∑' (i : ℕ), (μ.restrict (t ∩ u)) (disjointed w i)

pp: case hn
α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Pairwise (Disjoint on disjointed w)

pp: case h
α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∀ (i : ℕ), MeasurableSet (disjointed w i)

Tactic:
]

Goal state after:
case hn
α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Pairwise (Disjoint on disjointed w)

case h
α : 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) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∀ (i : ℕ), MeasurableSet (disjointed w i)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᵐ[μ] g
⊢ μ.restrict s ≪ μ

Tactic:
]

Goal state after:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᵐ[μ] g
⊢ μ.restrict s ≪ μ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t : Set α
p : α → Prop
ht : ∀ᵐ (x : α) ∂μ.restrict t, p x
htc : ∀ᵐ (x : α) ∂μ.restrict tᶜ, p x
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
s : Set α
t : Set β
f : α → β
hs : MeasurableSet s
⊢ μ ((f ⁻¹' t)ᶜ ∩ s) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s✝ : Set α
hs : MeasurableSet s✝
t✝ : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t✝ ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
⊢ ⨅ b ∈ m, b.toOuterMeasure s ≤ μ t

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s✝ : Set α
hs : MeasurableSet s✝
t✝ : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t✝ ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
⊢ ⨅ b ∈ m, b.toOuterMeasure s ≤ μ t
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 x = g x
⊢ f x = g x

Tactic:
]

Goal state after:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f / g =ᵐ[μ] 1
x : α
hx : f x = g x
⊢ f x = g x
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
]

Goal state after:
case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f =ᵐ[μ] g
x : α
hx : f x = g x
⊢ f x = g x
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t
⊢ (⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ μ (u ∩ s) + μ (u \ s)

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t
⊢ (⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ μ (u ∩ s) + μ (u \ s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : 1 ≤ᵐ[μ] g / f
a : α
ha : f a ≤ g a
⊢ f a ≤ g a

Tactic:
]

Goal state after:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : 1 ≤ᵐ[μ] g / f
a : α
ha : f a ≤ g a
⊢ f a ≤ g a
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure
s : Set α
hs : MeasurableSet s
⊢ (sInf (toOuterMeasure '' m)) s ≤ μ s

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure
s : Set α
hs : MeasurableSet s
⊢ (sInf (toOuterMeasure '' m)) s ≤ μ s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : f ≤ᵐ[μ] g
a : α
ha : f a ≤ g a
⊢ f a ≤ g a

Tactic:
]

Goal state after:
case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : f ≤ᵐ[μ] g
a : α
ha : f a ≤ g a
⊢ f a ≤ g a