Style/usability question on multiple related theorems

Stream: new members

[J. J. Issai (project started by GRP)]

I have at least three choices for formalizing a result involving natural numbers:

theorem option_1 (assumptions_1) : \forall j (A(j) \and B(j) ) := by sorry_1

theorem option_2 (assumptions_1): \forall j A(j) \and \forall j B(j) := by sorry_2

theorem option_3a (assumptions_1) : \forall j A(j) := by sorry_3
theorem option_3b (assumptions_1):\forall j B(j) := by sorry_4

For concision, I would prefer option 1 or option 2. For use, I will want both option3a and option 3b (I almost never need both in the same section of proof). If A(j) and B(j) are of interest in including in Mathlib, what form is preferred and why? Or would all three options be of use?

If it matters, for j sufficiently large, B(j) implies A(j). Also, if \forall is moved into the assumptions this effectively becomes options 1 and 3ab.

[Snir Broshi]

AFAIK Mathlib (and I think ITPs in general) prefer option 3, since it's easier to use

[Snir Broshi]

Similar to how (A ∧ B) → ... is discouraged over A → B → ....
I think ∧ is mostly used under ∃

[J. J. Issai (project started by GRP)]

@Snir Broshi: Thanks. If I went with option 3ab and needed to show option1, what is a good idiom for this?

[Snir Broshi]

Well you can do fun j ↦ ⟨option_3a assumptions_1 j, option_3b assumptions_1 j⟩, and there's probably a small theorem that can even convert it for you if you prefer

[J. J. Issai (project started by GRP)]

And to be clear

Snir Broshi said:

Similar to how (A ∧ B) → ... is discouraged over A → B → ....
I think ∧ is mostly used under ∃

the first option with \and is discouraged and the option with \implies is encouraged? (making sure I understand)

[Snir Broshi]

You can use docs#forall_and to convert if it's shorter than the manual option I wrote above