Disprove Exercise 3.5.6 without nonempty hypotheses

[Chessing234]

Summary

• The positive prod_subset_prod needs A,B,C,D ≠ ∅.
• The decidable drop of those hypotheses is false: ∅ × {0} ⊆ {0} × ∅ holds while {0} ⊈ ∅.
• Decide with apply isFalse and that counterexample.

Test plan

• CI / lake build on Section_3_5

[teorth]

Closing this one under the repository's solutions policy — see the consolidated note on #667 for the full explanation and for what would be most welcome instead.

Briefly: this PR discharges sorrys that are reader exercises in Analysis I, and removes the accompanying hint comment ("the first line of this construction should be either apply isTrue or apply isFalse"). From the README:

Portions of the text that were left as exercises to the reader are rendered in this translation as sorrys. Readers are welcome to fork the repository here to try their hand at these exercises, but I do not intend to place solutions in this repository directly.

Nothing wrong with the mathematics here — this is purely about what belongs in the main repository.