Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Regression.20in.20simp) and [the synthInstance trace](https://gist.github.com/collares/8590a08c79eed16879a823233b03ba70) for context. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
- Loading branch information