Membership in optional-line occupancy

This instance-independent characterization avoids unfolding the finite union's equality implementation when specializing to encoded vector spaces.

theorem Algebraic.MassProduction.Nonuniform.mem_phaseOccupied_iff {capacity active : ℕ} {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] (state : PhaseState V (Projectivization K V) capacity active) (point : V) : point ∈ phaseOccupied state ↔ ∃ (slot : Fin capacity) (line : V × Projectivization K V), state.1 slot = some line ∧ point ∈ puncturedLine line.1 line.2

An occupied point belongs to one of the present line descriptions.