coproduct

Lean v4.3.0 change to `simp` defaults breaks proofs

3

In Lean v4.3.0, "`simp` will no longer try to use Decidable instances to rewrite terms" by default ([release notes](https://github.com/leanprover/lean4/releases/tag/v4.3.0)). This change broke these proofs in chapter 3: ``` lean theorem...