Commit 2023-11-01 16:07 bc2e2797
View on Github →chore: demote charZero_of_expChar_one' instance to a theorem (#7777)
The low-priority instance charZero_of_expChar_one' takes as an input a Nontrivial R and a ExpChar R 1 instance, but there are no such ExpChar instances in Mathlib. It is tried before StrictOrderedSemiring.to_charZero when synthesizing CharZero Nat, and the former takes a long time to fail (~100ms) because Lean tries to construct Nontrivial Nat in all possible ways before giving up, for some reason. See Zulip thread and the synthInstance trace for context.