Where should I put these data theorems?

Stream: mathlib4

[David Ledvinka]

Where should I put these?

import Mathlib

/-#min_imports in :
Mathlib.Order.SetNotationdd
-/
theorem pi_iUnion_eq_iInter_pi {ι ι' : Type*} {α : ι → Type*} (s : ι' → Set ι)
    (t : (i : ι) → Set (α i)) : (⋃ i, s i).pi t = ⋂ i, (s i).pi t := by
  sorry

/-
#min_imports in:
import Mathlib.Order.SetNotation
import Mathlib.Data.Finset.Insert
-/
theorem iUnion_finset_eq_set {ι : Type*} (s : Set ι) :
    ⋃ s' : Finset s, Subtype.val '' (s' : Set s) = s := by
  sorry

In general I struggle to figure out where to put these kinds of theorems when #min_imports and #find_home don't seem helpful.

[Kevin Buzzard]

#loogle Set.pi only produces 6 hits (to my mild surprise) but there seem to a bunch of theorems about Set.pi in Mathlib/Data/Set/Prod.lean` so I'd go there for the first one.

[David Ledvinka]

It seems to not import iUnion(and my understanding is that you typically aren't supposed to add imports to these lower level data files?)

[Etienne Marion]

@loogle Set.pi, Set.iUnion

[loogle]

:search: Set.iUnion_univ_pi, Set.pi_diff_pi_subset, and 6 more

[Etienne Marion]

suggests that Data.Set.Lattice should be ok

[David Ledvinka]

Thanks!

[Etienne Marion]

@loogle ⋃ _ : Finset _, _

[loogle]

:search: Set.iUnion_eq_iUnion_finset, Set.iUnion_eq_iUnion_finset', and 11 more

[Etienne Marion]

Maybe Mathlib.Order.CompleteLattice.Finset?