Counting independent choices after fixing a complement

For a selected set of coordinates, the allowed values at each selected coordinate may depend on all the unselected coordinates. After those values are fixed, counting factors as a product over the selected coordinates.

theorem Algebraic.MassProduction.Nonuniform.cardConditionallyRestricted_le {Index : Type u_1} {Choice : Type u_2} [Fintype Index] [Fintype Choice] [DecidableEq Index] (selected : Finset Index) (allowed : ({ index : Index // index ∉ selected } → Choice) → ↥selected → Finset Choice) (bound : ℕ) (allowedSmall : ∀ (outside : { index : Index // index ∉ selected } → Choice) (index : ↥selected), (allowed outside index).card ≤ bound) : Nat.card { assignment : Index → Choice // ∀ (index : ↥selected), assignment ↑index ∈ allowed (fun (outside : { index : Index // index ∉ selected }) => assignment ↑outside) index } ≤ Fintype.card Choice ^ (Fintype.card Index - selected.card) * bound ^ selected.card

Fixing the complementary coordinates permits a product bound on the number of assignments satisfying all selected-coordinate restrictions.