If I was trying to be as pedantic as possible, can I deduce this in one step? Let a and b be statements.
Assume (a and b). Obviously ((a or c) and (b or d)).
If I was trying to be as pedantic as possible, could I deduce that in one step? If so what rule would I be using?  My thought is the basic rules of logic don't let you do something in the middle like that.
Or would I need to do it in multiple steps:
(a and b) Assumption
(a) Conjunctive elimination
(b) Conjunctive elimination
(a or c) Disjunction introduction
(b or d) Disjunction introduction
((a or c) and (b or d)) Conjunctive introduction
 A: It depends on what proof system you are using, i.e. what the exact rules are in your system. In practice, most proof systems are intentionally designed to do things in small steps. For example, in natural deduction or the sequent calculus connectives are usually defined by rules such that each rule only involves a single connective. This means there is no way to manipulate two different connectives (e.g. $\land$ versus $\lor$) in a single rule application. It's also typically the case that a rule can only be applied at one location at a time. Related to this, most systems require the connective being manipulated to be the outermost connective which may require "busywork" to "dig out" the relevant subformula and often "rebury" it. You can see this in your proof with the matching $\land$-eliminations and $\land$-introduction.  So-called deep inference systems allow applying a rule deep within a formula to avoid this. These systems are fairly unusual, though.
For practical software proof assistants, this issue is usually resolved in one of two ways. First, many proof assistants support tactics which are programs that attempt to create proofs. So all the individual steps remain necessary, but some program writes them instead of you. The second common approach is to incorporate calling out to a decision procedure as a rule. This will allow quite complicated manipulations to be done in a single step. This is also typically very efficient compared to the alternative. The cost of this is usually decision procedures are complicated and provide little in the way of evidence that their result is correct, so you have to just trust them. (Some do provide certificates, and you could, theoretically, prove the correctness [of the implementation!] of the decision procedure within your logic.)
