mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
ms : Set (OuterMeasure α)
m : OuterMeasure α
hm : m ∈ ms
s : Set α
⊢ m s ≤ (sSup ms) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
μ₁ μ₂ : OuterMeasure α
h : ∀ (s : Set α), s.Nonempty → μ₁ s = μ₂ s
s : Set α
he : s = ∅
⊢ μ₁ s = μ₂ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_3
f : ι → OuterMeasure α
s : Set α
⊢ (⨆ i, f i) s = ⨆ i, (f i) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_3
f : ι → OuterMeasure α
s : Set α
⊢ (⨆ i, f i) s = (⨆ i, ⇑(f i)) s

Tactic:
by

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

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
⊢ Disjoint (measurableAtom x) (measurableAtom y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ MeasurableSpace.comap Prod.fst mβ ≤ MeasurableSpace.map f m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a ↦ (f a).1
hf₂ : Measurable fun a ↦ (f a).2
⊢ MeasurableSpace.comap Prod.snd mγ ≤ MeasurableSpace.map f m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
⊢ (m₁ ⊔ m₂) s = max (m₁ s) (m₂ s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
ι : Sort u_4
f : ι → OuterMeasure α
c : R
s : Set α
⊢ (c • ⨆ i, f i) s = (⨆ i, c • f i) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : (s ×ˢ t).Nonempty
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.16
f : α → β
m : OuterMeasure α
s : ℕ → Set β
x✝ : Pairwise (Disjoint on s)
⊢ m (f ⁻¹' ⋃ i, s i) ≤ ∑' (i : ℕ), m (f ⁻¹' s i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
m m' : OuterMeasure α
s : Set β
⊢ ((map f) (m ⊔ m')) s = ((map f) m ⊔ (map f) m') s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
ι : Sort u_4
f : α → β
m : ι → OuterMeasure α
s : Set β
⊢ ((map f) (⨆ i, m i)) s = (⨆ i, (map f) (m i)) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ LawfulFunctor OuterMeasure

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
a : α
⊢ ∅.indicator (fun x ↦ 1) a = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
a : α
x✝¹ x✝ : Set α
h : x✝¹ ⊆ x✝
⊢ x✝¹.indicator (fun x ↦ 1) a ≤ x✝.indicator (fun x ↦ 1) a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
⊢ f ⁻¹' s = ⋃ y, ((fun x ↦ f (x, y)) ⁻¹' s) ×ˢ measurableAtom y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type ?u.14
f : ι → OuterMeasure α
⊢ ∑' (i : ι), (f i) ∅ = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type ?u.14
f : ι → OuterMeasure α
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ ∑' (i : ι), (f i) (⋃ i, s i) ≤ ∑' (i : ℕ) (i_1 : ι), (f i_1) (s i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : ℝ≥0∞
b : α
s : Set α
⊢ (a • dirac b) s = s.indicator (fun x ↦ a) b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.15
f : α → β
m : OuterMeasure β
⊢ m (f '' ∅) = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable α
f : α × β → γ
hf : ∀ (x : α), Measurable fun y ↦ f (x, y)
h'f : ∀ (x x' : α) (y : β), x' ∈ measurableAtom x → f (x', y) = f (x, y)
⊢ Measurable f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.15
f : α → β
m : OuterMeasure β
x✝¹ x✝ : Set α
h : x✝¹ ⊆ x✝
⊢ m (f '' x✝¹) ≤ m (f '' x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : ↑(Icc 0 1)
⊢ ↑x = 0 ↔ x = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
⊢ ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α × β → γ
hf : ∀ (x : α), Measurable fun y ↦ f (x, y)
⊢ ∀ (x x' : α) (y : β), x' ∈ measurableAtom x → f (x', y) = f (x, y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : ↑(Icc 0 1)
⊢ ↑x = 1 ↔ x = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.15
f : α → β
m : OuterMeasure β
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ m (f '' ⋃ i, s i) ≤ ∑' (i : ℕ), m (f '' s i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
ι : Sort u_4
f : α → β
m : ι → OuterMeasure β
s : Set α
⊢ ((comap f) (⨆ i, m i)) s = (⨆ i, (comap f) (m i)) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
m : OuterMeasure α
⊢ ((restrict s) m) t = m (t ∩ s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ ((restrict s) m) u ≤ ((restrict t) m') u

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
t : β
ht : t ∈ Icc 0 1
⊢ 1 - t ∈ Icc 0 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : OuterMeasure α
s : Set α
⊢ ((restrict univ) m) s = m s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : OuterMeasure α
s : Set α
⊢ ((restrict ∅) m) s = 0 s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ ⋃ i, t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (iUnionLift t f htf T hT ⁻¹' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_3
s : Set α
m : ι → OuterMeasure α
⊢ (restrict s) (⨆ i, m i) = ⨆ i, (restrict s) (m i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Icc 0 1)
⊢ 0 ≤ 1 - ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
m : OuterMeasure β
s : Set β
⊢ f '' f ⁻¹' s = Subtype.val '' Subtype.val ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Icc 0 1)
⊢ 1 - ↑x ≤ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → ↑(t i) → β
hfm : ∀ (i : ι), Measurable (f i)
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
htU : ⋃ i, t i = univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (liftCover t f hf htU ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Nontrivial R
⊢ 0 ∈ Ico 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Nontrivial R
x : ↑(Ico 0 1)
⊢ ↑x = 0 ↔ x = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
ma : OuterMeasure α
mb : OuterMeasure β
f : α → β
h : (map f) ma ≤ mb
s : Set β
⊢ ((map f) ma) s ≤ ((restrict (range f)) mb) s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
x : ↑(Ioc 0 1)
⊢ ↑x = 1 ↔ x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
t : β
ht : t ∈ Ioo 0 1
⊢ 1 - t ∈ Ioo 0 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
hf : Surjective f
m : OuterMeasure β
s : Set β
⊢ ((map f) ((comap f) m)) s = m s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Ioo 0 1)
⊢ 0 < 1 - ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Ioo 0 1)
⊢ 1 - ↑x < 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
hf : Injective f
m : OuterMeasure α
s : Set α
⊢ ((comap f) ((map f) m)) s = m s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Nonempty
a : α
as : a ∈ s
⊢ ∞ ≤ (∞ • dirac a) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
⊢ ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s = ∅
⊢ ⊤ s = ⨅ (_ : s = ∅), 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Nonempty
⊢ ⊤ s = ⨅ (_ : s = ∅), 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
hs : s.Nonempty
⊢ ((comap f) ⊤) s = ⊤ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
⊢ Measurable g ↔ ∀ (a : δ), Measurable fun x ↦ g x a

Tactic:
by

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

Goal state before:
pp: β : Type u_2
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
g : (a : δ) → β → X a
a : δ
⊢ MeasurableSpace.comap (g a) inferInstance ≤
    MeasurableSpace.comap (fun b c ↦ g c b) (MeasurableSpace.comap (fun b ↦ b a) (inst✝ a))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ((map f) ⊤) s = ((restrict (range f)) ⊤) s

Tactic:
by

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

Goal state before:
pp: β : Type u_2
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
g : (a : δ) → β → X a
a : δ
⊢ MeasurableSpace.comap (g a) inferInstance ≤ MeasurableSpace.comap (fun b c ↦ g c b) pi

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ (map f) ⊤ = ⊤

Tactic:
by

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

Goal state before:
pp: β : Type u_2
δ : Type u_4
X✝ : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X✝ a)
X : (a : δ) → β → X✝ a
⊢ MeasurableSpace.comap (fun b a ↦ X a b) inferInstance = ⨆ a, MeasurableSpace.comap (X a) inferInstance

Tactic:
by

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
a : δ
inst✝ : DecidableEq δ
⊢ Measurable fun p ↦ update p.1 a p.2

Tactic:
by

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Unique δ
⊢ Measurable uniqueElim

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
⊢ CauchySeq f

Tactic:
by

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : DecidableEq δ
s : Finset δ
⊢ Measurable fun p ↦ updateFinset p.1 s p.2

Tactic:
by

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
i i' : δ
h : i = i'
⊢ Measurable ⋯.mp

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ ∑' (m : ℕ), d (n + m)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ tsum d

Tactic:
by

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
ht : ∀ i ∈ s, MeasurableSet (t i)
⊢ MeasurableSet (s.pi t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
h : Summable fun n ↦ dist (f n) (f n.succ)
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f n.succ)

Tactic:
by

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
t : (i : δ) → Set (X i)
ht : ∀ (i : δ), MeasurableSet (t i)
⊢ univ.pi t = {f | ∀ (i : δ), f i ∈ t i}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ ¬Summable f ↔ Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop

Tactic:
by

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : (s.pi t).Nonempty
⊢ MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable f ↔ ¬Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop

Tactic:
by

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

Tactic:
by

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

Goal state before:
pp: case pos
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
this : Measurable fun f ↦ f ⟨j, hj⟩
⊢ Measurable fun x ↦ x.1 ⟨j, ⋯⟩

Tactic:
exact Measurable.comp this measurable_fst

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
⊢ Measurable ⇑(Equiv.piEquivPiSubtypeProd p X).symm

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_4
β : α → Type u_3
f : (x : α) × β x → ℝ
hf : ∀ (x : (x : α) × β x), 0 ≤ f x
⊢ Summable f ↔ (∀ (x : α), Summable fun y ↦ f ⟨x, y⟩) ∧ Summable fun x ↦ ∑' (y : β x), f ⟨x, y⟩

Tactic:
by

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (i : δ) → MeasurableSpace (X i)
l : List δ
⊢ Measurable (TProd.mk l)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_3
β : Type u_4
f : β → ℝ
hf : 0 ≤ f
s : α → Set β
hs : ∀ (i : β), ∃! j, i ∈ s j
⊢ Summable f ↔ (∀ (j : α), Summable fun i ↦ f ↑i) ∧ Summable fun j ↦ ∑' (i : ↑(s j)), f ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
⊢ Summable f

Tactic:
by

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (i : δ) → MeasurableSpace (X i)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
⊢ Measurable fun v ↦ v.elim hj

Tactic:
by

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (i : δ) → MeasurableSpace (X i)
l : List δ
s : (i : δ) → Set (X i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (Set.tprod l s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
⊢ MeasurableSet (Sum.inl '' s) ↔ MeasurableSet s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
⊢ MeasurableSet (Sum.inr '' s) ↔ MeasurableSet s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (range Sum.inl)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (range Sum.inl)

Tactic:
by
  rw [← image_univ]
  exact MeasurableSet.univ.inl_image

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (range Sum.inr)

Tactic:
by

Goal state after: