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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : Preorder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
⊢ Tendsto (fun x ↦ μ (Iic x)) atTop (𝓝 (μ univ))

Tactic:
by

Goal state after:
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
⊢ (sum fun i ↦ μ.restrict (s i)) ≤ M • μ.restrict (⋃ i, s i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : PartialOrder α
a : α
ha : μ {a} = 0
⊢ Iio a =ᵐ[μ] Iic a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.GDelta.MetrizableSpace

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsClosed s
⊢ IsGδ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.GDelta.MetrizableSpace

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : PseudoMetrizableSpace Y
f : X → Y
⊢ IsGδ {x | ContinuousAt f x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
⊢ t = ⋂ i, closure[inst✝¹] (g' i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
t_gd : IsGδ t
⊢ HasSeparatingCover s t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
⊢ y ⤳ x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_3
β : Type u_4
inst✝² : MeasurableSpace M
inst✝¹ : Mul M
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableMul₂ M
f g : α → β → M
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a ↦ (f a * g a) (h a)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableMul G
g : G
⊢ Measurable fun h ↦ h / g

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
n : ℕ
⊢ Measurable fun x ↦ (x, n).1 ^ (x, n).2

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: G : Type u_2
α : Type u_3
β : Type u_4
inst✝² : MeasurableSpace G
inst✝¹ : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableDiv₂ G
f g : α → β → G
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a ↦ (f a / g a) (h a)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
G : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β
f g : α → G
μ : Measure α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
⊢ MeasurableEq E

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
G : Type u_2
α : Type u_3
β✝ : Type u_4
inst✝⁸ : MeasurableSpace G
inst✝⁷ : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β✝
f g : α → G
μ : Measure α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
⊢ MeasurableEq β

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul G
inst✝ : MeasurableInv G
c : G
⊢ Measurable fun x ↦ c / x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul G
inst✝ : MeasurableInv G
c : G
⊢ Measurable fun x ↦ x / c

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
G : Type u_4
inst✝² : InvolutiveInv G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableInv G
f : α → G
h : Measurable fun x ↦ (f x)⁻¹
⊢ Measurable f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ : Measure α
G : Type u_4
inst✝² : InvolutiveInv G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableInv G
f : α → G
h : AEMeasurable (fun x ↦ (f x)⁻¹) μ
⊢ AEMeasurable f μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α : Type u_1
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℤ
⊢ Measurable fun x ↦ (x, n).1 ^ (x, n).2

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
⊢ Measurable fun p ↦ p.1 / p.2

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : Group α
inst✝ : MeasurableDiv α
⊢ Measurable Inv.inv

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
M : Type u_2
α : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : MeasurableConstSMul M α
s : Submonoid M
c : ↥s
⊢ Measurable fun x ↦ c • x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
M : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : SMul M X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M
g : α → X
inst✝⁴ : MeasurableConstSMul M X
inst✝³ : SMul M α
inst✝² : SMul Mᵐᵒᵖ α
inst✝¹ : IsCentralScalar M α
inst✝ : MeasurableConstSMul M α
⊢ ∀ (c : Mᵐᵒᵖ), Measurable fun x ↦ c • x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : SMul M X
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableSMul₂ M X
f : α → β → M
g : α → β → X
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a ↦ (f a • g a) (h a)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
X : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace X
inst✝² : SMul M X
m : MeasurableSpace α
μ : Measure α
f : α → M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableSMul M X
hf : AEMeasurable f μ
y : X
⊢ AEMeasurable (fun x ↦ f x • y) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁴ : MeasurableSpace M✝
inst✝³ : MeasurableSMul M✝ X
M : Type u_6
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
this : Measurable fun p ↦ p.2 • p.1
⊢ Measurable (Function.uncurry fun x1 x2 ↦ x1 • x2)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁴ : MeasurableSpace M✝
inst✝³ : MeasurableSMul M✝ X
M : Type u_6
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
⊢ Measurable (Function.uncurry fun x1 x2 ↦ x1 • x2)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁷ : MeasurableSpace X
inst✝⁶ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁵ : MeasurableSpace M✝
inst✝⁴ : MeasurableSMul M✝ X
M : Type u_6
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
this : Measurable fun p ↦ p.2 • p.1
⊢ Measurable (Function.uncurry fun x1 x2 ↦ x1 • x2)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
⊢ ∀ s ∈ f, IsOpen[t] s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁷ : MeasurableSpace X
inst✝⁶ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁵ : MeasurableSpace M✝
inst✝⁴ : MeasurableSMul M✝ X
M : Type u_6
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
⊢ Measurable (Function.uncurry fun x1 x2 ↦ x1 • x2)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : TopologicalSpace.IsOpen u
⊢ MeasurableSet u

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: β : Type u_5
α : Type u_6
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace α
f : α → β
G : Type u_7
inst✝² : Group G
inst✝¹ : MulAction G β
inst✝ : MeasurableConstSMul G β
c : G
h : Measurable fun x ↦ c • f x
⊢ Measurable f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
α : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
hα : BorelSpace α
p : α → Prop
⊢ instMeasurableSpace = borel (Subtype p)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: β : Type u_5
α : Type u_6
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace α
f : α → β
μ : Measure α
G : Type u_7
inst✝² : Group G
inst✝¹ : MulAction G β
inst✝ : MeasurableConstSMul G β
c : G
h : AEMeasurable (fun x ↦ c • f x) μ
⊢ AEMeasurable f μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝⁴ : Countable α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
this✝ : ∀ (s : Set α), MeasurableSet s
this : ∀ (s : Set α), MeasurableSet s
⊢ inst✝³ = borel α

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝⁴ : Countable α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ BorelSpace α

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
α : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
h : OpensMeasurableSpace α
p : α → Prop
⊢ borel (Subtype p) ≤ instMeasurableSpace

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
⊢ OpensMeasurableSpace α ↔ ∀ (s : Set α), IsOpen[inst✝¹] s → MeasurableSet s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
α : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
inst✝ : SecondCountableTopology α
⊢ CountablyGenerated α

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, Measurable f
⊢ Measurable l.prod

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
s : Set α
h : HasCountableSeparatingOn α IsOpen[inst✝¹²] s
⊢ CountablySeparated ↑s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
s : Set α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
h : IsGδ s
⊢ MeasurableSet s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
inst✝² : TopologicalSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
x y : γ
h✝ : Inseparable x y
s : Set γ
hs : MeasurableSet s
x✝² : ℕ → Set γ
x✝¹ : Pairwise (Function.onFun Disjoint x✝²)
x✝ : ∀ (i : ℕ), MeasurableSet (x✝² i)
h : ∀ (i : ℕ), x ∈ x✝² i ↔ y ∈ x✝² i
⊢ x ∈ ⋃ i, x✝² i ↔ y ∈ ⋃ i, x✝² i

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl : ∀ f ∈ l, AEMeasurable f μ
⊢ AEMeasurable l.prod μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, Measurable f
⊢ Measurable fun x ↦ (map (fun f ↦ f x) l).prod

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : R1Space γ
K s : Set γ
hK : IsCompact K
hs : MeasurableSet s
hKs : K ⊆ s
⊢ closure[inst✝³] K ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl : ∀ f ∈ l, AEMeasurable f μ
⊢ AEMeasurable (fun x ↦ (map (fun f ↦ f x) l).prod) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : R1Space γ
K : Set γ
hK : IsCompact K
μ : Measure γ
⊢ μ (closure[inst✝³] K) = μ K

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, Measurable f
⊢ ∀ f ∈ l, Measurable f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsOpen[inst✝³] s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l : Multiset (α → M)
hl : ∀ f ∈ l, Measurable f
⊢ Measurable l.prod

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, AEMeasurable f μ
⊢ ∀ f ∈ l, AEMeasurable f μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : Multiset (α → M)
hl : ∀ f ∈ l, AEMeasurable f μ
⊢ AEMeasurable l.prod μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
s : Multiset (α → M)
hs : ∀ f ∈ s, Measurable f
⊢ Measurable fun x ↦ (map (fun f ↦ f x) s).prod

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
s : Multiset (α → M)
hs : ∀ f ∈ s, AEMeasurable f μ
⊢ AEMeasurable (fun x ↦ (map (fun f ↦ f x) s).prod) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
ι : Type u_3
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun a ↦ ∏ i ∈ s, f i a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
ι : Type u_3
α : Type u_4
β : Type u_5
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
mβ : MeasurableSpace β
f : ι → α → β → M
g : α → β
s : Finset ι
hf : ∀ i ∈ s, Measurable ↿(f i)
hg : Measurable g
⊢ Measurable fun a ↦ (∏ i ∈ s, f i a) (g a)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
ι : Type u_3
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, AEMeasurable (f i) μ
⊢ AEMeasurable (fun a ↦ ∏ i ∈ s, f i a) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
⊢ Measurable f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
a : α
⊢ (𝓝 a).IsMeasurablyGenerated

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : OpensMeasurableSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : OpensMeasurableSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : TopologicalSpace γ₂
inst✝³ : MeasurableSpace γ₂
inst✝² : BorelSpace γ₂
inst✝¹ : MeasurableSpace δ
inst✝ : T0Space α
⊢ MeasurableSpace.SeparatesPoints α

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : Countable α
⊢ borel α = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι✝ : Sort y
s t u : Set α
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : MeasurableSpace α
inst✝¹⁴ : OpensMeasurableSpace α
inst✝¹³ : TopologicalSpace β
inst✝¹² : MeasurableSpace β
inst✝¹¹ : OpensMeasurableSpace β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : MeasurableSpace γ
inst✝⁸ : BorelSpace γ
inst✝⁷ : TopologicalSpace γ₂
inst✝⁶ : MeasurableSpace γ₂
inst✝⁵ : BorelSpace γ₂
inst✝⁴ : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst✝³ : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
⊢ topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = (↑i).pi s}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι✝ : Sort y
s t u : Set α
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : MeasurableSpace α
inst✝¹⁴ : OpensMeasurableSpace α
inst✝¹³ : TopologicalSpace β
inst✝¹² : MeasurableSpace β
inst✝¹¹ : OpensMeasurableSpace β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : MeasurableSpace γ
inst✝⁸ : BorelSpace γ
inst✝⁷ : TopologicalSpace γ₂
inst✝⁶ : MeasurableSpace γ₂
inst✝⁵ : BorelSpace γ₂
inst✝⁴ : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst✝³ : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
⊢ OpensMeasurableSpace ((i : ι) → X i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ b, a ⋖ b
t : Set α
hat : t ⊆ Ioi a
htc : t.Countable
htU : ⋃ i ∈ t, Ioi i = ⋃ i ∈ Ioi a, Ioi i
⊢ Ioi a = ⋃ b ∈ t, Ici b

Tactic:
by

Goal state after: