0 is not reducibly defeq to 1 - 1 if defined via Zero class

[gebner]

class Zero (α : Type u) where
  zero : α

instance Zero.toOfNat0 [Zero α] : OfNat α (nat_lit 0) where
  ofNat := Zero.zero

instance : Zero Nat where
  zero := 0  -- this can also be `nat_lit 0`, doesn't make a difference

example : @OfNat.ofNat Nat (nat_lit 0) inferInstance = 1 - 1 := by
  with_reducible rfl -- works

example : @OfNat.ofNat Nat (nat_lit 0) Zero.toOfNat0 = 1 - 1 := by
  with_reducible rfl -- fails

It is very surprising that it works with the default instance, but not if we go via the auxiliary Zero class. Note that we have quite a few lemmas in mathlib which are stated in terms of the Zero instance because they apply generally to additive monoids.

This came up in mathlib: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/isDefEq.20not.20transitive.3F/near/327881064

[leodemoura]

@semorrison @jcommelin Is this still an issue in Mathlib? Note that both of examples now fail in master.

[Kha]

Assuming solved