Is Paving Analytic For is Capacitable

theorem IsPavingAnalyticFor.isCapacitable (hp_empty : ∅ ∈ p) (hp_inter : InfClosed p)    (hp_union : SupClosed p) (hs : IsPavingAnalyticFor p 𝓚 s) :    IsCapacitable m s := by  obtain ⟨q, hq_empty, hq, A, hA, rfl⟩ := hs  have hq'_empty : ∅ ∈ infClosure q := subset_infClosure hq_empty  have hq' : IsCompactSystem (infClosure q) := hq.infClosure  refine IsCapacitable.fst hp_empty hp_inter hp_union m hq'_empty infClosed_infClosure hq' ?_  refine isCapacitable_mem_countableInfClosure_countableSupClosure _ ?_ ?_ ?_ ?_  · exact subset_supClosure ⟨∅, hp_empty, ∅, hq'_empty, by simp⟩  · exact InfClosed.supClosure (hp_inter.image2_prod infClosed_infClosure)  · exact fun s hs t ht ↦ supClosed_supClosure hs ht  · unfold prodSigmaDelta at hA    rw [mem_countableInfClosure_iff_iInf] at hA ⊢    obtain ⟨B, hB, rfl⟩ := hA    refine ⟨B, fun n ↦ ?_, rfl⟩    simp_rw [mem_countableSupClosure_iff_iSup] at hB ⊢    obtain ⟨C, hC, hB_eq⟩ := hB n    simp_rw [← hB_eq]    refine ⟨C, fun m ↦ ?_, rfl⟩    refine subset_supClosure ?_    obtain ⟨u, v, hu, hv, h_eq⟩ := hC m    exact ⟨u, v, hu, subset_infClosure hv, h_eq⟩