mathlib-initiative/mathlib-tactics huggingface dataset:
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)
s : ι → Set ((i : ι) × E i) := fun i ↦ Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.1 p.2 < 1}
⊢ CompleteSpace ((i : ι) × E i)

Tactic:
have hc : ∀ i, IsComplete (s i) := fun i => by
    simp only [s, ← range_sigmaMk]
    exact (isometry_mk i).isUniformInducing.isComplete_range

Goal state after:
ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i ↦ Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.1 p.2 < 1}
hc : ∀ (i : ι), IsComplete (s i)
⊢ CompleteSpace ((i : ι) × E i)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case a
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
ε : ℝ
εpos : ε > 0
⊢ {p | dist p.1 p.2 < ε} ∈ ⨅ i, 𝓟 {a | a.1 i = a.2 i}

Tactic:
obtain ⟨n, hn⟩ : ∃ n, (1 / 2 : ℝ) ^ n < ε := exists_pow_lt_of_lt_one εpos (by norm_num)

Goal state after:
case a
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
⊢ {p | dist p.1 p.2 < ε} ∈ ⨅ i, 𝓟 {a | a.1 i = a.2 i}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: case e_μ
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : AEMeasurable f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ Measure.map g μ = Measure.map (AEMeasurable.mk g hg) μ

Tactic:
exact Measure.map_congr hg.ae_eq_mk

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc α ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a ↦ f (g a)
⊢ f₀.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ f a), g_1.lintegral (Measure.map g μ)

Tactic:
rw [← f₀.extend_comp_eq hg (const _ 0), ← SimpleFunc.lintegral_map, ←
      SimpleFunc.lintegral_eq_lintegral, ← lintegral]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc α ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a ↦ f (g a)
⊢ ∫⁻ (a : β), (f₀.extend g hg (const β 0)) a ∂Measure.map g μ ≤ ∫⁻ (a : β), f a ∂Measure.map g μ
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:
[

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
⊢ f y = A.some
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst✝¹] g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ AnalyticSet (f '' s)

Tactic:
this

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst✝¹] g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ AnalyticSet (range (f ∘ g))
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : ν₁ s = 0
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : μ t = 0
htν₂ : ν₂ tᶜ = 0
this : μ s = μ (s ∩ tᶜ)
⊢ μ s = 0

