no goals
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type ?u.571614
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeq hf p i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x
simp only [aeSeq, hx, if_true]