Finset Shatters to Set Shatters

theorem _root_.Finset.Shatters.toSetShatters {𝒜 : Finset (Finset α)} {s : Finset α}    (h : 𝒜.Shatters s) :    SetShatters      {c : α → Bool | ∃ t ∈ 𝒜, ∀ x, c x = decide (x ∈ t)} ↑s := by  intro W' hW'  have hfin : Set.Finite W' := s.finite_toSet.subset hW'  set t := hfin.toFinset  have ht_eq : (↑t : Set α) = W' := hfin.coe_toFinset  have ht_sub : t ⊆ s := Finset.coe_subset.mp (ht_eq ▸ hW')  obtain ⟨u, hu, hsu⟩ := h ht_sub  have hut : u ∩ s = t := by rwa [Finset.inter_comm] at hsu  refine ⟨fun x => decide (x ∈ u), ⟨u, hu, fun _ => rfl⟩, ?_⟩  rw [← ht_eq]  ext x  simp only [mem_inter_iff, mem_preimage, mem_singleton_iff,    decide_eq_true_eq, Finset.mem_coe]  exact ⟨fun ⟨h1, h2⟩ => hut ▸ Finset.mem_inter.mpr ⟨h1, h2⟩,    fun h => Finset.mem_inter.mp (hut.symm ▸ h)⟩