ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.363672
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
h_eq : (fun n => f n x) = fun n => aeSeq hf p n x
⊢ p x fun n => f n x
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.363672
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_eq : (fun n => f n x) = fun n => aeSeq hf p n x :=
  funext fun n => (aeSeq_eq_fun_of_mem_aeSeqSet hf hx n).symm
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.363672
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
h_eq : (fun n => f n x) = fun n => aeSeq hf p n x
⊢ p x fun n => aeSeq hf p n x
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.363672
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
h_eq : (fun n => f n x) = fun n => aeSeq hf p n x
⊢ p x fun n => f n x
rw [h_eq]
no goals
ι : Sort u_3
α : Type u_1
β : Type u_2
γ : Type ?u.363672
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
h_eq : (fun n => f n x) = fun n => aeSeq hf p n x
⊢ p x fun n => aeSeq hf p n x
exact prop_of_mem_aeSeqSet hf hx