mathlib

4aa2a2e1 - chore(logic/basic): add move eq_true from core, as eq_true_iff (#17060)

chore(logic/basic): add move eq_true from core, as eq_true_iff (#17060) We want to delete `eq_true` and `eq_false` in core, per https://github.com/leanprover-community/lean/pull/774, as they have different meanings in Lean 4. This reintrodues `eq_true`, renamed to `eq_true_iff`, into mathlib3. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>