Tactic:
this

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : ν₁ s = 0
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : μ t = 0
htν₂ : ν₂ tᶜ = 0
this : μ s = μ (s ∩ tᶜ)
⊢ μ (s ∩ tᶜ) = 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:
[

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
⊢ f x = A.some
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : (μ ⊓ ν) univ = 0
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Tactic:
[

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : (μ ⊓ ν) univ = 0
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε
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:
by
  rw [← MeasurableEquiv.map_symm]; exact isProbabilityMeasure_map f.symm.measurable.aemeasurable

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 : 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:
[

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
⊢ f x = 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:
[

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
⊢ f y = Ay.some
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ μ (measurableAtom x) = ∑' (i : ↑(range points)), μ (measurableAtom ↑i) * (dirac ↑i) (measurableAtom x)

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ μ (measurableAtom x) = ∑' (i : ↑(range points)), μ (measurableAtom ↑i) * (dirac ↑i) (measurableAtom x)
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint (ae μ) (ae ν)
⊢ Disjoint μ ν

Tactic:
[

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint (ae μ) (ae ν)
⊢ Disjoint μ ν
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case refine_2
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ Disjoint (⋃ m, t m) (⋃ m, ⋂ n, u m n)

Tactic:
[

Goal state after:
case refine_2
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ Disjoint (⋃ m, t m) (⋃ m, ⋂ n, u m n)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ ⋃ x ∈ ↑s, {x}) = (∑ a ∈ s, μ {a} • dirac a) t

Tactic:
[

Goal state after:
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ ⋃ x ∈ ↑s, {x}) = (∑ a ∈ s, μ {a} • dirac a) t
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
mα : MeasurableSpace α✝
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (b.1 + b.2) s

Tactic:
[

Goal state after:
α✝ : Type u_1
β : Type u_2
mα : MeasurableSpace α✝
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (b.1 + b.2) s
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ (map f b) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ (map f b) s
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (dirac b) s

Tactic:
[

Goal state after:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (dirac b) s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ (fun i ↦ ε ≤ a i) = fun i ↦ ↑ε ≤ (ofNNReal ∘ a) i

Tactic:
simp only [ENNReal.coe_le_coe, Function.comp]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ∑' (i : α), (ofNNReal ∘ a) i = ↑(∑' (i : α), a i)

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ∑' (i : α), (ofNNReal ∘ a) i = ↑(∑' (i : α), a i)
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Function.onFun Disjoint f)
⊢ ∫⁻ (μ : Measure α), μ (⋃ i, f i) ∂m = ∑' (i : ℕ), ∫⁻ (μ : Measure α), μ (f i) ∂m

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Function.onFun Disjoint f)
⊢ ∫⁻ (μ : Measure α), μ (⋃ i, f i) ∂m = ∑' (i : ℕ), ∫⁻ (μ : Measure α), μ (f i) ∂m
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_3
m : ι → Measure (Measure α)
s : Set α
hs : MeasurableSet s
⊢ (sum m).join s = (sum fun i ↦ (m i).join) s

Tactic:
[

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_3
m : ι → Measure (Measure α)
s : Set α
hs : MeasurableSet s
⊢ (sum m).join s = (sum fun i ↦ (m i).join) s
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
hfm : Measurable f
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
[

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
hfm : Measurable f
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this✝ : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
L : Tendsto (fun n ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
N : ℕ
y : ℕ → ℕ
hxy : y ∈ ball x ((1 / 2) ^ N)
ys : y ∈ s
n : ℕ
hn : n ≤ N
this : x n = y n
⊢ closedBall (u (x n)) ((1 / 2) ^ n) = closedBall (u (y n)) ((1 / 2) ^ n)

Tactic:
this

Goal state after:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this✝ : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
L : Tendsto (fun n ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
N : ℕ
y : ℕ → ℕ
hxy : y ∈ ball x ((1 / 2) ^ N)
ys : y ∈ s
n : ℕ
hn : n ≤ N
this : x n = y n
⊢ closedBall (u (y n)) ((1 / 2) ^ n) = closedBall (u (y n)) ((1 / 2) ^ n)
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∑ b ∈ s n, ∫⁻ (a : Measure α), b * f n b a ∂m

Tactic:
[

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∑ b ∈ s n, ∫⁻ (a : Measure α), b * f n b a ∂m
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case left.hU
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j // j ∉ K }), 2⁻¹ ^ encode ↑i < ε / 2
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ * ↑K.card < ε / 2
x y : (i : ι) → F i
hxy : (x, y) ∈ ⋂ i, {p | edist (p.1 ↑i) (p.2 ↑i) < δ}
⊢ (x, y) ∈ {p | edist p.1 p.2 < ε}

Tactic:
simp only [mem_iInter, mem_ofPred_eq, SetCoe.forall, Finset.mem_coe] at hxy

Goal state after:
case left.hU
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j // j ∉ K }), 2⁻¹ ^ encode ↑i < ε / 2
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ * ↑K.card < ε / 2
x y : (i : ι) → F i
hxy : ∀ (x_1 : ι) (h : x_1 ∈ K), edist (x x_1) (y x_1) < δ
⊢ (x, y) ∈ {p | edist p.1 p.2 < ε}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), μ (s n) < ∞
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
δsum : ∑' (i : ℕ), μ (s i) * ↑(δ i) < ε
N : α → ℕ := spanningSetsIndex μ
hN_meas : Measurable N
hNs : ∀ (n : ℕ), N ⁻¹' {n} = s n
⊢ ∫⁻ (x : α), ↑((δ ∘ N) x) ∂μ < ε

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), μ (s n) < ∞
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
δsum : ∑' (i : ℕ), μ (s i) * ↑(δ i) < ε
N : α → ℕ := spanningSetsIndex μ
hN_meas : Measurable N
hNs : ∀ (n : ℕ), N ⁻¹' {n} = s n
⊢ ∫⁻ (x : α), ↑((δ ∘ N) x) ∂μ < ε
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_3
m : ι → Measure α
f : α → Measure β
h : AEMeasurable f (sum fun i ↦ m i)
⊢ (sum fun i ↦ m i).bind f = sum fun i ↦ (m i).bind f

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_3
m : ι → Measure α
f : α → Measure β
h : AEMeasurable f (sum fun i ↦ m i)
⊢ (sum fun i ↦ m i).bind f = sum fun i ↦ (m i).bind f
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure α
f : α → Measure β
⊢ (c • m).bind f = c • m.bind f

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure α
f : α → Measure β
⊢ (c • m).bind f = c • m.bind f
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : Measure α), (map f a) s ∂μ = ∫⁻ (μ : Measure α), μ (f ⁻¹' s) ∂μ

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : Measure α), (map f a) s ∂μ = ∫⁻ (μ : Measure α), μ (f ⁻¹' s) ∂μ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case compl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ s : Set (α × β)
hs : MeasurableSet s
ihs : Measurable fun x ↦ ν (Prod.mk x ⁻¹' s)
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' sᶜ)

Tactic:
[

Goal state after:
case compl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ s : Set (α × β)
hs : MeasurableSet s
ihs : Measurable fun x ↦ ν (Prod.mk x ⁻¹' s)
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' 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 (α × β)
hs : MeasurableSet s
⊢ Measurable fun x ↦ (sum (sfiniteSeq ν)) (Prod.mk x ⁻¹' s)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x ↦ (sum (sfiniteSeq ν)) (Prod.mk x ⁻¹' 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 (α × β)
hs : MeasurableSet s
⊢ Measurable fun b ↦ (map (Prod.mk b) ν) s

Tactic:
[

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 (α × β)
hs : MeasurableSet s
⊢ Measurable fun b ↦ (map (fun x ↦ (x, b)) μ) s

Tactic:
[

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: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
⊢ Measurable fun y ↦ map (fun x ↦ (x, y)) μ

Tactic:
apply measurable_of_measurable_coe; intro s hs
  simp_rw [map_apply measurable_prodMk_right hs]
  exact measurable_measure_prodMk_right hs

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(f x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
[

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(f x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