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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ (toMeasurable μ s) = μ s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯
⊢ ∀ (t : Set α) (ht : MeasurableSet t), C t ht

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
⊢ μ (aeSeqSet hf p)ᶜ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeq hf p i x = AEMeasurable.mk (f i) ⋯ x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
hg : AEMeasurable g μ
a : δ
⊢ AEMeasurable (fun x ↦ g x a) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝¹ : SupSet β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
⊢ ⨆ n, aeSeq hf p n =ᵐ[μ] ⨆ n, f n

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
t : Set α
ht : t ∈ {s}
⊢ (fun x ↦ x ∈ s) ⁻¹' {True} = t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s : Set α
⊢ generateFrom {s} = MeasurableSpace.comap (fun x ↦ x ∈ s) ⊤

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : MeasurableSpace M
s : Set α
c : M
⊢ s ∈ {s}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
this : x = univ
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ AEMeasurable g μ ↔ ∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

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

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
this : x ⊆ ∅
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s✝ t : Set α
l : Filter α
inst✝ : CountableInterFilter l
s : ℕ → Set α
hs : ∀ (i : ℕ), ∃ t, MeasurableSet t ∧ s i =ᶠ[l] t
⊢ ∃ t, MeasurableSet t ∧ ⋃ i, s i =ᶠ[l] t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : Set α
l : Filter α
inst✝ : CountableInterFilter l
ht : EventuallyMeasurableSet m l t
hst : s =ᶠ[l] t
⊢ EventuallyMeasurableSet m l s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
⊢ extend m s₁ ≤ extend m s₂

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : f.IsMeasurablyGenerated
inst✝ : g.IsMeasurablyGenerated
⊢ (f ⊓ g).IsMeasurablyGenerated

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ (𝓟 s).IsMeasurablyGenerated ↔ MeasurableSet s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
⊢ (⨅ i, f i).IsMeasurablyGenerated

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
⊢ MeasurableSet {x | Tendsto (fun n ↦ f n x) l l'}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet (⋃ i, s i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet (⋂ i, s i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_5
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet (⋃ i, s i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_5
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet (⋂ i, s i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
⊢ ∀ (s : ℕ → Set α), extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (blimsup s atTop p)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (bliminf s atTop p)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ MeasurableSet (limsup s atTop)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ MeasurableSet (liminf s atTop)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ : OuterMeasure α
H : ∀ {s : Set α}, MeasurableSet s → m₁ s = m₂ s
⊢ m₁.trim = m₂.trim

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
⊢ m.trim ≤ m.trim

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ : OuterMeasure α
s : Set α
hs : MeasurableSet s
⊢ m₁.trim s ≤ m₂ s ↔ m₁ s ≤ m₂ s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ : OuterMeasure α
⊢ m₁.trim = m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → m₁ s = m₂ s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ m.trim s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ m.trim s = ⨅ t, m ↑t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
⊢ trim 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
⊢ ∀ (i : Set α),
    s ⊆ i → MeasurableSet i → ∑' (i : ι), ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m i) t ≤ ∑' (i_3 : ι), (m i_3) i

Tactic:
exact fun t st ht =>
    ENNReal.tsum_le_tsum fun i => iInf_le_of_le t <| iInf_le_of_le st <| iInf_le _ ht

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
⊢ (sum fun i ↦ (m i).trim) s ≤ (sum m).trim s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
h : MeasurableSet (f '' s)
⊢ MeasurableSet s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (_root_.id '' s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (g ∘ f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs✝ : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
⊢ ∃ t, MeasurableSet t ∧ s ⊆ t ∧ m t < r

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
⊢ MeasurableSet (range f)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set β
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (rangeSplitting f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
⊢ ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (extend f g g')

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
this : Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
⊢ Measurable f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
⊢ ∀ (n : ℕ), ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < ms + (↑n)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
⊢ Measurable (g ∘ f) ↔ Measurable f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
i₁ : α₁ → α
i₂ : α₂ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
h : univ ⊆ range i₁ ∪ range i₂
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
⊢ MeasurableSet s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
α₃ : Type u_8
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
mα₃ : MeasurableSpace α₃
i₁ : α₁ → α
i₂ : α₂ → α
i₃ : α₃ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
hi₃ : MeasurableEmbedding i₃
h : univ ⊆ range i₁ ∪ range i₂ ∪ range i₃
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
hs₃ : MeasurableSet (i₃ ⁻¹' s)
⊢ MeasurableSet s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Injective toEquiv

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
t : Set α
⊢ s = ⇑e '' t ↔ ⇑e.symm '' s = t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
⊢ ⇑e '' ⇑e ⁻¹' s = s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set α
⊢ ⇑e ⁻¹' ⇑e '' s = s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
h : MeasurableSet (⇑e ⁻¹' s)
⊢ MeasurableSet s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
⊢ MeasurableSet (⇑e '' s) ↔ MeasurableSet s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ⇑e)
⊢ Measurable f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable ⇑(Equiv.prodAssoc α β γ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable ⇑(Equiv.prodAssoc α β γ).symm

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
s : Set α
t : Set β
⊢ Measurable fun a ↦ ⟨(↑a).1, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
s : Set α
t : Set β
⊢ Measurable fun a ↦ ⟨(↑a).2, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
s : Set α
t : Set β
⊢ Measurable fun x ↦ (↑x.1, ↑x.2)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (⇑(Equiv.Set.rangeInl α β) ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (⇑(Equiv.Set.rangeInr α β) ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ univ ⊆ range Sum.inl ×ˢ univ ∪ range Sum.inr ×ˢ univ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = m.trim s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
h : m.trim s = 0
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.27
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable ⇑(Equiv.sumProdDistrib α β γ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝¹ : (x : δ') → MeasurableSpace (π x)
inst✝ : (x : δ') → MeasurableSpace (π' x)
f : δ ≃ δ'
⊢ Measurable ⇑(Equiv.piCongrLeft π f).symm

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: δ : Type u_4
δ' : Type u_5
π : δ' → Type u_6
inst✝ : (x : δ') → MeasurableSpace (π x)
f : δ ≃ δ'
⊢ ⇑(piCongrLeft π f) = ⇑(Equiv.piCongrLeft π f)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: ι : Type u_8
ι' : Type u_9
e : ι ≃ ι'
β : ι' → Type u_10
inst✝ : (i' : ι') → MeasurableSpace (β i')
x : (i : ι) → β (e i)
i : ι
⊢ (piCongrLeft (fun i' ↦ β i') e) x (e i) = x i

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝³ : (x : δ') → MeasurableSpace (π x)
inst✝² : (x : δ') → MeasurableSpace (π' x)
α : Type u_8
β : Type u_9
γ : Type u_10
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable ⇑(Equiv.arrowProdEquivProdArrow γ (fun i ↦ α) fun i ↦ β)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s

Tactic:
by

Goal state after: