ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n => AEMeasurable.mk (f n) (_ : AEMeasurable (f n)) x
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n => aeSeq hf p n x
simp only [aeSeq, hx, if_true]
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n => f n x
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n => AEMeasurable.mk (f n) (_ : AEMeasurable (f n)) x
rw [funext fun n => mk_eq_fun_of_mem_aeSeqSet hf hx n]
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
h_ss : aeSeqSet hf p ⊆ {x | p x fun n => f n x}
⊢ p x fun n => f n x
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n => f n x
have h_ss : aeSeqSet hf p ⊆ { x | p x fun n => f n x } := by
  rw [← compl_compl { x | p x fun n => f n x }, aeSeqSet, Set.compl_subset_compl]
  refine' Set.Subset.trans (Set.compl_subset_compl.mpr _) (subset_toMeasurable _ _)
  exact fun x hx => hx.2
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
h_ss : aeSeqSet hf p ⊆ {x | p x fun n => f n x}
hx' : x ∈ {x | p x fun n => f n x}
⊢ p x fun n => f n x
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
h_ss : aeSeqSet hf p ⊆ {x | p x fun n => f n x}
⊢ p x fun n => f n x
have hx' := Set.mem_of_subset_of_mem h_ss hx
no goals
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
h_ss : aeSeqSet hf p ⊆ {x | p x fun n => f n x}
hx' : x ∈ {x | p x fun n => f n x}
⊢ p x fun n => f n x
exact hx'
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ {x | p x fun n => f n x}ᶜ ⊆
    toMeasurable μ ({x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ)
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeqSet hf p ⊆ {x | p x fun n => f n x}
rw [← compl_compl { x | p x fun n => f n x }, aeSeqSet, Set.compl_subset_compl]
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x} ⊆
    {x | p x fun n => f n x}
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ {x | p x fun n => f n x}ᶜ ⊆
    toMeasurable μ ({x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ)
refine' Set.Subset.trans (Set.compl_subset_compl.mpr _) (subset_toMeasurable _ _)
no goals
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.311116
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x} ⊆
    {x | p x fun n => f n x}
exact fun x hx => hx.2