mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
⊢ F' ≤ᵐ[μ] F

Tactic:
filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_tendsto : Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
⊢ F' a ≤ F a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
⊢ F ≤ᵐ[μ] F'

Tactic:
filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
a : α
h_le : ∀ (i : ℕ), F a ≤ f i a
h_tendsto : Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
⊢ F a ≤ F' a
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyMetrizableSpace X
⊢ TopologicalSpace.MetrizableSpace X

Tactic:
let := upgradeIsCompletelyMetrizable X

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyMetrizableSpace X
this : UpgradedIsCompletelyMetrizableSpace X := upgradeIsCompletelyMetrizable X
⊢ TopologicalSpace.MetrizableSpace X
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
⊢ CauchySeq fun n ↦ ↑(u n)

Tactic:
refine cauchySeq_of_le_tendsto_0 (fun n : ℕ => (1 / 2) ^ n) (fun n m N hNn hNm => ?_) ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
n m N : ℕ
hNn : N ≤ n
hNm : N ≤ m
⊢ dist ↑(u n) ↑(u m) ≤ (1 / 2) ^ N

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
⊢ Tendsto (fun n ↦ (1 / 2) ^ n) atTop (𝓝 0)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
⊢ CompleteSpace ((i : ι) × E i)

Tactic:
set s : ι → Set (Σ i, E i) := fun i => Sigma.fst ⁻¹' {i}
  set U := { p : (Σ k, E k) × Σ k, E k | dist p.1 p.2 < 1 }
  have hc : ∀ i, IsComplete (s i) := fun i => by
    simp only [s, ← range_sigmaMk]
    exact (isometry_mk i).isUniformInducing.isComplete_range
  have hd : ∀ (i j), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j := fun i j x hx y hy hxy =>
    (Eq.symm hx).trans ((fst_eq_of_dist_lt_one _ _ hxy).trans hy)
  refine completeSpace_of_isComplete_univ ?_
  convert! isComplete_iUnion_separated hc (dist_mem_uniformity zero_lt_one) hd
  simp only [s, ← preimage_iUnion, iUnion_of_singleton, preimage_univ]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ toInductiveLimit I n.succ ∘ f n = toInductiveLimit I n

Tactic:
funext x

Goal state after:
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ (toInductiveLimit I n.succ ∘ f n) x = toInductiveLimit I n x
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case hy
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n, x⟩.fst ≤ n.succ

