Decide on style for `[def]rule_tac ... [and ...] in ...`

[Xaphiosis]

We had some discussions on the Proofcraft mattermost (present were myself, @lsf37 , @corlewis , @michaelmcinerney ), which ended up with things not quite nailed down in the end. Let's nail it down and put it in the style guide.

General considerations:

• we need a left-operator (and) and right-operator (and) version
• does the in belong to the rule_tac, or the instantiation? (in previous discussions: to the rule_tac)
• right-alignment of the and/in to utilise space better (similar to : alignment on method args)

At the time of discussion, we settled roughly on:

(* left-operator space-utilising / pretty version 1 - preferred *)
apply (rule_tac x=longthing
            and y=longthing2
             in the_rule)

(* right-operator version - preferred when using right operator wrapping style *)
apply (rule_tac x="..." and
                y="..." and
                z=True
                in some_rule) (* this must not go on previous line for multi-line instantiations *)

(* left-operator naive version (something a tool could potentially handle) - permitted *)
apply (rule_tac x="..."
                and y="..."
                and z=True
                in some_rule)

The following were ruled out:

left-wrap pretty version 2:
apply (rule_tac x="..."
            and y="..."
            and z=True
                in some_rule)

left-wrap pretty version 3:
apply (rule_tac x="..."
            and y="..."
            and z=True
         in some_rule)

However, the above consensus caused friction in the following (one-variable long instantiation) case (pointed out by @lsf37), bringing us back to a need to go over this and pin things down:

(* one-long-instantiation version 1 *)
apply (rule_tac x="long instantiation"
             in some_rule)
vs
(* one-long-instantiation version 2 *)
apply (rule_tac x="long instantiation"
                in some_rule)

For recent proofs I've been going with version 1, because of its consistency with pretty version 1 above. One of these days maybe we'll have a tool, but even then we'd still have to decide what the tool reformats to.