mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
n : ℕ
⊢ (n + 1) • r ≤ ∑ x ∈ Finset.range (n + 1), μ (s x)

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
n : ℕ
⊢ (n + 1) • r ≤ ∑ x ∈ Finset.range (n + 1), μ (s x)
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inr.inr.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ((s n).indicator fun x ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet t

Tactic:
]

Goal state after:
case refine_2.inr.inr.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ((s n).indicator fun x ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet t
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
⊢ (∏ i, (κ a) (Y i ⁻¹' t i))⁻¹ * (κ a) (⋂ i, g i) = (∏ i, (κ a) (Y i ⁻¹' t i))⁻¹ * (κ a) (⋂ i, g i)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : Set.univ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t

Tactic:
]

Goal state after:
case refine_2.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : Set.univ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
⊢ ∫⁻ (x : α), limsup (fun x_1 ↦ f x_1 x) atTop ∂μ ≤ ∫⁻ (x : α), 1 ∂μ

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
⊢ ∫⁻ (x : α), limsup (fun x_1 ↦ f x_1 x) atTop ∂μ ≤ ∫⁻ (x : α), 1 ∂μ
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
⊢ (∏ i, (κ a) (Y i ⁻¹' t i))⁻¹ * ∏ i, (κ a) (g i) = (∏ i, (κ a) (Y i ⁻¹' t i))⁻¹ * ∏ i, (κ a) (g i)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : Set.univ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = Set.univ
⊢ MeasurableSet Set.univ

Tactic:
]

Goal state after:
case refine_2.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : Set.univ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = Set.univ
⊢ MeasurableSet Set.univ
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
⊢ (∏ i, ((κ a) (Y i ⁻¹' t i))⁻¹) * ∏ i, (κ a) (g i) = (∏ x, ((κ a) (Y x ⁻¹' t x))⁻¹) * ∏ x, (κ a) (g x)

pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
⊢ (↑Finset.univ).Pairwise fun i j ↦ (κ a) (Y i ⁻¹' t i) ≠ 0 ∨ (κ a) (Y j ⁻¹' t j) ≠ ⊤

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
⊢ (↑Finset.univ).Pairwise fun i j ↦ (κ a) (Y i ⁻¹' t i) ≠ 0 ∨ (κ a) (Y j ⁻¹' t j) ≠ ⊤
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : s n = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = s n
⊢ MeasurableSet t

Tactic:
]

Goal state after:
case refine_2.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : s n = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = s n
⊢ MeasurableSet t
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : s n = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = s n
⊢ MeasurableSet (s n)

Tactic:
]

Goal state after:
case refine_2.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : s n = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = s n
⊢ MeasurableSet (s n)
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inr.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : (s n)ᶜ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t

Tactic:
]

Goal state after:
case refine_2.inr.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : (s n)ᶜ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inr.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : (s n)ᶜ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet (s n)ᶜ

Tactic:
]

Goal state after:
case refine_2.inr.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : (s n)ᶜ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet (s n)ᶜ
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inr.inr.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet t

Tactic:
]

Goal state after:
case refine_2.inr.inr.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet t
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inr.inr.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet ∅

Tactic:
]

Goal state after:
case refine_2.inr.inr.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet ∅
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count

Goal state before:
pp: α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ ‖f i‖ₑ = ‖f i‖ₑ

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
⊢ StronglyMeasurable
    (if h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω)) then Classical.choose h
    else 0)

Tactic:
]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
⊢ StronglyMeasurable
    (if h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω)) then Classical.choose h
    else 0)
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
⊢ MemLp
    (if h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω)) then Classical.choose h
    else 0)
    p μ

Tactic:
]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
⊢ MemLp
    (if h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω)) then Classical.choose h
    else 0)
    p μ
Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableConstSMul M α
c : M
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
b : E
⊢ μ s ≠ ∞

Tactic:
]

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableConstSMul M α
c : M
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
b : E
⊢ μ s ≠ ∞
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
h : ¬∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))
⊢ MemLp 0 p μ

Tactic:
exact MemLp.zero

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁴ : (i : ι) → TopologicalSpace (β i)
inst✝³ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝² : ∀ (i : ι), BorelSpace (β i)
inst✝¹ : Preorder ι
X : ι → Type u_4
inst✝ : (i : ι) → MeasurableSpace (X i)
i j : ι
hij : i ≤ j
⊢ MeasurableSpace.comap (restrictLe j) (MeasurableSpace.comap (restrictLe₂ hij) MeasurableSpace.pi) ≤
    MeasurableSpace.comap (restrictLe j) MeasurableSpace.pi

Tactic:
]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁴ : (i : ι) → TopologicalSpace (β i)
inst✝³ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝² : ∀ (i : ι), BorelSpace (β i)
inst✝¹ : Preorder ι
X : ι → Type u_4
inst✝ : (i : ι) → MeasurableSpace (X i)
i j : ι
hij : i ≤ j
⊢ MeasurableSpace.comap (restrictLe j) (MeasurableSpace.comap (restrictLe₂ hij) MeasurableSpace.pi) ≤
    MeasurableSpace.comap (restrictLe j) MeasurableSpace.pi
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case a
ι : Type u_2
inst✝² : Preorder ι
X : ι → Type u_4
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : LocallyFiniteOrderBot ι
i : ι
⊢ MeasurableSpace.comap (restrictLe i)
      (MeasurableSpace.comap (⇑(MeasurableEquiv.piCongrLeft (fun i_1 ↦ X ↑i_1) (Equiv.IicFinsetSet i).symm))
        MeasurableSpace.pi) ≤
    ↑piLE i

Tactic:
]

Goal state after:
case a
ι : Type u_2
inst✝² : Preorder ι
X : ι → Type u_4
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : LocallyFiniteOrderBot ι
i : ι
⊢ MeasurableSpace.comap (restrictLe i)
      (MeasurableSpace.comap (⇑(MeasurableEquiv.piCongrLeft (fun i_1 ↦ X ↑i_1) (Equiv.IicFinsetSet i).symm))
        MeasurableSpace.pi) ≤
    ↑piLE i