Commit 2022-11-02 22:11 fabc6b98

feat: port core Lean 3 init.data.bool.{basic,lemmas} (#523) Because Lean 3 band and and have become Lean 4 and and And, and because of Lean 4 naming conventions, there are various name clashes between booly and proppy lemmas (e.g. and_assoc in Lean 4 is about Props). I resolve this by putting all the booly lemmas into the Bool namespace. In this PR I port all core Lean 3 bool lemmas which aren't in core Lean 4 into mathlib4, and do a lot of #align ing (including aligning core Lean 3 lemmas with their corresponding core Lean 4 names). This PR is a prerequisite for a port of mathlib3 data.bool.basic, which I have also completed and will PR next, but it seemed to me that this PR already had the possibility of generating some discussion points so I thought I'd try this first. Some core Lean 3 lemma names are quite idiosyncratic but I've faithfully copied them over mindlessly, at least in this initial commit.