Tactic:
· exact le_succ _

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : MeasurableSet s
⊢ map f (μa.restrict (f ⁻¹' s)) = μb.restrict s

Tactic:
by rw [← hf.map_eq, restrict_map hf.measurable hs]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving (⇑e) μc μa
hg : MeasurePreserving (g ∘ ⇑e) μc μb
⊢ g = (g ∘ ⇑e) ∘ ⇑e.symm

Tactic:
simp [Function.comp_assoc g e e.symm]

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : y ∉ s
A : (s ∩ cylinder y (longestPrefix y s)).Nonempty
⊢ f y = A.some

Tactic:
f,

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : y ∉ s
A : (s ∩ cylinder y (longestPrefix y s)).Nonempty
⊢ (if y ∈ s then y else ⋯.some) = A.some
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
s : Set β
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

Tactic:
rw [← hg.map_eq, hge.restrict_map, hge.lintegral_map]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
⊢ μ ≪ ν₁

Tactic:
refine AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : ν₁ s = 0
⊢ μ s = 0
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∈ s
A : (s ∩ cylinder x (longestPrefix x s)).Nonempty
⊢ f x = A.some

Tactic:
f,

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∈ s
A : (s ∩ cylinder x (longestPrefix x s)).Nonempty
⊢ (if x ∈ s then x else ⋯.some) = A.some
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
p : α → Prop
f✝ : β → α
f : β ≃ᵐ α
⊢ IsProbabilityMeasure (Measure.comap (⇑f) μ)

Tactic:
← MeasurableEquiv.map_symm

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
p : α → Prop
f✝ : β → α
f : β ≃ᵐ α
⊢ IsProbabilityMeasure (Measure.map (⇑f.symm) μ)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
⊢ f x = Ax.some

Tactic:
f,

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
⊢ (if x ∈ s then x else ⋯.some) = Ax.some
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
⊢ f y = Ay.some

Tactic:
f,

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
⊢ (if y ∈ s then y else ⋯.some) = Ay.some
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ (dirac a) s = s.indicator 1 a

Tactic:
indicator_of_notMem h,

Goal state after:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ (dirac a) s = 0
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∉ s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Tactic:
· have : s ∩ {a} = {a} := by simpa
    simp [*]

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∉ s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ count ↑(Finset.image f s) = count ↑s

Tactic:
count_apply_finset' _,

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ ↑(#(Finset.image f s)) = count ↑s

α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ MeasurableSet ↑(Finset.image f s)
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a ↦ (μ a) s
h_univ : Measurable fun a ↦ (μ a) univ
s : Set β
⊢ MeasurableSet s → Measurable fun b ↦ (μ b) s

Tactic:
hs

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a ↦ (μ a) s
h_univ : Measurable fun a ↦ (μ a) univ
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ (μ b) s
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
⊢ s ∈ ae m.join → s ∈ (ae m).bind ae

Tactic:
hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
⊢ s ∈ (ae m).bind ae
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
⊢ MeasurableSet s → Measurable fun b ↦ (map (Prod.mk b) ν) s

Tactic:
hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b ↦ (map (Prod.mk b) ν) s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
s : Set (α × β)
⊢ MeasurableSet s → Measurable fun b ↦ (map (fun x ↦ (x, b)) μ) s

Tactic:
hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b ↦ (map (fun x ↦ (x, b)) μ) s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
⊢ MeasurableSet s → Measurable fun x ↦ ∫⁻ (y : β), s.indicator (fun x ↦ c) (x, y) ∂ν

Tactic:
hs

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x ↦ ∫⁻ (y : β), s.indicator (fun x ↦ c) (x, y) ∂ν
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν) →
          Measurable fun x ↦ ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν

Tactic:
intro f hf h2f h3f

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν
⊢ Measurable fun x ↦ ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_3
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
s : Set (α × β)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
⊢ ∀ (f : ℕ → Set (α × β)),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), μ (f i) = ν (f i)) → μ (⋃ i, f i) = ν (⋃ i, f i)

Tactic:
intro f h_disj hf h_eq

Goal state after:
case refine_3
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
s : Set (α × β)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), μ (f i) = ν (f i)
⊢ μ (⋃ i, f i) = ν (⋃ i, f i)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
⊢ (x • μ).OuterRegular

Tactic:
refine ⟨fun A _ r hr => ?_⟩
    rw [smul_apply, A.measure_eq_iInf_isOpen, smul_eq_mul] at hr
    simpa only [ENNReal.mul_iInf_of_ne h0 hx, gt_iff_lt, iInf_lt_iff, exists_prop] using! hr

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

Goal state before:
pp: case refine_5
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
⊢ ∀ (f : ℕ → Set (α × β × γ)),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), μ (f i) = ν (f i)) → μ (⋃ i, f i) = ν (⋃ i, f i)

Tactic:
intro f h_disj hf h_eq

Goal state after:
case refine_5
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
f : ℕ → Set (α × β × γ)
h_disj : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), μ (f i) = ν (f i)
⊢ μ (⋃ i, f i) = ν (⋃ i, f i)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
⊢ μ = ν ↔
    ∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s → MeasurableSet t → MeasurableSet u → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)

Tactic:
rw [← MeasurableEquiv.prodAssoc.map_measurableEquiv_injective.eq_iff, ext_prod₃_iff]

Goal state after:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
⊢ (∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)) ↔
    ∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s → MeasurableSet t → MeasurableSet u → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
i : ℕ × ℕ
s : Set β
t : Set α
⊢ MeasurableSet s →
    MeasurableSet t →
      (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) (s ×ˢ t) =
        (sfiniteSeq ν i.1) s * (sfiniteSeq μ i.2) t

Tactic:
hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
i : ℕ × ℕ
s : Set β
t : Set α
hs : MeasurableSet s
⊢ MeasurableSet t →
    (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) (s ×ˢ t) = (sfiniteSeq ν i.1) s * (sfiniteSeq μ i.2) t