Is Paving Analytic For fst

lemma IsPavingAnalyticFor.fst {𝓚' : Type*} (hq_empty : ∅ ∈ q) (hq : IsCompactSystem q)    {s : Set (𝓧 × 𝓚)} (hs : IsPavingAnalyticFor (Set.image2 (· ×ˢ ·) p q) 𝓚' s) :    IsPavingAnalyticFor p (𝓚 × 𝓚') (Prod.fst '' s) := by  obtain ⟨q', hq'_empty, hq', K, hK, rfl⟩ := hs  refine ⟨Set.image2 (· ×ˢ ·) q q', ?_, hq.image2_prod hq', Equiv.prodAssoc 𝓧 𝓚 𝓚' '' K, ?_,    by ext; simp⟩  · exact ⟨∅, hq_empty, ∅, hq'_empty, by simp⟩  simp_rw [mem_prodSigmaDelta_iff] at hK ⊢  obtain ⟨B, hB, K', hK', rfl⟩ := hK  choose A hA K hK h_eq using hB  refine ⟨A, hA, fun n m ↦ K n m ×ˢ K' n m, fun n m ↦ ?_, ?_⟩  · exact ⟨K n m, hK n m, K' n m, hK' n m, rfl⟩  · rw [Set.image_iInter (Equiv.prodAssoc 𝓧 𝓚 𝓚').bijective]    simp_rw [Set.image_iUnion]    congr    ext    simp    grind