cc tactic can't unify def-eq instances in OfNat.ofNat #13362
Description
We can't recover cc here in bernoulliPowerSeries_mul_exp_sub_one on Mathlib.NumberTheory.Bernoulli:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
⊢ (↑x.2! * (↑x.2 + 1) = (↑x.2 + 1) * ↑x.2! ∨ (x.1 + x.2)! = 0) ∨ bernoulli x.1 = 0
As a porter of cc, I'm trying to fix this regression.